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   | RId     : forall a        ,                Arrange           a                  a
  18   | RCanL   : forall a        ,                Arrange  (    [],,a   )      (       a   )
  19   | RCanR   : forall a        ,                Arrange  (    a,,[]   )      (       a   )
  20   | RuCanL  : forall a        ,                Arrange  (       a    )      (  [],,a    )
  21   | RuCanR  : forall a        ,                Arrange  (       a    )      (  a,,[]    )
  22   | RAssoc  : forall a b c    ,                Arrange  (a,,(b,,c)   )      ((a,,b),,c  )
  23   | RCossa  : forall a b c    ,                Arrange  ((a,,b),,c   )      ( a,,(b,,c) )
  24   | RExch   : forall a b      ,                Arrange  (   (b,,a)   )      (  (a,,b)   )
  25   | RWeak   : forall a        ,                Arrange  (       []   )      (       a   )
  26   | RCont   : forall a        ,                Arrange  (  (a,,a)    )      (       a   )
  27   | RLeft   : forall {h}{c} x , Arrange h c -> Arrange  (    x,,h    )      (       x,,c)
  28   | RRight  : forall {h}{c} x , Arrange h c -> Arrange  (    h,,x    )      (       c,,x)
  29   | RComp   : 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 RId.
  40     apply RCanL.
  41     apply RCanR.
  42     apply RuCanL.
  43     apply RuCanR.
  44     apply RAssoc.
  45     apply RCossa.
  46     apply RExch.
  47     apply RWeak.
  48     apply RCont.
  49     apply RLeft; auto.
  50     apply RRight; auto.
  51     eapply RComp; [ 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 RComp.
  58     apply RCossa.
  59     eapply RComp.
  60     eapply RLeft.
  61     eapply RComp.
  62     eapply RAssoc.
  63     eapply RRight.
  64     apply RExch.
  65     eapply RComp.
  66     eapply RLeft.
  67     eapply RCossa.
  68     eapply RAssoc.
  69     Defined.
  70
  71   (* like RExch, 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     RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
  74
  75   (* like RExch, 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     RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
  78
  79   Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
  80     eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
  81     eapply RComp; [ idtac | apply RCossa ].
  82     eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
  83     apply RAssoc.
  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 RuCanL.
  97       apply RuCanR.
  98       simpl.
  99       apply RuCanL.
 100       simpl in *.
 101       eapply RComp; [ idtac | apply arrangeSwapMiddle ].
 102       eapply RComp.
 103       eapply RLeft.
 104       apply IHΣ2.
 105       eapply RRight.
 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 RCanL.
 120       apply RCanR.
 121       simpl.
 122       apply RCanL.
 123       simpl in *.
 124       eapply RComp; [ apply arrangeSwapMiddle | idtac ].
 125       eapply RComp.
 126       eapply RLeft.
 127       apply IHΣ2.
 128       eapply RRight.
 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 RId.
 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 RComp.
 173         eapply RRight.
 174         rewrite <- H1.
 175         apply x1.
 176       eapply RComp.
 177         apply RCanL.
 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 RId.
 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 RComp.
 196         apply RuCanL.
 197       eapply RComp.
 198         eapply RRight.
 199         apply x1.
 200       eapply RComp.
 201         eapply RLeft.
 202         apply x2.
 203       rewrite H.
 204       apply RId.
 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         | RId  a               => let case_RId := tt    in RId _
 214         | RCanL  a             => let case_RCanL := tt  in _
 215         | RCanR  a             => let case_RCanR := tt  in _
 216         | RuCanL a             => let case_RuCanL := tt in _
 217         | RuCanR a             => let case_RuCanR := tt in _
 218         | RAssoc a b c         => let case_RAssoc := tt in RAssoc _ _ _
 219         | RCossa a b c         => let case_RCossa := tt in RCossa _ _ _
 220         | RExch  a b           => let case_RExch := tt  in RExch _ _
 221         | RWeak  a             => let case_RWeak := tt  in _
 222         | RCont  a             => let case_RCont := tt  in _
 223         | RLeft  a b c r'      => let case_RLeft := tt  in RLeft  _ (arrangeTake _ _ r')
 224         | RRight a b c r'      => let case_RRight := tt in RRight _ (arrangeTake _ _ r')
 225         | RComp  a b c r1 r2   => let case_RComp := tt  in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2)
 226       end)); clear arrangeTake; intros.
 227
 228     destruct case_RCanL.
 229       simpl; destruct (pred None); simpl; apply RCanL.
 230
 231     destruct case_RCanR.
 232       simpl; destruct (pred None); simpl; apply RCanR.
 233
 234     destruct case_RuCanL.
 235       simpl; destruct (pred None); simpl; apply RuCanL.
 236
 237     destruct case_RuCanR.
 238       simpl; destruct (pred None); simpl; apply RuCanR.
 239
 240     destruct case_RWeak.
 241       simpl; destruct (pred None); simpl; apply RWeak.
 242
 243     destruct case_RCont.
 244       simpl; destruct (pred None); simpl; apply RCont.
 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.