1 (*********************************************************************************************************************************)
2 (* NaturalDeductionContext: *)
4 (* Manipulations of a context in natural deduction proofs. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
13 Section NaturalDeductionContext.
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
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),
36 Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
51 eapply RComp; [ apply IHX1 | apply IHX2 ].
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)).
72 forall {T} (Σ:Tree ??T) (f:T -> bool),
73 Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
79 destruct (f t); simpl.
85 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
94 forall {T} (Σ:Tree ??T) (f:T -> bool),
95 Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ.
101 destruct (f t); simpl.
107 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
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 _ _ _).
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 _ _ _).
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)) ].
128 End NaturalDeductionContext.