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 - 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)).
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 _ _ _).
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 _ _ _).
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)) ].
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)) Σ)))).
95 destruct (f t); simpl.
101 eapply RComp; [ idtac | apply arrangeSwapMiddle ].
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)) Σ)))) Σ.
118 destruct (f t); simpl.
124 eapply RComp; [ apply arrangeSwapMiddle | idtac ].
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.
139 | T_Branch b1 b2 => let b1' := foo b1 in let b2' := foo b2 in _
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 ->
169 destruct t; try destruct o; inversion H.
170 set (IHq1 _ H1) as x1.
171 set (IHq2 _ H2) as x2.
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 ->
192 destruct t; try destruct o; inversion H.
193 set (IHq1 _ H1) as x1.
194 set (IHq2 _ H2) as x2.
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 Σ₂)).
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.
229 simpl; destruct (pred None); simpl; apply RCanL.
232 simpl; destruct (pred None); simpl; apply RCanR.
234 destruct case_RuCanL.
235 simpl; destruct (pred None); simpl; apply RuCanL.
237 destruct case_RuCanR.
238 simpl; destruct (pred None); simpl; apply RuCanR.
241 simpl; destruct (pred None); simpl; apply RWeak.
244 simpl; destruct (pred None); simpl; apply RCont.
248 (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
250 Lemma arrangeTake {T} pred
251 : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
255 End NaturalDeductionContext.