From: Adam Megacz Date: Sat, 28 May 2011 03:43:15 +0000 (-0700) Subject: move Arrange into NaturalDeductionContext X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=db8c9d54c285980e162e393efd1b7316887e5b80 move Arrange into NaturalDeductionContext --- diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 4da66c7..d500e79 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -13,6 +13,7 @@ Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import HaskKinds. Require Import HaskLiterals. diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 9b3a163..cc9c9aa 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. @@ -45,52 +46,6 @@ Set Printing Width 130. *) Section HaskFlattener. - Definition getlev {Γ}{κ}(lht:LeveledHaskType Γ κ) : HaskLevel Γ := - match lht with t @@ l => l end. - - Definition arrange : - forall {T} (Σ:Tree ??T) (f:T -> bool), - Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))). - intros. - induction Σ. - simpl. - destruct a. - simpl. - destruct (f t); simpl. - apply RuCanL. - apply RuCanR. - simpl. - apply RuCanL. - simpl in *. - eapply RComp; [ idtac | apply arrangeSwapMiddle ]. - eapply RComp. - eapply RLeft. - apply IHΣ2. - eapply RRight. - apply IHΣ1. - Defined. - - Definition arrange' : - forall {T} (Σ:Tree ??T) (f:T -> bool), - Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ. - intros. - induction Σ. - simpl. - destruct a. - simpl. - destruct (f t); simpl. - apply RCanL. - apply RCanR. - simpl. - apply RCanL. - simpl in *. - eapply RComp; [ apply arrangeSwapMiddle | idtac ]. - eapply RComp. - eapply RLeft. - apply IHΣ2. - eapply RRight. - apply IHΣ1. - Defined. Ltac eqd_dec_refl' := match goal with diff --git a/src/HaskProof.v b/src/HaskProof.v index d92dd6b..c887b8a 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -10,6 +10,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. @@ -44,23 +45,6 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava }. Implicit Arguments ProofCaseBranch [ ]. -(* 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 -. - (* Figure 3, production $\vdash_E$, all rules *) Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := @@ -174,41 +158,3 @@ Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), Fa auto. Qed. -(* "Arrange" objects are parametric in the type of the leaves of the tree *) -Definition arrangeMap : - forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R), - Arrange Σ₁ Σ₂ -> - 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 ]. - Defined. - -(* a frequently-used Arrange *) -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. - Defined. diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 4319a1c..9d88e79 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import HaskKinds. diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 97ef42b..e70322e 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. diff --git a/src/HaskSkolemizer.v b/src/HaskSkolemizer.v index bb4dc92..76e1bdb 100644 --- a/src/HaskSkolemizer.v +++ b/src/HaskSkolemizer.v @@ -9,6 +9,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 8a49c81..8aa4005 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -6,6 +6,7 @@ Generalizable All Variables. Require Import Preamble. Require Import General. Require Import NaturalDeduction. +Require Import NaturalDeductionContext. Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import Coq.Init.Specif. @@ -15,20 +16,7 @@ Require Import HaskStrong. Require Import HaskProof. Section HaskStrongToProof. - -Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := - RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). - -Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := - RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). - -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. - Defined. - + Context {VV:Type}{eqd_vv:EqDecidable VV}. (* maintenance of Xi *) diff --git a/src/NaturalDeductionContext.v b/src/NaturalDeductionContext.v new file mode 100644 index 0000000..4e9a802 --- /dev/null +++ b/src/NaturalDeductionContext.v @@ -0,0 +1,128 @@ +(*********************************************************************************************************************************) +(* NaturalDeductionContext: *) +(* *) +(* Manipulations of a context in natural deduction proofs. *) +(* *) +(*********************************************************************************************************************************) + +Generalizable All Variables. +Require Import Preamble. +Require Import General. +Require Import NaturalDeduction. + +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 + . + + (* "Arrange" objects are parametric in the type of the leaves of the tree *) + Definition arrangeMap : + forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R), + Arrange Σ₁ Σ₂ -> + 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 ]. + Defined. + + (* a frequently-used Arrange *) + 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. + Defined. + + Definition arrange : + forall {T} (Σ:Tree ??T) (f:T -> bool), + Arrange Σ (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))). + intros. + induction Σ. + simpl. + destruct a. + simpl. + destruct (f t); simpl. + apply RuCanL. + apply RuCanR. + simpl. + apply RuCanL. + simpl in *. + eapply RComp; [ idtac | apply arrangeSwapMiddle ]. + eapply RComp. + eapply RLeft. + apply IHΣ2. + eapply RRight. + apply IHΣ1. + Defined. + + Definition arrange' : + forall {T} (Σ:Tree ??T) (f:T -> bool), + Arrange (dropT (mkFlags (liftBoolFunc false f) Σ),,( (dropT (mkFlags (liftBoolFunc false (bnot ○ f)) Σ)))) Σ. + intros. + induction Σ. + simpl. + destruct a. + simpl. + destruct (f t); simpl. + apply RCanL. + apply RCanR. + simpl. + apply RCanL. + simpl in *. + eapply RComp; [ apply arrangeSwapMiddle | idtac ]. + eapply RComp. + eapply RLeft. + apply IHΣ2. + eapply RRight. + apply IHΣ1. + Defined. + + Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := + RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). + + Definition pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) := + RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _). + + 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. + Defined. + +End NaturalDeductionContext.