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 NaturalDeductionContext.
10 Require Import Coq.Strings.String.
11 Require Import Coq.Lists.List.
12 Require Import Coq.Init.Specif.
13 Require Import HaskKinds.
14 Require Import HaskStrongTypes.
15 Require Import HaskStrong.
16 Require Import HaskProof.
18 Section HaskStrongToProof.
20 Context {VV:Type}{eqd_vv:EqDecidable VV}.
22 (* maintenance of Xi *)
23 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
26 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
29 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
31 | T_Leaf None => T_Leaf None
32 | T_Leaf (Some x) => T_Leaf (f x)
33 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
36 (* later: use mapOptionTreeAndFlatten *)
37 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
38 mapOptionTree' (dropVar lv).
40 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
52 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
56 rewrite <- app_comm_cons.
63 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
72 set (IHl1 _ H3) as H3'.
75 apply distinct_cons; auto.
81 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
82 mapOptionTree' g (mapOptionTree' f t)
84 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
88 destruct (f t); reflexivity.
95 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
97 rewrite mapOptionTree'_compose.
105 destruct (eqd_dec v a0).
106 destruct (eqd_dec v a); reflexivity.
115 Lemma strip_nil_lemma t : stripOutVars nil t = t.
118 destruct a; reflexivity.
119 rewrite <- IHt1 at 2.
120 rewrite <- IHt2 at 2.
124 Lemma strip_swap0_lemma : forall a a0 y t,
125 stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t.
129 destruct a1; simpl; [ idtac | reflexivity ].
130 destruct (eqd_dec v a); subst.
131 destruct (eqd_dec a a0); subst.
134 destruct (eqd_dec v a0); subst.
143 Lemma strip_swap1_lemma : forall a y t,
144 stripOutVars (a :: nil) (stripOutVars y t) =
145 stripOutVars y (stripOutVars (a :: nil) t).
148 rewrite strip_nil_lemma.
149 rewrite strip_nil_lemma.
151 rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)).
154 rewrite <- (strip_lemma a y t).
155 rewrite <- strip_lemma.
156 rewrite <- strip_lemma.
157 apply strip_swap0_lemma.
160 Lemma strip_swap_lemma : forall x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t).
165 rewrite strip_nil_lemma.
166 rewrite strip_nil_lemma.
169 rewrite (strip_lemma a x [v]).
172 apply strip_swap1_lemma.
174 unfold stripOutVars in *.
181 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
183 apply strip_nil_lemma.
187 rewrite <- strip_lemma.
191 Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
194 destruct a0; try reflexivity.
198 destruct (eqd_dec v a).
205 rewrite <- IHy1 at 2.
206 rewrite <- IHy2 at 2.
210 eapply In_both' in H0.
214 eapply In_both in H0.
218 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
223 destruct (eqd_dec v a).
225 assert False. apply H.
235 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
242 rewrite <- app_comm_cons.
245 rewrite <- app_comm_cons in H.
253 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
256 apply distinct_app in H; auto.
258 rewrite <- app_comm_cons.
260 rewrite <- ass_app in H.
261 rewrite <- app_comm_cons in H.
271 rewrite <- ass_app in H.
272 rewrite <- app_comm_cons in H.
278 Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
283 induction y; try destruct a; auto.
289 apply distinct_app in H; destruct H; auto.
290 apply distinct_app in H; destruct H; auto.
291 rewrite <- app_comm_cons in H.
296 apply notin_strip_inert.
304 Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
312 destruct (eqd_dec v a).
317 Lemma updating_stripped_tree_is_inert'
319 (ξ:VV -> LeveledHaskType Γ ★)
321 mapOptionTree (update_xi ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
322 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
325 destruct a; [ idtac | reflexivity ]; simpl.
326 induction lv; [ reflexivity | idtac ]; simpl.
328 set (eqd_dec v v0) as q; destruct q; auto.
329 set (dropVar (map (@fst _ _) lv) v) as b in *.
330 assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
331 destruct b; [ idtac | reflexivity ].
332 apply dropvar_lemma in H.
337 destruct (eqd_dec v0 v1).
339 assert False. apply n. intros; auto. inversion H.
341 unfold stripOutVars in *.
343 rewrite <- IHtree2_1.
344 rewrite <- IHtree2_2.
348 Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
349 intros; induction a; auto.
357 rewrite <- app_comm_cons in H.
360 apply distinct_cons; auto.
367 Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
370 induction b; intros; simpl; auto.
371 rewrite <- app_comm_cons in H.
375 inversion H0; subst; auto.
376 apply distinct_bogus in H; inversion H.
377 induction b; intros; simpl; auto.
379 apply distinct_app in H.
383 Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
384 induction a; intros; simpl; auto.
385 rewrite <- app_comm_cons in H.
389 set (IHa _ _ H0) as H'.
395 Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
397 induction a; simpl; auto.
400 assert (distinct (app a1 b)) as Q.
404 rewrite <- app_comm_cons in H.
405 inversion H; subst; auto.
406 apply distinct_cons; [ idtac | apply Q ].
410 rewrite <- app_comm_cons in H.
411 inversion H; subst; auto.
414 rewrite <- app_comm_cons in H.
415 inversion H; subst; auto.
417 apply In_both'; auto.
422 Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
423 induction a; intros; simpl; auto.
426 Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
429 rewrite <- app_nil_end in H; auto.
430 rewrite <- app_comm_cons.
431 set (distinct_lemma _ _ _ H) as H'.
433 apply distinct_cons; [ idtac | apply H'' ].
438 apply distinct_app in H.
442 rewrite nil_app in H.
443 rewrite ass_app in H.
444 apply distinct_app in H.
446 apply distinct_swap' in H.
450 Lemma update_xiv_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
452 distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
453 mapOptionTree (update_xi ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
454 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
455 induction varstypes; intros.
456 destruct a; simpl; [ idtac | reflexivity ].
460 induction (leaves v1).
462 destruct (eqd_dec v v); auto.
463 assert False. apply n. auto. inversion H0.
466 destruct (eqd_dec v0 v); subst; auto.
468 rewrite map_app in H.
470 rewrite nil_app in H.
471 apply distinct_swap in H.
472 rewrite app_ass in H.
473 apply distinct_app in H.
475 apply distinct_swap in H0.
485 set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
486 set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
495 clear i1 i2 IHvarstypes1 IHvarstypes2.
496 repeat rewrite ass_app in *; auto.
497 clear i1 i2 IHvarstypes1 IHvarstypes2.
498 repeat rewrite ass_app in *; auto.
501 Lemma update_xiv_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
502 distinct (map (@fst _ _) (leaves varstypes)) ->
503 mapOptionTree (update_xi ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
504 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
505 set (update_xiv_lemma' Γ ξ lev varstypes [] []) as q.
507 rewrite <- app_nil_end in q.
511 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') : Tree ??VV :=
512 match exp as E in Expr Γ Δ ξ τ l with
513 | EGlobal Γ Δ ξ _ _ _ => []
514 | EVar Γ Δ ξ ev => [ev]
515 | ELit Γ Δ ξ lit lev => []
516 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
517 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
518 | ELet Γ Δ ξ tv t lev v ev ebody => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody)))
519 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
520 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
521 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
522 | ENote Γ Δ ξ t l n e => expr2antecedent e
523 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
524 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
525 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
526 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
527 | ELetRec Γ Δ ξ l τ vars _ branches body =>
528 let branch_context := eLetRecContext branches
529 in let all_contexts := branch_context,,(expr2antecedent body)
530 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
531 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
532 ((fix varsfromalts (alts:
533 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
534 & Expr (sac_gamma sac Γ)
535 (sac_delta sac Γ atypes (weakCK'' Δ))
537 (weakT' tbranches) (weakL' l)} }
541 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
542 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
543 end) alts),,(expr2antecedent e')
545 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
547 | ELR_nil Γ Δ ξ lev => []
548 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
549 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
552 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
553 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
554 & Expr (sac_gamma sac Γ)
555 (sac_delta sac Γ atypes (weakCK'' Δ))
557 (weakT' tbranches) (weakL' l) } })
558 : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
562 {| pcb_freevars := mapOptionTree ξ
563 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
564 (expr2antecedent (projT2 s)))
569 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
571 | ELR_nil Γ Δ ξ lev => []
572 | ELR_leaf Γ Δ ξ lev v t e => [t]
573 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
576 Lemma stripping_nothing_is_inert
578 (ξ:VV -> LeveledHaskType Γ ★)
580 stripOutVars nil tree = tree.
582 simpl; destruct a; reflexivity.
586 fold (stripOutVars nil).
587 rewrite <- IHtree1 at 2.
588 rewrite <- IHtree2 at 2.
592 Definition factorContextLeft
593 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
594 v (* variable to be pivoted, if found *)
595 ctx (* initial context *)
596 (ξ:VV -> LeveledHaskType Γ ★)
599 (* a proof concluding in a context where that variable does not appear *)
601 (mapOptionTree ξ ctx )
602 (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx)) ))
604 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
606 (mapOptionTree ξ ctx )
607 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) )).
611 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
615 unfold stripOutVars in *; simpl.
617 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
619 destruct (eqd_dec v' v); subst.
621 (* where the leaf is v *)
626 (* where the leaf is NOT v *)
632 apply inl; simpl in *.
640 | inr rpf => let case_Both := tt in _
641 | inl rpf => let case_Left := tt in _
645 | inr rpf => let case_Right := tt in _
646 | inl rpf => let case_Neither := tt in _
648 end); clear IHctx1; clear IHctx2.
650 destruct case_Neither.
653 eapply AComp; [idtac | apply AuCanL ].
655 (* order will not matter because these are central as morphisms *)
656 (ARight _ (AComp lpf (ACanL _)))
657 (ALeft _ (AComp rpf (ACanL _)))).
661 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
662 fold (stripOutVars (v::nil)).
663 eapply AComp; [ idtac | eapply pivotContext' ].
674 fold (stripOutVars (v::nil)).
682 eapply AComp; [ idtac | eapply AuAssoc ].
689 eapply AComp; [ idtac | eapply ARight; eapply ACont ].
690 eapply AComp; [ eapply ARight; eapply lpf | idtac ].
691 eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
694 apply arrangeSwapMiddle.
697 Definition factorContextRight
698 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
699 v (* variable to be pivoted, if found *)
700 ctx (* initial context *)
701 (ξ:VV -> LeveledHaskType Γ ★)
704 (* a proof concluding in a context where that variable does not appear *)
706 (mapOptionTree ξ ctx )
707 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
709 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
711 (mapOptionTree ξ ctx )
712 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
716 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
720 unfold stripOutVars in *; simpl.
722 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
724 destruct (eqd_dec v' v); subst.
726 (* where the leaf is v *)
731 (* where the leaf is NOT v *)
737 apply inl; simpl in *.
745 | inr rpf => let case_Both := tt in _
746 | inl rpf => let case_Left := tt in _
750 | inr rpf => let case_Right := tt in _
751 | inl rpf => let case_Neither := tt in _
753 end); clear IHctx1; clear IHctx2.
755 destruct case_Neither.
757 eapply AComp; [idtac | apply AuCanR ].
759 (* order will not matter because these are central as morphisms *)
760 (ARight _ (AComp lpf (ACanR _)))
761 (ALeft _ (AComp rpf (ACanR _)))).
766 fold (stripOutVars (v::nil)).
767 set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q.
773 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
774 eapply AComp; [ idtac | apply AAssoc ].
780 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
781 fold (stripOutVars (v::nil)).
782 eapply AComp; [ idtac | eapply pivotContext ].
783 set (AComp rpf (ACanR _ )) as rpf'.
784 set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
786 eapply AComp; [ idtac | apply qq ].
788 apply (ARight (mapOptionTree ξ ctx2)).
793 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
794 fold (stripOutVars (v::nil)).
795 eapply AComp; [ idtac | eapply copyAndPivotContext ].
796 (* order will not matter because these are central as morphisms *)
797 exact (AComp (ARight _ lpf) (ALeft _ rpf)).
801 (* same as before, but use AWeak if necessary *)
802 Definition factorContextLeftAndWeaken
803 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
804 v (* variable to be pivoted, if found *)
805 ctx (* initial context *)
806 (ξ:VV -> LeveledHaskType Γ ★) :
808 (mapOptionTree ξ ctx )
809 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ).
810 set (factorContextLeft Γ Δ v ctx ξ) as q.
812 eapply AComp; [ apply a | idtac ].
813 refine (ARight _ (AWeak _)).
816 Definition factorContextLeftAndWeaken''
817 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
818 v (* variable to be pivoted, if found *)
819 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
820 distinct (leaves v) ->
822 ((mapOptionTree ξ ctx) )
823 ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
827 unfold mapOptionTree in *.
829 fold (mapOptionTree ξ) in *.
831 set (@factorContextLeftAndWeaken) as q.
836 unfold mapOptionTree; simpl in *.
838 rewrite (@stripping_nothing_is_inert Γ); auto.
841 unfold mapOptionTree in *.
843 fold (mapOptionTree ξ) in *.
844 set (mapOptionTree ξ) as X in *.
846 set (distinct_app _ _ _ H) as H'.
847 destruct H' as [H1 H2].
849 set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
853 rewrite <- strip_twice_lemma.
854 set (notin_strip_inert' v2 (leaves v1)) as q.
855 unfold stripOutVars in q.
858 eapply AComp; [ idtac | eapply AAssoc ].
859 eapply AComp; [ idtac | eapply IHv1' ].
866 (* same as before, but use AWeak if necessary *)
867 Definition factorContextRightAndWeaken
868 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
869 v (* variable to be pivoted, if found *)
870 ctx (* initial context *)
871 (ξ:VV -> LeveledHaskType Γ ★) :
873 (mapOptionTree ξ ctx )
874 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
875 set (factorContextRight Γ Δ v ctx ξ) as q.
877 eapply AComp; [ apply a | idtac ].
878 refine (ALeft _ (AWeak _)).
881 Definition factorContextRightAndWeaken''
882 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
883 v (* variable to be pivoted, if found *)
884 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
885 distinct (leaves v) ->
887 ((mapOptionTree ξ ctx) )
888 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
892 unfold mapOptionTree in *.
894 fold (mapOptionTree ξ) in *.
896 apply factorContextRightAndWeaken.
899 unfold mapOptionTree; simpl in *.
901 rewrite (@stripping_nothing_is_inert Γ); auto.
904 unfold mapOptionTree in *.
906 fold (mapOptionTree ξ) in *.
907 set (mapOptionTree ξ) as X in *.
909 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
910 unfold stripOutVars in IHv2'.
912 fold (stripOutVars (leaves v2)) in IHv2'.
913 fold (stripOutVars (leaves v1)) in IHv2'.
915 unfold mapOptionTree in IHv2'.
917 fold (mapOptionTree ξ) in IHv2'.
919 set (distinct_app _ _ _ H) as H'.
920 destruct H' as [H1 H2].
921 set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
924 clear qq IHv2' IHv2 IHv1.
925 rewrite strip_swap_lemma.
926 rewrite strip_twice_lemma.
927 rewrite (notin_strip_inert' v1 (leaves v2)).
933 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
934 mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
935 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
936 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
942 (* TODO: use multi-conclusion proofs instead *)
943 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
944 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
945 | lrsp_leaf : forall v t e ,
946 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) ->
947 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
948 | lrsp_cons : forall t1 t2 b1 b2,
949 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
950 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
951 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
953 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
954 LetRecSubproofs Γ Δ ξ lev tree branches ->
955 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
956 |- (mapOptionTree (@snd _ _) tree) @ lev ].
957 intro X; induction X; intros; simpl in *.
964 eapply nd_comp; [ idtac | eapply RCut' ].
965 eapply nd_comp; [ apply nd_llecnac | idtac ].
968 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
972 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
973 forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
974 ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
975 LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
976 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
978 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
985 assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
987 rewrite mapleaves in disti'.
989 set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
990 rewrite <- mapOptionTree_compose in ξlemma.
992 set ((update_xi ξ lev (leaves tree))) as ξ' in *.
993 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
994 set (mapOptionTree (@fst _ _) tree) as pctx.
995 set (mapOptionTree ξ' pctx) as passback.
996 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
997 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
1000 set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
1001 unfold passback in *; clear passback.
1002 unfold pctx in *; clear pctx.
1003 set (q' disti) as q''.
1006 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
1007 rewrite <- mapleaves in zz.
1011 Opaque stripOutVars.
1013 rewrite <- mapOptionTree_compose in q''.
1015 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
1020 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1022 eapply nd_comp; [ idtac | eapply RCut' ].
1023 eapply nd_comp; [ apply nd_llecnac | idtac ].
1026 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
1030 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1031 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1033 vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1034 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1037 unfold scbwv_varstypes.
1038 set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1039 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1041 rewrite <- mapleaves' in q.
1042 rewrite <- mapleaves' in q.
1043 rewrite <- mapleaves' in q.
1044 rewrite <- mapleaves' in q.
1045 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1046 rewrite vec2list_map_list2vec in q'.
1047 rewrite fst_zip in q'.
1048 rewrite vec2list_map_list2vec in q'.
1049 rewrite vec2list_map_list2vec in q'.
1050 rewrite snd_zip in q'.
1051 rewrite leaves_unleaves in q'.
1052 rewrite vec2list_map_list2vec in q'.
1053 rewrite vec2list_map_list2vec in q'.
1056 apply scbwv_exprvars_distinct.
1060 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1062 ??{sac : StrongAltCon &
1063 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1064 Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1065 (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
1067 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
1068 (mapOptionTree mkProofCaseBranch alts'))
1070 mapOptionTree ξ (expr2antecedent e) =
1072 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1075 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1080 unfold mkProofCaseBranch.
1091 Definition expr2proof :
1092 forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
1093 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
1095 refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
1096 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
1097 match exp as E in Expr Γ Δ ξ τ l with
1098 | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
1099 | EVar Γ Δ ξ ev => let case_EVar := tt in _
1100 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
1101 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
1102 (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
1103 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1104 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
1105 (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
1106 | ELetRec Γ Δ ξ lev t tree disti branches ebody =>
1107 let ξ' := update_xi ξ lev (leaves tree) in
1108 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
1109 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1110 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1111 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1112 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1113 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
1114 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
1115 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1117 ) _ _ _ _ tree branches)
1118 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1119 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1120 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1121 | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1122 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1123 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1124 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1125 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1126 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
1129 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1130 & Expr (sac_gamma sac Γ)
1131 (sac_delta sac Γ atypes (weakCK'' Δ))
1133 (weakT' tbranches) (weakL' l) } })
1134 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
1135 match alts as ALTS return ND Rule []
1136 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
1137 | T_Leaf None => let case_nil := tt in _
1138 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1139 | T_Leaf (Some x) =>
1140 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
1141 existT sac (existT scbx ex) =>
1142 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
1145 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1147 ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.
1149 destruct case_EGlobal.
1152 apply (RGlobal _ _ _ g).
1156 unfold mapOptionTree; simpl.
1165 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1166 eapply nd_comp; [ idtac
1168 apply (@RApp _ _ _ _ t2 t1) ].
1169 eapply nd_comp; [ apply nd_llecnac | idtac ].
1170 apply nd_prod; auto.
1172 destruct case_ELam; intros.
1173 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1174 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1175 set (update_xi ξ lev ((v,t1)::nil)) as ξ'.
1176 set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1177 eapply RArrange in pfx.
1178 unfold mapOptionTree in pfx; simpl in pfx.
1180 rewrite updating_stripped_tree_is_inert in pfx.
1181 unfold update_xi in pfx.
1182 destruct (eqd_dec v v).
1183 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1191 destruct case_ELet; intros; simpl in *.
1192 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1193 eapply nd_comp; [ apply nd_rlecnac | idtac ].
1196 eapply nd_comp; [ apply pf_body | idtac ].
1197 fold (@mapOptionTree VV).
1198 fold (mapOptionTree ξ).
1199 set (update_xi ξ v ((lev,tv)::nil)) as ξ'.
1200 set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1201 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1203 rewrite updating_stripped_tree_is_inert in n.
1204 unfold update_xi in n.
1205 destruct (eqd_dec lev lev).
1208 eapply RArrange in n.
1210 assert False. apply n0; auto. inversion H.
1213 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1216 destruct case_EBrak; intros.
1217 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1220 destruct case_ECast.
1221 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1225 destruct case_ENote.
1226 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1230 destruct case_ETyApp; simpl in *; intros.
1231 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1235 destruct case_ECoLam; simpl in *; intros.
1236 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1239 destruct case_ECoApp; simpl in *; intros.
1240 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1244 destruct case_ETyLam; intros.
1245 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1246 unfold mapOptionTree in e'.
1247 rewrite mapOptionTree_compose in e'.
1248 unfold mapOptionTree.
1252 clear o x alts alts' e.
1253 eapply nd_comp; [ apply e' | idtac ].
1260 rewrite <- mapOptionTree_compose.
1262 rewrite <- mapleaves'.
1263 rewrite vec2list_map_list2vec.
1265 rewrite <- (scbwv_coherent scbx l ξ).
1266 rewrite <- vec2list_map_list2vec.
1268 set (@factorContextRightAndWeaken'') as q.
1270 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1271 unfold scbwv_varstypes in z.
1272 rewrite vec2list_map_list2vec in z.
1273 rewrite fst_zip in z.
1277 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1278 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1280 apply (sac_delta sac Γ atypes (weakCK'' Δ)).
1281 rewrite leaves_unleaves.
1282 apply (scbwv_exprvars_distinct scbx).
1283 rewrite leaves_unleaves.
1289 destruct case_branch.
1290 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1295 destruct case_ECase.
1296 set (@RCase Γ Δ l tc) as q.
1297 rewrite <- case_lemma.
1298 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1299 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1300 rewrite <- mapOptionTree_compose.
1304 destruct case_ELetRec; intros.
1309 apply letRecSubproofsToND'.
1315 End HaskStrongToProof.