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 Definition pivotContext {T} a b c : @Arrange T ((a,,b),,c) ((a,,c),,b) :=
20 RComp (RComp (RCossa _ _ _) (RLeft a (RExch c b))) (RAssoc _ _ _).
22 Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
23 eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
24 eapply RComp; [ idtac | apply RCossa ].
25 eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
29 Context {VV:Type}{eqd_vv:EqDecidable VV}.
31 (* maintenance of Xi *)
32 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
35 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
38 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
40 | T_Leaf None => T_Leaf None
41 | T_Leaf (Some x) => T_Leaf (f x)
42 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
45 (* later: use mapOptionTreeAndFlatten *)
46 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
47 mapOptionTree' (dropVar lv).
49 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
61 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
65 rewrite <- app_comm_cons.
72 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
81 set (IHl1 _ H3) as H3'.
84 apply distinct_cons; auto.
90 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
91 mapOptionTree' g (mapOptionTree' f t)
93 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
97 destruct (f t); reflexivity.
104 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
106 rewrite mapOptionTree'_compose.
114 destruct (eqd_dec v a0).
115 destruct (eqd_dec v a); reflexivity.
124 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
130 rewrite mapOptionTree'_compose.
132 destruct a; try reflexivity.
134 destruct (dropVar y v); reflexivity.
141 rewrite <- strip_lemma.
142 rewrite app_comm_cons.
148 Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
151 destruct a0; try reflexivity.
155 destruct (eqd_dec v a).
162 rewrite <- IHy1 at 2.
163 rewrite <- IHy2 at 2.
167 eapply In_both' in H0.
171 eapply In_both in H0.
175 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
180 destruct (eqd_dec v a).
182 assert False. apply H.
192 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
199 rewrite <- app_comm_cons.
202 rewrite <- app_comm_cons in H.
210 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
213 apply distinct_app in H; auto.
215 rewrite <- app_comm_cons.
217 rewrite <- ass_app in H.
218 rewrite <- app_comm_cons in H.
228 rewrite <- ass_app in H.
229 rewrite <- app_comm_cons in H.
235 Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
240 induction y; try destruct a; auto.
246 apply distinct_app in H; destruct H; auto.
247 apply distinct_app in H; destruct H; auto.
248 rewrite <- app_comm_cons in H.
253 apply strip_distinct.
261 Lemma updating_stripped_tree_is_inert'
263 (ξ:VV -> LeveledHaskType Γ ★)
265 mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
266 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
275 set (eqd_dec v v0) as q.
278 set (dropVar (map (@fst _ _) lv) v) as b in *.
285 unfold stripOutVars in *.
286 rewrite <- IHtree2_1.
287 rewrite <- IHtree2_2.
291 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
292 distinct (map (@fst _ _) (leaves varstypes)) ->
293 mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
294 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
302 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
303 match exp as E in Expr Γ Δ ξ τ with
304 | EGlobal Γ Δ ξ _ _ => []
305 | EVar Γ Δ ξ ev => [ev]
306 | ELit Γ Δ ξ lit lev => []
307 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
308 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
309 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
310 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
311 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
312 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
313 | ENote Γ Δ ξ t n e => expr2antecedent e
314 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
315 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
316 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
317 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
318 | ELetRec Γ Δ ξ l τ vars branches body =>
319 let branch_context := eLetRecContext branches
320 in let all_contexts := (expr2antecedent body),,branch_context
321 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
322 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
323 ((fix varsfromalts (alts:
324 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
326 (sac_Δ sac Γ atypes (weakCK'' Δ))
328 (weakLT' (tbranches@@l)) } }
332 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
333 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
334 end) alts),,(expr2antecedent e')
336 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
338 | ELR_nil Γ Δ ξ lev => []
339 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
340 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
343 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
344 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
346 (sac_Δ sac Γ atypes (weakCK'' Δ))
348 (weakLT' (tbranches@@l)) } })
349 : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
353 {| pcb_freevars := mapOptionTree ξ
354 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
355 (expr2antecedent (projT2 s)))
360 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
362 | ELR_nil Γ Δ ξ lev => []
363 | ELR_leaf Γ Δ ξ lev v t e => [t]
364 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
367 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
369 | ELR_nil Γ Δ ξ lev => []
370 | ELR_leaf Γ Δ ξ lev v _ _ e => [v]
371 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
374 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
376 | ELR_nil Γ Δ ξ lev => []
377 | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)]
378 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
382 Lemma stripping_nothing_is_inert
384 (ξ:VV -> LeveledHaskType Γ ★)
386 stripOutVars nil tree = tree.
388 simpl; destruct a; reflexivity.
392 fold (stripOutVars nil).
393 rewrite <- IHtree1 at 2.
394 rewrite <- IHtree2 at 2.
398 Definition arrangeContext
399 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
400 v (* variable to be pivoted, if found *)
401 ctx (* initial context *)
402 (ξ:VV -> LeveledHaskType Γ ★)
405 (* a proof concluding in a context where that variable does not appear *)
407 (mapOptionTree ξ ctx )
408 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
410 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
412 (mapOptionTree ξ ctx )
413 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
417 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
421 unfold stripOutVars in *; simpl.
423 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
425 destruct (eqd_dec v' v); subst.
427 (* where the leaf is v *)
432 (* where the leaf is NOT v *)
438 apply inl; simpl in *.
446 | inr rpf => let case_Both := tt in _
447 | inl rpf => let case_Left := tt in _
451 | inr rpf => let case_Right := tt in _
452 | inl rpf => let case_Neither := tt in _
454 end); clear IHctx1; clear IHctx2.
456 destruct case_Neither.
458 eapply RComp; [idtac | apply RuCanR ].
460 (* order will not matter because these are central as morphisms *)
461 (RRight _ (RComp lpf (RCanR _)))
462 (RLeft _ (RComp rpf (RCanR _)))).
467 fold (stripOutVars (v::nil)).
468 set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q.
474 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
475 eapply RComp; [ idtac | apply RAssoc ].
481 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
482 fold (stripOutVars (v::nil)).
483 eapply RComp; [ idtac | eapply pivotContext ].
484 set (RComp rpf (RCanR _ )) as rpf'.
485 set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
487 eapply RComp; [ idtac | apply qq ].
489 apply (RRight (mapOptionTree ξ ctx2)).
494 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
495 fold (stripOutVars (v::nil)).
496 eapply RComp; [ idtac | eapply copyAndPivotContext ].
497 (* order will not matter because these are central as morphisms *)
498 exact (RComp (RRight _ lpf) (RLeft _ rpf)).
502 (* same as before, but use RWeak if necessary *)
503 Definition arrangeContextAndWeaken
504 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
505 v (* variable to be pivoted, if found *)
506 ctx (* initial context *)
507 (ξ:VV -> LeveledHaskType Γ ★) :
509 (mapOptionTree ξ ctx )
510 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
511 set (arrangeContext Γ Δ v ctx ξ) as q.
513 eapply RComp; [ apply a | idtac ].
514 refine (RLeft _ (RWeak _)).
517 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
521 Definition arrangeContextAndWeaken''
522 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
523 v (* variable to be pivoted, if found *)
524 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
525 distinct (leaves v) ->
527 ((mapOptionTree ξ ctx) )
528 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
532 unfold mapOptionTree in *.
534 fold (mapOptionTree ξ) in *.
536 apply arrangeContextAndWeaken.
539 unfold mapOptionTree; simpl in *.
541 rewrite (@stripping_nothing_is_inert Γ); auto.
544 unfold mapOptionTree in *.
546 fold (mapOptionTree ξ) in *.
547 set (mapOptionTree ξ) as X in *.
549 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
550 unfold stripOutVars in IHv2'.
552 fold (stripOutVars (leaves v2)) in IHv2'.
553 fold (stripOutVars (leaves v1)) in IHv2'.
555 unfold mapOptionTree in IHv2'.
557 fold (mapOptionTree ξ) in IHv2'.
559 set (distinct_app _ _ _ H) as H'.
560 destruct H' as [H1 H2].
561 set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
564 clear qq IHv2' IHv2 IHv1.
565 rewrite strip_twice_lemma.
567 rewrite (strip_distinct' v1 (leaves v2)).
573 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
574 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
575 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
576 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
582 (* IDEA: use multi-conclusion proofs instead *)
583 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
584 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
585 | lrsp_leaf : forall v t e ,
586 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
587 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
588 | lrsp_cons : forall t1 t2 b1 b2,
589 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
590 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
591 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
593 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
594 LetRecSubproofs Γ Δ ξ lev tree branches ->
595 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
596 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
597 intro X; induction X; intros; simpl in *.
604 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
605 eapply nd_comp; [ apply nd_llecnac | idtac ].
609 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
610 forall branches body,
611 distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
612 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
613 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
614 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
616 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
623 rewrite mapleaves in disti.
624 set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
625 rewrite <- mapOptionTree_compose in ξlemma.
627 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
628 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
629 set (mapOptionTree (@fst _ _) tree) as pctx.
630 set (mapOptionTree ξ' pctx) as passback.
631 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
632 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
635 set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
636 unfold passback in *; clear passback.
637 unfold pctx in *; clear pctx.
638 rewrite <- mapleaves in disti.
639 set (q' disti) as q''.
642 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
643 rewrite <- mapleaves in zz.
649 rewrite <- mapOptionTree_compose in q''.
651 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
656 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
657 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
658 eapply nd_comp; [ apply nd_llecnac | idtac ].
664 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
665 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
667 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
668 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
671 unfold scbwv_varstypes.
672 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
673 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
675 rewrite <- mapleaves' in q.
676 rewrite <- mapleaves' in q.
677 rewrite <- mapleaves' in q.
678 rewrite <- mapleaves' in q.
679 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
680 rewrite vec2list_map_list2vec in q'.
681 rewrite fst_zip in q'.
682 rewrite vec2list_map_list2vec in q'.
683 rewrite vec2list_map_list2vec in q'.
684 rewrite snd_zip in q'.
685 rewrite leaves_unleaves in q'.
686 rewrite vec2list_map_list2vec in q'.
687 rewrite vec2list_map_list2vec in q'.
690 apply scbwv_exprvars_distinct.
694 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
696 ??{sac : StrongAltCon &
697 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
698 Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
699 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
701 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
702 (mapOptionTree mkProofCaseBranch alts'))
704 mapOptionTree ξ (expr2antecedent e) =
706 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
709 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
714 unfold mkProofCaseBranch.
725 Definition expr2proof :
726 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
727 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
729 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
730 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
731 match exp as E in Expr Γ Δ ξ τ with
732 | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
733 | EVar Γ Δ ξ ev => let case_EVar := tt in _
734 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
735 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
736 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
737 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
738 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
739 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
740 | ELetRec Γ Δ ξ lev t tree branches ebody =>
741 let ξ' := update_ξ ξ lev (leaves tree) in
742 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
743 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
744 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
745 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
746 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
747 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
748 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
749 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
751 ) _ _ _ _ tree branches)
752 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
753 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
754 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
755 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
756 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
757 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
758 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
759 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
760 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
763 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
765 (sac_Δ sac Γ atypes (weakCK'' Δ))
767 (weakLT' (tbranches@@l)) } })
768 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
769 match alts as ALTS return ND Rule []
770 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
771 | T_Leaf None => let case_nil := tt in _
772 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
774 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
775 existT sac (existT scbx ex) =>
776 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
779 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
781 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
783 destruct case_EGlobal.
786 destruct t as [t lev].
787 apply (RGlobal _ _ _ _ wev).
791 unfold mapOptionTree; simpl.
800 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
801 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
802 eapply nd_comp; [ apply nd_llecnac | idtac ].
807 destruct case_ELam; intros.
808 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
809 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
810 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
811 set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
812 eapply RArrange in pfx.
813 unfold mapOptionTree in pfx; simpl in pfx.
815 rewrite updating_stripped_tree_is_inert in pfx.
816 unfold update_ξ in pfx.
817 destruct (eqd_dec v v).
818 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
826 destruct case_ELet; intros; simpl in *.
827 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
828 eapply nd_comp; [ apply nd_llecnac | idtac ].
829 apply nd_prod; [ idtac | apply pf_let].
831 eapply nd_comp; [ apply pf_body | idtac ].
833 fold (@mapOptionTree VV).
834 fold (mapOptionTree ξ).
835 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
836 set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
837 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
839 rewrite updating_stripped_tree_is_inert in n.
840 unfold update_ξ in n.
841 destruct (eqd_dec lev lev).
844 eapply RArrange in n.
846 assert False. apply n0; auto. inversion H.
849 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
852 destruct case_EBrak; intros.
853 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
857 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
863 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
867 destruct case_ETyApp; simpl in *; intros.
868 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
872 destruct case_ECoLam; simpl in *; intros.
873 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
876 destruct case_ECoApp; simpl in *; intros.
877 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
881 destruct case_ETyLam; intros.
882 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
883 unfold mapOptionTree in e'.
884 rewrite mapOptionTree_compose in e'.
885 unfold mapOptionTree.
889 clear o x alts alts' e.
890 eapply nd_comp; [ apply e' | idtac ].
897 rewrite <- mapOptionTree_compose.
899 rewrite <- mapleaves'.
900 rewrite vec2list_map_list2vec.
902 rewrite <- (scbwv_coherent scbx l ξ).
903 rewrite <- vec2list_map_list2vec.
905 set (@arrangeContextAndWeaken'') as q.
907 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
908 unfold scbwv_varstypes in z.
909 rewrite vec2list_map_list2vec in z.
910 rewrite fst_zip in z.
913 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
914 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
916 apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
917 rewrite leaves_unleaves.
918 apply (scbwv_exprvars_distinct scbx).
919 rewrite leaves_unleaves.
925 destruct case_branch.
926 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
932 set (@RCase Γ Δ l tc) as q.
933 rewrite <- case_lemma.
934 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
935 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
936 rewrite <- mapOptionTree_compose.
940 destruct case_ELetRec; intros.
945 apply letRecSubproofsToND'.
952 End HaskStrongToProof.