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.
20 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
21 * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
22 * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
23 * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
28 forall Δ:CoercionEnv Γ,
29 Tree ??(LeveledHaskType Γ ★) ->
30 Tree ??(LeveledHaskType Γ ★) ->
32 Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
34 (* A Uniform Judgment (UJudg) has its environment as a type index; we'll use these to distinguish proofs that have a single,
35 * uniform context throughout the whole proof. Such proofs are important because (1) we can do left and right context
36 * expansion on them (see rules RLeft and RRight) and (2) they will form the fiber categories of our fibration later on *)
37 Inductive UJudg (Γ:TypeEnv)(Δ:CoercionEnv Γ) :=
39 Tree ??(LeveledHaskType Γ ★) ->
40 Tree ??(LeveledHaskType Γ ★) ->
42 Notation "Γ >> Δ > a '|-' s" := (mkUJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
43 Definition ext_tree_left {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (ctx,,t) s end).
44 Definition ext_tree_right {Γ}{Δ} := (fun ctx (j:UJudg Γ Δ) => match j with mkUJudg t s => mkUJudg Γ Δ (t,,ctx) s end).
46 (* we can turn a UJudg into a Judg by simply internalizing the index *)
47 Definition UJudg2judg {Γ}{Δ}(ej:@UJudg Γ Δ) : Judg :=
48 match ej with mkUJudg t s => Γ > Δ > t |- s end.
49 Coercion UJudg2judg : UJudg >-> Judg.
51 (* information needed to define a case branch in a HaskProof *)
52 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars} :=
53 { pcb_scb : @StrongAltCon tc
54 ; pcb_freevars : Tree ??(LeveledHaskType Γ ★)
55 ; pcb_judg := sac_Γ pcb_scb Γ > sac_Δ pcb_scb Γ avars (map weakCK' Δ)
56 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
57 (vec2list (sac_types pcb_scb Γ 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 : ∀ h c, Note -> Rule h [ c ]
89 | RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@ l]]
92 | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
93 | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
94 | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
95 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
96 Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]]
97 | RBindingGroup : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
98 | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
99 | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,[σ₂@@l] |- [σ₁@@l] ],,[Γ>Δ> Σ₂ |- [σ₂@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₁ @@l]]
100 | REmptyGroup : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
101 | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
102 | RAbsT : ∀ Γ Δ Σ κ σ l,
103 Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
104 [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
105 | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
106 Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
107 | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
108 Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
109 [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
110 | RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
111 | RCase : forall Γ Δ lev tc Σ avars tbranches
112 (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
114 ((mapOptionTree pcb_judg alts),,
115 [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ])
116 [Γ > Δ > (mapOptionTreeAndFlatten pcb_freevars alts),,Σ |- [ tbranches @@ lev ] ]
118 Coercion RURule : URule >-> Rule.
121 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
122 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
123 | Flat_RURule : ∀ Γ Δ h c r , Rule_Flat (RURule Γ Δ h c r)
124 | Flat_RNote : ∀ x y z , Rule_Flat (RNote x y z)
125 | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
126 | Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
127 | Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
128 | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
129 | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
130 | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
131 | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
132 | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
133 | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
134 | Flat_RBindingGroup : ∀ q a b c d e , Rule_Flat (RBindingGroup q a b c d e)
135 | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x).
137 (* given a proof that uses only uniform rules, we can produce a general proof *)
138 Definition UND_to_ND Γ Δ h c : ND (@URule Γ Δ) h c -> ND Rule (mapOptionTree UJudg2judg h) (mapOptionTree UJudg2judg c)
139 := @nd_map' _ (@URule Γ Δ ) _ Rule (@UJudg2judg Γ Δ ) (fun h c r => nd_rule (RURule _ _ h c r)) h c.
141 Lemma no_urules_with_empty_conclusion : forall Γ Δ c h, @URule Γ Δ c h -> h=[] -> False.
144 induction 1; intros; inversion H.
145 simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1.
146 simpl in *; destruct c; try destruct o; simpl in *; try destruct u; inversion H; simpl in *; apply IHX; auto; inversion H1.
149 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
151 destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
152 apply no_urules_with_empty_conclusion in u.
157 Lemma no_urules_with_multiple_conclusions : forall Γ Δ c h,
158 @URule Γ Δ c h -> { h1:Tree ??(UJudg Γ Δ) & { h2:Tree ??(UJudg Γ Δ) & h=(h1,,h2) }} -> False.
162 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
163 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
164 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
165 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
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.
170 destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
173 exists c1. exists c2. auto.
176 destruct X0. destruct s. destruct c; try destruct o; try destruct u; simpl in *.
179 exists c1. exists c2. auto.
181 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
182 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
183 inversion X;inversion X0;inversion H;inversion X1;destruct c;try destruct o; inversion H2; apply IHX; exists c1;exists c2; auto.
186 Lemma no_rules_with_multiple_conclusions : forall c h,
187 Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
189 destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
190 try apply no_urules_with_empty_conclusion in u; try apply u.
191 destruct X0; destruct s; inversion e.
193 apply (no_urules_with_multiple_conclusions _ _ h (c1,,c2)) in u. inversion u. exists c1. exists c2. auto.
194 destruct X0; destruct s; inversion e.
195 destruct X0; destruct s; inversion e.
196 destruct X0; destruct s; inversion e.
197 destruct X0; destruct s; inversion e.
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.
213 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
215 eapply no_rules_with_multiple_conclusions.