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   (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
 249   (*
 250   Lemma arrangeTake {T} pred
 251     : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
 252     unfold takeT'.
 253     *)
 254
 255 End NaturalDeductionContext.