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   (*
 403   (* like Arrange, but without weakening or contraction *)
 404   Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type :=
 405   | PId     : forall a        ,                    Permutation           a                  a
 406   | PCanL   : forall a        ,                    Permutation  (    [],,a   )      (       a   )
 407   | PCanR   : forall a        ,                    Permutation  (    a,,[]   )      (       a   )
 408   | PuCanL  : forall a        ,                    Permutation  (       a    )      (  [],,a    )
 409   | PuCanR  : forall a        ,                    Permutation  (       a    )      (  a,,[]    )
 410   | PAssoc  : forall a b c    ,                    Permutation  (a,,(b,,c)   )      ((a,,b),,c  )
 411   | PuAssoc : forall a b c    ,                    Permutation  ((a,,b),,c   )      ( a,,(b,,c) )
 412   | PExch   : forall a b      ,                    Permutation  (   (b,,a)   )      (  (a,,b)   )
 413   | PLeft   : forall {h}{c} x , Permutation h c -> Permutation  (    x,,h    )      (       x,,c)
 414   | PRight  : forall {h}{c} x , Permutation h c -> Permutation  (    h,,x    )      (       c,,x)
 415   | PComp   : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c
 416   .
 417   Notation "a ≈ b" := (@Permutation _ a b) (at level 30).
 418
 419   Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b.
 420     admit.
 421     Defined.
 422
 423   Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a.
 424     admit.
 425     Defined.
 426
 427   Definition partition {Γ}{ec:HaskEC Γ} Σ :
 428      Σ ≈ ((dropEC ec Σ),, (takeEC ec Σ +@@@+ ec)).
 429      admit.
 430      Defined.
 431   *)
 432
 433 End NaturalDeductionContext.