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 cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
426 eLetRecTypes branches =
427 mapOptionTree (update_ξ'' ξ tree lev)
428 (mapOptionTree (@fst _ _) tree).
434 unfold mapOptionTree; simpl.
438 Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
439 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
442 ((mapOptionTreeAndFlatten
443 (fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
444 (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
446 ((mapOptionTreeAndFlatten pcb_freevars
447 (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
450 Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
453 Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
457 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
458 : LetRecSubproofs Γ Δ ξ lev tree branches ->
461 mapOptionTree ξ (eLetRecContext branches)
463 eLetRecTypes branches
466 induction X; intros; simpl in *.
476 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
477 eapply nd_comp; [ apply nd_llecnac | idtac ].
482 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
483 mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
489 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
490 forall branches body,
491 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
492 LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
493 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
495 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
502 (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
503 (leaves tree)))) as ξ' in *.
504 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
505 set (mapOptionTree (@fst _ _) tree) as pctx.
506 set (mapOptionTree ξ' pctx) as passback.
507 set (fun a b => @RLetRec Γ Δ a b passback) as z.
508 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
511 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
512 unfold passback in *; clear passback.
513 unfold pctx in *; clear pctx.
514 eapply UND_to_ND in q'.
517 set (@updating_stripped_tree_is_inert') as zz.
518 unfold update_ξ'' in *.
524 eapply nd_comp; [ idtac | apply q' ].
526 unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
530 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
532 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
533 eapply nd_comp; [ apply nd_llecnac | idtac ].
536 set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
537 unfold update_ξ'' in *.
543 Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
544 mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
545 (stripOutVars (vec2list (scbwv_exprvars x)) t)
547 mapOptionTree (weakLT' ○ ξ)
548 (stripOutVars (vec2list (scbwv_exprvars x)) t).
553 Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
554 (x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
555 (e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
556 (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) ,
557 mapOptionTree (weakLT' ○ ξ)
558 (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
559 unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
561 mapOptionTree (weakLT' ○ ξ)
562 (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
564 (update_ξ (weakLT' ○ ξ)
570 (app (vec2list (sac_ekinds x)) Γ)
571 ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩)
572 (vec_zip (scbwv_exprvars x)
573 (sac_types x Γ atypes)))))
574 (unleaves (vec2list (scbwv_exprvars x)))
582 Definition expr2proof :
583 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
584 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
586 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
587 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
588 match exp as E in Expr Γ Δ ξ τ with
589 | EVar Γ Δ ξ ev => let case_EVar := tt in _
590 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
591 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
592 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
593 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
594 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
595 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
596 | ELetRec Γ Δ ξ lev t tree branches ebody =>
597 let ξ' := update_ξ'' ξ tree lev in
598 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
599 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
600 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
601 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
602 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
603 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
604 | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
605 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
607 ) _ _ _ _ tree branches)
608 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
609 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
610 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
611 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
612 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
613 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
614 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
615 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
616 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
619 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
621 (sac_Δ scb Γ atypes (weakCK'' Δ))
623 (weakLT' (tbranches@@l)) })
624 : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
625 match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
626 | T_Leaf None => let case_nil := tt in _
627 | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
628 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
630 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
632 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
636 unfold mapOptionTree; simpl.
645 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
646 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
647 eapply nd_comp; [ apply nd_llecnac | idtac ].
652 destruct case_ELam; intros.
653 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
654 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
655 set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
656 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
657 apply UND_to_ND in pfx.
658 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
660 fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
661 rewrite updating_stripped_tree_is_inert in pfx.
662 unfold update_ξ in pfx.
663 destruct (eqd_dec v v).
664 eapply nd_comp; [ idtac | apply pfx ].
672 destruct case_ELet; intros; simpl in *.
673 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
674 eapply nd_comp; [ apply nd_llecnac | idtac ].
675 apply nd_prod; [ idtac | apply pf_let].
677 eapply nd_comp; [ apply pf_body | idtac ].
679 fold (@mapOptionTree VV).
680 fold (mapOptionTree ξ).
681 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
682 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
683 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
685 rewrite updating_stripped_tree_is_inert in n.
686 unfold update_ξ in n.
687 destruct (eqd_dec lev lev).
690 apply UND_to_ND in n.
692 assert False. apply n0; auto. inversion H.
695 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
698 destruct case_EBrak; intros.
699 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
703 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
708 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
712 destruct case_ETyApp; simpl in *; intros.
713 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
717 destruct case_ECoLam; simpl in *; intros.
718 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
721 destruct case_ECoApp; simpl in *; intros.
722 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
726 destruct case_ETyLam; intros.
727 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
728 unfold mapOptionTree in e'.
729 rewrite mapOptionTree_compose in e'.
730 unfold mapOptionTree.
736 repeat rewrite <- mapOptionTree_compose in *.
737 set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
738 (unleaves (vec2list (scbwv_exprvars (projT1 x))))
739 (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
744 unfold weakCK'' in q.
746 rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q.
760 destruct case_branch.
761 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
768 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
769 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
770 rewrite <- mapOptionTree_compose.
774 destruct case_ELetRec; simpl in *; intros.
775 set (@letRecSubproofsToND') as q.
784 End HaskStrongToProof.
788 (* Figure 7, production "decl"; actually not used in this formalization *)
790 | DeclDataType : forall tc:TyCon, (forall dc:DataCon tc, DataConDecl dc) -> Decl
791 | DeclTypeFunction : forall n t l, TypeFunctionDecl n t l -> Decl
792 | DeclAxiom : forall n ccon vk TV, @AxiomDecl n ccon vk TV -> Decl.
794 (* Figure 1, production "pgm" *)
796 mkPgm : forall (τ:HaskType Γ), list Decl -> ND Rule [] [Γ>Δ> [] |- [τ @@nil]] -> Pgm Γ Δ.