(* Figure 3, production $\vdash_E$, Uniform rules *)
Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
- | RId : forall a , Arrange a a
- | RCanL : forall a , Arrange ( [],,a ) ( a )
- | RCanR : forall a , Arrange ( a,,[] ) ( a )
- | RuCanL : forall a , Arrange ( a ) ( [],,a )
- | RuCanR : forall a , Arrange ( a ) ( a,,[] )
- | RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
- | RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
- | RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
- | RWeak : forall a , Arrange ( [] ) ( a )
- | RCont : forall a , Arrange ( (a,,a) ) ( a )
- | RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
- | RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
- | RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
+ | AId : forall a , Arrange a a
+ | ACanL : forall a , Arrange ( [],,a ) ( a )
+ | ACanR : forall a , Arrange ( a,,[] ) ( a )
+ | AuCanL : forall a , Arrange ( a ) ( [],,a )
+ | AuCanR : forall a , Arrange ( a ) ( a,,[] )
+ | AAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
+ | AuAssoc : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
+ | AExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
+ | AWeak : forall a , Arrange ( [] ) ( a )
+ | ACont : forall a , Arrange ( (a,,a) ) ( a )
+ | ALeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
+ | ARight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
+ | AComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
.
(* "Arrange" objects are parametric in the type of the leaves of the tree *)
Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
intros.
induction X; simpl.
- apply RId.
- apply RCanL.
- apply RCanR.
- apply RuCanL.
- apply RuCanR.
- apply RAssoc.
- apply RCossa.
- apply RExch.
- apply RWeak.
- apply RCont.
- apply RLeft; auto.
- apply RRight; auto.
- eapply RComp; [ apply IHX1 | apply IHX2 ].
+ apply AId.
+ apply ACanL.
+ apply ACanR.
+ apply AuCanL.
+ apply AuCanR.
+ apply AAssoc.
+ apply AuAssoc.
+ apply AExch.
+ apply AWeak.
+ apply ACont.
+ apply ALeft; auto.
+ apply ARight; auto.
+ eapply AComp; [ apply IHX1 | apply IHX2 ].
Defined.
- (* a frequently-used Arrange *)
+ (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *)
Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
- eapply RComp.
- apply RCossa.
- eapply RComp.
- eapply RLeft.
- eapply RComp.
- eapply RAssoc.
- eapply RRight.
- apply RExch.
- eapply RComp.
- eapply RLeft.
- eapply RCossa.
- eapply RAssoc.
+ eapply AComp.
+ apply AuAssoc.
+ eapply AComp.
+ eapply ALeft.
+ eapply AComp.
+ eapply AAssoc.
+ eapply ARight.
+ apply AExch.
+ eapply AComp.
+ eapply ALeft.
+ eapply AuAssoc.
+ eapply AAssoc.
Defined.
- Definition arrange :
+ (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
+ Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
+ AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _).
+
+ (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
+ Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
+ AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _).
+
+ Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
+ eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ].
+ eapply AComp; [ idtac | apply AuAssoc ].
+ eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ].
+ apply AAssoc.
+ Defined.
+
+ (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
+ Definition arrangePartition :
forall {T} (Σ:Tree ??T) (f:T -> bool),
Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
intros.
destruct a.
simpl.
destruct (f t); simpl.
- apply RuCanL.
- apply RuCanR.
+ apply AuCanL.
+ apply AuCanR.
simpl.
- apply RuCanL.
+ apply AuCanL.
simpl in *.
- eapply RComp; [ idtac | apply arrangeSwapMiddle ].
- eapply RComp.
- eapply RLeft.
+ eapply AComp; [ idtac | apply arrangeSwapMiddle ].
+ eapply AComp.
+ eapply ALeft.
apply IHΣ2.
- eapply RRight.
+ eapply ARight.
apply IHΣ1.
Defined.
- Definition arrange' :
+ (* inverse of arrangePartition *)
+ Definition arrangeUnPartition :
forall {T} (Σ:Tree ??T) (f:T -> bool),
Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
intros.
destruct a.
simpl.
destruct (f t); simpl.
- apply RCanL.
- apply RCanR.
+ apply ACanL.
+ apply ACanR.
simpl.
- apply RCanL.
+ apply ACanL.
simpl in *.
- eapply RComp; [ apply arrangeSwapMiddle | idtac ].
- eapply RComp.
- eapply RLeft.
+ eapply AComp; [ apply arrangeSwapMiddle | idtac ].
+ eapply AComp.
+ eapply ALeft.
apply IHΣ2.
- eapply RRight.
+ eapply ARight.
apply IHΣ1.
Defined.
- Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
- RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
-
- Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
- RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
-
- Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
- eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
- eapply RComp; [ idtac | apply RCossa ].
- eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
- apply RAssoc.
+ (* we can decide if a tree consists exclusively of (T_Leaf None)'s *)
+ Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
+ sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
+ intro T.
+ refine (fix foo t :=
+ match t with
+ | T_Leaf x => _
+ | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
+ end).
+ intros.
+ destruct x.
+ right; apply tt.
+ left.
+ exists (T_Leaf tt).
+ auto.
+ destruct b1'.
+ destruct b2'.
+ destruct s.
+ destruct s0.
+ subst.
+ left.
+ exists (x,,x0).
+ reflexivity.
+ right; auto.
+ right; auto.
Defined.
+ (* if a tree is empty, we can Arrange it to [] *)
+ Definition arrangeCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange t [].
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply AId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply AComp.
+ eapply ARight.
+ rewrite <- H1.
+ apply x1.
+ eapply AComp.
+ apply ACanL.
+ rewrite <- H2.
+ apply x2.
+ Defined.
+
+ (* if a tree is empty, we can Arrange it from [] *)
+ Definition arrangeUnCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
+ t = mapTree (fun _:A => None) q ->
+ Arrange [] t.
+ intros T A q.
+ induction q; intros.
+ simpl in H.
+ rewrite H.
+ apply AId.
+ simpl in *.
+ destruct t; try destruct o; inversion H.
+ set (IHq1 _ H1) as x1.
+ set (IHq2 _ H2) as x2.
+ eapply AComp.
+ apply AuCanL.
+ eapply AComp.
+ eapply ARight.
+ apply x1.
+ eapply AComp.
+ eapply ALeft.
+ apply x2.
+ rewrite H.
+ apply AId.
+ Defined.
+
+ (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
+ Lemma arrangeDrop {T} pred
+ : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (dropT (mkFlags pred Σ₁)) (dropT (mkFlags pred Σ₂)).
+
+ refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
+ match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with
+ | AId a => let case_AId := tt in AId _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _
+ | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _
+ | AExch a b => let case_AExch := tt in AExch _ _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in ALeft _ (arrangeTake _ _ r')
+ | ARight a b c r' => let case_ARight := tt in ARight _ (arrangeTake _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
+ end)); clear arrangeTake; intros.
+
+ destruct case_ACanL.
+ simpl; destruct (pred None); simpl; apply ACanL.
+
+ destruct case_ACanR.
+ simpl; destruct (pred None); simpl; apply ACanR.
+
+ destruct case_AuCanL.
+ simpl; destruct (pred None); simpl; apply AuCanL.
+
+ destruct case_AuCanR.
+ simpl; destruct (pred None); simpl; apply AuCanR.
+
+ destruct case_AWeak.
+ simpl; destruct (pred None); simpl; apply AWeak.
+
+ destruct case_ACont.
+ simpl; destruct (pred None); simpl; apply ACont.
+
+ Defined.
+
+ Lemma arrangePullback' {T Q}{f:T->Q}
+ : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??Q), Arrange Σ₁ Σ₂ ->
+ forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ .
+
+ refine ((fix arrangePullback Σ₁ Σ₂ (arr:Arrange Σ₁ Σ₂) {struct arr} :
+ forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ :=
+ match arr as R in Arrange A B return
+ forall Σ₂', B = (mapOptionTree f Σ₂') ->
+ { Σ₁' : Tree ??T & prod (A = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
+ with
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in (fun rec => _) (arrangePullback _ _ r')
+ | ARight a b c r' => let case_ARight := tt in (fun rec => _) (arrangePullback _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in (fun rec1 rec2 => _) (arrangePullback _ _ r1) (arrangePullback _ _ r2)
+ end)); clear arrangePullback; intros.
+
+ destruct case_AId.
+ exists Σ₂'; split.
+ subst.
+ reflexivity.
+ apply AId.
+
+ destruct case_ACanL.
+ exists ([],,Σ₂'); split.
+ subst.
+ simpl.
+ reflexivity.
+ apply ACanL.
+
+ destruct case_ACanR.
+ exists (Σ₂',,[]); split.
+ subst.
+ simpl.
+ reflexivity.
+ apply ACanR.
+
+ destruct case_AuCanL.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ eexists; split.
+ reflexivity.
+ simpl in H.
+ inversion H.
+ destruct Σ₂'1; try destruct o; inversion H2.
+ apply AuCanL.
+
+ destruct case_AuCanR.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ eexists; split.
+ reflexivity.
+ simpl in H.
+ inversion H.
+ destruct Σ₂'2; try destruct o; inversion H2.
+ apply AuCanR.
+
+ destruct case_AAssoc.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct Σ₂'1; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AAssoc.
+
+ destruct case_AuAssoc.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct Σ₂'2; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AuAssoc.
+
+ destruct case_AExch.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply AExch.
+
+ destruct case_AWeak.
+ exists []; split.
+ reflexivity.
+ apply AWeak.
+
+ destruct case_ACont.
+ exists (Σ₂',,Σ₂').
+ subst; split.
+ reflexivity.
+ apply ACont.
+
+ destruct case_ALeft.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct (rec _ (refl_equal _)).
+ destruct p.
+ rewrite e.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply ALeft.
+ apply a0.
+
+ destruct case_ARight.
+ destruct Σ₂'; try destruct o; inversion H; subst.
+ destruct (rec _ (refl_equal _)).
+ destruct p.
+ rewrite e.
+ rewrite <- mapOptionTree_distributes.
+ eexists; split.
+ reflexivity.
+ apply ARight.
+ apply a0.
+
+ destruct case_AComp.
+ destruct (rec2 _ H).
+ destruct p.
+ destruct (rec1 _ e).
+ destruct p.
+ rewrite e0.
+ eexists; split.
+ reflexivity.
+ eapply AComp.
+ apply a1.
+ apply a0.
+ Defined.
+
+ Lemma arrangePullback {T Q}{f:T->Q}
+ : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??T), Arrange Σ₁ (mapOptionTree f Σ₂) ->
+ { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂) }.
+ intros.
+ eapply arrangePullback'.
+ apply X.
+ reflexivity.
+ Defined.
+
+ (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
+ (*
+ Lemma arrangePullback {T} pred
+ : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
+ unfold takeT'.
+ *)
+
+ (* like Arrange, but without weakening or contraction *)
+ Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type :=
+ | PId : forall a , Permutation a a
+ | PCanL : forall a , Permutation ( [],,a ) ( a )
+ | PCanR : forall a , Permutation ( a,,[] ) ( a )
+ | PuCanL : forall a , Permutation ( a ) ( [],,a )
+ | PuCanR : forall a , Permutation ( a ) ( a,,[] )
+ | PAssoc : forall a b c , Permutation (a,,(b,,c) ) ((a,,b),,c )
+ | PuAssoc : forall a b c , Permutation ((a,,b),,c ) ( a,,(b,,c) )
+ | PExch : forall a b , Permutation ( (b,,a) ) ( (a,,b) )
+ | PLeft : forall {h}{c} x , Permutation h c -> Permutation ( x,,h ) ( x,,c)
+ | PRight : forall {h}{c} x , Permutation h c -> Permutation ( h,,x ) ( c,,x)
+ | PComp : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c
+ .
+ Notation "a ≈ b" := (@Permutation _ a b) (at level 30).
+ Notation "a ⊆ b" := (@Arrange _ a b) (at level 30).
+
+ Definition permuteSwapMiddle {T} (a b c d:Tree ??T) :
+ ((a,,b),,(c,,d)) ≈ ((a,,c),,(b,,d)).
+ eapply PComp.
+ apply PuAssoc.
+ eapply PComp.
+ eapply PLeft.
+ eapply PComp.
+ eapply PAssoc.
+ eapply PRight.
+ apply PExch.
+ eapply PComp.
+ eapply PLeft.
+ eapply PuAssoc.
+ eapply PAssoc.
+ Defined.
+
+ Definition permuteMap :
+ forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
+ Σ₁ ≈ Σ₂ ->
+ (mapOptionTree f Σ₁) ≈ (mapOptionTree f Σ₂).
+ intros.
+ induction X; simpl.
+ apply PId.
+ apply PCanL.
+ apply PCanR.
+ apply PuCanL.
+ apply PuCanR.
+ apply PAssoc.
+ apply PuAssoc.
+ apply PExch.
+ apply PLeft; auto.
+ apply PRight; auto.
+ eapply PComp; [ apply IHX1 | apply IHX2 ].
+ Defined.
+
+ (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
+ Definition partitionPermutation :
+ forall {T} (Σ:Tree ??T) (f:T -> bool),
+ Σ ≈ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
+ intros.
+ induction Σ.
+ simpl.
+ destruct a.
+ simpl.
+ destruct (f t); simpl.
+ apply PuCanL.
+ apply PuCanR.
+ simpl.
+ apply PuCanL.
+ simpl in *.
+ eapply PComp; [ idtac | apply permuteSwapMiddle ].
+ eapply PComp.
+ eapply PLeft.
+ apply IHΣ2.
+ eapply PRight.
+ apply IHΣ1.
+ Defined.
+
+ Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b.
+ intro arr.
+ induction arr.
+ apply AId.
+ apply ACanL.
+ apply ACanR.
+ apply AuCanL.
+ apply AuCanR.
+ apply AAssoc.
+ apply AuAssoc.
+ apply AExch.
+ apply ALeft; apply IHarr.
+ apply ARight; apply IHarr.
+ eapply AComp.
+ apply IHarr1.
+ apply IHarr2.
+ Defined.
+
+ Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a.
+ intro perm.
+ induction perm.
+ apply PId.
+ apply PuCanL.
+ apply PuCanR.
+ apply PCanL.
+ apply PCanR.
+ apply PuAssoc.
+ apply PAssoc.
+ apply PExch.
+ eapply PLeft; apply IHperm.
+ eapply PRight; apply IHperm.
+ eapply PComp.
+ apply IHperm2.
+ apply IHperm1.
+ Defined.
+
+ (*
+ Definition factorArrangementAsPermutation {T} : forall (a b:Tree ??T), a ⊆ b -> { c : _ & (c,,a) ≈ b }.
+
+ refine ((fix factor a b (arr:Arrange a b) :=
+ match arr as R in Arrange A B return
+ { c : _ & (c,,A) ≈ B }
+ with
+ | AId a => let case_AId := tt in _
+ | ACanL a => let case_ACanL := tt in _
+ | ACanR a => let case_ACanR := tt in _
+ | AuCanL a => let case_AuCanL := tt in _
+ | AuCanR a => let case_AuCanR := tt in _
+ | AAssoc a b c => let case_AAssoc := tt in _
+ | AuAssoc a b c => let case_AuAssoc := tt in _
+ | AExch a b => let case_AExch := tt in _
+ | AWeak a => let case_AWeak := tt in _
+ | ACont a => let case_ACont := tt in _
+ | ALeft a b c r' => let case_ALeft := tt in (fun r'' => _) (factor _ _ r')
+ | ARight a b c r' => let case_ARight := tt in (fun r'' => _) (factor _ _ r')
+ | AComp a b c r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (factor _ _ r1) (factor _ _ r2)
+ end)); clear factor; intros.
+
+ destruct case_AId.
+ exists []. apply PCanL.
+
+ destruct case_ACanL.
+ exists [].
+ eapply PComp.
+ apply PCanL.
+ apply PCanL.
+
+ destruct case_ACanR.
+ exists [].
+ eapply PComp.
+ apply PCanL.
+ apply PCanR.
+
+ destruct case_AuCanL.
+ exists [].
+ apply PRight.
+ apply PId.
+
+ destruct case_AuCanR.
+ exists [].
+ apply PExch.
+
+ destruct case_AAssoc.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PAssoc.
+
+ destruct case_AuAssoc.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PuAssoc.
+
+ destruct case_AExch.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ apply PExch.
+
+ destruct case_AWeak.
+ exists a0.
+ eapply PCanR.
+
+ destruct case_ACont.
+ exists [].
+ eapply PComp.
+ eapply PCanL.
+ eapply PComp.
+ eapply PLeft.
+ eapply
+
+ Defined.
+ *)
+
End NaturalDeductionContext.