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 Lemma stripping_nothing_is_inert
369 (ξ:VV -> LeveledHaskType Γ ★)
371 stripOutVars nil tree = tree.
373 simpl; destruct a; reflexivity.
377 fold (stripOutVars nil).
378 rewrite <- IHtree1 at 2.
379 rewrite <- IHtree2 at 2.
383 Definition arrangeContext
384 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
385 v (* variable to be pivoted, if found *)
386 ctx (* initial context *)
387 (ξ:VV -> LeveledHaskType Γ ★)
390 (* a proof concluding in a context where that variable does not appear *)
392 (mapOptionTree ξ ctx )
393 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
395 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
397 (mapOptionTree ξ ctx )
398 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
402 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
406 unfold stripOutVars in *; simpl.
408 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
410 destruct (eqd_dec v' v); subst.
412 (* where the leaf is v *)
417 (* where the leaf is NOT v *)
423 apply inl; simpl in *.
431 | inr rpf => let case_Both := tt in _
432 | inl rpf => let case_Left := tt in _
436 | inr rpf => let case_Right := tt in _
437 | inl rpf => let case_Neither := tt in _
439 end); clear IHctx1; clear IHctx2.
441 destruct case_Neither.
443 eapply RComp; [idtac | apply RuCanR ].
445 (* order will not matter because these are central as morphisms *)
446 (RRight _ (RComp lpf (RCanR _)))
447 (RLeft _ (RComp rpf (RCanR _)))).
452 fold (stripOutVars (v::nil)).
453 set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q.
459 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
460 eapply RComp; [ idtac | apply RAssoc ].
466 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
467 fold (stripOutVars (v::nil)).
468 eapply RComp; [ idtac | eapply pivotContext ].
469 set (RComp rpf (RCanR _ )) as rpf'.
470 set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
472 eapply RComp; [ idtac | apply qq ].
474 apply (RRight (mapOptionTree ξ ctx2)).
479 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
480 fold (stripOutVars (v::nil)).
481 eapply RComp; [ idtac | eapply copyAndPivotContext ].
482 (* order will not matter because these are central as morphisms *)
483 exact (RComp (RRight _ lpf) (RLeft _ rpf)).
487 (* same as before, but use RWeak if necessary *)
488 Definition arrangeContextAndWeaken
489 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
490 v (* variable to be pivoted, if found *)
491 ctx (* initial context *)
492 (ξ:VV -> LeveledHaskType Γ ★) :
494 (mapOptionTree ξ ctx )
495 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
496 set (arrangeContext Γ Δ v ctx ξ) as q.
498 eapply RComp; [ apply a | idtac ].
499 refine (RLeft _ (RWeak _)).
502 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
506 Definition arrangeContextAndWeaken''
507 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
508 v (* variable to be pivoted, if found *)
509 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
510 distinct (leaves v) ->
512 ((mapOptionTree ξ ctx) )
513 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
517 unfold mapOptionTree in *.
519 fold (mapOptionTree ξ) in *.
521 apply arrangeContextAndWeaken.
524 unfold mapOptionTree; simpl in *.
526 rewrite (@stripping_nothing_is_inert Γ); auto.
529 unfold mapOptionTree in *.
531 fold (mapOptionTree ξ) in *.
532 set (mapOptionTree ξ) as X in *.
534 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
535 unfold stripOutVars in IHv2'.
537 fold (stripOutVars (leaves v2)) in IHv2'.
538 fold (stripOutVars (leaves v1)) in IHv2'.
540 unfold mapOptionTree in IHv2'.
542 fold (mapOptionTree ξ) in IHv2'.
544 set (distinct_app _ _ _ H) as H'.
545 destruct H' as [H1 H2].
546 set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
549 clear qq IHv2' IHv2 IHv1.
550 rewrite strip_twice_lemma.
552 rewrite (strip_distinct' v1 (leaves v2)).
558 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
559 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
560 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
561 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
567 (* TODO: use multi-conclusion proofs instead *)
568 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
569 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
570 | lrsp_leaf : forall v t e ,
571 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
572 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
573 | lrsp_cons : forall t1 t2 b1 b2,
574 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
575 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
576 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
578 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
579 LetRecSubproofs Γ Δ ξ lev tree branches ->
580 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
581 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
582 intro X; induction X; intros; simpl in *.
589 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
590 eapply nd_comp; [ apply nd_llecnac | idtac ].
594 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
595 forall branches body,
596 distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
597 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
598 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
599 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
601 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
608 rewrite mapleaves in disti.
609 set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
610 rewrite <- mapOptionTree_compose in ξlemma.
612 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
613 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
614 set (mapOptionTree (@fst _ _) tree) as pctx.
615 set (mapOptionTree ξ' pctx) as passback.
616 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
617 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
620 set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
621 unfold passback in *; clear passback.
622 unfold pctx in *; clear pctx.
623 rewrite <- mapleaves in disti.
624 set (q' disti) as q''.
627 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
628 rewrite <- mapleaves in zz.
634 rewrite <- mapOptionTree_compose in q''.
636 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
641 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
642 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
643 eapply nd_comp; [ apply nd_llecnac | idtac ].
649 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
650 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
652 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
653 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
656 unfold scbwv_varstypes.
657 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
658 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
660 rewrite <- mapleaves' in q.
661 rewrite <- mapleaves' in q.
662 rewrite <- mapleaves' in q.
663 rewrite <- mapleaves' in q.
664 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
665 rewrite vec2list_map_list2vec in q'.
666 rewrite fst_zip in q'.
667 rewrite vec2list_map_list2vec in q'.
668 rewrite vec2list_map_list2vec in q'.
669 rewrite snd_zip in q'.
670 rewrite leaves_unleaves in q'.
671 rewrite vec2list_map_list2vec in q'.
672 rewrite vec2list_map_list2vec in q'.
675 apply scbwv_exprvars_distinct.
679 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
681 ??{sac : StrongAltCon &
682 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
683 Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
684 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
686 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
687 (mapOptionTree mkProofCaseBranch alts'))
689 mapOptionTree ξ (expr2antecedent e) =
691 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
694 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
699 unfold mkProofCaseBranch.
710 Definition expr2proof :
711 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
712 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
714 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
715 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
716 match exp as E in Expr Γ Δ ξ τ with
717 | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
718 | EVar Γ Δ ξ ev => let case_EVar := tt in _
719 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
720 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
721 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
722 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
723 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
724 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
725 | ELetRec Γ Δ ξ lev t tree branches ebody =>
726 let ξ' := update_ξ ξ lev (leaves tree) in
727 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
728 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
729 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
730 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
731 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
732 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
733 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
734 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
736 ) _ _ _ _ tree branches)
737 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
738 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
739 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
740 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
741 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
742 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
743 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
744 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
745 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
748 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
750 (sac_Δ sac Γ atypes (weakCK'' Δ))
752 (weakLT' (tbranches@@l)) } })
753 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
754 match alts as ALTS return ND Rule []
755 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
756 | T_Leaf None => let case_nil := tt in _
757 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
759 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
760 existT sac (existT scbx ex) =>
761 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
764 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
766 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
768 destruct case_EGlobal.
771 destruct t as [t lev].
772 apply (RGlobal _ _ _ _ wev).
776 unfold mapOptionTree; simpl.
785 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
786 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
787 eapply nd_comp; [ apply nd_llecnac | idtac ].
792 destruct case_ELam; intros.
793 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
794 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
795 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
796 set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
797 eapply RArrange in pfx.
798 unfold mapOptionTree in pfx; simpl in pfx.
800 rewrite updating_stripped_tree_is_inert in pfx.
801 unfold update_ξ in pfx.
802 destruct (eqd_dec v v).
803 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
811 destruct case_ELet; intros; simpl in *.
812 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
813 eapply nd_comp; [ apply nd_llecnac | idtac ].
817 eapply nd_comp; [ apply pf_body | idtac ].
819 fold (@mapOptionTree VV).
820 fold (mapOptionTree ξ).
821 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
822 set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
823 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
825 rewrite updating_stripped_tree_is_inert in n.
826 unfold update_ξ in n.
827 destruct (eqd_dec lev lev).
830 eapply RArrange in n.
832 assert False. apply n0; auto. inversion H.
835 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
838 destruct case_EBrak; intros.
839 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
843 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
849 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
853 destruct case_ETyApp; simpl in *; intros.
854 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
858 destruct case_ECoLam; simpl in *; intros.
859 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
862 destruct case_ECoApp; simpl in *; intros.
863 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
867 destruct case_ETyLam; intros.
868 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
869 unfold mapOptionTree in e'.
870 rewrite mapOptionTree_compose in e'.
871 unfold mapOptionTree.
875 clear o x alts alts' e.
876 eapply nd_comp; [ apply e' | idtac ].
883 rewrite <- mapOptionTree_compose.
885 rewrite <- mapleaves'.
886 rewrite vec2list_map_list2vec.
888 rewrite <- (scbwv_coherent scbx l ξ).
889 rewrite <- vec2list_map_list2vec.
891 set (@arrangeContextAndWeaken'') as q.
893 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
894 unfold scbwv_varstypes in z.
895 rewrite vec2list_map_list2vec in z.
896 rewrite fst_zip in z.
899 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
900 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
902 apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
903 rewrite leaves_unleaves.
904 apply (scbwv_exprvars_distinct scbx).
905 rewrite leaves_unleaves.
911 destruct case_branch.
912 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
918 set (@RCase Γ Δ l tc) as q.
919 rewrite <- case_lemma.
920 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
921 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
922 rewrite <- mapOptionTree_compose.
926 destruct case_ELetRec; intros.
931 apply letRecSubproofsToND'.
938 End HaskStrongToProof.