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 Section HaskStrongToProof.
19 (* Whereas RLeft/RRight perform left and right context expansion on a single uniform rule, these functions perform
20 * expansion on an entire uniform proof *)
21 Definition ext_left {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
22 := @nd_map' _ _ _ _ (ext_tree_left ctx) (fun h c r => nd_rule (@RLeft Γ Δ h c ctx r)).
23 Definition ext_right {Γ}{Δ}(ctx:Tree ??(LeveledHaskType Γ ★))
24 := @nd_map' _ _ _ _ (ext_tree_right ctx) (fun h c r => nd_rule (@RRight Γ Δ h c ctx r)).
26 Definition pivotContext {Γ}{Δ} a b c τ :
28 [ Γ >> Δ > (a,,b),,c |- τ]
29 [ Γ >> Δ > (a,,c),,b |- τ].
30 set (ext_left a _ _ (nd_rule (@RExch Γ Δ τ c b))) as q.
32 eapply nd_comp ; [ eapply nd_rule; apply RCossa | idtac ].
33 eapply nd_comp ; [ idtac | eapply nd_rule; apply RAssoc ].
37 Definition copyAndPivotContext {Γ}{Δ} a b c τ :
39 [ Γ >> Δ > (a,,b),,(c,,b) |- τ]
40 [ Γ >> Δ > (a,,c),,b |- τ].
41 set (ext_left (a,,c) _ _ (nd_rule (@RCont Γ Δ τ b))) as q.
43 eapply nd_comp; [ idtac | apply q ].
45 eapply nd_comp ; [ idtac | eapply nd_rule; apply RCossa ].
46 set (ext_right b _ _ (@pivotContext _ Δ a b c τ)) as q.
48 eapply nd_comp ; [ idtac | apply q ].
56 Context {VV:Type}{eqd_vv:EqDecidable VV}.
58 (* maintenance of Xi *)
59 Definition dropVar (lv:list VV)(v:VV) : ??VV :=
61 (fun a b:bool => if a then true else if b then true else false)
62 (map (fun lvv => if eqd_dec lvv v then true else false) lv)
66 (* later: use mapOptionTreeAndFlatten *)
67 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
68 mapTree (fun x => match x with None => None | Some vt => dropVar lv vt end).
70 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
71 match exp as E in Expr Γ Δ ξ τ with
72 | EGlobal Γ Δ ξ _ _ => []
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 | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
590 | EVar Γ Δ ξ ev => let case_EVar := tt in _
591 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
592 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
593 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
594 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
595 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
596 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
597 | ELetRec Γ Δ ξ lev t tree branches ebody =>
598 let ξ' := update_ξ'' ξ tree lev in
599 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
600 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
601 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
602 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
603 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
604 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
605 | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
606 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
608 ) _ _ _ _ tree branches)
609 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
610 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
611 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
612 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
613 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
614 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
615 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
616 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
617 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
620 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
622 (sac_Δ scb Γ atypes (weakCK'' Δ))
624 (weakLT' (tbranches@@l)) })
625 : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
626 match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
627 | T_Leaf None => let case_nil := tt in _
628 | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
629 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
631 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
633 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
635 destruct case_EGlobal.
638 destruct t as [t lev].
639 apply (RGlobal _ _ _ _ wev).
643 unfold mapOptionTree; simpl.
652 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
653 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
654 eapply nd_comp; [ apply nd_llecnac | idtac ].
659 destruct case_ELam; intros.
660 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
661 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
662 set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
663 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
664 apply UND_to_ND in pfx.
665 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
667 fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
668 rewrite updating_stripped_tree_is_inert in pfx.
669 unfold update_ξ in pfx.
670 destruct (eqd_dec v v).
671 eapply nd_comp; [ idtac | apply pfx ].
679 destruct case_ELet; intros; simpl in *.
680 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
681 eapply nd_comp; [ apply nd_llecnac | idtac ].
682 apply nd_prod; [ idtac | apply pf_let].
684 eapply nd_comp; [ apply pf_body | idtac ].
686 fold (@mapOptionTree VV).
687 fold (mapOptionTree ξ).
688 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
689 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
690 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
692 rewrite updating_stripped_tree_is_inert in n.
693 unfold update_ξ in n.
694 destruct (eqd_dec lev lev).
697 apply UND_to_ND in n.
699 assert False. apply n0; auto. inversion H.
702 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
705 destruct case_EBrak; intros.
706 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
710 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
716 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
720 destruct case_ETyApp; simpl in *; intros.
721 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
725 destruct case_ECoLam; simpl in *; intros.
726 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
729 destruct case_ECoApp; simpl in *; intros.
730 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
734 destruct case_ETyLam; intros.
735 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
736 unfold mapOptionTree in e'.
737 rewrite mapOptionTree_compose in e'.
738 unfold mapOptionTree.
744 repeat rewrite <- mapOptionTree_compose in *.
745 set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
746 (unleaves (vec2list (scbwv_exprvars (projT1 x))))
747 (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
752 unfold weakCK'' in q.
754 rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q.
768 destruct case_branch.
769 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
776 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
777 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
778 rewrite <- mapOptionTree_compose.
782 destruct case_ELetRec; simpl in *; intros.
783 set (@letRecSubproofsToND') as q.
792 End HaskStrongToProof.