src/NaturalDeductionContext.v

   1 (*********************************************************************************************************************************)
   2 (* NaturalDeductionContext:                                                                                                      *)
   3 (*                                                                                                                               *)
   4 (*   Manipulations of a context in natural deduction proofs.                                                                     *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   8 Generalizable All Variables.
   9 Require Import Preamble.
  10 Require Import General.
  11 Require Import NaturalDeduction.
  12
  13 Section NaturalDeductionContext.
  14
  15   (* Figure 3, production $\vdash_E$, Uniform rules *)
  16   Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
  17   | AId     : forall a        ,                Arrange           a                  a
  18   | ACanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
  19   | ACanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
  20   | AuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
  21   | AuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
  22   | AAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
  23   | AuAssoc  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
  24   | AExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
  25   | AWeak   : forall a        ,                Arrange  (       []   )      (       a   )
  26   | ACont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
  27   | ALeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
  28   | ARight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
  29   | AComp   : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
  30   .
  31
  32   (* "Arrange" objects are parametric in the type of the leaves of the tree *)
  33   Definition arrangeMap :
  34     forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
  35       Arrange Σ₁ Σ₂ ->
  36       Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
  37     intros.
  38     induction X; simpl.
  39     apply AId.
  40     apply ACanL.
  41     apply ACanR.
  42     apply AuCanL.
  43     apply AuCanR.
  44     apply AAssoc.
  45     apply AuAssoc.
  46     apply AExch.
  47     apply AWeak.
  48     apply ACont.
  49     apply ALeft; auto.
  50     apply ARight; auto.
  51     eapply AComp; [ apply IHX1 | apply IHX2 ].
  52     Defined.
  53
  54   (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *)
  55   Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
  56     Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).
  57     eapply AComp.
  58     apply AuAssoc.
  59     eapply AComp.
  60     eapply ALeft.
  61     eapply AComp.
  62     eapply AAssoc.
  63     eapply ARight.
  64     apply AExch.
  65     eapply AComp.
  66     eapply ALeft.
  67     eapply AuAssoc.
  68     eapply AAssoc.
  69     Defined.
  70
  71   (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
  72   Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
  73     AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _).
  74
  75   (* like AExch, but works on nodes which are an Assoc away from being adjacent *)
  76   Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
  77     AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _).
  78
  79   Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
  80     eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ].
  81     eapply AComp; [ idtac | apply AuAssoc ].
  82     eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ].
  83     apply AAssoc.
  84     Defined.
  85
  86   (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
  87   Definition arrangePartition :
  88     forall {T} (Σ:Tree ??T) (f:T -> bool),
  89       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
  90     intros.
  91     induction Σ.
  92       simpl.
  93       destruct a.
  94       simpl.
  95       destruct (f t); simpl.
  96       apply AuCanL.
  97       apply AuCanR.
  98       simpl.
  99       apply AuCanL.
 100       simpl in *.
 101       eapply AComp; [ idtac | apply arrangeSwapMiddle ].
 102       eapply AComp.
 103       eapply ALeft.
 104       apply IHΣ2.
 105       eapply ARight.
 106       apply IHΣ1.
 107       Defined.
 108
 109   (* inverse of arrangePartition *)
 110   Definition arrangeUnPartition :
 111     forall {T} (Σ:Tree ??T) (f:T -> bool),
 112       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
 113     intros.
 114     induction Σ.
 115       simpl.
 116       destruct a.
 117       simpl.
 118       destruct (f t); simpl.
 119       apply ACanL.
 120       apply ACanR.
 121       simpl.
 122       apply ACanL.
 123       simpl in *.
 124       eapply AComp; [ apply arrangeSwapMiddle | idtac ].
 125       eapply AComp.
 126       eapply ALeft.
 127       apply IHΣ2.
 128       eapply ARight.
 129       apply IHΣ1.
 130       Defined.
 131
 132   (* we can decide if a tree consists exclusively of (T_Leaf None)'s *)
 133   Definition decide_tree_empty : forall {T:Type}(t:Tree ??T),
 134     sum { q:Tree unit & t = mapTree (fun _ => None) q } unit.
 135     intro T.
 136     refine (fix foo t :=
 137       match t with
 138         | T_Leaf x => _
 139         | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
 140       end).
 141     intros.
 142     destruct x.
 143     right; apply tt.
 144     left.
 145       exists (T_Leaf tt).
 146       auto.
 147     destruct b1'.
 148     destruct b2'.
 149     destruct s.
 150     destruct s0.
 151     subst.
 152     left.
 153     exists (x,,x0).
 154     reflexivity.
 155     right; auto.
 156     right; auto.
 157     Defined.
 158
 159   (* if a tree is empty, we can Arrange it to [] *)
 160   Definition arrangeCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
 161     t = mapTree (fun _:A => None) q ->
 162     Arrange t [].
 163     intros T A q.
 164     induction q; intros.
 165       simpl in H.
 166       rewrite H.
 167       apply AId.
 168     simpl in *.
 169     destruct t; try destruct o; inversion H.
 170       set (IHq1 _ H1) as x1.
 171       set (IHq2 _ H2) as x2.
 172       eapply AComp.
 173         eapply ARight.
 174         rewrite <- H1.
 175         apply x1.
 176       eapply AComp.
 177         apply ACanL.
 178         rewrite <- H2.
 179         apply x2.
 180       Defined.
 181
 182   (* if a tree is empty, we can Arrange it from [] *)
 183   Definition arrangeUnCancelEmptyTree : forall {T}{A}(q:Tree A)(t:Tree ??T),
 184     t = mapTree (fun _:A => None) q ->
 185     Arrange [] t.
 186     intros T A q.
 187     induction q; intros.
 188       simpl in H.
 189       rewrite H.
 190       apply AId.
 191     simpl in *.
 192     destruct t; try destruct o; inversion H.
 193       set (IHq1 _ H1) as x1.
 194       set (IHq2 _ H2) as x2.
 195       eapply AComp.
 196         apply AuCanL.
 197       eapply AComp.
 198         eapply ARight.
 199         apply x1.
 200       eapply AComp.
 201         eapply ALeft.
 202         apply x2.
 203       rewrite H.
 204       apply AId.
 205       Defined.
 206
 207   (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *)
 208   Lemma arrangeDrop {T} pred
 209     : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (dropT (mkFlags pred Σ₁)) (dropT (mkFlags pred Σ₂)).
 210
 211     refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) :=
 212       match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with
 213         | AId  a               => let case_AId := tt    in AId _
 214         | ACanL  a             => let case_ACanL := tt  in _
 215         | ACanR  a             => let case_ACanR := tt  in _
 216         | AuCanL a             => let case_AuCanL := tt in _
 217         | AuCanR a             => let case_AuCanR := tt in _
 218         | AAssoc a b c         => let case_AAssoc := tt in AAssoc _ _ _
 219         | AuAssoc a b c         => let case_AuAssoc := tt in AuAssoc _ _ _
 220         | AExch  a b           => let case_AExch := tt  in AExch _ _
 221         | AWeak  a             => let case_AWeak := tt  in _
 222         | ACont  a             => let case_ACont := tt  in _
 223         | ALeft  a b c r'      => let case_ALeft := tt  in ALeft  _ (arrangeTake _ _ r')
 224         | ARight a b c r'      => let case_ARight := tt in ARight _ (arrangeTake _ _ r')
 225         | AComp  a b c r1 r2   => let case_AComp := tt  in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
 226       end)); clear arrangeTake; intros.
 227
 228     destruct case_ACanL.
 229       simpl; destruct (pred None); simpl; apply ACanL.
 230
 231     destruct case_ACanR.
 232       simpl; destruct (pred None); simpl; apply ACanR.
 233
 234     destruct case_AuCanL.
 235       simpl; destruct (pred None); simpl; apply AuCanL.
 236
 237     destruct case_AuCanR.
 238       simpl; destruct (pred None); simpl; apply AuCanR.
 239
 240     destruct case_AWeak.
 241       simpl; destruct (pred None); simpl; apply AWeak.
 242
 243     destruct case_ACont.
 244       simpl; destruct (pred None); simpl; apply ACont.
 245
 246       Defined.
 247
 248   Lemma arrangePullback' {T Q}{f:T->Q}
 249     : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??Q), Arrange Σ₁ Σ₂ ->
 250       forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
 251       { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
 252       .
 253
 254     refine ((fix arrangePullback Σ₁ Σ₂ (arr:Arrange Σ₁ Σ₂) {struct arr} :
 255       forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
 256       { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
 257       :=
 258       match arr as R in Arrange A B return
 259         forall Σ₂', B = (mapOptionTree f Σ₂') ->
 260         { Σ₁' : Tree ??T & prod (A = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
 261         with
 262         | AId  a               => let case_AId := tt     in _
 263         | ACanL  a             => let case_ACanL := tt   in _
 264         | ACanR  a             => let case_ACanR := tt   in _
 265         | AuCanL a             => let case_AuCanL := tt  in _
 266         | AuCanR a             => let case_AuCanR := tt  in _
 267         | AAssoc a b c         => let case_AAssoc := tt  in _
 268         | AuAssoc a b c        => let case_AuAssoc := tt in _
 269         | AExch  a b           => let case_AExch := tt   in _
 270         | AWeak  a             => let case_AWeak := tt   in _
 271         | ACont  a             => let case_ACont := tt   in _
 272         | ALeft  a b c r'      => let case_ALeft := tt   in (fun rec       => _) (arrangePullback _ _ r')
 273         | ARight a b c r'      => let case_ARight := tt  in (fun rec       => _) (arrangePullback _ _ r')
 274         | AComp  a b c r1 r2   => let case_AComp := tt   in (fun rec1 rec2 => _) (arrangePullback _ _ r1) (arrangePullback _ _ r2)
 275       end)); clear arrangePullback; intros.
 276
 277     destruct case_AId.
 278       exists Σ₂'; split.
 279       subst.
 280       reflexivity.
 281       apply AId.
 282
 283     destruct case_ACanL.
 284       exists ([],,Σ₂'); split.
 285       subst.
 286       simpl.
 287       reflexivity.
 288       apply ACanL.
 289
 290     destruct case_ACanR.
 291       exists (Σ₂',,[]); split.
 292       subst.
 293       simpl.
 294       reflexivity.
 295       apply ACanR.
 296
 297     destruct case_AuCanL.
 298       destruct Σ₂'; try destruct o; inversion H; subst.
 299       eexists; split.
 300       reflexivity.
 301       simpl in H.
 302       inversion H.
 303       destruct Σ₂'1; try destruct o; inversion H2.
 304       apply AuCanL.
 305
 306     destruct case_AuCanR.
 307       destruct Σ₂'; try destruct o; inversion H; subst.
 308       eexists; split.
 309       reflexivity.
 310       simpl in H.
 311       inversion H.
 312       destruct Σ₂'2; try destruct o; inversion H2.
 313       apply AuCanR.
 314
 315     destruct case_AAssoc.
 316       destruct Σ₂'; try destruct o; inversion H; subst.
 317       destruct Σ₂'1; try destruct o; inversion H; subst.
 318       rewrite <- mapOptionTree_distributes.
 319       rewrite <- mapOptionTree_distributes.
 320       eexists; split.
 321       reflexivity.
 322       apply AAssoc.
 323
 324     destruct case_AuAssoc.
 325       destruct Σ₂'; try destruct o; inversion H; subst.
 326       destruct Σ₂'2; try destruct o; inversion H; subst.
 327       rewrite <- mapOptionTree_distributes.
 328       rewrite <- mapOptionTree_distributes.
 329       eexists; split.
 330       reflexivity.
 331       apply AuAssoc.
 332
 333     destruct case_AExch.
 334       destruct Σ₂'; try destruct o; inversion H; subst.
 335       rewrite <- mapOptionTree_distributes.
 336       eexists; split.
 337       reflexivity.
 338       apply AExch.
 339
 340     destruct case_AWeak.
 341       exists []; split.
 342       reflexivity.
 343       apply AWeak.
 344
 345     destruct case_ACont.
 346       exists (Σ₂',,Σ₂').
 347       subst; split.
 348       reflexivity.
 349       apply ACont.
 350
 351     destruct case_ALeft.
 352       destruct Σ₂'; try destruct o; inversion H; subst.
 353       destruct (rec _ (refl_equal _)).
 354       destruct p.
 355       rewrite e.
 356       rewrite <- mapOptionTree_distributes.
 357       eexists; split.
 358       reflexivity.
 359       apply ALeft.
 360       apply a0.
 361
 362     destruct case_ARight.
 363       destruct Σ₂'; try destruct o; inversion H; subst.
 364       destruct (rec _ (refl_equal _)).
 365       destruct p.
 366       rewrite e.
 367       rewrite <- mapOptionTree_distributes.
 368       eexists; split.
 369       reflexivity.
 370       apply ARight.
 371       apply a0.
 372
 373     destruct case_AComp.
 374       destruct (rec2 _ H).
 375       destruct p.
 376       destruct (rec1 _ e).
 377       destruct p.
 378       rewrite e0.
 379       eexists; split.
 380       reflexivity.
 381       eapply AComp.
 382         apply a1.
 383         apply a0.
 384         Defined.
 385
 386   Lemma arrangePullback {T Q}{f:T->Q}
 387     : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??T), Arrange Σ₁ (mapOptionTree f Σ₂) ->
 388       { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂) }.
 389     intros.
 390     eapply arrangePullback'.
 391     apply X.
 392     reflexivity.
 393     Defined.
 394
 395   (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
 396   (*
 397   Lemma arrangePullback {T} pred
 398     : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
 399     unfold takeT'.
 400     *)
 401
 402   (* like Arrange, but without weakening or contraction *)
 403   Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type :=
 404   | PId     : forall a        ,                    Permutation           a                  a
 405   | PCanL   : forall a        ,                    Permutation  (    [],,a   )      (       a   )
 406   | PCanR   : forall a        ,                    Permutation  (    a,,[]   )      (       a   )
 407   | PuCanL  : forall a        ,                    Permutation  (       a    )      (  [],,a    )
 408   | PuCanR  : forall a        ,                    Permutation  (       a    )      (  a,,[]    )
 409   | PAssoc  : forall a b c    ,                    Permutation  (a,,(b,,c)   )      ((a,,b),,c  )
 410   | PuAssoc : forall a b c    ,                    Permutation  ((a,,b),,c   )      ( a,,(b,,c) )
 411   | PExch   : forall a b      ,                    Permutation  (   (b,,a)   )      (  (a,,b)   )
 412   | PLeft   : forall {h}{c} x , Permutation h c -> Permutation  (    x,,h    )      (       x,,c)
 413   | PRight  : forall {h}{c} x , Permutation h c -> Permutation  (    h,,x    )      (       c,,x)
 414   | PComp   : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c
 415   .
 416   Notation "a ≈ b" := (@Permutation _ a b) (at level 30).
 417   Notation "a ⊆ b" := (@Arrange _ a b) (at level 30).
 418
 419   Definition permuteSwapMiddle {T} (a b c d:Tree ??T) :
 420     ((a,,b),,(c,,d)) ≈ ((a,,c),,(b,,d)).
 421     eapply PComp.
 422     apply  PuAssoc.
 423     eapply PComp.
 424     eapply PLeft.
 425     eapply PComp.
 426     eapply PAssoc.
 427     eapply PRight.
 428     apply  PExch.
 429     eapply PComp.
 430     eapply PLeft.
 431     eapply PuAssoc.
 432     eapply PAssoc.
 433     Defined.
 434
 435   Definition permuteMap :
 436     forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
 437       Σ₁ ≈ Σ₂ ->
 438       (mapOptionTree f Σ₁) ≈ (mapOptionTree f Σ₂).
 439     intros.
 440     induction X; simpl.
 441     apply PId.
 442     apply PCanL.
 443     apply PCanR.
 444     apply PuCanL.
 445     apply PuCanR.
 446     apply PAssoc.
 447     apply PuAssoc.
 448     apply PExch.
 449     apply  PLeft; auto.
 450     apply  PRight; auto.
 451     eapply PComp; [ apply IHX1 | apply IHX2 ].
 452     Defined.
 453
 454   (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
 455   Definition partitionPermutation :
 456     forall {T} (Σ:Tree ??T) (f:T -> bool),
 457       Σ ≈ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
 458     intros.
 459     induction Σ.
 460       simpl.
 461       destruct a.
 462       simpl.
 463       destruct (f t); simpl.
 464       apply PuCanL.
 465       apply PuCanR.
 466       simpl.
 467       apply PuCanL.
 468       simpl in *.
 469       eapply PComp; [ idtac | apply permuteSwapMiddle ].
 470       eapply PComp.
 471       eapply PLeft.
 472       apply IHΣ2.
 473       eapply PRight.
 474       apply IHΣ1.
 475       Defined.
 476
 477   Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b.
 478     intro arr.
 479     induction arr.
 480     apply AId.
 481     apply ACanL.
 482     apply ACanR.
 483     apply AuCanL.
 484     apply AuCanR.
 485     apply AAssoc.
 486     apply AuAssoc.
 487     apply AExch.
 488     apply ALeft; apply IHarr.
 489     apply ARight; apply IHarr.
 490     eapply AComp.
 491       apply IHarr1.
 492       apply IHarr2.
 493       Defined.
 494
 495   Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a.
 496     intro perm.
 497     induction perm.
 498     apply PId.
 499     apply PuCanL.
 500     apply PuCanR.
 501     apply PCanL.
 502     apply PCanR.
 503     apply PuAssoc.
 504     apply PAssoc.
 505     apply PExch.
 506     eapply PLeft; apply IHperm.
 507     eapply PRight; apply IHperm.
 508     eapply PComp.
 509       apply IHperm2.
 510       apply IHperm1.
 511       Defined.
 512
 513   (*
 514   Definition factorArrangementAsPermutation {T} : forall (a b:Tree ??T), a ⊆ b -> { c : _ & (c,,a) ≈ b }.
 515
 516     refine ((fix factor a b (arr:Arrange a b) :=
 517       match arr as R in Arrange A B return
 518         { c : _ & (c,,A) ≈ B }
 519         with
 520         | AId  a               => let case_AId := tt    in _
 521         | ACanL  a             => let case_ACanL := tt  in _
 522         | ACanR  a             => let case_ACanR := tt  in _
 523         | AuCanL a             => let case_AuCanL := tt in _
 524         | AuCanR a             => let case_AuCanR := tt in _
 525         | AAssoc a b c         => let case_AAssoc := tt in _
 526         | AuAssoc a b c         => let case_AuAssoc := tt in _
 527         | AExch  a b           => let case_AExch := tt  in _
 528         | AWeak  a             => let case_AWeak := tt  in _
 529         | ACont  a             => let case_ACont := tt  in _
 530         | ALeft  a b c r'      => let case_ALeft := tt  in (fun r'' => _) (factor _ _ r')
 531         | ARight a b c r'      => let case_ARight := tt in (fun r'' => _) (factor _ _ r')
 532         | AComp  a b c r1 r2   => let case_AComp := tt  in (fun r1' r2' => _) (factor _ _ r1) (factor _ _ r2)
 533       end)); clear factor; intros.
 534
 535     destruct case_AId.
 536       exists []. apply PCanL.
 537
 538     destruct case_ACanL.
 539       exists [].
 540       eapply PComp.
 541       apply PCanL.
 542       apply PCanL.
 543
 544     destruct case_ACanR.
 545       exists [].
 546       eapply PComp.
 547       apply PCanL.
 548       apply PCanR.
 549
 550     destruct case_AuCanL.
 551       exists [].
 552       apply PRight.
 553       apply PId.
 554
 555     destruct case_AuCanR.
 556       exists [].
 557       apply PExch.
 558
 559     destruct case_AAssoc.
 560       exists [].
 561       eapply PComp.
 562         eapply PCanL.
 563         apply PAssoc.
 564
 565     destruct case_AuAssoc.
 566       exists [].
 567       eapply PComp.
 568         eapply PCanL.
 569         apply PuAssoc.
 570
 571     destruct case_AExch.
 572       exists [].
 573       eapply PComp.
 574         eapply PCanL.
 575         apply PExch.
 576
 577     destruct case_AWeak.
 578       exists a0.
 579       eapply PCanR.
 580
 581     destruct case_ACont.
 582       exists [].
 583       eapply PComp.
 584       eapply PCanL.
 585       eapply PComp.
 586       eapply PLeft.
 587       eapply
 588
 589   Defined.
 590   *)
 591
 592 End NaturalDeductionContext.