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 nd_rule; apply RJoin ].
965 eapply nd_comp; [ apply nd_llecnac | idtac ].
969 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
970 forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
971 ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
972 LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
973 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
975 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
982 assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
984 rewrite mapleaves in disti'.
986 set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
987 rewrite <- mapOptionTree_compose in ξlemma.
989 set ((update_xi ξ lev (leaves tree))) as ξ' in *.
990 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
991 set (mapOptionTree (@fst _ _) tree) as pctx.
992 set (mapOptionTree ξ' pctx) as passback.
993 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
994 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
997 set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
998 unfold passback in *; clear passback.
999 unfold pctx in *; clear pctx.
1000 set (q' disti) as q''.
1003 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
1004 rewrite <- mapleaves in zz.
1008 Opaque stripOutVars.
1010 rewrite <- mapOptionTree_compose in q''.
1012 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
1017 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1018 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
1019 eapply nd_comp; [ apply nd_rlecnac | idtac ].
1020 apply nd_prod; auto.
1023 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1024 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1026 vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1027 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1030 unfold scbwv_varstypes.
1031 set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1032 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1034 rewrite <- mapleaves' in q.
1035 rewrite <- mapleaves' in q.
1036 rewrite <- mapleaves' in q.
1037 rewrite <- mapleaves' in q.
1038 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1039 rewrite vec2list_map_list2vec in q'.
1040 rewrite fst_zip in q'.
1041 rewrite vec2list_map_list2vec in q'.
1042 rewrite vec2list_map_list2vec in q'.
1043 rewrite snd_zip in q'.
1044 rewrite leaves_unleaves in q'.
1045 rewrite vec2list_map_list2vec in q'.
1046 rewrite vec2list_map_list2vec in q'.
1049 apply scbwv_exprvars_distinct.
1053 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1055 ??{sac : StrongAltCon &
1056 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1057 Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1058 (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
1060 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
1061 (mapOptionTree mkProofCaseBranch alts'))
1063 mapOptionTree ξ (expr2antecedent e) =
1065 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1068 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1073 unfold mkProofCaseBranch.
1084 Definition expr2proof :
1085 forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
1086 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
1088 refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
1089 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
1090 match exp as E in Expr Γ Δ ξ τ l with
1091 | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
1092 | EVar Γ Δ ξ ev => let case_EVar := tt in _
1093 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
1094 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
1095 (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
1096 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1097 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
1098 (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
1099 | ELetRec Γ Δ ξ lev t tree disti branches ebody =>
1100 let ξ' := update_xi ξ lev (leaves tree) in
1101 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
1102 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1103 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1104 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1105 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1106 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
1107 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
1108 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1110 ) _ _ _ _ tree branches)
1111 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1112 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1113 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1114 | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1115 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1116 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1117 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1118 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1119 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
1122 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1123 & Expr (sac_gamma sac Γ)
1124 (sac_delta sac Γ atypes (weakCK'' Δ))
1126 (weakT' tbranches) (weakL' l) } })
1127 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
1128 match alts as ALTS return ND Rule []
1129 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
1130 | T_Leaf None => let case_nil := tt in _
1131 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1132 | T_Leaf (Some x) =>
1133 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
1134 existT sac (existT scbx ex) =>
1135 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ _ ex)
1138 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1140 ); clear exp ξ' τ' Γ' Δ' l' expr2proof; try clear mkdcsp.
1142 destruct case_EGlobal.
1145 apply (RGlobal _ _ _ g).
1149 unfold mapOptionTree; simpl.
1158 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1159 eapply nd_comp; [ idtac
1161 apply (@RApp _ _ _ _ t2 t1) ].
1162 eapply nd_comp; [ apply nd_llecnac | idtac ].
1163 apply nd_prod; auto.
1165 destruct case_ELam; intros.
1166 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1167 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1168 set (update_xi ξ lev ((v,t1)::nil)) as ξ'.
1169 set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1170 eapply RArrange in pfx.
1171 unfold mapOptionTree in pfx; simpl in pfx.
1173 rewrite updating_stripped_tree_is_inert in pfx.
1174 unfold update_xi in pfx.
1175 destruct (eqd_dec v v).
1176 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1184 destruct case_ELet; intros; simpl in *.
1185 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1186 eapply nd_comp; [ apply nd_rlecnac | idtac ].
1189 eapply nd_comp; [ apply pf_body | idtac ].
1190 fold (@mapOptionTree VV).
1191 fold (mapOptionTree ξ).
1192 set (update_xi ξ v ((lev,tv)::nil)) as ξ'.
1193 set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1194 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1196 rewrite updating_stripped_tree_is_inert in n.
1197 unfold update_xi in n.
1198 destruct (eqd_dec lev lev).
1201 eapply RArrange in n.
1203 assert False. apply n0; auto. inversion H.
1206 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1209 destruct case_EBrak; intros.
1210 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1213 destruct case_ECast.
1214 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1218 destruct case_ENote.
1219 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1223 destruct case_ETyApp; simpl in *; intros.
1224 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1228 destruct case_ECoLam; simpl in *; intros.
1229 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1232 destruct case_ECoApp; simpl in *; intros.
1233 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1237 destruct case_ETyLam; intros.
1238 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1239 unfold mapOptionTree in e'.
1240 rewrite mapOptionTree_compose in e'.
1241 unfold mapOptionTree.
1245 clear o x alts alts' e.
1246 eapply nd_comp; [ apply e' | idtac ].
1253 rewrite <- mapOptionTree_compose.
1255 rewrite <- mapleaves'.
1256 rewrite vec2list_map_list2vec.
1258 rewrite <- (scbwv_coherent scbx l ξ).
1259 rewrite <- vec2list_map_list2vec.
1261 set (@factorContextRightAndWeaken'') as q.
1263 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1264 unfold scbwv_varstypes in z.
1265 rewrite vec2list_map_list2vec in z.
1266 rewrite fst_zip in z.
1270 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1271 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1273 apply (sac_delta sac Γ atypes (weakCK'' Δ)).
1274 rewrite leaves_unleaves.
1275 apply (scbwv_exprvars_distinct scbx).
1276 rewrite leaves_unleaves.
1282 destruct case_branch.
1283 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1288 destruct case_ECase.
1289 set (@RCase Γ Δ l tc) as q.
1290 rewrite <- case_lemma.
1291 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1292 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1293 rewrite <- mapOptionTree_compose.
1297 destruct case_ELetRec; intros.
1302 apply letRecSubproofsToND'.
1308 End HaskStrongToProof.