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 NaturalDeductionContext.
14 Require Import Coq.Strings.String.
15 Require Import Coq.Lists.List.
16 Require Import HaskKinds.
17 Require Import HaskCoreTypes.
18 Require Import HaskLiterals.
19 Require Import HaskTyCons.
20 Require Import HaskStrongTypes.
21 Require Import HaskWeakVars.
23 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
24 * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
25 * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
26 * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
31 forall Δ:CoercionEnv Γ,
32 Tree ??(LeveledHaskType Γ ★) ->
33 Tree ??(HaskType Γ ★) ->
36 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).
38 (* information needed to define a case branch in a HaskProof *)
40 {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc}
41 (pcb_freevars : Tree ??(LeveledHaskType Γ ★)) :=
42 sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
43 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
44 (vec2list (sac_types sac Γ avars))))
45 |- [weakT' branchtype ] @ weakL' lev.
47 (* Figure 3, production $\vdash_E$, all rules *)
48 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
50 | RArrange : ∀ Γ Δ Σ₁ Σ₂ Σ l, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ @l] [Γ > Δ > Σ₂ |- Σ @l]
53 | RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t]@(v::l) ] [Γ > Δ > Σ |- [<[v|-t]> ] @l]
54 | REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> ] @l] [Γ > Δ > Σ |- [t]@(v::l) ]
56 (* Part of GHC, but not explicitly in System FC *)
57 | RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ ] @l] [Γ > Δ > Σ |- [τ ] @l]
58 | RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v ] @l]
61 | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ ] @l]
62 | RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v ] @l]
63 | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te] @l] [Γ>Δ> Σ |- [tx--->te ] @l]
64 | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
65 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁] @l] [Γ>Δ> Σ |- [σ₂ ] @l]
67 (* order is important here; we want to be able to skolemize without introducing new AExch'es *)
68 | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te]@l],,[Γ>Δ> Σ₂ |- [tx]@l]) [Γ>Δ> Σ₁,,Σ₂ |- [te]@l]
70 | RCut : ∀ Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l, Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> Σ,,((Σ₁₂@@@l),,Σ₂) |- Σ₃@l ]) [Γ>Δ> Σ,,(Σ₁,,Σ₂) |- Σ₃@l]
71 | RLeft : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> (Σ@@@l),,Σ₁ |- Σ,,Σ₂@l]
72 | RRight : ∀ Γ Δ Σ₁ Σ₂ Σ l, Rule [Γ>Δ> Σ₁ |- Σ₂ @l] [Γ>Δ> Σ₁,,(Σ@@@l) |- Σ₂,,Σ@l]
74 | RVoid : ∀ Γ Δ l, Rule [] [Γ > Δ > [] |- [] @l ]
76 | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ]@l] [Γ>Δ> Σ |- [substT σ τ]@l]
77 | RAbsT : ∀ Γ Δ Σ κ σ l,
78 Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) ]@(weakL l)]
79 [Γ>Δ > Σ |- [HaskTAll κ σ ]@l]
81 | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
82 Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ]@l] [Γ>Δ> Σ |- [σ ]@l]
83 | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
84 Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ ]@l]
85 [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
87 | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
88 | RCase : forall Γ Δ lev tc Σ avars tbranches
89 (alts:Tree ??( (@StrongAltCon tc) * (Tree ??(LeveledHaskType Γ ★)) )),
91 ((mapOptionTree (fun x => @pcb_judg tc Γ Δ lev tbranches avars (fst x) (snd x)) alts),,
92 [Γ > Δ > Σ |- [ caseType tc avars ] @lev])
93 [Γ > Δ > (mapOptionTreeAndFlatten (fun x => (snd x)) alts),,Σ |- [ tbranches ] @ lev]
96 Definition RCut' : ∀ Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l,
97 ND Rule ([Γ>Δ> Σ₁ |- Σ₁₂ @l],,[Γ>Δ> (Σ₁₂@@@l),,Σ₂ |- Σ₃@l ]) [Γ>Δ> Σ₁,,Σ₂ |- Σ₃@l].
99 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
100 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
108 Definition RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l,
109 ND Rule ([Γ>Δ> Σ₁ |- [σ₁]@l],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂]@l ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ ]@l].
111 eapply nd_comp; [ idtac | eapply nd_rule; eapply RArrange; eapply ACanL ].
112 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCut ].
115 eapply nd_rule; eapply RArrange; eapply AuCanL.
118 Definition RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l,
119 ND Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂]@l ],,[Γ>Δ> Σ₂ |- [σ₁]@l]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ ]@l].
121 eapply nd_comp; [ apply nd_exch | idtac ].
122 eapply nd_rule; eapply RCut.
125 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
126 (* TODO: change this to (if RBrak/REsc -> False) *)
127 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
128 | Flat_RArrange : ∀ Γ Δ h c r a l , Rule_Flat (RArrange Γ Δ h c r a l)
129 | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n)
130 | Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ )
131 | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
132 | Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
133 | Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
134 | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
135 | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
136 | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
137 | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
138 | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
139 | Flat_RVoid : ∀ q a l, Rule_Flat (RVoid q a l)
140 | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
141 | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
143 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
145 destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
148 Lemma no_rules_with_multiple_conclusions : forall c h,
149 Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
151 destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
152 try apply no_urules_with_empty_conclusion in u; try apply u.
153 destruct X0; destruct s; inversion e.
155 destruct X0; destruct s; inversion e.
156 destruct X0; destruct s; inversion e.
157 destruct X0; destruct s; inversion e.
158 destruct X0; destruct s; inversion e.
159 destruct X0; destruct s; inversion e.
160 destruct X0; destruct s; inversion e.
161 destruct X0; destruct s; inversion e.
162 destruct X0; destruct s; inversion e.
163 destruct X0; destruct s; inversion e.
164 destruct X0; destruct s; inversion e.
165 destruct X0; destruct s; inversion e.
166 destruct X0; destruct s; inversion e.
167 destruct X0; destruct s; inversion e.
168 destruct X0; destruct s; inversion e.
169 destruct X0; destruct s; inversion e.
170 destruct X0; destruct s; inversion e.
171 destruct X0; destruct s; inversion e.
172 destruct X0; destruct s; inversion e.
173 destruct X0; destruct s; inversion e.
176 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
178 eapply no_rules_with_multiple_conclusions.