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 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 e => expr2antecedent e
83 | ENote Γ Δ ξ t n e => expr2antecedent e
84 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
85 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
86 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
87 | ETyApp Γ Δ κ σ τ ξ l 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 Γ Δ ξ l tc tbranches sac atypes e' alts =>
93 ((fix varsfromalts (alts:
94 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc sac atypes
96 (sac_Δ scb Γ atypes (weakCK'' Δ))
98 (weakLT' (tbranches@@l)) }
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 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 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 e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _
576 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _
577 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _
578 | ECase Γ Δ ξ l tc tbranches sac atypes 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 ].
633 destruct case_ELet; intros.
634 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
635 eapply nd_comp; [ apply nd_llecnac | idtac ].
636 apply nd_prod; [ idtac | apply pf_let].
638 eapply nd_comp; [ apply pf_body | idtac ].
640 fold (@mapOptionTree VV).
641 fold (mapOptionTree ξ).
642 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
643 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
644 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
646 rewrite updating_stripped_tree_is_inert in n.
647 unfold update_ξ in n.
648 destruct (eqd_dec lev lev).
651 apply UND_to_ND in n.
653 assert False. apply n0; auto. inversion H.
656 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
659 destruct case_EBrak; intros.
660 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
664 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
669 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
673 destruct case_ETyApp; intros.
674 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
678 destruct case_ECoLam; intros.
679 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
682 destruct case_ECoApp; intros.
683 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
687 destruct case_ETyLam; intros.
688 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
689 unfold mapOptionTree in e'.
690 rewrite mapOptionTree_compose in e'.
691 unfold mapOptionTree.
695 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
696 apply (fail "ECase not implemented").
698 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
699 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
700 rewrite <- mapOptionTree_compose.
705 destruct case_elr_leaf; intros.
706 assert (unlev (ξ0 v) = t0).
708 set (@lrsp_leaf Γ0 Δ0 ξ0 l v) as q.
713 destruct case_ELetRec; intros.
714 set (@letRecSubproofsToND') as q.
725 clear mkdcsp alts0 o ecb Γ Δ ξ lev tc avars e alts u.
726 repeat rewrite <- mapOptionTree_compose in *.
728 (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _ (unshape corevars) _ _))) as q.
730 assert (unshape (scb_types alt) = (mapOptionTree (update_ξ''' (weakenX' ξ0) (scb_types alt) corevars) (unshape corevars))).
731 apply update_ξ_and_reapply.
734 unfold mapOptionTree in q; simpl in q.
735 set (@updating_stripped_tree_is_inert''') as u.
736 unfold mapOptionTree in u.
739 unfold weakenX' in *.
741 unfold mapOptionTree in *.
743 (@weakenT' _ (sac_ekinds alt) (coreTypeToType φ tbranches0))
745 (coreTypeToType (updatePhi φ (sac_evars alt)) tbranches0).
749 destruct case_branch.
750 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
758 End HaskStrongToProof.
762 (* Figure 7, production "decl"; actually not used in this formalization *)
764 | DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
765 | DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
766 | DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
768 (* Figure 1, production "pgm" *)
770 mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.