1 (*********************************************************************************************************************************)
4 (* Natural Deduction proofs of the well-typedness of a Haskell term. Proofs use explicit structural rules (Gentzen-style) *)
5 (* and are in System FC extended with modal types indexed by Taha-Nielsen environment classifiers (λ^α) *)
7 (*********************************************************************************************************************************)
9 Generalizable All Variables.
10 Require Import Preamble.
11 Require Import General.
12 Require Import NaturalDeduction.
13 Require Import Coq.Strings.String.
14 Require Import Coq.Lists.List.
15 Require Import HaskKinds.
16 Require Import HaskCoreTypes.
17 Require Import HaskLiteralsAndTyCons.
18 Require Import HaskStrongTypes.
19 Require Import HaskWeakVars.
21 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
22 * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
23 * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
24 * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
29 forall Δ:CoercionEnv Γ,
30 Tree ??(LeveledHaskType Γ ★) ->
31 Tree ??(LeveledHaskType Γ ★) ->
33 Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
35 (* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
36 * uniform context throughout the whole proof. Such proofs are important because (1) we can do left and right context
37 * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
38 Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
40 Tree ??(LeveledHaskType Γ ★) ->
41 Tree ??(LeveledHaskType Γ ★) ->
43 Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
44 Definition ext_tree_left {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
45 Definition ext_tree_right {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
47 (* we can turn a UJudg into a Judg by simply internalizing the index *)
48 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
49 match ej with mkUJudg t s => Γ > Δ > t |- s end.
50 Coercion UJudg2judg : UJudg >-> Judg.
52 (* information needed to define a case branch in a HaskProof *)
53 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
54 { pcb_freevars : Tree ??(LeveledHaskType Γ ★)
55 ; pcb_judg := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
56 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
57 (vec2list (sac_types sac Γ avars))))
58 |- [weakLT' (branchtype @@ lev)]
60 (*Coercion pcb_scb : ProofCaseBranch >-> StrongAltCon.*)
61 Implicit Arguments ProofCaseBranch [ ].
63 (* Figure 3, production $\vdash_E$, Uniform rules *)
64 Inductive URule {Γ}{Δ} : Tree ??(UJudg Γ Δ) -> Tree ??(UJudg Γ Δ) -> Type :=
65 | RCanL : ∀ t a , URule [Γ>>Δ> [],,a |- t ] [Γ>>Δ> a |- t ]
66 | RCanR : ∀ t a , URule [Γ>>Δ> a,,[] |- t ] [Γ>>Δ> a |- t ]
67 | RuCanL : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> [],,a |- t ]
68 | RuCanR : ∀ t a , URule [Γ>>Δ> a |- t ] [Γ>>Δ> a,,[] |- t ]
69 | RAssoc : ∀ t a b c , URule [Γ>>Δ>a,,(b,,c) |- t ] [Γ>>Δ>(a,,b),,c |- t ]
70 | RCossa : ∀ t a b c , URule [Γ>>Δ>(a,,b),,c |- t ] [Γ>>Δ> a,,(b,,c) |- t ]
71 | RLeft : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_left x) h) (mapOptionTree (ext_tree_left x) c)
72 | RRight : ∀ h c x , URule h c -> URule (mapOptionTree (ext_tree_right x) h) (mapOptionTree (ext_tree_right x) c)
73 | RExch : ∀ t a b , URule [Γ>>Δ> (b,,a) |- t ] [Γ>>Δ> (a,,b) |- t ]
74 | RWeak : ∀ t a , URule [Γ>>Δ> [] |- t ] [Γ>>Δ> a |- t ]
75 | RCont : ∀ t a , URule [Γ>>Δ> (a,,a) |- t ] [Γ>>Δ> a |- t ].
78 (* Figure 3, production $\vdash_E$, all rules *)
79 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
81 | RURule : ∀ Γ Δ h c, @URule Γ Δ h c -> Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
84 | RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]]
85 | REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l) ]]
87 (* Part of GHC, but not explicitly in System FC *)
88 | RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@ l]]
89 | RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]]
92 | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
93 | RGlobal : ∀ Γ Δ τ l, WeakExprVar -> Rule [ ] [Γ>Δ> [] |- [τ @@l]]
94 | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
95 | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
96 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
97 Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]]
98 | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
99 | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
100 | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
101 | REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
102 | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
103 | RAbsT : ∀ Γ Δ Σ κ σ l,
104 Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
105 [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
106 | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
107 Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
108 | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
109 Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
110 [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
111 | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- ([τ₁],,τ₂)@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
112 | RCase : forall Γ Δ lev tc Σ avars tbranches
113 (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
115 ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
116 [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ])
117 [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ]
119 Coercion RURule : URule >-> Rule.
122 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
123 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
124 | Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r)
125 | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n)
126 | Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ )
127 | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
128 | Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
129 | Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
130 | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
131 | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
132 | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
133 | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
134 | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
135 | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
136 | Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e)
137 | Flat_REmptyGroup : ∀ q a , Rule_Flat (REmptyGroup q a)
138 | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
139 | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
141 (* given a proof that uses only uniform rules, we can produce a general proof *)
142 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
143 := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
145 Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
148 induction 1; intros; inversion H.
149 simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1.
150 simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1.
153 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
155 destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
156 apply no_urules_with_empty_conclusion in u.
161 Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
162 @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
166 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
167 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
168 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
169 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
170 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
171 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
174 destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
177 exists c1. exists c2. auto.
180 destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
183 exists c1. exists c2. auto.
185 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
186 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
187 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
190 Lemma no_rules_with_multiple_conclusions : forall c h,
191 Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
193 destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
194 try apply no_urules_with_empty_conclusion in u; try apply u.
195 destruct X0; destruct s; inversion e.
197 apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto.
198 destruct X0; destruct s; inversion e.
199 destruct X0; destruct s; inversion e.
200 destruct X0; destruct s; inversion e.
201 destruct X0; destruct s; inversion e.
202 destruct X0; destruct s; inversion e.
203 destruct X0; destruct s; inversion e.
204 destruct X0; destruct s; inversion e.
205 destruct X0; destruct s; inversion e.
206 destruct X0; destruct s; inversion e.
207 destruct X0; destruct s; inversion e.
208 destruct X0; destruct s; inversion e.
209 destruct X0; destruct s; inversion e.
210 destruct X0; destruct s; inversion e.
211 destruct X0; destruct s; inversion e.
212 destruct X0; destruct s; inversion e.
213 destruct X0; destruct s; inversion e.
214 destruct X0; destruct s; inversion e.
215 destruct X0; destruct s; inversion e.
218 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
220 eapply no_rules_with_multiple_conclusions.