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 pivotContext' {T} a b c : @Arrange T (a,,(b,,c)) (b,,(a,,c)) :=
23 RComp (RComp (RAssoc _ _ _) (RRight c (RExch b a))) (RCossa _ _ _).
25 Definition copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
26 eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
27 eapply RComp; [ idtac | apply RCossa ].
28 eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
32 Context {VV:Type}{eqd_vv:EqDecidable VV}.
34 (* maintenance of Xi *)
35 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
38 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
41 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
43 | T_Leaf None => T_Leaf None
44 | T_Leaf (Some x) => T_Leaf (f x)
45 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
48 (* later: use mapOptionTreeAndFlatten *)
49 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
50 mapOptionTree' (dropVar lv).
52 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
64 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
68 rewrite <- app_comm_cons.
75 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
84 set (IHl1 _ H3) as H3'.
87 apply distinct_cons; auto.
93 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
94 mapOptionTree' g (mapOptionTree' f t)
96 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
100 destruct (f t); reflexivity.
107 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
109 rewrite mapOptionTree'_compose.
117 destruct (eqd_dec v a0).
118 destruct (eqd_dec v a); reflexivity.
127 Lemma strip_nil_lemma t : stripOutVars nil t = t.
130 destruct a; reflexivity.
131 rewrite <- IHt1 at 2.
132 rewrite <- IHt2 at 2.
136 Lemma strip_swap0_lemma : forall a a0 y t,
137 stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t.
141 destruct a1; simpl; [ idtac | reflexivity ].
142 destruct (eqd_dec v a); subst.
143 destruct (eqd_dec a a0); subst.
146 destruct (eqd_dec v a0); subst.
155 Lemma strip_swap1_lemma : forall a y t,
156 stripOutVars (a :: nil) (stripOutVars y t) =
157 stripOutVars y (stripOutVars (a :: nil) t).
160 rewrite strip_nil_lemma.
161 rewrite strip_nil_lemma.
163 rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)).
166 rewrite <- (strip_lemma a y t).
167 rewrite <- strip_lemma.
168 rewrite <- strip_lemma.
169 apply strip_swap0_lemma.
172 Lemma strip_swap_lemma : forall x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t).
177 rewrite strip_nil_lemma.
178 rewrite strip_nil_lemma.
181 rewrite (strip_lemma a x [v]).
184 apply strip_swap1_lemma.
186 unfold stripOutVars in *.
193 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
195 apply strip_nil_lemma.
199 rewrite <- strip_lemma.
203 Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
206 destruct a0; try reflexivity.
210 destruct (eqd_dec v a).
217 rewrite <- IHy1 at 2.
218 rewrite <- IHy2 at 2.
222 eapply In_both' in H0.
226 eapply In_both in H0.
230 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
235 destruct (eqd_dec v a).
237 assert False. apply H.
247 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
254 rewrite <- app_comm_cons.
257 rewrite <- app_comm_cons in H.
265 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
268 apply distinct_app in H; auto.
270 rewrite <- app_comm_cons.
272 rewrite <- ass_app in H.
273 rewrite <- app_comm_cons in H.
283 rewrite <- ass_app in H.
284 rewrite <- app_comm_cons in H.
290 Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
295 induction y; try destruct a; auto.
301 apply distinct_app in H; destruct H; auto.
302 apply distinct_app in H; destruct H; auto.
303 rewrite <- app_comm_cons in H.
308 apply notin_strip_inert.
316 Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
324 destruct (eqd_dec v a).
329 Lemma updating_stripped_tree_is_inert'
331 (ξ:VV -> LeveledHaskType Γ ★)
333 mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
334 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
337 destruct a; [ idtac | reflexivity ]; simpl.
338 induction lv; [ reflexivity | idtac ]; simpl.
340 set (eqd_dec v v0) as q; destruct q; auto.
341 set (dropVar (map (@fst _ _) lv) v) as b in *.
342 assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
343 destruct b; [ idtac | reflexivity ].
344 apply dropvar_lemma in H.
349 destruct (eqd_dec v0 v1).
351 assert False. apply n. intros; auto. inversion H.
353 unfold stripOutVars in *.
355 rewrite <- IHtree2_1.
356 rewrite <- IHtree2_2.
360 Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
361 intros; induction a; auto.
369 rewrite <- app_comm_cons in H.
372 apply distinct_cons; auto.
379 Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
382 induction b; intros; simpl; auto.
383 rewrite <- app_comm_cons in H.
387 inversion H0; subst; auto.
388 apply distinct_bogus in H; inversion H.
389 induction b; intros; simpl; auto.
391 apply distinct_app in H.
395 Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
396 induction a; intros; simpl; auto.
397 rewrite <- app_comm_cons in H.
401 set (IHa _ _ H0) as H'.
407 Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
409 induction a; simpl; auto.
412 assert (distinct (app a1 b)) as Q.
416 rewrite <- app_comm_cons in H.
417 inversion H; subst; auto.
418 apply distinct_cons; [ idtac | apply Q ].
422 rewrite <- app_comm_cons in H.
423 inversion H; subst; auto.
426 rewrite <- app_comm_cons in H.
427 inversion H; subst; auto.
429 apply In_both'; auto.
434 Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
435 induction a; intros; simpl; auto.
438 Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
441 rewrite <- app_nil_end in H; auto.
442 rewrite <- app_comm_cons.
443 set (distinct_lemma _ _ _ H) as H'.
445 apply distinct_cons; [ idtac | apply H'' ].
450 apply distinct_app in H.
454 rewrite nil_app in H.
455 rewrite ass_app in H.
456 apply distinct_app in H.
458 apply distinct_swap' in H.
462 Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
464 distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
465 mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
466 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
467 induction varstypes; intros.
468 destruct a; simpl; [ idtac | reflexivity ].
472 induction (leaves v1).
474 destruct (eqd_dec v v); auto.
475 assert False. apply n. auto. inversion H0.
478 destruct (eqd_dec v0 v); subst; auto.
480 rewrite map_app in H.
482 rewrite nil_app in H.
483 apply distinct_swap in H.
484 rewrite app_ass in H.
485 apply distinct_app in H.
487 apply distinct_swap in H0.
497 set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
498 set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
507 clear i1 i2 IHvarstypes1 IHvarstypes2.
508 repeat rewrite ass_app in *; auto.
509 clear i1 i2 IHvarstypes1 IHvarstypes2.
510 repeat rewrite ass_app in *; auto.
513 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
514 distinct (map (@fst _ _) (leaves varstypes)) ->
515 mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
516 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
517 set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q.
519 rewrite <- app_nil_end in q.
523 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
524 match exp as E in Expr Γ Δ ξ τ with
525 | EGlobal Γ Δ ξ _ _ _ => []
526 | EVar Γ Δ ξ ev => [ev]
527 | ELit Γ Δ ξ lit lev => []
528 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e1),,(expr2antecedent e2)
529 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
530 | ELet Γ Δ ξ tv t lev v ev ebody => (expr2antecedent ev),,((stripOutVars (v::nil) (expr2antecedent ebody)))
531 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
532 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
533 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
534 | ENote Γ Δ ξ t n e => expr2antecedent e
535 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
536 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
537 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
538 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
539 | ELetRec Γ Δ ξ l τ vars _ branches body =>
540 let branch_context := eLetRecContext branches
541 in let all_contexts := branch_context,,(expr2antecedent body)
542 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
543 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
544 ((fix varsfromalts (alts:
545 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
547 (sac_Δ sac Γ atypes (weakCK'' Δ))
549 (weakLT' (tbranches@@l)) } }
553 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
554 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
555 end) alts),,(expr2antecedent e')
557 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
559 | ELR_nil Γ Δ ξ lev => []
560 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
561 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
564 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
565 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
567 (sac_Δ sac Γ atypes (weakCK'' Δ))
569 (weakLT' (tbranches@@l)) } })
570 : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
574 {| pcb_freevars := mapOptionTree ξ
575 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
576 (expr2antecedent (projT2 s)))
581 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
583 | ELR_nil Γ Δ ξ lev => []
584 | ELR_leaf Γ Δ ξ lev v t e => [t]
585 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
588 Lemma stripping_nothing_is_inert
590 (ξ:VV -> LeveledHaskType Γ ★)
592 stripOutVars nil tree = tree.
594 simpl; destruct a; reflexivity.
598 fold (stripOutVars nil).
599 rewrite <- IHtree1 at 2.
600 rewrite <- IHtree2 at 2.
604 Definition factorContextLeft
605 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
606 v (* variable to be pivoted, if found *)
607 ctx (* initial context *)
608 (ξ:VV -> LeveledHaskType Γ ★)
611 (* a proof concluding in a context where that variable does not appear *)
613 (mapOptionTree ξ ctx )
614 (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx)) ))
616 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
618 (mapOptionTree ξ ctx )
619 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) )).
623 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
627 unfold stripOutVars in *; simpl.
629 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
631 destruct (eqd_dec v' v); subst.
633 (* where the leaf is v *)
638 (* where the leaf is NOT v *)
644 apply inl; simpl in *.
652 | inr rpf => let case_Both := tt in _
653 | inl rpf => let case_Left := tt in _
657 | inr rpf => let case_Right := tt in _
658 | inl rpf => let case_Neither := tt in _
660 end); clear IHctx1; clear IHctx2.
662 destruct case_Neither.
665 eapply RComp; [idtac | apply RuCanL ].
667 (* order will not matter because these are central as morphisms *)
668 (RRight _ (RComp lpf (RCanL _)))
669 (RLeft _ (RComp rpf (RCanL _)))).
673 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
674 fold (stripOutVars (v::nil)).
675 eapply RComp; [ idtac | eapply pivotContext' ].
686 fold (stripOutVars (v::nil)).
694 eapply RComp; [ idtac | eapply RCossa ].
701 eapply RComp; [ idtac | eapply RRight; eapply RCont ].
702 eapply RComp; [ eapply RRight; eapply lpf | idtac ].
703 eapply RComp; [ eapply RLeft; eapply rpf | idtac ].
706 apply arrangeSwapMiddle.
709 Definition factorContextRight
710 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
711 v (* variable to be pivoted, if found *)
712 ctx (* initial context *)
713 (ξ:VV -> LeveledHaskType Γ ★)
716 (* a proof concluding in a context where that variable does not appear *)
718 (mapOptionTree ξ ctx )
719 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
721 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
723 (mapOptionTree ξ ctx )
724 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
728 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
732 unfold stripOutVars in *; simpl.
734 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
736 destruct (eqd_dec v' v); subst.
738 (* where the leaf is v *)
743 (* where the leaf is NOT v *)
749 apply inl; simpl in *.
757 | inr rpf => let case_Both := tt in _
758 | inl rpf => let case_Left := tt in _
762 | inr rpf => let case_Right := tt in _
763 | inl rpf => let case_Neither := tt in _
765 end); clear IHctx1; clear IHctx2.
767 destruct case_Neither.
769 eapply RComp; [idtac | apply RuCanR ].
771 (* order will not matter because these are central as morphisms *)
772 (RRight _ (RComp lpf (RCanR _)))
773 (RLeft _ (RComp rpf (RCanR _)))).
778 fold (stripOutVars (v::nil)).
779 set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q.
785 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
786 eapply RComp; [ idtac | apply RAssoc ].
792 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
793 fold (stripOutVars (v::nil)).
794 eapply RComp; [ idtac | eapply pivotContext ].
795 set (RComp rpf (RCanR _ )) as rpf'.
796 set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
798 eapply RComp; [ idtac | apply qq ].
800 apply (RRight (mapOptionTree ξ ctx2)).
805 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
806 fold (stripOutVars (v::nil)).
807 eapply RComp; [ idtac | eapply copyAndPivotContext ].
808 (* order will not matter because these are central as morphisms *)
809 exact (RComp (RRight _ lpf) (RLeft _ rpf)).
813 (* same as before, but use RWeak if necessary *)
814 Definition factorContextLeftAndWeaken
815 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
816 v (* variable to be pivoted, if found *)
817 ctx (* initial context *)
818 (ξ:VV -> LeveledHaskType Γ ★) :
820 (mapOptionTree ξ ctx )
821 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ).
822 set (factorContextLeft Γ Δ v ctx ξ) as q.
824 eapply RComp; [ apply a | idtac ].
825 refine (RRight _ (RWeak _)).
828 Definition factorContextLeftAndWeaken''
829 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
830 v (* variable to be pivoted, if found *)
831 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
832 distinct (leaves v) ->
834 ((mapOptionTree ξ ctx) )
835 ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
839 unfold mapOptionTree in *.
841 fold (mapOptionTree ξ) in *.
843 set (@factorContextLeftAndWeaken) as q.
848 unfold mapOptionTree; simpl in *.
850 rewrite (@stripping_nothing_is_inert Γ); auto.
853 unfold mapOptionTree in *.
855 fold (mapOptionTree ξ) in *.
856 set (mapOptionTree ξ) as X in *.
858 set (distinct_app _ _ _ H) as H'.
859 destruct H' as [H1 H2].
861 set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
865 rewrite <- strip_twice_lemma.
866 set (notin_strip_inert' v2 (leaves v1)) as q.
867 unfold stripOutVars in q.
870 eapply RComp; [ idtac | eapply RAssoc ].
871 eapply RComp; [ idtac | eapply IHv1' ].
878 (* same as before, but use RWeak if necessary *)
879 Definition factorContextRightAndWeaken
880 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
881 v (* variable to be pivoted, if found *)
882 ctx (* initial context *)
883 (ξ:VV -> LeveledHaskType Γ ★) :
885 (mapOptionTree ξ ctx )
886 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
887 set (factorContextRight Γ Δ v ctx ξ) as q.
889 eapply RComp; [ apply a | idtac ].
890 refine (RLeft _ (RWeak _)).
893 Definition factorContextRightAndWeaken''
894 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
895 v (* variable to be pivoted, if found *)
896 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
897 distinct (leaves v) ->
899 ((mapOptionTree ξ ctx) )
900 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
904 unfold mapOptionTree in *.
906 fold (mapOptionTree ξ) in *.
908 apply factorContextRightAndWeaken.
911 unfold mapOptionTree; simpl in *.
913 rewrite (@stripping_nothing_is_inert Γ); auto.
916 unfold mapOptionTree in *.
918 fold (mapOptionTree ξ) in *.
919 set (mapOptionTree ξ) as X in *.
921 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
922 unfold stripOutVars in IHv2'.
924 fold (stripOutVars (leaves v2)) in IHv2'.
925 fold (stripOutVars (leaves v1)) in IHv2'.
927 unfold mapOptionTree in IHv2'.
929 fold (mapOptionTree ξ) in IHv2'.
931 set (distinct_app _ _ _ H) as H'.
932 destruct H' as [H1 H2].
933 set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
936 clear qq IHv2' IHv2 IHv1.
937 rewrite strip_swap_lemma.
938 rewrite strip_twice_lemma.
939 rewrite (notin_strip_inert' v1 (leaves v2)).
945 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
946 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
947 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
948 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
954 (* TODO: use multi-conclusion proofs instead *)
955 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
956 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
957 | lrsp_leaf : forall v t e ,
958 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
959 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
960 | lrsp_cons : forall t1 t2 b1 b2,
961 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
962 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
963 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
965 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
966 LetRecSubproofs Γ Δ ξ lev tree branches ->
967 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
968 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
969 intro X; induction X; intros; simpl in *.
976 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
977 eapply nd_comp; [ apply nd_llecnac | idtac ].
981 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
982 forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
983 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
984 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
985 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]].
987 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
994 assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
996 rewrite mapleaves in disti'.
998 set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma.
999 rewrite <- mapOptionTree_compose in ξlemma.
1001 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
1002 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
1003 set (mapOptionTree (@fst _ _) tree) as pctx.
1004 set (mapOptionTree ξ' pctx) as passback.
1005 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
1006 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
1009 set (@factorContextRightAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
1010 unfold passback in *; clear passback.
1011 unfold pctx in *; clear pctx.
1012 set (q' disti) as q''.
1015 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
1016 rewrite <- mapleaves in zz.
1020 Opaque stripOutVars.
1022 rewrite <- mapOptionTree_compose in q''.
1024 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
1029 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1030 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
1031 eapply nd_comp; [ apply nd_rlecnac | idtac ].
1032 apply nd_prod; auto.
1037 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1038 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1040 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
1041 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1044 unfold scbwv_varstypes.
1045 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1046 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1048 rewrite <- mapleaves' in q.
1049 rewrite <- mapleaves' in q.
1050 rewrite <- mapleaves' in q.
1051 rewrite <- mapleaves' in q.
1052 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1053 rewrite vec2list_map_list2vec in q'.
1054 rewrite fst_zip in q'.
1055 rewrite vec2list_map_list2vec in q'.
1056 rewrite vec2list_map_list2vec in q'.
1057 rewrite snd_zip in q'.
1058 rewrite leaves_unleaves in q'.
1059 rewrite vec2list_map_list2vec in q'.
1060 rewrite vec2list_map_list2vec in q'.
1063 apply scbwv_exprvars_distinct.
1067 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1069 ??{sac : StrongAltCon &
1070 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1071 Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
1072 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
1074 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
1075 (mapOptionTree mkProofCaseBranch alts'))
1077 mapOptionTree ξ (expr2antecedent e) =
1079 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1082 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1087 unfold mkProofCaseBranch.
1098 Definition expr2proof :
1099 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
1100 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
1102 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
1103 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
1104 match exp as E in Expr Γ Δ ξ τ with
1105 | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
1106 | EVar Γ Δ ξ ev => let case_EVar := tt in _
1107 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
1108 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
1109 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
1110 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1111 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
1112 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
1113 | ELetRec Γ Δ ξ lev t tree disti branches ebody =>
1114 let ξ' := update_ξ ξ lev (leaves tree) in
1115 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
1116 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1117 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1118 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1119 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1120 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
1121 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
1122 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1124 ) _ _ _ _ tree branches)
1125 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1126 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1127 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1128 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1129 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1130 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1131 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1132 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1133 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
1136 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1137 & Expr (sac_Γ sac Γ)
1138 (sac_Δ sac Γ atypes (weakCK'' Δ))
1140 (weakLT' (tbranches@@l)) } })
1141 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
1142 match alts as ALTS return ND Rule []
1143 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
1144 | T_Leaf None => let case_nil := tt in _
1145 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1146 | T_Leaf (Some x) =>
1147 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
1148 existT sac (existT scbx ex) =>
1149 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
1152 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
1154 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
1156 destruct case_EGlobal.
1159 apply (RGlobal _ _ _ g).
1163 unfold mapOptionTree; simpl.
1172 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1173 eapply nd_comp; [ idtac
1175 apply (@RApp _ _ _ _ t2 t1) ].
1176 eapply nd_comp; [ apply nd_llecnac | idtac ].
1177 apply nd_prod; auto.
1179 destruct case_ELam; intros.
1180 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1181 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1182 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
1183 set (factorContextRightAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1184 eapply RArrange in pfx.
1185 unfold mapOptionTree in pfx; simpl in pfx.
1187 rewrite updating_stripped_tree_is_inert in pfx.
1188 unfold update_ξ in pfx.
1189 destruct (eqd_dec v v).
1190 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1198 destruct case_ELet; intros; simpl in *.
1199 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1200 eapply nd_comp; [ apply nd_rlecnac | idtac ].
1203 eapply nd_comp; [ apply pf_body | idtac ].
1204 fold (@mapOptionTree VV).
1205 fold (mapOptionTree ξ).
1206 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
1207 set (factorContextLeftAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1208 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1210 rewrite updating_stripped_tree_is_inert in n.
1211 unfold update_ξ in n.
1212 destruct (eqd_dec lev lev).
1215 eapply RArrange in n.
1217 assert False. apply n0; auto. inversion H.
1220 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1223 destruct case_EBrak; intros.
1224 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1227 destruct case_ECast.
1228 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1232 destruct case_ENote.
1234 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1238 destruct case_ETyApp; simpl in *; intros.
1239 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1243 destruct case_ECoLam; simpl in *; intros.
1244 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1247 destruct case_ECoApp; simpl in *; intros.
1248 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1252 destruct case_ETyLam; intros.
1253 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1254 unfold mapOptionTree in e'.
1255 rewrite mapOptionTree_compose in e'.
1256 unfold mapOptionTree.
1260 clear o x alts alts' e.
1261 eapply nd_comp; [ apply e' | idtac ].
1268 rewrite <- mapOptionTree_compose.
1270 rewrite <- mapleaves'.
1271 rewrite vec2list_map_list2vec.
1273 rewrite <- (scbwv_coherent scbx l ξ).
1274 rewrite <- vec2list_map_list2vec.
1276 set (@factorContextRightAndWeaken'') as q.
1278 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1279 unfold scbwv_varstypes in z.
1280 rewrite vec2list_map_list2vec in z.
1281 rewrite fst_zip in z.
1285 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1286 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1288 apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
1289 rewrite leaves_unleaves.
1290 apply (scbwv_exprvars_distinct scbx).
1291 rewrite leaves_unleaves.
1297 destruct case_branch.
1298 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1303 destruct case_ECase.
1304 set (@RCase Γ Δ l tc) as q.
1305 rewrite <- case_lemma.
1306 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1307 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1308 rewrite <- mapOptionTree_compose.
1312 destruct case_ELetRec; intros.
1317 apply letRecSubproofsToND'.
1323 End HaskStrongToProof.