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 HaskLiterals.
18 Require Import HaskTyCons.
19 Require Import HaskStrongTypes.
20 Require Import HaskWeakVars.
22 (* A judgment consists of an environment shape (Γ and Δ) and a pair of trees of leveled types (the antecedent and succedent) valid
23 * in any context of that shape. Notice that the succedent contains a tree of types rather than a single type; think
24 * of [ T1 |- T2 ] as asserting that a letrec with branches having types corresponding to the leaves of T2 is well-typed
25 * in environment T1. This subtle distinction starts to matter when we get into substructural (linear, affine, ordered, etc)
30 forall Δ:CoercionEnv Γ,
31 Tree ??(LeveledHaskType Γ ★) ->
32 Tree ??(LeveledHaskType Γ ★) ->
34 Notation "Γ > Δ > a '|-' s" := (mkJudg Γ Δ a s) (at level 52, Δ at level 50, a at level 52, s at level 50).
36 (* information needed to define a case branch in a HaskProof *)
37 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
38 { pcb_freevars : Tree ??(LeveledHaskType Γ ★)
39 ; pcb_judg := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
40 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
41 (vec2list (sac_types sac Γ avars))))
42 |- [weakLT' (branchtype @@ lev)]
44 Implicit Arguments ProofCaseBranch [ ].
46 (* Figure 3, production $\vdash_E$, Uniform rules *)
47 Inductive Arrange {T} : Tree ??T -> Tree ??T -> Type :=
48 | RId : forall a , Arrange a a
49 | RCanL : forall a , Arrange ( [],,a ) ( a )
50 | RCanR : forall a , Arrange ( a,,[] ) ( a )
51 | RuCanL : forall a , Arrange ( a ) ( [],,a )
52 | RuCanR : forall a , Arrange ( a ) ( a,,[] )
53 | RAssoc : forall a b c , Arrange (a,,(b,,c) ) ((a,,b),,c )
54 | RCossa : forall a b c , Arrange ((a,,b),,c ) ( a,,(b,,c) )
55 | RExch : forall a b , Arrange ( (b,,a) ) ( (a,,b) )
56 | RWeak : forall a , Arrange ( [] ) ( a )
57 | RCont : forall a , Arrange ( (a,,a) ) ( a )
58 | RLeft : forall {h}{c} x , Arrange h c -> Arrange ( x,,h ) ( x,,c)
59 | RRight : forall {h}{c} x , Arrange h c -> Arrange ( h,,x ) ( c,,x)
60 | RComp : forall {a}{b}{c}, Arrange a b -> Arrange b c -> Arrange a c
63 (* Figure 3, production $\vdash_E$, all rules *)
64 Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
66 | RArrange : ∀ Γ Δ Σ₁ Σ₂ Σ, Arrange Σ₁ Σ₂ -> Rule [Γ > Δ > Σ₁ |- Σ ] [Γ > Δ > Σ₂ |- Σ ]
69 | RBrak : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [t @@ (v::l) ]] [Γ > Δ > Σ |- [<[v|-t]> @@l]]
70 | REsc : ∀ Γ Δ t v Σ l, Rule [Γ > Δ > Σ |- [<[v|-t]> @@ l]] [Γ > Δ > Σ |- [t @@ (v::l)]]
72 (* Part of GHC, but not explicitly in System FC *)
73 | RNote : ∀ Γ Δ Σ τ l, Note -> Rule [Γ > Δ > Σ |- [τ @@ l]] [Γ > Δ > Σ |- [τ @@l]]
74 | RLit : ∀ Γ Δ v l, Rule [ ] [Γ > Δ > []|- [literalType v @@l]]
77 | RVar : ∀ Γ Δ σ l, Rule [ ] [Γ>Δ> [σ@@l] |- [σ @@l]]
78 | RGlobal : forall Γ Δ l (g:Global Γ) v, Rule [ ] [Γ>Δ> [] |- [g v @@l]]
79 | RLam : forall Γ Δ Σ (tx:HaskType Γ ★) te l, Rule [Γ>Δ> Σ,,[tx@@l]|- [te@@l] ] [Γ>Δ> Σ |- [tx--->te @@l]]
80 | RCast : forall Γ Δ Σ (σ₁ σ₂:HaskType Γ ★) l,
81 HaskCoercion Γ Δ (σ₁∼∼∼σ₂) -> Rule [Γ>Δ> Σ |- [σ₁@@l] ] [Γ>Δ> Σ |- [σ₂ @@l]]
83 | RJoin : ∀ Γ Δ Σ₁ Σ₂ τ₁ τ₂ , Rule ([Γ > Δ > Σ₁ |- τ₁ ],,[Γ > Δ > Σ₂ |- τ₂ ]) [Γ>Δ> Σ₁,,Σ₂ |- τ₁,,τ₂ ]
85 (* order is important here; we want to be able to skolemize without introducing new RExch'es *)
86 | RApp : ∀ Γ Δ Σ₁ Σ₂ tx te l, Rule ([Γ>Δ> Σ₁ |- [tx--->te @@l]],,[Γ>Δ> Σ₂ |- [tx@@l]]) [Γ>Δ> Σ₁,,Σ₂ |- [te @@l]]
88 | RLet : ∀ Γ Δ Σ₁ Σ₂ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁ |- [σ₁@@l]],,[Γ>Δ> [σ₁@@l],,Σ₂ |- [σ₂@@l] ]) [Γ>Δ> Σ₁,,Σ₂ |- [σ₂ @@l]]
89 | RWhere : ∀ Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ l, Rule ([Γ>Δ> Σ₁,,([σ₁@@l],,Σ₃) |- [σ₂@@l] ],,[Γ>Δ> Σ₂ |- [σ₁@@l]]) [Γ>Δ> Σ₁,,(Σ₂,,Σ₃) |- [σ₂ @@l]]
91 | RVoid : ∀ Γ Δ , Rule [] [Γ > Δ > [] |- [] ]
93 | RAppT : forall Γ Δ Σ κ σ (τ:HaskType Γ κ) l, Rule [Γ>Δ> Σ |- [HaskTAll κ σ @@l]] [Γ>Δ> Σ |- [substT σ τ @@l]]
94 | RAbsT : ∀ Γ Δ Σ κ σ l,
95 Rule [(κ::Γ)> (weakCE Δ) > mapOptionTree weakLT Σ |- [ HaskTApp (weakF σ) (FreshHaskTyVar _) @@ (weakL l)]]
96 [Γ>Δ > Σ |- [HaskTAll κ σ @@ l]]
98 | RAppCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ l,
99 Rule [Γ>Δ> Σ |- [σ₁∼∼σ₂ ⇒ σ@@l]] [Γ>Δ> Σ |- [σ @@l]]
100 | RAbsCo : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
101 Rule [Γ > ((σ₁∼∼∼σ₂)::Δ) > Σ |- [σ @@ l]]
102 [Γ > Δ > Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
104 | RLetRec : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁])@@@lev ] [Γ > Δ > Σ₁ |- [τ₁@@lev] ]
105 | RCase : forall Γ Δ lev tc Σ avars tbranches
106 (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
108 ((mapOptionTree (fun x => pcb_judg (projT2 x)) alts),,
109 [Γ > Δ > Σ |- [ caseType tc avars @@ lev ] ])
110 [Γ > Δ > (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x)) alts),,Σ |- [ tbranches @@ lev ] ]
114 (* A rule is considered "flat" if it is neither RBrak nor REsc *)
115 (* TODO: change this to (if RBrak/REsc -> False) *)
116 Inductive Rule_Flat : forall {h}{c}, Rule h c -> Prop :=
117 | Flat_RArrange : ∀ Γ Δ h c r a , Rule_Flat (RArrange Γ Δ h c r a)
118 | Flat_RNote : ∀ Γ Δ Σ τ l n , Rule_Flat (RNote Γ Δ Σ τ l n)
119 | Flat_RLit : ∀ Γ Δ Σ τ , Rule_Flat (RLit Γ Δ Σ τ )
120 | Flat_RVar : ∀ Γ Δ σ l, Rule_Flat (RVar Γ Δ σ l)
121 | Flat_RLam : ∀ Γ Δ Σ tx te q , Rule_Flat (RLam Γ Δ Σ tx te q )
122 | Flat_RCast : ∀ Γ Δ Σ σ τ γ q , Rule_Flat (RCast Γ Δ Σ σ τ γ q )
123 | Flat_RAbsT : ∀ Γ Σ κ σ a q , Rule_Flat (RAbsT Γ Σ κ σ a q )
124 | Flat_RAppT : ∀ Γ Δ Σ κ σ τ q , Rule_Flat (RAppT Γ Δ Σ κ σ τ q )
125 | Flat_RAppCo : ∀ Γ Δ Σ σ₁ σ₂ σ γ q l, Rule_Flat (RAppCo Γ Δ Σ σ₁ σ₂ σ γ q l)
126 | Flat_RAbsCo : ∀ Γ Σ κ σ σ₁ σ₂ q1 q2 , Rule_Flat (RAbsCo Γ Σ κ σ σ₁ σ₂ q1 q2 )
127 | Flat_RApp : ∀ Γ Δ Σ tx te p l, Rule_Flat (RApp Γ Δ Σ tx te p l)
128 | Flat_RLet : ∀ Γ Δ Σ σ₁ σ₂ p l, Rule_Flat (RLet Γ Δ Σ σ₁ σ₂ p l)
129 | Flat_RJoin : ∀ q a b c d e , Rule_Flat (RJoin q a b c d e)
130 | Flat_RVoid : ∀ q a , Rule_Flat (RVoid q a)
131 | Flat_RCase : ∀ Σ Γ T κlen κ θ l x , Rule_Flat (RCase Σ Γ T κlen κ θ l x)
132 | Flat_RLetRec : ∀ Γ Δ Σ₁ τ₁ τ₂ lev, Rule_Flat (RLetRec Γ Δ Σ₁ τ₁ τ₂ lev).
134 Lemma no_rules_with_empty_conclusion : forall c h, @Rule c h -> h=[] -> False.
136 destruct X; try destruct c; try destruct o; simpl in *; try inversion H.
139 Lemma no_rules_with_multiple_conclusions : forall c h,
140 Rule c h -> { h1:Tree ??Judg & { h2:Tree ??Judg & h=(h1,,h2) }} -> False.
142 destruct X; try destruct c; try destruct o; simpl in *; try inversion H;
143 try apply no_urules_with_empty_conclusion in u; try apply u.
144 destruct X0; destruct s; inversion e.
146 destruct X0; destruct s; inversion e.
147 destruct X0; destruct s; inversion e.
148 destruct X0; destruct s; inversion e.
149 destruct X0; destruct s; inversion e.
150 destruct X0; destruct s; inversion e.
151 destruct X0; destruct s; inversion e.
152 destruct X0; destruct s; inversion e.
153 destruct X0; destruct s; inversion e.
154 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.
167 Lemma systemfc_all_rules_one_conclusion : forall h c1 c2 (r:Rule h (c1,,c2)), False.
169 eapply no_rules_with_multiple_conclusions.
176 (* "Arrange" objects are parametric in the type of the leaves of the tree *)
177 Definition arrangeMap :
178 forall {T} (Σ₁ Σ₂:Tree ??T) {R} (f:T -> R),
180 Arrange (mapOptionTree f Σ₁) (mapOptionTree f Σ₂).
195 eapply RComp; [ apply IHX1 | apply IHX2 ].
198 (* a frequently-used Arrange *)
199 Definition arrangeSwapMiddle {T} (a b c d:Tree ??T) :
200 Arrange ((a,,b),,(c,,d)) ((a,,c),,(b,,d)).