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 | EVar Γ Δ ξ ev => [ev]
73 | ELit Γ Δ ξ lit lev => []
74 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
75 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
76 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
77 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
78 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
79 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
80 | ENote Γ Δ ξ t n e => expr2antecedent e
81 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
82 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
83 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
84 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
85 | ELetRec Γ Δ ξ l τ vars branches body =>
86 let branch_context := eLetRecContext branches
87 in let all_contexts := (expr2antecedent body),,branch_context
88 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
89 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
90 ((fix varsfromalts (alts:
91 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
93 (sac_Δ scb Γ atypes (weakCK'' Δ))
95 (weakLT' (tbranches@@l)) }
99 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 h))) (expr2antecedent (projT2 h))
100 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
101 end) alts),,(expr2antecedent e')
103 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
105 | ELR_nil Γ Δ ξ lev => []
106 | ELR_leaf Γ Δ ξ lev v e => expr2antecedent e
107 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
110 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
111 (alt: { scb : StrongCaseBranchWithVVs _ _ tc atypes
113 (sac_Δ scb Γ atypes (weakCK'' Δ))
115 (weakLT' (tbranches@@l)) })
116 : ProofCaseBranch tc Γ Δ l tbranches atypes.
118 {| pcb_scb := projT1 alt
119 ; pcb_freevars := mapOptionTree ξ (stripOutVars (vec2list (scbwv_exprvars (projT1 alt))) (expr2antecedent (projT2 alt)))
123 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(LeveledHaskType Γ ★) :=
125 | ELR_nil Γ Δ ξ lev => []
126 | ELR_leaf Γ Δ ξ lev v e => [ξ v]
127 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
130 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
132 | ELR_nil Γ Δ ξ lev => []
133 | ELR_leaf Γ Δ ξ lev v e => [v]
134 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
137 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * LeveledHaskType Γ ★):=
139 | ELR_nil Γ Δ ξ lev => []
140 | ELR_leaf Γ Δ ξ lev v e => [(v, ξ v)]
141 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
145 Lemma stripping_nothing_is_inert
147 (ξ:VV -> LeveledHaskType Γ ★)
149 stripOutVars nil tree = tree.
151 simpl; destruct a; reflexivity.
155 fold (stripOutVars nil).
163 Definition arrangeContext
164 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
165 v (* variable to be pivoted, if found *)
166 ctx (* initial context *)
167 τ (* type of succedent *)
168 (ξ:VV -> LeveledHaskType Γ ★)
171 (* a proof concluding in a context where that variable does not appear *)
173 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
174 [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ])
176 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
178 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
179 [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
181 induction ctx; simpl in *.
183 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end); simpl in *.
187 unfold stripOutVars in *; simpl.
189 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
190 destruct (eqd_dec v v'); simpl in *.
192 (* where the leaf is v *)
198 (* where the leaf is NOT v *)
205 apply inl; simpl in *.
214 | inr rpf => let case_Both := tt in _
215 | inl rpf => let case_Left := tt in _
219 | inr rpf => let case_Right := tt in _
220 | inl rpf => let case_Neither := tt in _
222 end); clear IHctx1; clear IHctx2.
224 destruct case_Neither.
226 eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
228 (* order will not matter because these are central as morphisms *)
229 (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
230 (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
235 fold (stripOutVars (v::nil)).
236 set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
242 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
243 eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
244 set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
245 [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq.
252 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
253 fold (stripOutVars (v::nil)).
254 eapply nd_comp; [ idtac | eapply pivotContext ].
255 set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
256 set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
258 eapply nd_comp; [ idtac | apply qq ].
260 set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
267 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
268 fold (stripOutVars (v::nil)).
269 eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
271 (* order will not matter because these are central as morphisms *)
272 (ext_right _ _ _ lpf)
273 (ext_left _ _ _ rpf)).
277 (* same as before, but use RWeak if necessary *)
278 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
280 [Γ >> Δ>mapOptionTree ξ ctx |- τ]
281 [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ].
282 set (arrangeContext Γ Δ v ctx τ ξ) as q.
284 eapply nd_comp; [ apply n | idtac ].
286 refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
289 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
291 [Γ >> Δ>(mapOptionTree ξ ctx) |- z]
292 [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
296 unfold mapOptionTree in *.
298 fold (mapOptionTree ξ) in *.
300 apply arrangeContextAndWeaken.
302 unfold mapOptionTree; simpl in *.
304 rewrite (@stripping_nothing_is_inert Γ); auto.
308 unfold mapOptionTree in *.
310 fold (mapOptionTree ξ) in *.
311 set (mapOptionTree ξ) as X in *.
313 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
314 unfold stripOutVars in IHv2'.
316 fold (stripOutVars (leaves v2)) in IHv2'.
317 fold (stripOutVars (leaves v1)) in IHv2'.
319 unfold mapOptionTree in IHv2'.
321 fold (mapOptionTree ξ) in IHv2'.
323 set (nd_comp (IHv1 _ _) IHv2') as qq.
326 clear qq IHv2' IHv2 IHv1.
328 assert ((stripOutVars (leaves v2) (stripOutVars (leaves v1) ctx))=(stripOutVars (app (leaves v1) (leaves v2)) ctx)).
333 (* FIXME: this only works because the variables are all distinct, but I need to prove that *)
334 assert ((stripOutVars (leaves v2) v1) = v1).
343 Definition update_ξ'' {Γ} ξ tree lev :=
345 (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
348 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree lev :
349 mapOptionTree (update_ξ ξ ((v,lev)::nil)) (stripOutVars (v :: nil) tree)
350 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
351 induction tree; simpl in *; try reflexivity; auto.
353 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *; fold (mapOptionTree (update_ξ ξ ((v,lev)::nil))) in *.
354 destruct a; simpl; try reflexivity.
357 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
361 set (eqd_dec v v0) as q.
362 assert (q=eqd_dec v v0).
369 unfold mapOptionTree.
370 unfold mapOptionTree in IHtree1.
371 unfold mapOptionTree in IHtree2.
374 fold (stripOutVars (v::nil)).
382 Lemma updating_stripped_tree_is_inert'
384 (ξ:VV -> LeveledHaskType Γ ★)
386 mapOptionTree (update_ξ'' ξ tree lev) (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2)
387 = mapOptionTree ξ (stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) tree2).
391 Lemma updating_stripped_tree_is_inert''
393 (ξ:VV -> LeveledHaskType Γ ★)
395 mapOptionTree (update_ξ'' ξ (unleaves v) lev) (stripOutVars (map (@fst _ _) v) tree)
396 = mapOptionTree ξ (stripOutVars (map (@fst _ _) v) tree).
401 Lemma updating_stripped_tree_is_inert'''
403 (ξ:VV -> LeveledHaskType Γ)
405 (idx:Tree ??T) (types:ShapedTree (LeveledHaskType Γ) idx)(vars:ShapedTree VV idx) tree
407 mapOptionTree (update_ξ''' ξ types vars) (stripOutVars (leaves (unshape vars)) tree)
408 = mapOptionTree ξ (stripOutVars (leaves (unshape vars)) tree).
413 (* IDEA: use multi-conclusion proofs instead *)
414 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
415 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
416 | lrsp_leaf : forall v e,
417 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [unlev (ξ v) @@ lev]]) ->
418 LetRecSubproofs Γ Δ ξ lev [(v, unlev (ξ v))] (ELR_leaf _ _ _ _ _ e)
419 | lrsp_cons : forall t1 t2 b1 b2,
420 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
421 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
422 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
424 Lemma cheat1 : forall Γ Δ ξ lev tree (branches:ELetRecBindings Γ Δ ξ lev tree),
425 eLetRecTypes branches =
426 mapOptionTree (update_ξ'' ξ tree lev)
427 (mapOptionTree (@fst _ _) tree).
433 unfold mapOptionTree; simpl.
437 Lemma cheat2 : forall Γ Δ ξ l tc tbranches atypes e alts',
438 mapOptionTree ξ (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts'))
441 ((mapOptionTreeAndFlatten
442 (fun h => stripOutVars (vec2list (scbwv_exprvars (projT1 h)))
443 (expr2antecedent (projT2 h))) alts'),,(expr2antecedent e)).
445 ((mapOptionTreeAndFlatten pcb_freevars
446 (mapOptionTree mkProofCaseBranch alts')),,mapOptionTree ξ (expr2antecedent e)).
449 Lemma cheat3 : forall {A}{B}{f:A->B} l, unleaves (map f l) = mapOptionTree f (unleaves l).
452 Lemma cheat4 : forall {A}(t:list A), leaves (unleaves t) = t.
456 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches
457 : LetRecSubproofs Γ Δ ξ lev tree branches ->
460 mapOptionTree ξ (eLetRecContext branches)
462 eLetRecTypes branches
465 induction X; intros; simpl in *.
475 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
476 eapply nd_comp; [ apply nd_llecnac | idtac ].
481 Lemma update_twice_useless : forall Γ (ξ:VV -> LeveledHaskType Γ ★) tree z lev,
482 mapOptionTree (@update_ξ'' Γ ξ tree lev) z = mapOptionTree (update_ξ'' (update_ξ'' ξ tree lev) tree lev) z.
488 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
489 forall branches body,
490 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ'' ξ tree lev) (expr2antecedent body) |- [τ @@ lev]] ->
491 LetRecSubproofs Γ Δ (update_ξ'' ξ tree lev) lev tree branches ->
492 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
494 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
501 (map (fun x : VV * HaskType Γ ★ => ⟨fst x, snd x @@ lev ⟩)
502 (leaves tree)))) as ξ' in *.
503 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
504 set (mapOptionTree (@fst _ _) tree) as pctx.
505 set (mapOptionTree ξ' pctx) as passback.
506 set (fun a b => @RLetRec Γ Δ a b passback) as z.
507 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
510 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
511 unfold passback in *; clear passback.
512 unfold pctx in *; clear pctx.
513 eapply UND_to_ND in q'.
516 set (@updating_stripped_tree_is_inert') as zz.
517 unfold update_ξ'' in *.
523 eapply nd_comp; [ idtac | apply q' ].
525 unfold mapOptionTree. simpl. fold (mapOptionTree (update_ξ'' ξ tree lev)).
529 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
531 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
532 eapply nd_comp; [ apply nd_llecnac | idtac ].
535 set (@update_twice_useless Γ ξ tree ((mapOptionTree (@fst _ _) tree)) lev) as zz.
536 unfold update_ξ'' in *.
542 Lemma updating_stripped_tree_is_inert''' : forall Γ tc ξ l t atypes x,
543 mapOptionTree (scbwv_ξ(Γ:=Γ)(tc:=tc)(atypes:=atypes) x ξ l)
544 (stripOutVars (vec2list (scbwv_exprvars x)) t)
546 mapOptionTree (weakLT' ○ ξ)
547 (stripOutVars (vec2list (scbwv_exprvars x)) t).
552 Lemma updating_stripped_tree_is_inert'''' : forall Γ Δ ξ l tc atypes tbranches
553 (x:StrongCaseBranchWithVVs(Γ:=Γ) VV eqd_vv tc atypes)
554 (e0:Expr (sac_Γ x Γ) (sac_Δ x Γ atypes (weakCK'' Δ))
555 (scbwv_ξ x ξ l) (weakT' tbranches @@ weakL' l)) ,
556 mapOptionTree (weakLT' ○ ξ)
557 (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
558 unleaves (vec2list (sac_types x Γ atypes)) @@@ weakL' l
560 mapOptionTree (weakLT' ○ ξ)
561 (stripOutVars (vec2list (scbwv_exprvars x)) (expr2antecedent e0)),,
563 (update_ξ (weakLT' ○ ξ)
569 (app (vec2list (sac_ekinds x)) Γ)
570 ★ => ⟨fst x0, snd x0 @@ weakL' l ⟩)
571 (vec_zip (scbwv_exprvars x)
572 (sac_types x Γ atypes)))))
573 (unleaves (vec2list (scbwv_exprvars x)))
581 Definition expr2proof :
582 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
583 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
585 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
586 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
587 match exp as E in Expr Γ Δ ξ τ with
588 | EVar Γ Δ ξ ev => let case_EVar := tt in _
589 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
590 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
591 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
592 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
593 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
594 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
595 | ELetRec Γ Δ ξ lev t tree branches ebody =>
596 let ξ' := update_ξ'' ξ tree lev in
597 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
598 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
599 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
600 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
601 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
602 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
603 | ELR_leaf Γ Δ ξ l v e => lrsp_leaf Γ Δ ξ l v e (expr2proof _ _ _ _ e)
604 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
606 ) _ _ _ _ tree branches)
607 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
608 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
609 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
610 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
611 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
612 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
613 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
614 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
615 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
618 Tree ??{ scb : StrongCaseBranchWithVVs _ _ tc atypes
620 (sac_Δ scb Γ atypes (weakCK'' Δ))
622 (weakLT' (tbranches@@l)) })
623 : ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) alts) :=
624 match alts as ALTS return ND Rule [] (mapOptionTree (pcb_judg ○ mkProofCaseBranch) ALTS) with
625 | T_Leaf None => let case_nil := tt in _
626 | T_Leaf (Some x) => (fun ecb' => let case_leaf := tt in _) (expr2proof _ _ _ _ (projT2 x))
627 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
629 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
631 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
635 unfold mapOptionTree; simpl.
644 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
645 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
646 eapply nd_comp; [ apply nd_llecnac | idtac ].
651 destruct case_ELam; intros.
652 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
653 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
654 set (update_ξ ξ ((v,t1@@lev)::nil)) as ξ'.
655 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
656 apply UND_to_ND in pfx.
657 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
659 fold (mapOptionTree (update_ξ ξ ((v,(t1@@lev))::nil))) in pfx.
660 rewrite updating_stripped_tree_is_inert in pfx.
661 unfold update_ξ in pfx.
662 destruct (eqd_dec v v).
663 eapply nd_comp; [ idtac | apply pfx ].
671 destruct case_ELet; intros; simpl in *.
672 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
673 eapply nd_comp; [ apply nd_llecnac | idtac ].
674 apply nd_prod; [ idtac | apply pf_let].
676 eapply nd_comp; [ apply pf_body | idtac ].
678 fold (@mapOptionTree VV).
679 fold (mapOptionTree ξ).
680 set (update_ξ ξ ((lev,(tv @@ v))::nil)) as ξ'.
681 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
682 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
684 rewrite updating_stripped_tree_is_inert in n.
685 unfold update_ξ in n.
686 destruct (eqd_dec lev lev).
689 apply UND_to_ND in n.
691 assert False. apply n0; auto. inversion H.
694 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
697 destruct case_EBrak; intros.
698 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
702 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
707 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
711 destruct case_ETyApp; simpl in *; intros.
712 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
716 destruct case_ECoLam; simpl in *; intros.
717 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
720 destruct case_ECoApp; simpl in *; intros.
721 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
725 destruct case_ETyLam; intros.
726 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
727 unfold mapOptionTree in e'.
728 rewrite mapOptionTree_compose in e'.
729 unfold mapOptionTree.
735 repeat rewrite <- mapOptionTree_compose in *.
736 set (nd_comp ecb' (UND_to_ND _ _ _ _ (@arrangeContextAndWeaken'' _ _ _
737 (unleaves (vec2list (scbwv_exprvars (projT1 x))))
738 (*(unleaves (vec2list (sac_types (projT1 x) Γ atypes)))*)
743 unfold weakCK'' in q.
745 rewrite (updating_stripped_tree_is_inert''' Γ tc ξ l _ atypes (projT1 x)) in q.
759 destruct case_branch.
760 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
767 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
768 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
769 rewrite <- mapOptionTree_compose.
773 destruct case_ELetRec; simpl in *; intros.
774 set (@letRecSubproofsToND') as q.
783 End HaskStrongToProof.