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 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
62 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
65 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
67 | T_Leaf None => T_Leaf None
68 | T_Leaf (Some x) => T_Leaf (f x)
69 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
72 (* later: use mapOptionTreeAndFlatten *)
73 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
74 mapOptionTree' (dropVar lv).
76 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
88 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
92 rewrite <- app_comm_cons.
99 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
102 induction l1; intros.
108 set (IHl1 _ H3) as H3'.
111 apply distinct_cons; auto.
117 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
118 mapOptionTree' g (mapOptionTree' f t)
120 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
124 destruct (f t); reflexivity.
131 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
133 rewrite mapOptionTree'_compose.
141 destruct (eqd_dec v a0).
142 destruct (eqd_dec v a); reflexivity.
151 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app y x) t.
157 rewrite mapOptionTree'_compose.
159 destruct a; try reflexivity.
161 destruct (dropVar y v); reflexivity.
168 rewrite <- strip_lemma.
169 rewrite app_comm_cons.
175 Lemma strip_distinct a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
178 destruct a0; try reflexivity.
182 destruct (eqd_dec v a).
189 rewrite <- IHy1 at 2.
190 rewrite <- IHy2 at 2.
194 eapply In_both' in H0.
198 eapply In_both in H0.
202 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
207 destruct (eqd_dec v a).
209 assert False. apply H.
219 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
226 rewrite <- app_comm_cons.
229 rewrite <- app_comm_cons in H.
237 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
240 apply distinct_app in H; auto.
242 rewrite <- app_comm_cons.
244 rewrite <- ass_app in H.
245 rewrite <- app_comm_cons in H.
255 rewrite <- ass_app in H.
256 rewrite <- app_comm_cons in H.
262 Lemma strip_distinct' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
267 induction y; try destruct a; auto.
273 apply distinct_app in H; destruct H; auto.
274 apply distinct_app in H; destruct H; auto.
275 rewrite <- app_comm_cons in H.
280 apply strip_distinct.
288 Lemma updating_stripped_tree_is_inert'
290 (ξ:VV -> LeveledHaskType Γ ★)
292 mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
293 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
302 set (eqd_dec v v0) as q.
305 set (dropVar (map (@fst _ _) lv) v) as b in *.
312 unfold stripOutVars in *.
313 rewrite <- IHtree2_1.
314 rewrite <- IHtree2_2.
318 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} : forall Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)),
319 distinct (map (@fst _ _) (leaves varstypes)) ->
320 mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
321 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
329 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
330 match exp as E in Expr Γ Δ ξ τ with
331 | EGlobal Γ Δ ξ _ _ => []
332 | EVar Γ Δ ξ ev => [ev]
333 | ELit Γ Δ ξ lit lev => []
334 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
335 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
336 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
337 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
338 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
339 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
340 | ENote Γ Δ ξ t n e => expr2antecedent e
341 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
342 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
343 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
344 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
345 | ELetRec Γ Δ ξ l τ vars branches body =>
346 let branch_context := eLetRecContext branches
347 in let all_contexts := (expr2antecedent body),,branch_context
348 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
349 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
350 ((fix varsfromalts (alts:
351 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
353 (sac_Δ sac Γ atypes (weakCK'' Δ))
355 (weakLT' (tbranches@@l)) } }
359 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
360 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
361 end) alts),,(expr2antecedent e')
363 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
365 | ELR_nil Γ Δ ξ lev => []
366 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
367 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
370 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
371 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
373 (sac_Δ sac Γ atypes (weakCK'' Δ))
375 (weakLT' (tbranches@@l)) } })
376 : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
380 {| pcb_freevars := mapOptionTree ξ
381 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
382 (expr2antecedent (projT2 s)))
387 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
389 | ELR_nil Γ Δ ξ lev => []
390 | ELR_leaf Γ Δ ξ lev v t e => [t]
391 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
394 Fixpoint eLetRecVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??VV :=
396 | ELR_nil Γ Δ ξ lev => []
397 | ELR_leaf Γ Δ ξ lev v _ _ e => [v]
398 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecVars b1),,(eLetRecVars b2)
401 Fixpoint eLetRecTypesVars {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(VV * HaskType Γ ★):=
403 | ELR_nil Γ Δ ξ lev => []
404 | ELR_leaf Γ Δ ξ lev v t _ e => [(v, t)]
405 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypesVars b1),,(eLetRecTypesVars b2)
409 Lemma stripping_nothing_is_inert
411 (ξ:VV -> LeveledHaskType Γ ★)
413 stripOutVars nil tree = tree.
415 simpl; destruct a; reflexivity.
419 fold (stripOutVars nil).
420 rewrite <- IHtree1 at 2.
421 rewrite <- IHtree2 at 2.
425 Definition arrangeContext
426 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
427 v (* variable to be pivoted, if found *)
428 ctx (* initial context *)
429 τ (* type of succedent *)
430 (ξ:VV -> LeveledHaskType Γ ★)
433 (* a proof concluding in a context where that variable does not appear *)
435 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
436 [Γ >> Δ > mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] |- τ])
438 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
440 [Γ >> Δ > mapOptionTree ξ ctx |- τ]
441 [Γ >> Δ > mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ]).
445 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
449 unfold stripOutVars in *; simpl.
451 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
453 destruct (eqd_dec v' v); subst.
455 (* where the leaf is v *)
461 (* where the leaf is NOT v *)
468 apply inl; simpl in *.
477 | inr rpf => let case_Both := tt in _
478 | inl rpf => let case_Left := tt in _
482 | inr rpf => let case_Right := tt in _
483 | inl rpf => let case_Neither := tt in _
485 end); clear IHctx1; clear IHctx2.
487 destruct case_Neither.
489 eapply nd_comp; [idtac | eapply nd_rule; apply RuCanR ].
491 (* order will not matter because these are central as morphisms *)
492 (ext_right _ _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _))))
493 (ext_left _ _ _ (nd_comp rpf (nd_rule (@RCanR _ _ _ _))))).
498 fold (stripOutVars (v::nil)).
499 set (ext_right (mapOptionTree ξ ctx2) _ _ (nd_comp lpf (nd_rule (@RCanR _ _ _ _)))) as q.
505 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
506 eapply nd_comp; [ idtac | eapply nd_rule; apply RAssoc ].
507 set (ext_left (mapOptionTree ξ (stripOutVars (v :: nil) ctx1)) [Γ >> Δ>mapOptionTree ξ ctx2 |- τ]
508 [Γ >> Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx2),,[ξ v]) |- τ]) as qq.
515 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
516 fold (stripOutVars (v::nil)).
517 eapply nd_comp; [ idtac | eapply pivotContext ].
518 set (nd_comp rpf (nd_rule (@RCanR _ _ _ _ ) ) ) as rpf'.
519 set (ext_left ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) _ _ rpf') as qq.
521 eapply nd_comp; [ idtac | apply qq ].
523 set (ext_right (mapOptionTree ξ ctx2) [Γ >>Δ> mapOptionTree ξ ctx1 |- τ] [Γ >>Δ> (mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v]) |- τ]) as q.
530 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
531 fold (stripOutVars (v::nil)).
532 eapply nd_comp; [ idtac | eapply copyAndPivotContext ].
534 (* order will not matter because these are central as morphisms *)
535 (ext_right _ _ _ lpf)
536 (ext_left _ _ _ rpf)).
540 (* same as before, but use RWeak if necessary *)
541 Definition arrangeContextAndWeaken v ctx Γ Δ τ ξ :
543 [Γ >> Δ>mapOptionTree ξ ctx |- τ]
544 [Γ >> Δ>mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) |- τ].
545 set (arrangeContext Γ Δ v ctx τ ξ) as q.
547 eapply nd_comp; [ apply n | idtac ].
549 refine (ext_left _ _ _ (nd_rule (RWeak _ _))).
552 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
553 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
554 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
555 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
561 Lemma cheat : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
565 Definition arrangeContextAndWeaken'' Γ Δ ξ v : forall ctx z,
566 distinct (leaves v) ->
568 [Γ >> Δ>(mapOptionTree ξ ctx) |- z]
569 [Γ >> Δ>(mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v) |- z].
573 unfold mapOptionTree in *.
575 fold (mapOptionTree ξ) in *.
577 apply arrangeContextAndWeaken.
579 unfold mapOptionTree; simpl in *.
581 rewrite (@stripping_nothing_is_inert Γ); auto.
585 unfold mapOptionTree in *.
587 fold (mapOptionTree ξ) in *.
588 set (mapOptionTree ξ) as X in *.
590 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1) z) as IHv2'.
591 unfold stripOutVars in IHv2'.
593 fold (stripOutVars (leaves v2)) in IHv2'.
594 fold (stripOutVars (leaves v1)) in IHv2'.
596 unfold mapOptionTree in IHv2'.
598 fold (mapOptionTree ξ) in IHv2'.
600 set (distinct_app _ _ _ H) as H'.
601 destruct H' as [H1 H2].
602 set (nd_comp (IHv1 _ _ H1) (IHv2' H2)) as qq.
605 clear qq IHv2' IHv2 IHv1.
606 rewrite strip_twice_lemma.
608 rewrite (strip_distinct' v1 (leaves v2)).
615 (* IDEA: use multi-conclusion proofs instead *)
616 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
617 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
618 | lrsp_leaf : forall v t e ,
619 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
620 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
621 | lrsp_cons : forall t1 t2 b1 b2,
622 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
623 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
624 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
626 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
627 LetRecSubproofs Γ Δ ξ lev tree branches ->
628 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
629 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
630 intro X; induction X; intros; simpl in *.
637 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
638 eapply nd_comp; [ apply nd_llecnac | idtac ].
642 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
643 forall branches body,
644 distinct (leaves (mapOptionTree (@fst _ _) tree)) ->
645 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
646 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
647 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree branches body)) |- [τ @@ lev]].
649 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
656 rewrite mapleaves in disti.
657 set (@update_ξ_lemma _ Γ ξ lev tree disti) as ξlemma.
658 rewrite <- mapOptionTree_compose in ξlemma.
660 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
661 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
662 set (mapOptionTree (@fst _ _) tree) as pctx.
663 set (mapOptionTree ξ' pctx) as passback.
664 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
665 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
668 set (@arrangeContextAndWeaken'' Γ Δ ξ' pctx (expr2antecedent body,,eLetRecContext branches)) as q'.
669 unfold passback in *; clear passback.
670 unfold pctx in *; clear pctx.
671 eapply UND_to_ND in q'.
674 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
675 rewrite <- mapleaves in zz.
681 rewrite <- mapOptionTree_compose in q'.
683 eapply nd_comp; [ idtac | apply q' ].
687 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
688 eapply nd_comp; [ idtac | eapply nd_rule; apply RBindingGroup ].
689 eapply nd_comp; [ apply nd_llecnac | idtac ].
695 rewrite <- mapleaves in disti.
699 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
700 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
702 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
703 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
706 unfold scbwv_varstypes.
707 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
708 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
710 rewrite <- mapleaves' in q.
711 rewrite <- mapleaves' in q.
712 rewrite <- mapleaves' in q.
713 rewrite <- mapleaves' in q.
714 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
715 rewrite vec2list_map_list2vec in q'.
716 rewrite fst_zip in q'.
717 rewrite vec2list_map_list2vec in q'.
718 rewrite vec2list_map_list2vec in q'.
719 rewrite snd_zip in q'.
720 rewrite leaves_unleaves in q'.
721 rewrite vec2list_map_list2vec in q'.
722 rewrite vec2list_map_list2vec in q'.
725 apply scbwv_exprvars_distinct.
729 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
731 ??{sac : StrongAltCon &
732 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
733 Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
734 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
736 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
737 (mapOptionTree mkProofCaseBranch alts'))
739 mapOptionTree ξ (expr2antecedent e) =
741 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
744 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
749 unfold mkProofCaseBranch.
760 Definition expr2proof :
761 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
762 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
764 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
765 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
766 match exp as E in Expr Γ Δ ξ τ with
767 | EGlobal Γ Δ ξ t wev => let case_EGlobal := tt in _
768 | EVar Γ Δ ξ ev => let case_EVar := tt in _
769 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
770 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
771 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
772 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
773 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
774 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
775 | ELetRec Γ Δ ξ lev t tree branches ebody =>
776 let ξ' := update_ξ ξ lev (leaves tree) in
777 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
778 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
779 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
780 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
781 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
782 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
783 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
784 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
786 ) _ _ _ _ tree branches)
787 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
788 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
789 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
790 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
791 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
792 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
793 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
794 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
795 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
798 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
800 (sac_Δ sac Γ atypes (weakCK'' Δ))
802 (weakLT' (tbranches@@l)) } })
803 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
804 match alts as ALTS return ND Rule []
805 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
806 | T_Leaf None => let case_nil := tt in _
807 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
809 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
810 existT sac (existT scbx ex) =>
811 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
814 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
816 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
818 destruct case_EGlobal.
821 destruct t as [t lev].
822 apply (RGlobal _ _ _ _ wev).
826 unfold mapOptionTree; simpl.
835 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
836 eapply nd_comp; [ idtac | eapply nd_rule; apply RApp ].
837 eapply nd_comp; [ apply nd_llecnac | idtac ].
842 destruct case_ELam; intros.
843 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
844 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
845 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
846 set (arrangeContextAndWeaken v (expr2antecedent e) Γ Δ [t2 @@ lev] ξ') as pfx.
847 apply UND_to_ND in pfx.
848 unfold mapOptionTree in pfx; simpl in pfx; fold (mapOptionTree ξ) in pfx.
850 fold (mapOptionTree (update_ξ ξ lev ((v,t1)::nil))) in pfx.
851 rewrite updating_stripped_tree_is_inert in pfx.
852 unfold update_ξ in pfx.
853 destruct (eqd_dec v v).
854 eapply nd_comp; [ idtac | apply pfx ].
862 destruct case_ELet; intros; simpl in *.
863 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
864 eapply nd_comp; [ apply nd_llecnac | idtac ].
865 apply nd_prod; [ idtac | apply pf_let].
867 eapply nd_comp; [ apply pf_body | idtac ].
869 fold (@mapOptionTree VV).
870 fold (mapOptionTree ξ).
871 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
872 set (arrangeContextAndWeaken lev (expr2antecedent ebody) Γ Δ [t@@v] ξ') as n.
873 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
875 rewrite updating_stripped_tree_is_inert in n.
876 unfold update_ξ in n.
877 destruct (eqd_dec lev lev).
880 apply UND_to_ND in n.
882 assert False. apply n0; auto. inversion H.
885 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
888 destruct case_EBrak; intros.
889 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
893 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
899 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
903 destruct case_ETyApp; simpl in *; intros.
904 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
908 destruct case_ECoLam; simpl in *; intros.
909 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
912 destruct case_ECoApp; simpl in *; intros.
913 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
917 destruct case_ETyLam; intros.
918 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
919 unfold mapOptionTree in e'.
920 rewrite mapOptionTree_compose in e'.
921 unfold mapOptionTree.
925 clear o x alts alts' e.
926 eapply nd_comp; [ apply e' | idtac ].
928 set (fun q r x1 x2 y1 y2 => @UND_to_ND q r [q >> r > x1 |- y1] [q >> r > x2 |- y2]).
935 rewrite <- mapOptionTree_compose.
937 rewrite <- mapleaves'.
938 rewrite vec2list_map_list2vec.
940 rewrite <- (scbwv_coherent scbx l ξ).
941 rewrite <- vec2list_map_list2vec.
943 set (@arrangeContextAndWeaken'') as q.
945 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
946 unfold scbwv_varstypes in z.
947 rewrite vec2list_map_list2vec in z.
948 rewrite fst_zip in z.
951 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
952 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
954 rewrite leaves_unleaves.
955 apply (scbwv_exprvars_distinct scbx).
956 rewrite leaves_unleaves.
962 destruct case_branch.
963 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
969 set (@RCase Γ Δ l tc) as q.
970 rewrite <- case_lemma.
971 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
972 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
973 rewrite <- mapOptionTree_compose.
977 destruct case_ELetRec; intros.
982 apply letRecSubproofsToND'.
989 End HaskStrongToProof.