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.
Require Import HaskCoreTypes.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskStrongTypes.
Require Import HaskWeakVars.
forall Γ:TypeEnv,
forall Δ:CoercionEnv Γ,
Tree ??(LeveledHaskType Γ ★) ->
- Tree ??(LeveledHaskType Γ ★) ->
+ Tree ??(HaskType Γ ★) ->
+ HaskLevel Γ ->
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.
+ Notation "Γ > Δ > a '|-' s '@' l" := (mkJudg Γ Δ a s l) (at level 52, Δ at level 50, a at level 52, s at level 50, l at level 50).
(* 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 Γ ★)
-; pcb_judg := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
+; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
> (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
(vec2list (sac_types sac Γ avars))))
- |- [weakLT' (branchtype @@ lev)]
+ |- [weakT' branchtype ] @ weakL' lev
}.
-(*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
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 ].
-
-
(* 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 : ∀ Γ Δ Σ₁ Σ₂ Σ l, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ @l] [Γ > Δ > Σ₂ |- Σ @l]
(* λ^α rules *)
-| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]]
-| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]]
+| RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t]@(v::l) ] [Γ > Δ > Σ |- [<[v|-t]> ] @l]
+| REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> ] @l] [Γ > Δ > Σ |- [t]@(v::l) ]
(* Part of GHC, but not explicitly in System FC *)
-| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
-| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]]
+| RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ ] @l] [Γ > Δ > Σ |- [τ ] @l]
+| RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v ] @l]
(* SystemFC rules *)
-| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
-| RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]]
-| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
+| RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ ] @l]
+| RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v ] @l]
+| RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te] @l] [Γ>Δ> Σ |- [tx--->te ] @l]
| RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) 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]]
-| REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
-| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
+ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l]
+
+(* order is important here; we want to be able to skolemize without introducing new AExch'es *)
+| RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
+
+| RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
+| RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
+| RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
+
+| RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
+
+| RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
| RAbsT : ∀ Γ Δ Σ κ σ l,
- Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
- [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
+ Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
+ [Γ>Δ > Σ |- [HaskTAll κ σ ]@l]
+
| RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
- Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
+ Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ> Σ |- [σ ]@l]
| RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
- Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
- [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
+ Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ ]@l]
+ [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
+
+| RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
| RCase : forall Γ Δ lev tc Σ avars tbranches
(alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
Rule
((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
- [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ])
- [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ]
+ [Γ > Δ > Σ |- [ caseType tc avars ] @lev])
+ [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches ] @ lev]
.
-Coercion RURule : URule >-> Rule.
+Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
+ ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+ apply nd_prod.
+ apply nd_id.
+ apply nd_rule.
+ apply RArrange.
+ apply AuCanL.
+ Defined.
+
+Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,
+ ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l].
+ intros.
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
+ eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
+ apply nd_prod.
+ apply nd_id.
+ eapply nd_rule; eapply RArrange; eapply AuCanL.
+ Defined.
+
+Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,
+ ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l].
+ intros.
+ eapply nd_comp; [ apply nd_exch | idtac ].
+ eapply nd_rule; eapply RCut.
+ Defined.
(* A rule is considered "flat" if it is neither RBrak nor REsc *)
+(* TODO: change this to (if RBrak/REsc -> False) *)
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 l , Rule_Flat (RArrange Γ Δ h c r a l)
| Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n)
+| Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ )
| Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
| Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
| Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
| Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
| Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
| Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
-| Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
-| Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e)
-| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
-
-(* 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.
+| Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l)
+| Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
+| Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
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.
destruct X0; destruct s; inversion e.
auto.
Qed.
-
projects / coq-hetmet.git / blobdiff