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.
apply t.
Defined.
+(*
Definition env := ★::nil.
Definition freshTV : HaskType env ★ := haskTyVarToType (FreshHaskTyVar _).
Definition idproof0 : ND Rule [] [env > nil > [] |- [freshTV--->freshTV @@ nil]].
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)) (
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 Γ ★)
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]]
| 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]]
[Γ > Δ > Σ |- [ 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)
| 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,
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.
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 ))
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"
| 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
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)
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 _
| 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.
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
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.
(* 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 *)
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.
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 *.
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'.
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 _ _ _ _)
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.
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} :
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.
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.
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.
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.
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.
projects / coq-hetmet.git / commitdiff