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 HaskWeakVars.
16 Require Import HaskProof.
18 Section HaskStrongToProof.
20 (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
21 * expansion on an entire uniform proof *)
22 Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
23 := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
24 Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
25 := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
27 Definition pivotContext {Γ}{Δ} a b c τ :
29 [ Γ >> Δ > (a,,b),,c |- τ]
30 [ Γ >> Δ > (a,,c),,b |- τ].
31 set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
33 eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ].
34 eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
38 Definition copyAndPivotContext {Γ}{Δ} a b c τ :
40 [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
41 [ Γ >> Δ > (a,,c),,b |- τ].
42 set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
44 eapply nd_comp; [ idtac | apply q ].
46 eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
47 set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
49 eapply nd_comp ; [ idtac | apply q ].
57 Context {VV:Type}{eqd_vv:EqDecidable VV}.
59 (* maintenance of Xi *)
60 Definition dropVar (lv:list VV)(v:VV) : ??VV :=
62 (fun a b:bool => if a then true else if b then true else false)
63 (map (fun lvv => if eqd_dec lvv v then true else false) lv)
67 (* later: use mapOptionTreeAndFlatten *)
68 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
69 mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
71 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
72 match exp as E in Expr Γ Δ ξ τ with
73 | EVar Γ Δ ξ ev => [ev]
74 | ELit Γ Δ ξ lit lev => []
75 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
76 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
77 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
78 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
79 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
80 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
81 | ENote Γ Δ ξ t n e => expr2antecedent e
82 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
83 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
84 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
85 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
86 | ELetRec Γ Δ ξ l τ vars branches body =>
87 let branch_context := eLetRecContext branches
88 in let all_contexts := (expr2antecedent body),,branch_context
89 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
90 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
91 ((fix varsfromalts (alts:
92 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
94 (sac_Δ scb Γ atypes (weakCK'' Δ))
96 (weakLT' (tbranches@@l)) }
100 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
101 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
102 end) alts),,(expr2antecedent e')
104 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
106 | ELR_nil Γ Δ ξ lev => []
107 | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e
108 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
111 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
112 (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
114 (sac_Δ scb Γ atypes (weakCK'' Δ))
116 (weakLT' (tbranches@@l)) })
117 : ProofCaseBranch tc Γ Δ l tbranches atypes.
119 {| pcb_scb := projT1 alt
120 ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
124 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
126 | ELR_nil Γ Δ ξ lev => []
127 | ELR_leaf Γ Δ ξ lev v e => [ξ v]
128 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
131 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
133 | ELR_nil Γ Δ ξ lev => []
134 | ELR_leaf Γ Δ ξ lev v e => [v]
135 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
138 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
140 | ELR_nil Γ Δ ξ lev => []
141 | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)]
142 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
146 Lemma stripping_nothing_is_inert
148 (ξ:VV -> LeveledHaskType Γ ★)
150 stripOutVars nil tree = tree.
152 simpl; destruct a; reflexivity.
156 fold (stripOutVars nil).
164 Definition arrangeContext
165 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
166 v (* variable to be pivoted, if found *)
167 ctx (* initial context *)
168 τ (* type of succedent *)
169 (ξ:VV -> LeveledHaskType Γ ★)
172 (* a proof concluding in a context where that variable does not appear *)
174 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
175 [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ])
177 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
179 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
180 [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
182 induction ctx; simpl in *.
184 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
188 unfold stripOutVars in *; simpl.
190 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
191 destruct (eqd_dec v v'); simpl in *.
193 (* where the leaf is v *)
199 (* where the leaf is NOT v *)
206 apply inl; simpl in *.
215 | inr rpf => let case_Both := tt in _
216 | inl rpf => let case_Left := tt in _
220 | inr rpf => let case_Right := tt in _
221 | inl rpf => let case_Neither := tt in _
223 end); clear IHctx1; clear IHctx2.
225 destruct case_Neither.
227 eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
229 (* order will not matter because these are central as morphisms *)
230 (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
231 (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
236 fold (stripOutVars (v::nil)).
237 set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
243 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
244 eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
245 set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
246 [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq.
253 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
254 fold (stripOutVars (v::nil)).
255 eapply nd_comp; [ idtac | eapply pivotContext ].
256 set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
257 set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
259 eapply nd_comp; [ idtac | apply qq ].
261 set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
268 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
269 fold (stripOutVars (v::nil)).
270 eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
272 (* order will not matter because these are central as morphisms *)
273 (ext_right _ _ _ lpf)
274 (ext_left _ _ _ rpf)).
278 (* same as before, but use RWeak if necessary *)
279 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
281 [Γ >> Δ>mapOptionTree ξ ctx |- τ]
282 [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ].
283 set (arrangeContext Γ Δ v ctx τ ξ) as q.
285 eapply nd_comp; [ apply n | idtac ].
287 refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
290 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
292 [Γ >> Δ>(mapOptionTree ξ ctx) |- z]
293 [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
297 unfold mapOptionTree in *.
299 fold (mapOptionTree ξ) in *.
301 apply arrangeContextAndWeaken.
303 unfold mapOptionTree; simpl in *.
305 rewrite (@stripping_nothing_is_inert Γ); auto.
309 unfold mapOptionTree in *.
311 fold (mapOptionTree ξ) in *.
312 set (mapOptionTree ξ) as X in *.
314 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
315 unfold stripOutVars in IHv2'.
317 fold (stripOutVars (leaves v2)) in IHv2'.
318 fold (stripOutVars (leaves v1)) in IHv2'.
320 unfold mapOptionTree in IHv2'.
322 fold (mapOptionTree ξ) in IHv2'.
324 set (nd_comp (IHv1 _ _) IHv2') as qq.
327 clear qq IHv2' IHv2 IHv1.
329 assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
334 (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
335 assert ((stripOutVars (leaves v2) v1) = v1).
344 Definition update_ξ'' {Γ} ξ tree lev :=
346 (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
349 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
350 mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
351 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
352 induction tree; simpl in *; try reflexivity; auto.
354 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
355 destruct a; simpl; try reflexivity.
358 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
362 set (eqd_dec v v0) as q.
363 assert (q=eqd_dec v v0).
370 unfold mapOptionTree.
371 unfold mapOptionTree in IHtree1.
372 unfold mapOptionTree in IHtree2.
375 fold (stripOutVars (v::nil)).
383 Lemma updating_stripped_tree_is_inert'
385 (ξ:VV -> LeveledHaskType Γ ★)
387 mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
388 = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
392 Lemma updating_stripped_tree_is_inert''
394 (ξ:VV -> LeveledHaskType Γ ★)
396 mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
397 = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree).
402 Lemma updating_stripped_tree_is_inert'''
404 (ξ:VV -> LeveledHaskType Γ)
406 (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
408 mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
409 = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
414 (* IDEA: use multi-conclusion proofs instead *)
415 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
416 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
417 | lrsp_leaf : forall v e,
418 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
419 LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
420 | lrsp_cons : forall t1 t2 b1 b2,
421 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
422 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
423 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
425 Lemma cheat9 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
427 eLetRecTypes branches =
428 mapOptionTree (update_ξ'' ξ tree lev)
429 (mapOptionTree (@fst _ _) tree).
435 unfold mapOptionTree; simpl.
440 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
441 : LetRecSubproofs Γ Δ ξ lev tree branches ->
444 mapOptionTree ξ (eLetRecContext branches)
446 eLetRecTypes branches
449 induction X; intros; simpl in *.
452 unfold mapOptionTree.
456 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
457 eapply nd_comp; [ apply nd_llecnac | idtac ].
462 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
463 mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
469 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
470 forall branches body,
471 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
472 LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
473 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
475 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
482 (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
483 (leaves tree)))) as ξ' in *.
484 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
485 set (mapOptionTree (@fst _ _) tree) as pctx.
486 set (mapOptionTree ξ' pctx) as passback.
487 set (fun a b => @RLetRec Γ Δ a b passback) as z.
488 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
491 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
492 unfold passback in *; clear passback.
493 unfold pctx in *; clear pctx.
494 eapply UND_to_ND in q'.
497 set (@updating_stripped_tree_is_inert') as zz.
498 unfold update_ξ'' in *.
504 eapply nd_comp; [ idtac | apply q' ].
506 unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
510 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
512 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
513 eapply nd_comp; [ apply nd_llecnac | idtac ].
516 set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
517 unfold update_ξ'' in *.
523 Lemma update_ξ_and_reapply : forall Γ ξ {T}(idx:Tree ??T)(types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx),
524 unshape types = mapOptionTree (update_ξ''' ξ types vars) (unshape vars).
529 Lemma cheat0 : forall Γ Δ ξ l tc tbranches atypes e alts',
530 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
533 ((mapOptionTreeAndFlatten
534 (fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
535 (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
537 ((mapOptionTreeAndFlatten pcb_freevars
538 (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
542 Lemma cheat1 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
545 Lemma cheat2 : forall {A}(t:list A), leaves (unleaves t) = t.
549 Definition expr2proof :
550 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
551 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
553 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
554 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
555 match exp as E in Expr Γ Δ ξ τ with
556 | EVar Γ Δ ξ ev => let case_EVar := tt in _
557 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
558 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
559 let e1' := expr2proof _ _ _ _ e1 in
560 let e2' := expr2proof _ _ _ _ e2 in _
561 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in
562 let e' := expr2proof _ _ _ _ e in _
563 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
564 let pf_let := (expr2proof _ _ _ _ ev) in
565 let pf_body := (expr2proof _ _ _ _ ebody) in _
566 | ELetRec Γ Δ ξ lev t tree branches ebody =>
567 let e' := expr2proof _ _ _ _ ebody in
568 let ξ' := update_ξ'' ξ tree lev in
569 let subproofs := ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
570 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
571 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
572 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
573 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
574 | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
575 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
577 ) _ _ _ _ tree branches) in
578 let case_ELetRec := tt in _
579 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in let e' := expr2proof _ _ _ _ e in _
580 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in let e' := expr2proof _ _ _ _ e in _
581 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in let e' := expr2proof _ _ _ _ e in _
582 | ENote Γ Δ ξ t n e => let case_ENote := tt in let e' := expr2proof _ _ _ _ e in _
583 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in let e' := expr2proof _ _ _ _ e in _
584 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in let e' := expr2proof _ _ _ _ e in _
585 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in let e' := expr2proof _ _ _ _ e in _
586 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in let e' := expr2proof _ _ _ _ e in _
587 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
590 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
592 (sac_Δ scb Γ atypes (weakCK'' Δ))
594 (weakLT' (tbranches@@l)) })
595 : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
596 match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
597 | T_Leaf None => let case_nil := tt in _
598 | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
599 | T_Branch b1 b2 => let case_branch := tt in _
601 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
603 ); clear exp ξ' τ' Γ' Δ'.
607 unfold mapOptionTree; simpl.
616 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
617 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
618 eapply nd_comp; [ apply nd_llecnac | idtac ].
621 destruct case_ELam; intros.
622 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
623 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
624 set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
625 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
626 apply UND_to_ND in pfx.
627 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
629 fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
630 rewrite updating_stripped_tree_is_inert in pfx.
631 unfold update_ξ in pfx.
632 destruct (eqd_dec v v).
633 eapply nd_comp; [ idtac | apply pfx ].
641 destruct case_ELet; intros; simpl in *.
642 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
643 eapply nd_comp; [ apply nd_llecnac | idtac ].
644 apply nd_prod; [ idtac | apply pf_let].
646 eapply nd_comp; [ apply pf_body | idtac ].
648 fold (@mapOptionTree VV).
649 fold (mapOptionTree ξ).
650 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
651 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
652 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
654 rewrite updating_stripped_tree_is_inert in n.
655 unfold update_ξ in n.
656 destruct (eqd_dec lev lev).
659 apply UND_to_ND in n.
661 assert False. apply n0; auto. inversion H.
664 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
667 destruct case_EBrak; intros.
668 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
672 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
677 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
681 destruct case_ETyApp; simpl in *; intros.
682 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
686 destruct case_ECoApp; simpl in *; intros.
687 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
694 repeat rewrite <- mapOptionTree_compose in *.
695 set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
696 (unleaves (vec2list (scbwv_exprvars (projT1 x))))
697 (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
703 unfold weakCK'' in q.
707 replace (mapOptionTree ((@weakLT' Γ (tyConKind tc) _) ○ ξ)
708 (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
709 (expr2antecedent (projT2 x))))
710 with (mapOptionTree (scbwv_ξ (projT1 x) ξ l)
711 (stripOutVars (vec2list (scbwv_exprvars (projT1 x)))
712 (expr2antecedent (projT2 x)))).
713 rewrite <- cheat1 in q.
714 rewrite vec2list_map_list2vec in q.
715 unfold mapOptionTree.
716 fold (@mapOptionTree (HaskType (app (tyConKind tc) Γ) ★)
717 (LeveledHaskType (app (tyConKind tc) Γ) ★) (fun t' => t' @@ weakL' l)).
725 unleaves (vec2list (vec_map (scbwv_ξ (projT1 x) ξ l) (scbwv_exprvars (projT1 x))))
727 unleaves (vec2list (sac_types (projT1 x) Γ atypes)) @@@ weakL'(κ:=tyConKind tc) l).
729 Set Printing Implicit.
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).
753 destruct case_branch.
754 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
761 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
762 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
763 rewrite <- mapOptionTree_compose.
767 destruct case_ELetRec; simpl in *; intros.
768 set (@letRecSubproofsToND') as q.
776 destruct case_ECoLam; simpl in *; intros.
777 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
780 destruct case_ETyLam; intros.
781 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
782 unfold mapOptionTree in e'.
783 rewrite mapOptionTree_compose in e'.
784 unfold mapOptionTree.
789 End HaskStrongToProof.
793 (* Figure 7, production "decl"; actually not used in this formalization *)
795 | DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
796 | DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
797 | DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
799 (* Figure 1, production "pgm" *)
801 mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.