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 | 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
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 AComp; [ 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 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 _ _ _).
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 _ _ _).
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)) ].
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 AComp; [ 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 AComp; [ 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 | 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.
229 simpl; destruct (pred None); simpl; apply ACanL.
232 simpl; destruct (pred None); simpl; apply ACanR.
234 destruct case_AuCanL.
235 simpl; destruct (pred None); simpl; apply AuCanL.
237 destruct case_AuCanR.
238 simpl; destruct (pred None); simpl; apply AuCanR.
241 simpl; destruct (pred None); simpl; apply AWeak.
244 simpl; destruct (pred None); simpl; apply ACont.
248 Lemma arrangePullback' {T Q}{f:T->Q}
249 : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??Q), Arrange Σ₁ Σ₂ ->
250 forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
251 { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
254 refine ((fix arrangePullback Σ₁ Σ₂ (arr:Arrange Σ₁ Σ₂) {struct arr} :
255 forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') ->
256 { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
258 match arr as R in Arrange A B return
259 forall Σ₂', B = (mapOptionTree f Σ₂') ->
260 { Σ₁' : Tree ??T & prod (A = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') }
262 | AId a => let case_AId := tt in _
263 | ACanL a => let case_ACanL := tt in _
264 | ACanR a => let case_ACanR := tt in _
265 | AuCanL a => let case_AuCanL := tt in _
266 | AuCanR a => let case_AuCanR := tt in _
267 | AAssoc a b c => let case_AAssoc := tt in _
268 | AuAssoc a b c => let case_AuAssoc := tt in _
269 | AExch a b => let case_AExch := tt in _
270 | AWeak a => let case_AWeak := tt in _
271 | ACont a => let case_ACont := tt in _
272 | ALeft a b c r' => let case_ALeft := tt in (fun rec => _) (arrangePullback _ _ r')
273 | ARight a b c r' => let case_ARight := tt in (fun rec => _) (arrangePullback _ _ r')
274 | AComp a b c r1 r2 => let case_AComp := tt in (fun rec1 rec2 => _) (arrangePullback _ _ r1) (arrangePullback _ _ r2)
275 end)); clear arrangePullback; intros.
284 exists ([],,Σ₂'); split.
291 exists (Σ₂',,[]); split.
297 destruct case_AuCanL.
298 destruct Σ₂'; try destruct o; inversion H; subst.
303 destruct Σ₂'1; try destruct o; inversion H2.
306 destruct case_AuCanR.
307 destruct Σ₂'; try destruct o; inversion H; subst.
312 destruct Σ₂'2; try destruct o; inversion H2.
315 destruct case_AAssoc.
316 destruct Σ₂'; try destruct o; inversion H; subst.
317 destruct Σ₂'1; try destruct o; inversion H; subst.
318 rewrite <- mapOptionTree_distributes.
319 rewrite <- mapOptionTree_distributes.
324 destruct case_AuAssoc.
325 destruct Σ₂'; try destruct o; inversion H; subst.
326 destruct Σ₂'2; try destruct o; inversion H; subst.
327 rewrite <- mapOptionTree_distributes.
328 rewrite <- mapOptionTree_distributes.
334 destruct Σ₂'; try destruct o; inversion H; subst.
335 rewrite <- mapOptionTree_distributes.
352 destruct Σ₂'; try destruct o; inversion H; subst.
353 destruct (rec _ (refl_equal _)).
356 rewrite <- mapOptionTree_distributes.
362 destruct case_ARight.
363 destruct Σ₂'; try destruct o; inversion H; subst.
364 destruct (rec _ (refl_equal _)).
367 rewrite <- mapOptionTree_distributes.
386 Lemma arrangePullback {T Q}{f:T->Q}
387 : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??T), Arrange Σ₁ (mapOptionTree f Σ₂) ->
388 { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂) }.
390 eapply arrangePullback'.
395 (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *)
397 Lemma arrangePullback {T} pred
398 : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)).
402 (* like Arrange, but without weakening or contraction *)
403 Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type :=
404 | PId : forall a , Permutation a a
405 | PCanL : forall a , Permutation ( [],,a ) ( a )
406 | PCanR : forall a , Permutation ( a,,[] ) ( a )
407 | PuCanL : forall a , Permutation ( a ) ( [],,a )
408 | PuCanR : forall a , Permutation ( a ) ( a,,[] )
409 | PAssoc : forall a b c , Permutation (a,,(b,,c) ) ((a,,b),,c )
410 | PuAssoc : forall a b c , Permutation ((a,,b),,c ) ( a,,(b,,c) )
411 | PExch : forall a b , Permutation ( (b,,a) ) ( (a,,b) )
412 | PLeft : forall {h}{c} x , Permutation h c -> Permutation ( x,,h ) ( x,,c)
413 | PRight : forall {h}{c} x , Permutation h c -> Permutation ( h,,x ) ( c,,x)
414 | PComp : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c
416 Notation "a ≈ b" := (@Permutation _ a b) (at level 30).
417 Notation "a ⊆ b" := (@Arrange _ a b) (at level 30).
419 Definition permuteSwapMiddle {T} (a b c d:Tree ??T) :
420 ((a,,b),,(c,,d)) ≈ ((a,,c),,(b,,d)).
435 Definition permuteMap :
436 forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
438 (mapOptionTree f Σ₁) ≈ (mapOptionTree f Σ₂).
451 eapply PComp; [ apply IHX1 | apply IHX2 ].
454 (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *)
455 Definition partitionPermutation :
456 forall {T} (Σ:Tree ??T) (f:T -> bool),
457 Σ ≈ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))).
463 destruct (f t); simpl.
469 eapply PComp; [ idtac | apply permuteSwapMiddle ].
477 Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b.
488 apply ALeft; apply IHarr.
489 apply ARight; apply IHarr.
495 Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a.
506 eapply PLeft; apply IHperm.
507 eapply PRight; apply IHperm.
514 Definition factorArrangementAsPermutation {T} : forall (a b:Tree ??T), a ⊆ b -> { c : _ & (c,,a) ≈ b }.
516 refine ((fix factor a b (arr:Arrange a b) :=
517 match arr as R in Arrange A B return
518 { c : _ & (c,,A) ≈ B }
520 | AId a => let case_AId := tt in _
521 | ACanL a => let case_ACanL := tt in _
522 | ACanR a => let case_ACanR := tt in _
523 | AuCanL a => let case_AuCanL := tt in _
524 | AuCanR a => let case_AuCanR := tt in _
525 | AAssoc a b c => let case_AAssoc := tt in _
526 | AuAssoc a b c => let case_AuAssoc := tt in _
527 | AExch a b => let case_AExch := tt in _
528 | AWeak a => let case_AWeak := tt in _
529 | ACont a => let case_ACont := tt in _
530 | ALeft a b c r' => let case_ALeft := tt in (fun r'' => _) (factor _ _ r')
531 | ARight a b c r' => let case_ARight := tt in (fun r'' => _) (factor _ _ r')
532 | AComp a b c r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (factor _ _ r1) (factor _ _ r2)
533 end)); clear factor; intros.
536 exists []. apply PCanL.
550 destruct case_AuCanL.
555 destruct case_AuCanR.
559 destruct case_AAssoc.
565 destruct case_AuAssoc.
592 End NaturalDeductionContext.