From fd337b235014f43000773eb0d95168d89e93a893 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Mon, 28 Mar 2011 01:44:04 -0700 Subject: [PATCH 1/1] replace UJudg with Arrange --- src/ExtractionMain.v | 13 ++- src/HaskProof.v | 97 ++++----------------- src/HaskProofCategory.v | 4 +- src/HaskProofToLatex.v | 54 ++++++------ src/HaskProofToStrong.v | 215 ++++++++++++++++++----------------------------- src/HaskStrongToProof.v | 209 +++++++++++++++++++-------------------------- 6 files changed, 221 insertions(+), 371 deletions(-) diff --git a/src/ExtractionMain.v b/src/ExtractionMain.v index 2f0856f..ba0c241 100644 --- a/src/ExtractionMain.v +++ b/src/ExtractionMain.v @@ -35,13 +35,11 @@ Require Import HaskWeakToCore. Require Import HaskProofToStrong. Require Import ProgrammingLanguage. - Require Import HaskProofCategory. -(* -Require Import HaskStrongCategory. -*) Require Import ReificationsIsomorphicToGeneralizedArrows. +(*Require Import HaskStrongCategory.*) + Open Scope string_scope. Extraction Language Haskell. @@ -228,6 +226,7 @@ Section core2proof. apply t. Defined. +(* Definition env := ★::nil. Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _). Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]]. @@ -235,13 +234,13 @@ Section core2proof. eapply nd_comp. eapply nd_rule. apply RVar. - eapply nd_rule. - eapply (RURule _ _ _ _ (RuCanL _ _)) . + eapply nd_rule + eapply (RArrange _ _ _ _ (RuCanL _ _)) . eapply nd_rule. eapply RLam. Defined. -(* + Definition coreToCoreExpr' (ce:@CoreExpr CoreVar) : ???(@CoreExpr CoreVar) := addErrorMessage ("input CoreSyn: " +++ toString ce) (addErrorMessage ("input CoreType: " +++ toString (coreTypeOfCoreExpr ce)) ( diff --git a/src/HaskProof.v b/src/HaskProof.v index 7e3ef1c..4cc4605 100644 --- a/src/HaskProof.v +++ b/src/HaskProof.v @@ -32,23 +32,6 @@ Inductive Judg := Judg. Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). -(* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single, - * uniform context throughout the whole proof. Such proofs are important because (1) we can do left and right context - * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *) -Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) := - mkUJudg : - Tree ??(LeveledHaskType Γ ★) -> - Tree ??(LeveledHaskType Γ ★) -> - UJudg Γ Δ. - Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50). - Definition ext_tree_left {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end). - Definition ext_tree_right {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end). - -(* we can turn a UJudg into a Judg by simply internalizing the index *) -Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg := - match ej with mkUJudg t s => Γ > Δ > t |- s end. - Coercion UJudg2judg : UJudg >-> Judg. - (* information needed to define a case branch in a HaskProof *) Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} := { pcb_freevars : Tree ??(LeveledHaskType Γ ★) @@ -61,24 +44,25 @@ Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{ava Implicit Arguments ProofCaseBranch [ ]. (* Figure 3, production $\vdash_E$, Uniform rules *) -Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type := -| RCanL : ∀ t a , URule [Γ>>Δ> [],,a |- t ] [Γ>>Δ> a |- t ] -| RCanR : ∀ t a , URule [Γ>>Δ> a,,[] |- t ] [Γ>>Δ> a |- t ] -| RuCanL : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> [],,a |- t ] -| RuCanR : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> a,,[] |- t ] -| RAssoc : ∀ t a b c , URule [Γ>>Δ>a,,(b,,c) |- t ] [Γ>>Δ>(a,,b),,c |- t ] -| RCossa : ∀ t a b c , URule [Γ>>Δ>(a,,b),,c |- t ] [Γ>>Δ> a,,(b,,c) |- t ] -| RLeft : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c) -| RRight : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c) -| RExch : ∀ t a b , URule [Γ>>Δ> (b,,a) |- t ] [Γ>>Δ> (a,,b) |- t ] -| RWeak : ∀ t a , URule [Γ>>Δ> [] |- t ] [Γ>>Δ> a |- t ] -| RCont : ∀ t a , URule [Γ>>Δ> (a,,a) |- t ] [Γ>>Δ> a |- t ]. - +Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type := +| 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 := -| RURule : ∀ Γ Δ h c, @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) +| RArrange : ∀ Γ Δ Σ₁ Σ₂ Σ, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ ] [Γ > Δ > Σ₂ |- Σ ] (* λ^α rules *) | RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]] @@ -93,8 +77,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type := | RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]] | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]] | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l, -HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> - Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] + HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]] | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ] | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]] | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]] @@ -116,12 +99,11 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ]) [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ] . -Coercion RURule : URule >-> Rule. (* A rule is considered "flat" if it is neither RBrak nor REsc *) Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := -| Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r) +| Flat_RArrange : ∀ Γ Δ h c r a , Rule_Flat (RArrange Γ Δ h c r a) | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n) | Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ ) | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l) @@ -138,53 +120,9 @@ Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop := | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x) | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev). -(* given a proof that uses only uniform rules, we can produce a general proof *) -Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c) - := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c. - -Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False. - intro. - intro. - induction 1; intros; inversion H. - simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1. - simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1. - Qed. - Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False. intros. destruct X; try destruct c; try destruct o; simpl in *; try inversion H. - apply no_urules_with_empty_conclusion in u. - apply u. - auto. - Qed. - -Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h, - @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False. - intro. - intro. - induction 1; intros. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - - apply IHX. - destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *. - inversion e. - inversion e. - exists c1. exists c2. auto. - - apply IHX. - destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *. - inversion e. - inversion e. - exists c1. exists c2. auto. - - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. - inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto. Qed. Lemma no_rules_with_multiple_conclusions : forall c h, @@ -194,7 +132,6 @@ Lemma no_rules_with_multiple_conclusions : forall c h, try apply no_urules_with_empty_conclusion in u; try apply u. destruct X0; destruct s; inversion e. auto. - apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto. destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. destruct X0; destruct s; inversion e. diff --git a/src/HaskProofCategory.v b/src/HaskProofCategory.v index e74d580..18da307 100644 --- a/src/HaskProofCategory.v +++ b/src/HaskProofCategory.v @@ -44,15 +44,13 @@ Open Scope nd_scope. Section HaskProofCategory. - Implicit Arguments RURule [[Γ][Δ][h][c]]. - Context (ndr_systemfc:@ND_Relation _ Rule). (* Rules allowed in PCF; i.e. rules we know how to turn into GArrows *) (* Rule_PCF consists of the rules allowed in flat PCF: everything except *) (* AppT, AbsT, AppC, AbsC, Cast, Global, and some Case statements *) Inductive Rule_PCF {Γ}{Δ} : ∀ h c, Rule (mapOptionTree (@UJudg2judg Γ Δ) h) (mapOptionTree (@UJudg2judg Γ Δ) c) -> Type := - | PCF_RCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a )) + | PCF_RArrange : ∀ x y , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanL t a )) | PCF_RCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RCanR t a )) | PCF_RuCanL : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanL t a )) | PCF_RuCanR : ∀ t a , Rule_PCF [_>>_>_|-_] [_>>_>_|-_] (RURule (RuCanR t a )) diff --git a/src/HaskProofToLatex.v b/src/HaskProofToLatex.v index 39dd8ba..fb8c2fa 100644 --- a/src/HaskProofToLatex.v +++ b/src/HaskProofToLatex.v @@ -157,24 +157,25 @@ Definition judgmentToRawLatexMath (j:Judg) : LatexMath := Instance ToLatexMathJudgment : ToLatexMath Judg := { toLatexMath := judgmentToRawLatexMath }. -Fixpoint nd_uruleToRawLatexMath {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : string := +Fixpoint nd_uruleToRawLatexMath {T}{h}{c}(r:@Arrange T h c) : string := match r with | RLeft _ _ _ r => nd_uruleToRawLatexMath r | RRight _ _ _ r => nd_uruleToRawLatexMath r - | RCanL _ _ => "CanL" - | RCanR _ _ => "CanR" - | RuCanL _ _ => "uCanL" - | RuCanR _ _ => "uCanR" - | RAssoc _ _ _ _ => "Assoc" - | RCossa _ _ _ _ => "Cossa" - | RExch _ _ _ => "Exch" - | RWeak _ _ => "Weak" - | RCont _ _ => "Cont" + | RCanL _ => "CanL" + | RCanR _ => "CanR" + | RuCanL _ => "uCanL" + | RuCanR _ => "uCanR" + | RAssoc _ _ _ => "Assoc" + | RCossa _ _ _ => "Cossa" + | RExch _ _ => "Exch" + | RWeak _ => "Weak" + | RCont _ => "Cont" + | RComp _ _ _ _ _ => "Comp" (* FIXME: do a better job here *) end. Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := match r with - | RURule _ _ _ _ r => nd_uruleToRawLatexMath r + | RArrange _ _ _ _ _ r => nd_uruleToRawLatexMath r | RNote _ _ _ _ _ _ => "Note" | RLit _ _ _ _ => "Lit" | RVar _ _ _ _ => "Var" @@ -195,25 +196,26 @@ Fixpoint nd_ruleToRawLatexMath {h}{c}(r:Rule h c) : string := | REmptyGroup _ _ => "REmptyGroup" end. -Fixpoint nd_hideURule {Γ}{Δ}{h}{c}(r:@URule Γ Δ h c) : bool := +Fixpoint nd_hideURule {T}{h}{c}(r:@Arrange T h c) : bool := match r with - | RLeft _ _ _ r => nd_hideURule r - | RRight _ _ _ r => nd_hideURule r - | RCanL _ _ => true - | RCanR _ _ => true - | RuCanL _ _ => true - | RuCanR _ _ => true - | RAssoc _ _ _ _ => true - | RCossa _ _ _ _ => true - | RExch _ (T_Leaf None) b => true - | RExch _ a (T_Leaf None) => true - | RWeak _ (T_Leaf None) => true - | RCont _ (T_Leaf None) => true - | _ => false + | RLeft _ _ _ r => nd_hideURule r + | RRight _ _ _ r => nd_hideURule r + | RCanL _ => true + | RCanR _ => true + | RuCanL _ => true + | RuCanR _ => true + | RAssoc _ _ _ => true + | RCossa _ _ _ => true + | RExch (T_Leaf None) b => true + | RExch a (T_Leaf None) => true + | RWeak (T_Leaf None) => true + | RCont (T_Leaf None) => true + | RComp _ _ _ _ _ => false (* FIXME: do better *) + | _ => false end. Fixpoint nd_hideRule {h}{c}(r:Rule h c) : bool := match r with - | RURule _ _ _ _ r => nd_hideURule r + | RArrange _ _ _ _ _ r => nd_hideURule r | REmptyGroup _ _ => true | RBindingGroup _ _ _ _ _ _ => true | _ => false diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 3dee0fe..0218ddd 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -228,172 +228,125 @@ Section HaskProofToStrong. inversion pf2. Defined. - Definition urule2expr : forall Γ Δ h j (r:@URule Γ Δ h j) (ξ:VV -> LeveledHaskType Γ ★), - ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j. - - refine (fix urule2expr Γ Δ h j (r:@URule Γ Δ h j) ξ {struct r} : - ITree _ (ujudg2exprType ξ) h -> ITree _ (ujudg2exprType ξ) j := - match r as R in URule H C return ITree _ (ujudg2exprType ξ) H -> ITree _ (ujudg2exprType ξ) C with - | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ _ r) - | RCanL t a => let case_RCanL := tt in _ - | RCanR t a => let case_RCanR := tt in _ - | RuCanL t a => let case_RuCanL := tt in _ - | RuCanR t a => let case_RuCanR := tt in _ - | RAssoc t a b c => let case_RAssoc := tt in _ - | RCossa t a b c => let case_RCossa := tt in _ - | RExch t a b => let case_RExch := tt in _ - | RWeak t a => let case_RWeak := tt in _ - | RCont t a => let case_RCont := tt in _ + Definition urule2expr : forall Γ Δ h j t (r:@Arrange _ h j) (ξ:VV -> LeveledHaskType Γ ★), + ujudg2exprType ξ (Γ >> Δ > h |- t) -> + ujudg2exprType ξ (Γ >> Δ > j |- t) + . + intros Γ Δ. + refine (fix urule2expr h j t (r:@Arrange _ h j) ξ {struct r} : + ujudg2exprType ξ (Γ >> Δ > h |- t) -> + ujudg2exprType ξ (Γ >> Δ > j |- t) := + match r as R in Arrange H C return ujudg2exprType ξ (Γ >> Δ > H |- t) -> + ujudg2exprType ξ (Γ >> Δ > C |- t) with + | RLeft h c ctx r => let case_RLeft := tt in (fun e => _) (urule2expr _ _ _ r) + | RRight h c ctx r => let case_RRight := tt in (fun e => _) (urule2expr _ _ _ r) + | 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 _ + | RCossa a b c => let case_RCossa := tt in _ + | RExch a b => let case_RExch := tt in _ + | RWeak a => let case_RWeak := tt in _ + | RCont a => let case_RCont := tt in _ + | RComp a b c f g => let case_RComp := tt in (fun e1 e2 => _) (urule2expr _ _ _ f) (urule2expr _ _ _ g) end); clear urule2expr; intros. destruct case_RCanL. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 ([],,vars)). + simpl; intros. + simpl in X. + apply (X ([],,vars)). simpl; rewrite <- H; auto. destruct case_RCanR. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 (vars,,[])). + simpl; intros. + simpl in X. + apply (X (vars,,[])). simpl; rewrite <- H; auto. destruct case_RuCanL. - apply ILeaf; simpl; intros. + simpl; intros. destruct vars; try destruct o; inversion H. - inversion X. - simpl in X0. - apply (X0 vars2); auto. + simpl in X. + apply (X vars2); auto. destruct case_RuCanR. - apply ILeaf; simpl; intros. + simpl; intros. destruct vars; try destruct o; inversion H. - inversion X. - simpl in X0. - apply (X0 vars1); auto. + simpl in X. + apply (X vars1); auto. destruct case_RAssoc. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. + simpl; intros. + simpl in X. destruct vars; try destruct o; inversion H. destruct vars1; try destruct o; inversion H. - apply (X0 (vars1_1,,(vars1_2,,vars2))). + apply (X (vars1_1,,(vars1_2,,vars2))). subst; auto. destruct case_RCossa. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. + simpl; intros. + simpl in X. destruct vars; try destruct o; inversion H. destruct vars2; try destruct o; inversion H. - apply (X0 ((vars1,,vars2_1),,vars2_2)). + apply (X ((vars1,,vars2_1),,vars2_2)). subst; auto. + destruct case_RExch. + simpl; intros. + simpl in X. + destruct vars; try destruct o; inversion H. + apply (X (vars2,,vars1)). + inversion H; subst; auto. + + destruct case_RWeak. + simpl; intros. + simpl in X. + apply (X []). + auto. + + destruct case_RCont. + simpl; intros. + simpl in X. + apply (X (vars,,vars)). + simpl. + rewrite <- H. + auto. + destruct case_RLeft. - destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. - destruct o; [ idtac | apply INone ]. - destruct u; simpl in *. - apply ILeaf; simpl; intros. + intro vars; intro H. destruct vars; try destruct o; inversion H. - set (fun q => ileaf (e ξ q)) as r'. - simpl in r'. - apply r' with (vars:=vars2). - clear r' e. - clear r0. - induction h0. - destruct a. - destruct u. + apply (fun q => e ξ q vars2 H2). + clear r0 e H2. simpl in X. - apply ileaf in X. - apply ILeaf. simpl. - simpl in X. intros. apply X with (vars:=vars1,,vars). - simpl. rewrite H0. rewrite H1. + simpl. reflexivity. - apply INone. - apply IBranch. - apply IHh0_1. inversion X; auto. - apply IHh0_2. inversion X; auto. - auto. - + destruct case_RRight. - destruct c; [ idtac | apply no_urules_with_multiple_conclusions in r0; inversion r0; exists c1; exists c2; auto ]. - destruct o; [ idtac | apply INone ]. - destruct u; simpl in *. - apply ILeaf; simpl; intros. + intro vars; intro H. destruct vars; try destruct o; inversion H. - set (fun q => ileaf (e ξ q)) as r'. - simpl in r'. - apply r' with (vars:=vars1). - clear r' e. - clear r0. - induction h0. - destruct a. - destruct u. + apply (fun q => e ξ q vars1 H1). + clear r0 e H2. simpl in X. - apply ileaf in X. - apply ILeaf. simpl. - simpl in X. intros. apply X with (vars:=vars,,vars2). - simpl. rewrite H0. - rewrite H2. + inversion H. + simpl. reflexivity. - apply INone. - apply IBranch. - apply IHh0_1. inversion X; auto. - apply IHh0_2. inversion X; auto. - auto. - destruct case_RExch. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - destruct vars; try destruct o; inversion H. - apply (X0 (vars2,,vars1)). - inversion H; subst; auto. - - destruct case_RWeak. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 []). - auto. - - destruct case_RCont. - apply ILeaf; simpl; intros. - inversion X. - simpl in X0. - apply (X0 (vars,,vars)). - simpl. - rewrite <- H. - auto. + destruct case_RComp. + apply e2. + apply e1. + apply X. Defined. - Definition bridge Γ Δ (c:Tree ??(UJudg Γ Δ)) ξ : - ITree Judg judg2exprType (mapOptionTree UJudg2judg c) -> ITree (UJudg Γ Δ) (ujudg2exprType ξ) c. - intro it. - induction c. - destruct a. - destruct u; simpl in *. - apply ileaf in it. - apply ILeaf. - simpl in *. - intros; apply it with (vars:=vars); auto. - apply INone. - apply IBranch; [ apply IHc1 | apply IHc2 ]; inversion it; auto. - Defined. - Definition letrec_helper Γ Δ l (varstypes:Tree ??(VV * HaskType Γ ★)) ξ' : ITree (LeveledHaskType Γ ★) (fun t : LeveledHaskType Γ ★ => Expr Γ Δ ξ' t) @@ -553,7 +506,7 @@ Section HaskProofToStrong. intros h j r. refine (match r as R in Rule H C return ITree _ judg2exprType H -> ITree _ judg2exprType C with - | RURule a b c d e => let case_RURule := tt in _ + | RArrange a b c d e r => let case_RURule := tt in _ | RNote Γ Δ Σ τ l n => let case_RNote := tt in _ | RLit Γ Δ l _ => let case_RLit := tt in _ | RVar Γ Δ σ p => let case_RVar := tt in _ @@ -574,19 +527,17 @@ Section HaskProofToStrong. | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _ end); intro X_; try apply ileaf in X_; simpl in X_. - destruct case_RURule. - destruct d; try destruct o. - apply ILeaf; destruct u; simpl; intros. - set (@urule2expr a b _ _ e ξ) as q. - set (fun z => ileaf (q z)) as q'. + destruct case_RURule. + apply ILeaf. simpl. intros. + set (@urule2expr a b _ _ e r0 ξ) as q. + set (fun z => q z) as q'. simpl in q'. apply q' with (vars:=vars). clear q' q. - apply bridge. - apply X_. + intros. + apply X_ with (vars:=vars0). + auto. auto. - apply no_urules_with_empty_conclusion in e; inversion e; auto. - apply no_urules_with_multiple_conclusions in e; inversion e; auto; exists d1; exists d2; auto. destruct case_RBrak. apply ILeaf; simpl; intros; refine (X_ ξ vars H >>>= fun X => return ILeaf _ _). apply FreshMon. diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v index 79e16cd..b0c5b11 100644 --- a/src/HaskStrongToProof.v +++ b/src/HaskStrongToProof.v @@ -16,51 +16,24 @@ Require Import HaskProof. Section HaskStrongToProof. -(* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform - * expansion on an entire uniform proof *) -Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) - := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)). -Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★)) - := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)). - -Definition pivotContext {Γ}{Δ} a b c τ : - @ND _ (@URule Γ Δ) - [ Γ >> Δ > (a,,b),,c |- τ] - [ Γ >> Δ > (a,,c),,b |- τ]. - set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q. - simpl in *. - eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ]. - eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ]. - apply q. +Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) := + RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _). + +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. - -Definition copyAndPivotContext {Γ}{Δ} a b c τ : - @ND _ (@URule Γ Δ) - [ Γ >> Δ > (a,,b),,(c,,b) |- τ] - [ Γ >> Δ > (a,,c),,b |- τ]. - set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q. - simpl in *. - eapply nd_comp; [ idtac | apply q ]. - clear q. - eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ]. - set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q. - simpl in *. - eapply nd_comp ; [ idtac | apply q ]. - clear q. - apply nd_rule. - apply RAssoc. - Defined. - - Context {VV:Type}{eqd_vv:EqDecidable VV}. - (* maintenance of Xi *) - Fixpoint dropVar (lv:list VV)(v:VV) : ??VV := - match lv with - | nil => Some v - | v'::lv' => if eqd_dec v v' then None else dropVar lv' v - end. +(* maintenance of Xi *) +Fixpoint dropVar (lv:list VV)(v:VV) : ??VV := + match lv with + | nil => Some v + | v'::lv' => if eqd_dec v v' then None else dropVar lv' v + end. Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b := match t with @@ -422,23 +395,22 @@ Lemma stripping_nothing_is_inert reflexivity. Qed. -Definition arrangeContext +Definition arrangeContext (Γ:TypeEnv)(Δ:CoercionEnv Γ) v (* variable to be pivoted, if found *) ctx (* initial context *) - τ (* type of succedent *) (ξ:VV -> LeveledHaskType Γ ★) : (* a proof concluding in a context where that variable does not appear *) - sum (ND (@URule Γ Δ) - [Γ >> Δ > mapOptionTree ξ ctx |- τ] - [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ]) + sum (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] )) (* or a proof concluding in a context where that variable appears exactly once in the left branch *) - (ND (@URule Γ Δ) - [Γ >> Δ > mapOptionTree ξ ctx |- τ] - [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]). + (Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )). induction ctx. @@ -455,18 +427,15 @@ Definition arrangeContext (* where the leaf is v *) apply inr. subst. - apply nd_rule. apply RuCanL. (* where the leaf is NOT v *) apply inl. - apply nd_rule. apply RuCanR. (* empty leaf *) destruct case_None. apply inl; simpl in *. - apply nd_rule. apply RuCanR. (* branch *) @@ -486,87 +455,77 @@ Definition arrangeContext destruct case_Neither. apply inl. - eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ]. - exact (nd_comp + eapply RComp; [idtac | apply RuCanR ]. + exact (RComp (* order will not matter because these are central as morphisms *) - (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) - (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))). + (RRight _ (RComp lpf (RCanR _))) + (RLeft _ (RComp rpf (RCanR _)))). destruct case_Right. apply inr. fold (stripOutVars (v::nil)). - set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q. + set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q. simpl in *. - eapply nd_comp. + eapply RComp. apply q. clear q. clear lpf. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. - eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ]. - set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ] - [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq. - apply qq. - clear qq. + eapply RComp; [ idtac | apply RAssoc ]. + apply RLeft. apply rpf. destruct case_Left. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply nd_comp; [ idtac | eapply pivotContext ]. - set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'. - set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq. + eapply RComp; [ idtac | eapply pivotContext ]. + set (RComp rpf (RCanR _ )) as rpf'. + set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq. simpl in *. - eapply nd_comp; [ idtac | apply qq ]. + eapply RComp; [ idtac | apply qq ]. clear qq rpf' rpf. - set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q. - apply q. - clear q. + apply (RRight (mapOptionTree ξ ctx2)). apply lpf. destruct case_Both. apply inr. unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *. fold (stripOutVars (v::nil)). - eapply nd_comp; [ idtac | eapply copyAndPivotContext ]. - exact (nd_comp - (* order will not matter because these are central as morphisms *) - (ext_right _ _ _ lpf) - (ext_left _ _ _ rpf)). + eapply RComp; [ idtac | eapply copyAndPivotContext ]. + (* order will not matter because these are central as morphisms *) + exact (RComp (RRight _ lpf) (RLeft _ rpf)). Defined. (* same as before, but use RWeak if necessary *) -Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ : - ND (@URule Γ Δ) - [Γ >> Δ>mapOptionTree ξ ctx |- τ] - [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]. - set (arrangeContext Γ Δ v ctx τ ξ) as q. +Definition arrangeContextAndWeaken + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + ctx (* initial context *) + (ξ:VV -> LeveledHaskType Γ ★) : + Arrange + (mapOptionTree ξ ctx ) + (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ). + set (arrangeContext Γ Δ v ctx ξ) as q. destruct q; auto. - eapply nd_comp; [ apply n | idtac ]. - clear n. - refine (ext_left _ _ _ (nd_rule (RWeak _ _))). + eapply RComp; [ apply a | idtac ]. + refine (RLeft _ (RWeak _)). Defined. -Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : - mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) - = mapOptionTree ξ (stripOutVars (v :: nil) tree). - set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. - rewrite p. - simpl. - reflexivity. - Qed. - Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a). admit. Qed. -Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, +Definition arrangeContextAndWeaken'' + (Γ:TypeEnv)(Δ:CoercionEnv Γ) + v (* variable to be pivoted, if found *) + (ξ:VV -> LeveledHaskType Γ ★) : forall ctx, distinct (leaves v) -> - ND (@URule Γ Δ) - [Γ >> Δ>(mapOptionTree ξ ctx) |- z] - [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z]. + Arrange + ((mapOptionTree ξ ctx) ) + ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)). induction v; intros. destruct a. @@ -575,11 +534,11 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, fold (mapOptionTree ξ) in *. intros. apply arrangeContextAndWeaken. + apply Δ. unfold mapOptionTree; simpl in *. intros. rewrite (@stripping_nothing_is_inert Γ); auto. - apply nd_rule. apply RuCanR. intros. unfold mapOptionTree in *. @@ -587,7 +546,7 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, fold (mapOptionTree ξ) in *. set (mapOptionTree ξ) as X in *. - set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'. + set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'. unfold stripOutVars in IHv2'. simpl in IHv2'. fold (stripOutVars (leaves v2)) in IHv2'. @@ -599,19 +558,27 @@ Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z, fold X in IHv2'. set (distinct_app _ _ _ H) as H'. destruct H' as [H1 H2]. - set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) as qq. - eapply nd_comp. + set (RComp (IHv1 _ H1) (IHv2' H2)) as qq. + eapply RComp. apply qq. clear qq IHv2' IHv2 IHv1. rewrite strip_twice_lemma. rewrite (strip_distinct' v1 (leaves v2)). - apply nd_rule. apply RCossa. apply cheat. auto. Defined. +Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev : + mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree) + = mapOptionTree ξ (stripOutVars (v :: nil) tree). + set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p. + rewrite p. + simpl. + reflexivity. + Qed. + (* IDEA: use multi-conclusion proofs instead *) Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type := | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _) @@ -665,23 +632,25 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : eapply nd_comp; [ idtac | eapply nd_rule; apply z ]. clear z. - set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'. + set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'. unfold passback in *; clear passback. unfold pctx in *; clear pctx. - eapply UND_to_ND in q'. + rewrite <- mapleaves in disti. + set (q' disti) as q''. unfold ξ' in *. set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz. rewrite <- mapleaves in zz. - rewrite zz in q'. + rewrite zz in q''. clear zz. clear ξ'. Opaque stripOutVars. simpl. - rewrite <- mapOptionTree_compose in q'. + rewrite <- mapOptionTree_compose in q''. rewrite <- ξlemma. - eapply nd_comp; [ idtac | apply q' ]. + eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ]. clear q'. + clear q''. simpl. set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q. @@ -690,10 +659,6 @@ Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree : apply nd_prod; auto. rewrite ξlemma. apply q. - clear q'. - - rewrite <- mapleaves in disti. - apply disti. Defined. Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} : @@ -843,15 +808,14 @@ Definition expr2proof : unfold mapOptionTree; simpl; fold (mapOptionTree ξ). eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ]. set (update_ξ ξ lev ((v,t1)::nil)) as ξ'. - set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx. - apply UND_to_ND in pfx. - unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx. + set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx. + eapply RArrange in pfx. + unfold mapOptionTree in pfx; simpl in pfx. unfold ξ' in pfx. - fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx. rewrite updating_stripped_tree_is_inert in pfx. unfold update_ξ in pfx. destruct (eqd_dec v v). - eapply nd_comp; [ idtac | apply pfx ]. + eapply nd_comp; [ idtac | apply (nd_rule pfx) ]. clear pfx. apply e'. assert False. @@ -869,7 +833,7 @@ Definition expr2proof : fold (@mapOptionTree VV). fold (mapOptionTree ξ). set (update_ξ ξ v ((lev,tv)::nil)) as ξ'. - set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n. + set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n. unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n. unfold ξ' in n. rewrite updating_stripped_tree_is_inert in n. @@ -877,8 +841,8 @@ Definition expr2proof : destruct (eqd_dec lev lev). unfold ξ'. unfold update_ξ. - apply UND_to_ND in n. - apply n. + eapply RArrange in n. + apply (nd_rule n). assert False. apply n0; auto. inversion H. destruct case_EEsc. @@ -925,11 +889,9 @@ Definition expr2proof : clear o x alts alts' e. eapply nd_comp; [ apply e' | idtac ]. clear e'. - set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]). - simpl in n. - apply n. - clear n. - + apply nd_rule. + apply RArrange. + simpl. rewrite mapleaves'. simpl. rewrite <- mapOptionTree_compose. @@ -951,6 +913,7 @@ Definition expr2proof : replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))). apply q. + apply (sac_Δ sac Γ atypes (weakCK'' Δ)). rewrite leaves_unleaves. apply (scbwv_exprvars_distinct scbx). rewrite leaves_unleaves. -- 1.7.10.4