1 (*********************************************************************************************************************************)
2 (* HaskStrongToProof: convert HaskStrong to HaskProof *)
3 (*********************************************************************************************************************************)
5 Generalizable All Variables.
6 Require Import Preamble.
7 Require Import General.
8 Require Import NaturalDeduction.
9 Require Import Coq.Strings.String.
10 Require Import Coq.Lists.List.
11 Require Import Coq.Init.Specif.
12 Require Import HaskKinds.
13 Require Import HaskStrongTypes.
14 Require Import HaskStrong.
15 Require Import HaskProof.
17 Axiom fail : forall {A}, string -> A.
18 Extract Inlined Constant fail => "Prelude.error".
20 Section HaskStrongToProof.
22 (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
23 * expansion on an entire uniform proof *)
24 Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ))
25 := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
26 Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ))
27 := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
29 Definition pivotContext {Γ}{Δ} a b c τ :
31 [ Γ >> Δ > (a,,b),,c |- τ]
32 [ Γ >> Δ > (a,,c),,b |- τ].
33 set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
35 eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ].
36 eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
40 Definition copyAndPivotContext {Γ}{Δ} a b c τ :
42 [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
43 [ Γ >> Δ > (a,,c),,b |- τ].
44 set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
46 eapply nd_comp; [ idtac | apply q ].
48 eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
49 set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
51 eapply nd_comp ; [ idtac | apply q ].
59 Context {VV:Type}{eqd_vv:EqDecidable VV}.
61 (* maintenance of Xi *)
62 Definition dropVar (lv:list VV)(v:VV) : ??VV :=
64 (fun a b:bool => if a then true else if b then true else false)
65 (map (fun lvv => if eqd_dec lvv v then true else false) lv)
69 (* later: use mapOptionTreeAndFlatten *)
70 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
71 mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
73 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
74 match exp as E in Expr Γ Δ ξ τ with
75 | EVar Γ Δ ξ ev => [ev]
76 | ELit Γ Δ ξ lit lev => []
77 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
78 | ELam Γ Δ ξ t1 t2 lev v pf e => stripOutVars (v::nil) (expr2antecedent e)
79 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
80 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
81 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
82 | ECast Γ Δ ξ γ t1 t2 lev wfco e => expr2antecedent e
83 | ENote Γ Δ ξ t n e => expr2antecedent e
84 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
85 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => expr2antecedent e
86 | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => expr2antecedent e
87 | ETyApp Γ Δ κ σ τ ξ l pf e => expr2antecedent e
88 | ELetRec Γ Δ ξ l τ vars branches body =>
89 let branch_context := eLetRecContext branches
90 in let all_contexts := (expr2antecedent body),,branch_context
91 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
92 | ECase Γ Δ ξ lev tc avars tbranches e' alts =>
93 ((fix varsfromalts (alts:
94 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc avars
96 (sac_Δ scb Γ avars (weakCK'' Δ))
98 (weakLT' (tbranches@@lev)) }
102 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
103 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
104 end) alts),,(expr2antecedent e')
106 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
108 | ELR_nil Γ Δ ξ lev => []
109 | ELR_leaf Γ Δ ξ t lev v e => expr2antecedent e
110 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
114 Definition caseBranchRuleInfoFromEStrongAltCon
115 `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
116 @StrongAltConRuleInfo n tc Γ lev tbranches.
117 set (ecase2antecedent _ _ _ _ _ _ _ _ ecb) as Σ.
119 apply Build_StrongAltConRuleInfo with (pcb_scb := alt)(pcb_Σ := mapOptionTree ξ Σ).
122 Definition judgFromEStrongAltCon
123 `(ecb:EStrongAltCon Γ Δ ξ lev n tc avars tbranches) :
125 apply caseBranchRuleInfoFromEStrongAltCon in ecb.
130 Implicit Arguments caseBranchRuleInfoFromEStrongAltCon [ [Γ] [Δ] [ξ] [lev] [tc] [avars] [tbranches] ].
132 Definition unlev {Γ:TypeEnv}(lht:LeveledHaskType Γ) : HaskType Γ := match lht with t @@ l => t end.
133 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ) :=
135 | ELR_nil Γ Δ ξ lev => []
136 | ELR_leaf Γ Δ ξ t lev v e => [unlev (ξ v) @@ lev]
137 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
140 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
142 | ELR_nil Γ Δ ξ lev => []
143 | ELR_leaf Γ Δ ξ t lev v e => [v]
144 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
147 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ):=
149 | ELR_nil Γ Δ ξ lev => []
150 | ELR_leaf Γ Δ ξ t lev v e => [(v, ξ v)]
151 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
155 Lemma stripping_nothing_is_inert
157 (ξ:VV -> LeveledHaskType Γ)
159 stripOutVars nil tree = tree.
161 simpl; destruct a; reflexivity.
165 fold (stripOutVars nil).
173 Definition arrangeContext
174 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
175 v (* variable to be pivoted, if found *)
176 ctx (* initial context *)
177 τ (* type of succedent *)
178 (ξ:VV -> LeveledHaskType Γ)
181 (* a proof concluding in a context where that variable does not appear *)
183 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
184 [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ])
186 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
188 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
189 [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
191 induction ctx; simpl in *.
193 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
197 unfold stripOutVars in *; simpl.
199 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
200 destruct (eqd_dec v v'); simpl in *.
202 (* where the leaf is v *)
208 (* where the leaf is NOT v *)
215 apply inl; simpl in *.
224 | inr rpf => let case_Both := tt in _
225 | inl rpf => let case_Left := tt in _
229 | inr rpf => let case_Right := tt in _
230 | inl rpf => let case_Neither := tt in _
232 end); clear IHctx1; clear IHctx2.
234 destruct case_Neither.
236 eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
238 (* order will not matter because these are central as morphisms *)
239 (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
240 (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
245 fold (stripOutVars (v::nil)).
246 set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
252 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
253 eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
254 set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
255 [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq.
262 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
263 fold (stripOutVars (v::nil)).
264 eapply nd_comp; [ idtac | eapply pivotContext ].
265 set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
266 set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
268 eapply nd_comp; [ idtac | apply qq ].
270 set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
277 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
278 fold (stripOutVars (v::nil)).
279 eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
281 (* order will not matter because these are central as morphisms *)
282 (ext_right _ _ _ lpf)
283 (ext_left _ _ _ rpf)).
287 (* same as before, but use RWeak if necessary *)
288 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
290 [Γ >> Δ>mapOptionTree ξ ctx |- τ]
291 [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ].
292 set (arrangeContext Γ Δ v ctx τ ξ) as q.
294 eapply nd_comp; [ apply n | idtac ].
296 refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
299 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
301 [Γ >> Δ>(mapOptionTree ξ ctx) |- z]
302 [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
306 unfold mapOptionTree in *.
308 fold (mapOptionTree ξ) in *.
310 apply arrangeContextAndWeaken.
312 unfold mapOptionTree; simpl in *.
314 rewrite (@stripping_nothing_is_inert Γ); auto.
318 unfold mapOptionTree in *.
320 fold (mapOptionTree ξ) in *.
321 set (mapOptionTree ξ) as X in *.
323 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
324 unfold stripOutVars in IHv2'.
326 fold (stripOutVars (leaves v2)) in IHv2'.
327 fold (stripOutVars (leaves v1)) in IHv2'.
329 unfold mapOptionTree in IHv2'.
331 fold (mapOptionTree ξ) in IHv2'.
333 set (nd_comp (IHv1 _ _) IHv2') as qq.
336 clear qq IHv2' IHv2 IHv1.
338 assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
343 (* FIXME TOTAL BOGOSITY *)
344 assert ((stripOutVars (leaves v2) v1) = v1).
353 Definition update_ξ'' {Γ} ξ tree lev :=
355 (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩)
358 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ) v tree lev :
359 mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
360 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
361 induction tree; simpl in *; try reflexivity; auto.
363 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
364 destruct a; simpl; try reflexivity.
367 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
371 set (eqd_dec v v0) as q.
372 assert (q=eqd_dec v v0).
379 unfold mapOptionTree.
380 unfold mapOptionTree in IHtree1.
381 unfold mapOptionTree in IHtree2.
384 fold (stripOutVars (v::nil)).
392 Lemma updating_stripped_tree_is_inert'
394 (ξ:VV -> LeveledHaskType Γ)
396 mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
397 = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
401 Lemma updating_stripped_tree_is_inert''
403 (ξ:VV -> LeveledHaskType Γ)
405 mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
406 = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree).
411 Lemma updating_stripped_tree_is_inert'''
413 (ξ:VV -> LeveledHaskType Γ)
415 (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
417 mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
418 = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
423 (* IDEA: use multi-conclusion proofs instead *)
424 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
425 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
426 | lrsp_leaf : forall v e,
427 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [((unlev (ξ v) @@ lev))]]) ->
428 LetRecSubproofs Γ Δ ξ lev [(v, (unlev (ξ v)))] (ELR_leaf _ _ _ _ _ _ e)
429 | lrsp_cons : forall t1 t2 b1 b2,
430 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
431 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
432 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
434 Lemma dork : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
436 eLetRecTypes branches =
437 mapOptionTree (update_ξ'' ξ tree lev)
438 (mapOptionTree (@fst _ _) tree).
444 unfold mapOptionTree; simpl.
449 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
450 : LetRecSubproofs Γ Δ ξ lev tree branches ->
453 mapOptionTree ξ (eLetRecContext branches)
455 eLetRecTypes branches
458 induction X; intros; simpl in *.
461 unfold mapOptionTree.
464 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
465 eapply nd_comp; [ apply nd_llecnac | idtac ].
470 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ) tree z lev,
471 mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
477 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
478 forall branches body,
479 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
480 LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
481 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
483 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
490 (map (fun x : VV * HaskType Γ => ⟨fst x, snd x @@ lev ⟩)
491 (leaves tree)))) as ξ' in *.
492 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
493 set (mapOptionTree (@fst _ _) tree) as pctx.
494 set (mapOptionTree ξ' pctx) as passback.
495 set (fun a b => @RLetRec Γ Δ a b passback) as z.
496 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
499 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
500 unfold passback in *; clear passback.
501 unfold pctx in *; clear pctx.
502 eapply UND_to_ND in q'.
505 set (@updating_stripped_tree_is_inert') as zz.
506 unfold update_ξ'' in *.
512 eapply nd_comp; [ idtac | apply q' ].
514 unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
518 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
520 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
521 eapply nd_comp; [ apply nd_llecnac | idtac ].
524 set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
525 unfold update_ξ'' in *.
531 Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx),
532 unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars).
536 Lemma cheat : forall {T} (a b:T), a=b.
540 Definition expr2proof :
541 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
542 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
544 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
545 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
546 match exp as E in Expr Γ Δ ξ τ with
547 | EVar Γ Δ ξ ev => let case_EVar := tt in _
548 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
549 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
550 let e1' := expr2proof _ _ _ _ e1 in
551 let e2' := expr2proof _ _ _ _ e2 in _
552 | ELam Γ Δ ξ t1 t2 lev v pf e => let case_ELam := tt in
553 let e' := expr2proof _ _ _ _ e in _
554 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
555 let pf_let := (expr2proof _ _ _ _ ev) in
556 let pf_body := (expr2proof _ _ _ _ ebody) in _
557 | ELetRec Γ Δ ξ lev t tree branches ebody =>
558 let e' := expr2proof _ _ _ _ ebody in
559 let ξ' := update_ξ'' ξ tree lev in
560 let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ''))
561 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
562 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
563 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
564 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
565 | ELR_leaf Γ Δ ξ t l v e => (fun e' => let case_elr_leaf := tt in _) (expr2proof _ _ _ _ e)
566 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
568 ) _ _ _ _ tree branches) in
569 let case_ELetRec := tt in _
570 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _
571 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _
572 | ECast Γ Δ ξ γ t1 t2 lev wfco e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _
573 | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _
574 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _
575 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l wfco1 wfco2 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _
576 | ECoApp Γ Δ γ σ₁ σ₂ σ ξ l wfco e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _
577 | ETyApp Γ Δ κ σ τ ξ l pf e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _
578 | ECase Γ Δ ξ lev tbranches tc avars e alts =>
582 Tree ??{ scb : StrongCaseBranchWithVVs tc avars
584 (sac_Δ scb Γ avars (weakCK'' Δ))
586 (weakLT' (tbranches@@lev)) })
587 : ND Rule [] (mapOptionTree judgFromEStrongAltCon alts) :=
588 match alts as ALTS return ND Rule [] (mapOptionTree judgFromEStrongAltCon ALTS) with
589 | T_Leaf None => let case_nil := tt in _
590 | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
591 | T_Branch b1 b2 => let case_branch := tt in _
593 in *) let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
595 ); clear exp ξ' τ' Γ' Δ'; simpl in *.
599 unfold mapOptionTree; simpl.
608 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
609 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
610 eapply nd_comp; [ apply nd_llecnac | idtac ].
613 destruct case_ELam; intros.
614 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
615 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
616 set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
617 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
618 apply UND_to_ND in pfx.
619 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
621 fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
622 rewrite updating_stripped_tree_is_inert in pfx.
623 unfold update_ξ in pfx.
624 destruct (eqd_dec v v).
625 eapply nd_comp; [ idtac | apply pfx ].
634 destruct case_ELet; intros.
635 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
636 eapply nd_comp; [ apply nd_llecnac | idtac ].
637 apply nd_prod; [ idtac | apply pf_let].
639 eapply nd_comp; [ apply pf_body | idtac ].
641 fold (@mapOptionTree VV).
642 fold (mapOptionTree ξ).
643 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
644 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
645 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
647 rewrite updating_stripped_tree_is_inert in n.
648 unfold update_ξ in n.
649 destruct (eqd_dec lev lev).
652 apply UND_to_ND in n.
654 assert False. apply n0; auto. inversion H.
657 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
660 destruct case_EBrak; intros.
661 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
665 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast with (γ:=γ)].
670 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
674 destruct case_ETyApp; intros.
675 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
679 destruct case_ECoLam; intros.
680 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
685 destruct case_ECoApp; intros.
686 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) σ₁ σ₂ σ γ l) ].
690 destruct case_ETyLam; intros.
691 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
692 unfold mapOptionTree in e'.
693 rewrite mapOptionTree_compose in e'.
694 unfold mapOptionTree.
698 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
699 apply (fail "ECase not implemented").
701 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
702 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
703 rewrite <- mapOptionTree_compose.
708 destruct case_elr_leaf; intros.
709 assert (unlev (ξ0 v) = t0).
711 set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q.
716 destruct case_ELetRec; intros.
717 set (@letRecSubproofsToND') as q.
728 clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u.
729 repeat rewrite <- mapOptionTree_compose in *.
731 (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q.
733 assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
734 apply update_ξ_and_reapply.
737 unfold mapOptionTree in q; simpl in q.
738 set (@updating_stripped_tree_is_inert''') as u.
739 unfold mapOptionTree in u.
742 unfold weakenX' in *.
744 unfold mapOptionTree in *.
746 (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0))
748 (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
752 destruct case_branch.
753 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
761 End HaskStrongToProof.
765 (* Figure 7, production "decl"; actually not used in this formalization *)
767 | DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
768 | DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
769 | DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
771 (* Figure 1, production "pgm" *)
773 mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.