1 (*********************************************************************************************************************************)
4 (* Skolemizes the portion of a proof which uses judgments at level >0 *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import NaturalDeduction.
12 Require Import NaturalDeductionContext.
13 Require Import Coq.Strings.String.
14 Require Import Coq.Lists.List.
16 Require Import HaskKinds.
17 Require Import HaskCoreTypes.
18 Require Import HaskCoreVars.
19 Require Import HaskWeakTypes.
20 Require Import HaskWeakVars.
21 Require Import HaskLiterals.
22 Require Import HaskTyCons.
23 Require Import HaskStrongTypes.
24 Require Import HaskProof.
25 Require Import NaturalDeduction.
27 Require Import HaskStrongTypes.
28 Require Import HaskStrong.
29 Require Import HaskProof.
30 Require Import HaskStrongToProof.
31 Require Import HaskProofToStrong.
32 Require Import HaskWeakToStrong.
35 Set Printing Width 130.
37 Section HaskSkolemizer.
40 Fixpoint debruijn2phoas {κ} (exp: RawHaskType (fun _ => nat) κ) : HaskType TV κ :=
43 | TAll _ y => TAll _ (fun v => debruijn2phoas (y (TVar v)))
44 | TApp _ _ x y => TApp (debruijn2phoas x) (debruijn2phoas y)
46 | TCoerc _ t1 t2 t => TCoerc (debruijn2phoas t1) (debruijn2phoas t2) (debruijn2phoas t)
48 | TCode v e => TCode (debruijn2phoas v) (debruijn2phoas e)
49 | TyFunApp tfc kl k lt => TyFunApp tfc kl k (debruijn2phoasyFunApp _ lt)
51 with debruijn2phoasyFunApp (lk:list Kind)(exp:@RawHaskTypeList (fun _ => nat) lk) : @HaskTypeList TV lk :=
52 match exp in @RawHaskTypeList _ LK return @RawHaskTypeList TV LK with
53 | TyFunApp_nil => TyFunApp_nil
54 | TyFunApp_cons κ kl t rest => TyFunApp_cons _ _ (debruijn2phoas t) (debruijn2phoasyFunApp _ rest)
57 Definition isNotBrakOrEsc {h}{c} (r:Rule h c) : Prop :=
59 | RBrak _ _ _ _ _ _ => False
60 | REsc _ _ _ _ _ _ => False
64 Fixpoint mkArrows {Γ}(lt:list (HaskType Γ ★))(t:HaskType Γ ★) : HaskType Γ ★ :=
67 | a::b => mkArrows b (a ---> t)
71 Fixpoint unleaves_ {Γ}(t:Tree ??(LeveledHaskType Γ ★))(l:list (HaskType Γ ★)) lev : Tree ??(LeveledHaskType Γ ★) :=
74 | a::b => unleaves_ (t,,[a @@ lev]) b lev
77 (* weak inverse of "leaves" *)
78 Fixpoint unleaves_ {A:Type}(l:list A) : Tree (option A) :=
82 | (a::b) => [a],,(unleaves_ b)
85 (* rules of skolemized proofs *)
86 Definition getΓ (j:Judg) := match j with Γ > _ > _ |- _ @ _ => Γ end.
88 Fixpoint take_trustme {Γ}
90 (l:forall TV, InstantiatedTypeEnv TV Γ -> list (RawHaskType TV ★))
91 : list (HaskType Γ ★) :=
95 | S n' => (fun TV ite => match l TV ite with
96 | nil => Prelude_error "impossible"
100 take_trustme n' (fun TV ite => match l TV ite with
101 | nil => Prelude_error "impossible"
106 Axiom phoas_extensionality : forall Γ Q (f g:forall TV, InstantiatedTypeEnv TV Γ -> Q TV),
107 (forall tv ite, f tv ite = g tv ite) -> f=g.
109 Definition take_arg_types_as_tree {Γ}(ht:HaskType Γ ★) : Tree ??(HaskType Γ ★ ) :=
112 (count_arg_types (ht _ (ite_unit _)))
113 (fun TV ite => take_arg_types (ht TV ite))).
115 Definition drop_arg_types_as_tree {Γ} (ht:HaskType Γ ★) : HaskType Γ ★ :=
116 fun TV ite => drop_arg_types (ht TV ite).
118 Implicit Arguments take_arg_types_as_tree [[Γ]].
119 Implicit Arguments drop_arg_types_as_tree [[Γ]].
121 Definition take_arrange : forall {Γ} (tx te:HaskType Γ ★) lev,
122 Arrange ([tx @@ lev],,take_arg_types_as_tree te @@@ lev)
123 (take_arg_types_as_tree (tx ---> te) @@@ lev).
125 destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
129 unfold take_arg_types_as_tree.
130 Opaque take_arg_types_as_tree.
132 destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
134 replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
136 apply phoas_extensionality.
138 apply (Prelude_error "should not be possible").
140 Transparent take_arg_types_as_tree.
142 Definition take_unarrange : forall {Γ} (tx te:HaskType Γ ★) lev,
143 Arrange (take_arg_types_as_tree (tx ---> te) @@@ lev)
144 ([tx @@ lev],,take_arg_types_as_tree te @@@ lev).
146 destruct (eqd_dec ([tx],,take_arg_types_as_tree te) (take_arg_types_as_tree (tx ---> te))).
150 unfold take_arg_types_as_tree.
151 Opaque take_arg_types_as_tree.
153 destruct (count_arg_types (te (fun _ : Kind => unit) (ite_unit Γ))).
155 replace (tx) with (fun (TV : Kind → Type) (ite : InstantiatedTypeEnv TV Γ) => tx TV ite).
157 apply phoas_extensionality.
159 apply (Prelude_error "should not be possible").
161 Transparent take_arg_types_as_tree.
163 Lemma drop_works : forall {Γ}(t1 t2:HaskType Γ ★),
164 drop_arg_types_as_tree (t1 ---> t2) = (drop_arg_types_as_tree t2).
166 unfold drop_arg_types_as_tree.
171 Inductive SRule : Tree ??Judg -> Tree ??Judg -> Type :=
172 (* | SFlat : forall h c (r:Rule h c), isNotBrakOrEsc r -> SRule h c*)
173 | SFlat : forall h c, Rule h c -> SRule h c
174 | SBrak : forall Γ Δ t ec Σ l,
176 [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)]
177 [Γ > Δ > Σ |- [<[ec |- t]> ] @l]
179 | SEsc : forall Γ Δ t ec Σ l,
181 [Γ > Δ > Σ |- [<[ec |- t]> ] @l]
182 [Γ > Δ > Σ,,(take_arg_types_as_tree t @@@ (ec::l)) |- [ drop_arg_types_as_tree t ] @ (ec::l)]
185 Definition take_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
186 match lt with t @@ l => take_arg_types_as_tree t @@@ l end.
188 Definition drop_arg_types_as_tree' {Γ}(lt:LeveledHaskType Γ ★) :=
189 match lt with t @@ l => drop_arg_types_as_tree t @@ l end.
191 Definition skolemize_judgment (j:Judg) : Judg :=
193 | Γ > Δ > Σ₁ |- Σ₂ @ nil => j
194 | Γ > Δ > Σ₁ |- Σ₂ @ lev =>
195 Γ > Δ > Σ₁,,(mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂ @@@ lev) |- mapOptionTree drop_arg_types_as_tree Σ₂ @ lev
198 Definition check_hof : forall {Γ}(t:HaskType Γ ★),
201 (take_arg_types_as_tree t = [] /\ drop_arg_types_as_tree t = t).
203 destruct (eqd_dec (take_arg_types_as_tree t) []);
204 destruct (eqd_dec (drop_arg_types_as_tree t) t).
211 Opaque take_arg_types_as_tree.
212 Definition skolemize_proof :
215 ND SRule (mapOptionTree skolemize_judgment h) (mapOptionTree skolemize_judgment c).
217 eapply nd_map'; [ idtac | apply X ].
221 refine (match X as R in Rule H C with
222 | RArrange Γ Δ a b x l d => let case_RArrange := tt in _
223 | RNote Γ Δ Σ τ l n => let case_RNote := tt in _
224 | RLit Γ Δ l _ => let case_RLit := tt in _
225 | RVar Γ Δ σ lev => let case_RVar := tt in _
226 | RGlobal Γ Δ σ l wev => let case_RGlobal := tt in _
227 | RLam Γ Δ Σ tx te lev => let case_RLam := tt in _
228 | RCast Γ Δ Σ σ τ lev γ => let case_RCast := tt in _
229 | RAbsT Γ Δ Σ κ σ lev => let case_RAbsT := tt in _
230 | RAppT Γ Δ Σ κ σ τ lev => let case_RAppT := tt in _
231 | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ lev => let case_RAppCo := tt in _
232 | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ lev => let case_RAbsCo := tt in _
233 | RApp Γ Δ Σ₁ Σ₂ tx te lev => let case_RApp := tt in _
234 | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ lev => let case_RLet := tt in _
235 | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _
236 | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _
237 | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _
238 | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ lev => let case_RWhere := tt in _
239 | RJoin Γ p lri m x q l => let case_RJoin := tt in _
240 | RVoid _ _ l => let case_RVoid := tt in _
241 | RBrak Γ Δ t ec succ lev => let case_RBrak := tt in _
242 | REsc Γ Δ t ec succ lev => let case_REsc := tt in _
243 | RCase Γ Δ lev tc Σ avars tbranches alts => let case_RCase := tt in _
244 | RLetRec Γ Δ lri x y t => let case_RLetRec := tt in _
247 destruct case_RArrange.
262 destruct lev; [ idtac | apply (Prelude_error "Brak with nesting depth >1") ].
268 destruct lev; [ idtac | apply (Prelude_error "Esc with nesting depth >1") ].
288 set (check_hof (@literalType l Γ)) as hof.
289 destruct hof; [ apply (Prelude_error "attempt to use a literal with higher-order type at depth>0") | idtac ].
294 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; apply AuCanL ].
302 apply nd_rule; apply SFlat; apply RVar.
303 set (check_hof σ) as hof.
304 destruct hof; [ apply (Prelude_error "attempt to use a variable with higher-order type at depth>0") | idtac ].
309 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
314 destruct case_RGlobal.
317 apply nd_rule; apply SFlat; apply RGlobal.
318 set (check_hof (l wev)) as hof.
319 destruct hof; [ apply (Prelude_error "attempt to use a global with higher-order type at depth>0") | idtac ].
324 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AuCanR ].
352 apply (Prelude_error "found RCast at level >0").
360 apply (Prelude_error "found RJoin at level >0").
369 set (check_hof tx) as hof_tx.
370 destruct hof_tx; [ apply (Prelude_error "attempt tp apply a higher-order function at depth>0") | idtac ].
376 eapply nd_prod; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
381 eapply take_unarrange.
383 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
384 eapply nd_rule; eapply SFlat; apply RWhere.
392 set (check_hof σ₁) as hof_tx.
393 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
399 eapply nd_prod; [ eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR | eapply nd_id ].
401 set (@RLet Γ Δ Σ₁ (Σ₂,,(take_arg_types_as_tree σ₂ @@@ (h::lev))) σ₁ (drop_arg_types_as_tree σ₂) (h::lev)) as q.
402 eapply nd_comp; [ idtac | eapply nd_rule; apply SFlat; eapply RArrange; apply AAssoc ].
403 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply q ].
411 destruct case_RWhere.
417 set (check_hof σ₁) as hof_tx.
418 destruct hof_tx; [ apply (Prelude_error "attempt to let-bind a higher-order function at depth>0") | idtac ].
424 eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
425 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
426 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AAssoc ].
427 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RWhere ].
428 apply nd_prod; [ idtac | eapply nd_id ].
429 eapply nd_rule; apply SFlat; eapply RArrange.
436 simpl; destruct l; [ apply nd_rule; apply SFlat; apply RCut | idtac ].
437 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₃) as Σ₃''.
438 set (mapOptionTree drop_arg_types_as_tree Σ₃) as Σ₃'''.
439 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₁₂) as Σ₁₂''.
440 set (mapOptionTree drop_arg_types_as_tree Σ₁₂) as Σ₁₂'''.
441 destruct (decide_tree_empty Σ₁₂''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
442 destruct (eqd_dec Σ₁₂ Σ₁₂'''); [ idtac | apply (Prelude_error "used RCut on a variable with function type") ].
445 eapply nd_prod; [ apply nd_id | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
446 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
447 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RCut ].
449 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ACanR ].
455 eapply arrangeCancelEmptyTree with (q:=x).
457 admit. (* FIXME, but not serious *)
461 simpl; destruct l; [ apply nd_rule; apply SFlat; apply RLeft | idtac ].
462 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
463 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
464 set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
465 set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
466 destruct (decide_tree_empty (Σ' @@@ (h::l)));
467 [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
468 destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RLeft on a variable with function type") ].
472 set (arrangeUnCancelEmptyTree _ _ e) as q.
473 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ARight; eapply q ].
474 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanL; eapply q ].
475 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
480 destruct case_RRight.
481 simpl; destruct l; [ apply nd_rule; apply SFlat; apply RRight | idtac ].
482 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ₂) as Σ₂'.
483 set (mapOptionTreeAndFlatten take_arg_types_as_tree Σ) as Σ'.
484 set (mapOptionTree drop_arg_types_as_tree Σ₂) as Σ₂''.
485 set (mapOptionTree drop_arg_types_as_tree Σ) as Σ''.
486 destruct (decide_tree_empty (Σ' @@@ (h::l)));
487 [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
488 destruct (eqd_dec Σ Σ''); [ idtac | apply (Prelude_error "used RRight on a variable with function type") ].
492 set (arrangeUnCancelEmptyTree _ _ e) as q.
493 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply ALeft; eapply q ].
494 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AuCanR ].
495 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AAssoc ].
496 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply ALeft; eapply AExch ]. (* yuck *)
497 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuAssoc ].
508 eapply nd_comp; [ idtac | eapply nd_rule; eapply SFlat; eapply RArrange; eapply AuCanL ].
515 destruct lev; [ apply nd_rule; apply SFlat; apply RAppT | idtac ].
516 apply (Prelude_error "RAppT at depth>0").
520 destruct lev; simpl; [ apply nd_rule; apply SFlat; apply (@RAbsT _ _ _ _ _ nil) | idtac ].
521 apply (Prelude_error "RAbsT at depth>0").
523 destruct case_RAppCo.
525 destruct lev; [ apply nd_rule; apply SFlat; apply RAppCo | idtac ].
527 apply (Prelude_error "RAppCo at depth>0").
529 destruct case_RAbsCo.
531 destruct lev; [ apply nd_rule; apply SFlat; apply RAbsCo | idtac ].
532 apply (Prelude_error "RAbsCo at depth>0").
534 destruct case_RLetRec.
539 apply (@RLetRec Γ Δ lri x y nil).
540 apply (Prelude_error "RLetRec at depth>0").
544 apply (Prelude_error "CASE: BIG FIXME").
547 Transparent take_arg_types_as_tree.