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 *)
  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   Definition arrange :
  72     forall {T} (Σ:Tree ??T) (f:T -> bool),
  73       Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
  74     intros.
  75     induction Σ.
  76       simpl.
  77       destruct a.
  78       simpl.
  79       destruct (f t); simpl.
  80       apply RuCanL.
  81       apply RuCanR.
  82       simpl.
  83       apply RuCanL.
  84       simpl in *.
  85       eapply RComp; [ idtac | apply arrangeSwapMiddle ].
  86       eapply RComp.
  87       eapply RLeft.
  88       apply IHΣ2.
  89       eapply RRight.
  90       apply IHΣ1.
  91       Defined.
  92
  93   Definition arrange' :
  94     forall {T} (Σ:Tree ??T) (f:T -> bool),
  95       Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
  96     intros.
  97     induction Σ.
  98       simpl.
  99       destruct a.
 100       simpl.
 101       destruct (f t); simpl.
 102       apply RCanL.
 103       apply RCanR.
 104       simpl.
 105       apply RCanL.
 106       simpl in *.
 107       eapply RComp; [ apply arrangeSwapMiddle | idtac ].
 108       eapply RComp.
 109       eapply RLeft.
 110       apply IHΣ2.
 111       eapply RRight.
 112       apply IHΣ1.
 113       Defined.
 114
 115   Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
 116     RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
 117
 118   Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
 119     RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
 120
 121   Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
 122     eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
 123     eapply RComp; [ idtac | apply RCossa ].
 124     eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
 125     apply RAssoc.
 126     Defined.
 127
 128 End NaturalDeductionContext.