X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FNaturalDeductionContext.v;h=4da89223e90419049776720208663105dfd653c1;hp=03fc70453ae884746d821519c3980f7d47cc5287;hb=6eacd82007b7dacd704e50e5da0a9c988827f86c;hpb=91f06dc68cf5888360f1819429b10e054f94b243 diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v index 03fc704..4da8922 100644 --- a/src/NaturalDeductionContext.v +++ b/src/NaturalDeductionContext.v @@ -14,19 +14,19 @@ Section NaturalDeductionContext. (* Figure 3, production $\vdash_E$, Uniform rules *) Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type := - | RId : forall a , Arrange a a - | RCanL : forall a , Arrange ( [],,a ) ( a ) - | RCanR : forall a , Arrange ( a,,[] ) ( a ) - | RuCanL : forall a , Arrange ( a ) ( [],,a ) - | RuCanR : forall a , Arrange ( a ) ( a,,[] ) - | RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c ) - | RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) ) - | RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) ) - | RWeak : forall a , Arrange ( [] ) ( a ) - | RCont : forall a , Arrange ( (a,,a) ) ( a ) - | RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c) - | RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x) - | RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c + | AId : forall a , Arrange a a + | ACanL : forall a , Arrange ( [],,a ) ( a ) + | ACanR : forall a , Arrange ( a,,[] ) ( a ) + | AuCanL : forall a , Arrange ( a ) ( [],,a ) + | AuCanR : forall a , Arrange ( a ) ( a,,[] ) + | AAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c ) + | AuAssoc : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) ) + | AExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) ) + | AWeak : forall a , Arrange ( [] ) ( a ) + | ACont : forall a , Arrange ( (a,,a) ) ( a ) + | ALeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c) + | ARight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x) + | AComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c . (* "Arrange" objects are parametric in the type of the leaves of the tree *) @@ -36,51 +36,51 @@ Section NaturalDeductionContext. Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂). intros. induction X; simpl. - apply RId. - apply RCanL. - apply RCanR. - apply RuCanL. - apply RuCanR. - apply RAssoc. - apply RCossa. - apply RExch. - apply RWeak. - apply RCont. - apply RLeft; auto. - apply RRight; auto. - eapply RComp; [ apply IHX1 | apply IHX2 ]. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. + apply AWeak. + apply ACont. + apply ALeft; auto. + apply ARight; auto. + eapply AComp; [ apply IHX1 | apply IHX2 ]. Defined. (* a frequently-used Arrange - swap the middle two elements of a four-element sequence *) Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) : Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)). - eapply RComp. - apply RCossa. - eapply RComp. - eapply RLeft. - eapply RComp. - eapply RAssoc. - eapply RRight. - apply RExch. - eapply RComp. - eapply RLeft. - eapply RCossa. - eapply RAssoc. + eapply AComp. + apply AuAssoc. + eapply AComp. + eapply ALeft. + eapply AComp. + eapply AAssoc. + eapply ARight. + apply AExch. + eapply AComp. + eapply ALeft. + eapply AuAssoc. + eapply AAssoc. Defined. - (* like RExch, but works on nodes which are an Assoc away from being adjacent *) + (* like AExch, but works on nodes which are an Assoc away from being adjacent *) Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := - RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). + AComp (AComp (AuAssoc _ _ _) (ALeft a (AExch c b))) (AAssoc _ _ _). - (* like RExch, but works on nodes which are an Assoc away from being adjacent *) + (* like AExch, but works on nodes which are an Assoc away from being adjacent *) Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := - RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). + AComp (AComp (AAssoc _ _ _) (ARight c (AExch b a))) (AuAssoc _ _ _). Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b). - eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ]. - eapply RComp; [ idtac | apply RCossa ]. - eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ]. - apply RAssoc. + eapply AComp; [ idtac | apply (ALeft (a,,c) (ACont b)) ]. + eapply AComp; [ idtac | apply AuAssoc ]. + eapply AComp; [ idtac | apply (ARight b (pivotContext a b c)) ]. + apply AAssoc. Defined. (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *) @@ -93,16 +93,16 @@ Section NaturalDeductionContext. destruct a. simpl. destruct (f t); simpl. - apply RuCanL. - apply RuCanR. + apply AuCanL. + apply AuCanR. simpl. - apply RuCanL. + apply AuCanL. simpl in *. - eapply RComp; [ idtac | apply arrangeSwapMiddle ]. - eapply RComp. - eapply RLeft. + eapply AComp; [ idtac | apply arrangeSwapMiddle ]. + eapply AComp. + eapply ALeft. apply IHΣ2. - eapply RRight. + eapply ARight. apply IHΣ1. Defined. @@ -116,16 +116,16 @@ Section NaturalDeductionContext. destruct a. simpl. destruct (f t); simpl. - apply RCanL. - apply RCanR. + apply ACanL. + apply ACanR. simpl. - apply RCanL. + apply ACanL. simpl in *. - eapply RComp; [ apply arrangeSwapMiddle | idtac ]. - eapply RComp. - eapply RLeft. + eapply AComp; [ apply arrangeSwapMiddle | idtac ]. + eapply AComp. + eapply ALeft. apply IHΣ2. - eapply RRight. + eapply ARight. apply IHΣ1. Defined. @@ -164,17 +164,17 @@ Section NaturalDeductionContext. induction q; intros. simpl in H. rewrite H. - apply RId. + apply AId. simpl in *. destruct t; try destruct o; inversion H. set (IHq1 _ H1) as x1. set (IHq2 _ H2) as x2. - eapply RComp. - eapply RRight. + eapply AComp. + eapply ARight. rewrite <- H1. apply x1. - eapply RComp. - apply RCanL. + eapply AComp. + apply ACanL. rewrite <- H2. apply x2. Defined. @@ -187,21 +187,21 @@ Section NaturalDeductionContext. induction q; intros. simpl in H. rewrite H. - apply RId. + apply AId. simpl in *. destruct t; try destruct o; inversion H. set (IHq1 _ H1) as x1. set (IHq2 _ H2) as x2. - eapply RComp. - apply RuCanL. - eapply RComp. - eapply RRight. + eapply AComp. + apply AuCanL. + eapply AComp. + eapply ARight. apply x1. - eapply RComp. - eapply RLeft. + eapply AComp. + eapply ALeft. apply x2. rewrite H. - apply RId. + apply AId. Defined. (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (dropT Σ₁) to (dropT Σ₂) *) @@ -210,46 +210,383 @@ Section NaturalDeductionContext. refine ((fix arrangeTake t1 t2 (arr:Arrange t1 t2) := match arr as R in Arrange A B return Arrange (dropT (mkFlags pred A)) (dropT (mkFlags pred B)) with - | RId a => let case_RId := tt in RId _ - | RCanL a => let case_RCanL := tt in _ - | RCanR a => let case_RCanR := tt in _ - | RuCanL a => let case_RuCanL := tt in _ - | RuCanR a => let case_RuCanR := tt in _ - | RAssoc a b c => let case_RAssoc := tt in RAssoc _ _ _ - | RCossa a b c => let case_RCossa := tt in RCossa _ _ _ - | RExch a b => let case_RExch := tt in RExch _ _ - | RWeak a => let case_RWeak := tt in _ - | RCont a => let case_RCont := tt in _ - | RLeft a b c r' => let case_RLeft := tt in RLeft _ (arrangeTake _ _ r') - | RRight a b c r' => let case_RRight := tt in RRight _ (arrangeTake _ _ r') - | RComp a b c r1 r2 => let case_RComp := tt in RComp (arrangeTake _ _ r1) (arrangeTake _ _ r2) + | AId a => let case_AId := tt in AId _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in AAssoc _ _ _ + | AuAssoc a b c => let case_AuAssoc := tt in AuAssoc _ _ _ + | AExch a b => let case_AExch := tt in AExch _ _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | ALeft a b c r' => let case_ALeft := tt in ALeft _ (arrangeTake _ _ r') + | ARight a b c r' => let case_ARight := tt in ARight _ (arrangeTake _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in AComp (arrangeTake _ _ r1) (arrangeTake _ _ r2) end)); clear arrangeTake; intros. - destruct case_RCanL. - simpl; destruct (pred None); simpl; apply RCanL. + destruct case_ACanL. + simpl; destruct (pred None); simpl; apply ACanL. - destruct case_RCanR. - simpl; destruct (pred None); simpl; apply RCanR. + destruct case_ACanR. + simpl; destruct (pred None); simpl; apply ACanR. - destruct case_RuCanL. - simpl; destruct (pred None); simpl; apply RuCanL. + destruct case_AuCanL. + simpl; destruct (pred None); simpl; apply AuCanL. - destruct case_RuCanR. - simpl; destruct (pred None); simpl; apply RuCanR. + destruct case_AuCanR. + simpl; destruct (pred None); simpl; apply AuCanR. - destruct case_RWeak. - simpl; destruct (pred None); simpl; apply RWeak. + destruct case_AWeak. + simpl; destruct (pred None); simpl; apply AWeak. - destruct case_RCont. - simpl; destruct (pred None); simpl; apply RCont. + destruct case_ACont. + simpl; destruct (pred None); simpl; apply ACont. Defined. + Lemma arrangePullback' {T Q}{f:T->Q} + : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??Q), Arrange Σ₁ Σ₂ -> + forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') -> + { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') } + . + + refine ((fix arrangePullback Σ₁ Σ₂ (arr:Arrange Σ₁ Σ₂) {struct arr} : + forall Σ₂', Σ₂ = (mapOptionTree f Σ₂') -> + { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') } + := + match arr as R in Arrange A B return + forall Σ₂', B = (mapOptionTree f Σ₂') -> + { Σ₁' : Tree ??T & prod (A = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂') } + with + | AId a => let case_AId := tt in _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in _ + | AuAssoc a b c => let case_AuAssoc := tt in _ + | AExch a b => let case_AExch := tt in _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | ALeft a b c r' => let case_ALeft := tt in (fun rec => _) (arrangePullback _ _ r') + | ARight a b c r' => let case_ARight := tt in (fun rec => _) (arrangePullback _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in (fun rec1 rec2 => _) (arrangePullback _ _ r1) (arrangePullback _ _ r2) + end)); clear arrangePullback; intros. + + destruct case_AId. + exists Σ₂'; split. + subst. + reflexivity. + apply AId. + + destruct case_ACanL. + exists ([],,Σ₂'); split. + subst. + simpl. + reflexivity. + apply ACanL. + + destruct case_ACanR. + exists (Σ₂',,[]); split. + subst. + simpl. + reflexivity. + apply ACanR. + + destruct case_AuCanL. + destruct Σ₂'; try destruct o; inversion H; subst. + eexists; split. + reflexivity. + simpl in H. + inversion H. + destruct Σ₂'1; try destruct o; inversion H2. + apply AuCanL. + + destruct case_AuCanR. + destruct Σ₂'; try destruct o; inversion H; subst. + eexists; split. + reflexivity. + simpl in H. + inversion H. + destruct Σ₂'2; try destruct o; inversion H2. + apply AuCanR. + + destruct case_AAssoc. + destruct Σ₂'; try destruct o; inversion H; subst. + destruct Σ₂'1; try destruct o; inversion H; subst. + rewrite <- mapOptionTree_distributes. + rewrite <- mapOptionTree_distributes. + eexists; split. + reflexivity. + apply AAssoc. + + destruct case_AuAssoc. + destruct Σ₂'; try destruct o; inversion H; subst. + destruct Σ₂'2; try destruct o; inversion H; subst. + rewrite <- mapOptionTree_distributes. + rewrite <- mapOptionTree_distributes. + eexists; split. + reflexivity. + apply AuAssoc. + + destruct case_AExch. + destruct Σ₂'; try destruct o; inversion H; subst. + rewrite <- mapOptionTree_distributes. + eexists; split. + reflexivity. + apply AExch. + + destruct case_AWeak. + exists []; split. + reflexivity. + apply AWeak. + + destruct case_ACont. + exists (Σ₂',,Σ₂'). + subst; split. + reflexivity. + apply ACont. + + destruct case_ALeft. + destruct Σ₂'; try destruct o; inversion H; subst. + destruct (rec _ (refl_equal _)). + destruct p. + rewrite e. + rewrite <- mapOptionTree_distributes. + eexists; split. + reflexivity. + apply ALeft. + apply a0. + + destruct case_ARight. + destruct Σ₂'; try destruct o; inversion H; subst. + destruct (rec _ (refl_equal _)). + destruct p. + rewrite e. + rewrite <- mapOptionTree_distributes. + eexists; split. + reflexivity. + apply ARight. + apply a0. + + destruct case_AComp. + destruct (rec2 _ H). + destruct p. + destruct (rec1 _ e). + destruct p. + rewrite e0. + eexists; split. + reflexivity. + eapply AComp. + apply a1. + apply a0. + Defined. + + Lemma arrangePullback {T Q}{f:T->Q} + : forall (Σ₁:Tree ??Q)(Σ₂:Tree ??T), Arrange Σ₁ (mapOptionTree f Σ₂) -> + { Σ₁' : Tree ??T & prod (Σ₁ = (mapOptionTree f Σ₁')) (Arrange Σ₁' Σ₂) }. + intros. + eapply arrangePullback'. + apply X. + reflexivity. + Defined. + (* given an Arrange from Σ₁ to Σ₂ and any predicate on tree nodes, we can construct an Arrange from (takeT Σ₁) to (takeT Σ₂) *) (* - Lemma arrangeTake {T} pred + Lemma arrangePullback {T} pred : forall (Σ₁ Σ₂: Tree ??T), Arrange Σ₁ Σ₂ -> Arrange (takeT' (mkFlags pred Σ₁)) (takeT' (mkFlags pred Σ₂)). unfold takeT'. *) + (* like Arrange, but without weakening or contraction *) + Inductive Permutation {T} : Tree ??T -> Tree ??T -> Type := + | PId : forall a , Permutation a a + | PCanL : forall a , Permutation ( [],,a ) ( a ) + | PCanR : forall a , Permutation ( a,,[] ) ( a ) + | PuCanL : forall a , Permutation ( a ) ( [],,a ) + | PuCanR : forall a , Permutation ( a ) ( a,,[] ) + | PAssoc : forall a b c , Permutation (a,,(b,,c) ) ((a,,b),,c ) + | PuAssoc : forall a b c , Permutation ((a,,b),,c ) ( a,,(b,,c) ) + | PExch : forall a b , Permutation ( (b,,a) ) ( (a,,b) ) + | PLeft : forall {h}{c} x , Permutation h c -> Permutation ( x,,h ) ( x,,c) + | PRight : forall {h}{c} x , Permutation h c -> Permutation ( h,,x ) ( c,,x) + | PComp : forall {a}{b}{c}, Permutation a b -> Permutation b c -> Permutation a c + . + Notation "a ≈ b" := (@Permutation _ a b) (at level 30). + Notation "a ⊆ b" := (@Arrange _ a b) (at level 30). + + Definition permuteSwapMiddle {T} (a b c d:Tree ??T) : + ((a,,b),,(c,,d)) ≈ ((a,,c),,(b,,d)). + eapply PComp. + apply PuAssoc. + eapply PComp. + eapply PLeft. + eapply PComp. + eapply PAssoc. + eapply PRight. + apply PExch. + eapply PComp. + eapply PLeft. + eapply PuAssoc. + eapply PAssoc. + Defined. + + Definition permuteMap : + forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R), + Σ₁ ≈ Σ₂ -> + (mapOptionTree f Σ₁) ≈ (mapOptionTree f Σ₂). + intros. + induction X; simpl. + apply PId. + apply PCanL. + apply PCanR. + apply PuCanL. + apply PuCanR. + apply PAssoc. + apply PuAssoc. + apply PExch. + apply PLeft; auto. + apply PRight; auto. + eapply PComp; [ apply IHX1 | apply IHX2 ]. + Defined. + + (* given any set of TreeFlags on a tree, we can Arrange all of the flagged nodes into the left subtree *) + Definition partitionPermutation : + forall {T} (Σ:Tree ??T) (f:T -> bool), + Σ ≈ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))). + intros. + induction Σ. + simpl. + destruct a. + simpl. + destruct (f t); simpl. + apply PuCanL. + apply PuCanR. + simpl. + apply PuCanL. + simpl in *. + eapply PComp; [ idtac | apply permuteSwapMiddle ]. + eapply PComp. + eapply PLeft. + apply IHΣ2. + eapply PRight. + apply IHΣ1. + Defined. + + Definition permutationToArrangement {T}{a b:Tree ??T} : a ≈ b -> a ⊆ b. + intro arr. + induction arr. + apply AId. + apply ACanL. + apply ACanR. + apply AuCanL. + apply AuCanR. + apply AAssoc. + apply AuAssoc. + apply AExch. + apply ALeft; apply IHarr. + apply ARight; apply IHarr. + eapply AComp. + apply IHarr1. + apply IHarr2. + Defined. + + Definition invertPermutation {T}{a b:Tree ??T} : a ≈ b -> b ≈ a. + intro perm. + induction perm. + apply PId. + apply PuCanL. + apply PuCanR. + apply PCanL. + apply PCanR. + apply PuAssoc. + apply PAssoc. + apply PExch. + eapply PLeft; apply IHperm. + eapply PRight; apply IHperm. + eapply PComp. + apply IHperm2. + apply IHperm1. + Defined. + + (* + Definition factorArrangementAsPermutation {T} : forall (a b:Tree ??T), a ⊆ b -> { c : _ & (c,,a) ≈ b }. + + refine ((fix factor a b (arr:Arrange a b) := + match arr as R in Arrange A B return + { c : _ & (c,,A) ≈ B } + with + | AId a => let case_AId := tt in _ + | ACanL a => let case_ACanL := tt in _ + | ACanR a => let case_ACanR := tt in _ + | AuCanL a => let case_AuCanL := tt in _ + | AuCanR a => let case_AuCanR := tt in _ + | AAssoc a b c => let case_AAssoc := tt in _ + | AuAssoc a b c => let case_AuAssoc := tt in _ + | AExch a b => let case_AExch := tt in _ + | AWeak a => let case_AWeak := tt in _ + | ACont a => let case_ACont := tt in _ + | ALeft a b c r' => let case_ALeft := tt in (fun r'' => _) (factor _ _ r') + | ARight a b c r' => let case_ARight := tt in (fun r'' => _) (factor _ _ r') + | AComp a b c r1 r2 => let case_AComp := tt in (fun r1' r2' => _) (factor _ _ r1) (factor _ _ r2) + end)); clear factor; intros. + + destruct case_AId. + exists []. apply PCanL. + + destruct case_ACanL. + exists []. + eapply PComp. + apply PCanL. + apply PCanL. + + destruct case_ACanR. + exists []. + eapply PComp. + apply PCanL. + apply PCanR. + + destruct case_AuCanL. + exists []. + apply PRight. + apply PId. + + destruct case_AuCanR. + exists []. + apply PExch. + + destruct case_AAssoc. + exists []. + eapply PComp. + eapply PCanL. + apply PAssoc. + + destruct case_AuAssoc. + exists []. + eapply PComp. + eapply PCanL. + apply PuAssoc. + + destruct case_AExch. + exists []. + eapply PComp. + eapply PCanL. + apply PExch. + + destruct case_AWeak. + exists a0. + eapply PCanR. + + destruct case_ACont. + exists []. + eapply PComp. + eapply PCanL. + eapply PComp. + eapply PLeft. + eapply + + Defined. + *) + End NaturalDeductionContext.