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 n 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 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
554 | ELR_nil Γ Δ ξ lev => []
555 | ELR_leaf Γ Δ ξ lev v t e => [t]
556 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
559 Lemma stripping_nothing_is_inert
561 (ξ:VV -> LeveledHaskType Γ ★)
563 stripOutVars nil tree = tree.
565 simpl; destruct a; reflexivity.
569 fold (stripOutVars nil).
570 rewrite <- IHtree1 at 2.
571 rewrite <- IHtree2 at 2.
575 Definition factorContextLeft
576 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
577 v (* variable to be pivoted, if found *)
578 ctx (* initial context *)
579 (ξ:VV -> LeveledHaskType Γ ★)
582 (* a proof concluding in a context where that variable does not appear *)
584 (mapOptionTree ξ ctx )
585 (mapOptionTree ξ ([],,(stripOutVars (v::nil) ctx)) ))
587 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
589 (mapOptionTree ξ ctx )
590 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) )).
594 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
598 unfold stripOutVars in *; simpl.
600 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
602 destruct (eqd_dec v' v); subst.
604 (* where the leaf is v *)
609 (* where the leaf is NOT v *)
615 apply inl; simpl in *.
623 | inr rpf => let case_Both := tt in _
624 | inl rpf => let case_Left := tt in _
628 | inr rpf => let case_Right := tt in _
629 | inl rpf => let case_Neither := tt in _
631 end); clear IHctx1; clear IHctx2.
633 destruct case_Neither.
636 eapply AComp; [idtac | apply AuCanL ].
638 (* order will not matter because these are central as morphisms *)
639 (ARight _ (AComp lpf (ACanL _)))
640 (ALeft _ (AComp rpf (ACanL _)))).
644 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
645 fold (stripOutVars (v::nil)).
646 eapply AComp; [ idtac | eapply pivotContext' ].
657 fold (stripOutVars (v::nil)).
665 eapply AComp; [ idtac | eapply AuAssoc ].
672 eapply AComp; [ idtac | eapply ARight; eapply ACont ].
673 eapply AComp; [ eapply ARight; eapply lpf | idtac ].
674 eapply AComp; [ eapply ALeft; eapply rpf | idtac ].
677 apply arrangeSwapMiddle.
680 Definition factorContextRight
681 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
682 v (* variable to be pivoted, if found *)
683 ctx (* initial context *)
684 (ξ:VV -> LeveledHaskType Γ ★)
687 (* a proof concluding in a context where that variable does not appear *)
689 (mapOptionTree ξ ctx )
690 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
692 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
694 (mapOptionTree ξ ctx )
695 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
699 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
703 unfold stripOutVars in *; simpl.
705 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
707 destruct (eqd_dec v' v); subst.
709 (* where the leaf is v *)
714 (* where the leaf is NOT v *)
720 apply inl; simpl in *.
728 | inr rpf => let case_Both := tt in _
729 | inl rpf => let case_Left := tt in _
733 | inr rpf => let case_Right := tt in _
734 | inl rpf => let case_Neither := tt in _
736 end); clear IHctx1; clear IHctx2.
738 destruct case_Neither.
740 eapply AComp; [idtac | apply AuCanR ].
742 (* order will not matter because these are central as morphisms *)
743 (ARight _ (AComp lpf (ACanR _)))
744 (ALeft _ (AComp rpf (ACanR _)))).
749 fold (stripOutVars (v::nil)).
750 set (ARight (mapOptionTree ξ ctx2) (AComp lpf ((ACanR _)))) as q.
756 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
757 eapply AComp; [ idtac | apply AAssoc ].
763 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
764 fold (stripOutVars (v::nil)).
765 eapply AComp; [ idtac | eapply pivotContext ].
766 set (AComp rpf (ACanR _ )) as rpf'.
767 set (ALeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
769 eapply AComp; [ idtac | apply qq ].
771 apply (ARight (mapOptionTree ξ ctx2)).
776 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
777 fold (stripOutVars (v::nil)).
778 eapply AComp; [ idtac | eapply copyAndPivotContext ].
779 (* order will not matter because these are central as morphisms *)
780 exact (AComp (ARight _ lpf) (ALeft _ rpf)).
784 (* same as before, but use AWeak if necessary *)
785 Definition factorContextLeftAndWeaken
786 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
787 v (* variable to be pivoted, if found *)
788 ctx (* initial context *)
789 (ξ:VV -> LeveledHaskType Γ ★) :
791 (mapOptionTree ξ ctx )
792 (mapOptionTree ξ ([v],,(stripOutVars (v::nil) ctx)) ).
793 set (factorContextLeft Γ Δ v ctx ξ) as q.
795 eapply AComp; [ apply a | idtac ].
796 refine (ARight _ (AWeak _)).
799 Definition factorContextLeftAndWeaken''
800 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
801 v (* variable to be pivoted, if found *)
802 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
803 distinct (leaves v) ->
805 ((mapOptionTree ξ ctx) )
806 ((mapOptionTree ξ v),,(mapOptionTree ξ (stripOutVars (leaves v) ctx))).
810 unfold mapOptionTree in *.
812 fold (mapOptionTree ξ) in *.
814 set (@factorContextLeftAndWeaken) as q.
819 unfold mapOptionTree; simpl in *.
821 rewrite (@stripping_nothing_is_inert Γ); auto.
824 unfold mapOptionTree in *.
826 fold (mapOptionTree ξ) in *.
827 set (mapOptionTree ξ) as X in *.
829 set (distinct_app _ _ _ H) as H'.
830 destruct H' as [H1 H2].
832 set (IHv1 (v2,,(stripOutVars (leaves v2) ctx))) as IHv1'.
836 rewrite <- strip_twice_lemma.
837 set (notin_strip_inert' v2 (leaves v1)) as q.
838 unfold stripOutVars in q.
841 eapply AComp; [ idtac | eapply AAssoc ].
842 eapply AComp; [ idtac | eapply IHv1' ].
849 (* same as before, but use AWeak if necessary *)
850 Definition factorContextRightAndWeaken
851 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
852 v (* variable to be pivoted, if found *)
853 ctx (* initial context *)
854 (ξ:VV -> LeveledHaskType Γ ★) :
856 (mapOptionTree ξ ctx )
857 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
858 set (factorContextRight Γ Δ v ctx ξ) as q.
860 eapply AComp; [ apply a | idtac ].
861 refine (ALeft _ (AWeak _)).
864 Definition factorContextRightAndWeaken''
865 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
866 v (* variable to be pivoted, if found *)
867 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
868 distinct (leaves v) ->
870 ((mapOptionTree ξ ctx) )
871 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
875 unfold mapOptionTree in *.
877 fold (mapOptionTree ξ) in *.
879 apply factorContextRightAndWeaken.
882 unfold mapOptionTree; simpl in *.
884 rewrite (@stripping_nothing_is_inert Γ); auto.
887 unfold mapOptionTree in *.
889 fold (mapOptionTree ξ) in *.
890 set (mapOptionTree ξ) as X in *.
892 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
893 unfold stripOutVars in IHv2'.
895 fold (stripOutVars (leaves v2)) in IHv2'.
896 fold (stripOutVars (leaves v1)) in IHv2'.
898 unfold mapOptionTree in IHv2'.
900 fold (mapOptionTree ξ) in IHv2'.
902 set (distinct_app _ _ _ H) as H'.
903 destruct H' as [H1 H2].
904 set (AComp (IHv1 _ H1) (IHv2' H2)) as qq.
907 clear qq IHv2' IHv2 IHv1.
908 rewrite strip_swap_lemma.
909 rewrite strip_twice_lemma.
910 rewrite (notin_strip_inert' v1 (leaves v2)).
916 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
917 mapOptionTree (update_xi ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
918 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
919 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
925 (* TODO: use multi-conclusion proofs instead *)
926 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
927 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
928 | lrsp_leaf : forall v t e ,
929 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t]@lev]) ->
930 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
931 | lrsp_cons : forall t1 t2 b1 b2,
932 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
933 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
934 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
936 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
937 LetRecSubproofs Γ Δ ξ lev tree branches ->
938 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
939 |- (mapOptionTree (@snd _ _) tree) @ lev ].
940 intro X; induction X; intros; simpl in *.
947 eapply nd_comp; [ idtac | eapply RCut' ].
948 eapply nd_comp; [ apply nd_llecnac | idtac ].
951 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
955 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
956 forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
957 ND Rule [] [Γ > Δ > mapOptionTree (update_xi ξ lev (leaves tree)) (expr2antecedent body) |- [τ ]@ lev] ->
958 LetRecSubproofs Γ Δ (update_xi ξ lev (leaves tree)) lev tree branches ->
959 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ ]@ lev].
961 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
968 assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
970 rewrite mapleaves in disti'.
972 set (@update_xiv_lemma _ Γ ξ lev tree disti') as ξlemma.
973 rewrite <- mapOptionTree_compose in ξlemma.
975 set ((update_xi ξ lev (leaves tree))) as ξ' in *.
976 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
977 set (mapOptionTree (@fst _ _) tree) as pctx.
978 set (mapOptionTree ξ' pctx) as passback.
979 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
980 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
983 set (@factorContextLeftAndWeaken'' Γ Δ pctx ξ' (eLetRecContext branches,,expr2antecedent body)) as q'.
984 unfold passback in *; clear passback.
985 unfold pctx in *; clear pctx.
986 set (q' disti) as q''.
989 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
990 rewrite <- mapleaves in zz.
996 rewrite <- mapOptionTree_compose in q''.
998 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ _ q'') ].
1003 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
1005 eapply nd_comp; [ idtac | eapply RCut' ].
1006 eapply nd_comp; [ apply nd_llecnac | idtac ].
1009 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLeft ].
1013 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
1014 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
1016 vec2list (vec_map (scbwv_xi scb ξ l) (scbwv_exprvars scb)) =
1017 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
1020 unfold scbwv_varstypes.
1021 set (@update_xiv_lemma _ _ (weakLT' ○ ξ) (weakL' l)
1022 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
1024 rewrite <- mapleaves' in q.
1025 rewrite <- mapleaves' in q.
1026 rewrite <- mapleaves' in q.
1027 rewrite <- mapleaves' in q.
1028 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
1029 rewrite vec2list_map_list2vec in q'.
1030 rewrite fst_zip in q'.
1031 rewrite vec2list_map_list2vec in q'.
1032 rewrite vec2list_map_list2vec in q'.
1033 rewrite snd_zip in q'.
1034 rewrite leaves_unleaves in q'.
1035 rewrite vec2list_map_list2vec in q'.
1036 rewrite vec2list_map_list2vec in q'.
1039 apply scbwv_exprvars_distinct.
1043 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
1044 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1045 & Expr (sac_gamma sac Γ)
1046 (sac_delta sac Γ atypes (weakCK'' Δ))
1048 (weakT' tbranches) (weakL' l) } })
1049 : @StrongAltCon tc * Tree ??(LeveledHaskType Γ ★).
1053 apply (mapOptionTree ξ
1054 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
1055 (expr2antecedent (projT2 s)))).
1058 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
1060 ??{sac : StrongAltCon &
1061 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
1062 Expr (sac_gamma sac Γ) (sac_delta sac Γ atypes (weakCK'' Δ))
1063 (scbwv_xi scb ξ l) (weakT' tbranches) (weakL' l)}}),
1065 (mapOptionTreeAndFlatten (fun x => snd x)
1066 (mapOptionTree mkProofCaseBranch alts'))
1068 mapOptionTree ξ (expr2antecedent e) =
1070 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
1073 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
1078 unfold mkProofCaseBranch.
1089 Definition expr2proof :
1090 forall Γ Δ ξ τ l (e:Expr Γ Δ ξ τ l),
1091 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ] @ l].
1093 refine (fix expr2proof Γ' Δ' ξ' τ' l' (exp:Expr Γ' Δ' ξ' τ' l') {struct exp}
1094 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ'] @ l'] :=
1095 match exp as E in Expr Γ Δ ξ τ l with
1096 | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
1097 | EVar Γ Δ ξ ev => let case_EVar := tt in _
1098 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
1099 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
1100 (fun e1' e2' => _) (expr2proof _ _ _ _ _ e1) (expr2proof _ _ _ _ _ e2)
1101 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1102 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
1103 (fun pf_let pf_body => _) (expr2proof _ _ _ _ _ ev) (expr2proof _ _ _ _ _ ebody)
1104 | ELetRec Γ Δ ξ lev t tree disti branches ebody =>
1105 let ξ' := update_xi ξ lev (leaves tree) in
1106 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ _ ebody)
1107 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
1108 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
1109 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
1110 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
1111 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
1112 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ _ e)
1113 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
1115 ) _ _ _ _ tree branches)
1116 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1117 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1118 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1119 | ENote Γ Δ ξ t _ n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1120 | ETyLam Γ Δ ξ κ σ l n e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1121 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1122 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1123 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
1124 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
1127 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
1128 & Expr (sac_gamma sac Γ)
1129 (sac_delta sac Γ atypes (weakCK'' Δ))
1131 (weakT' tbranches) (weakL' l) } })
1132 : ND Rule [] (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) alts) :=
1133 match alts as ALTS return ND Rule []
1134 (mapOptionTree (fun x => pcb_judg (snd (mkProofCaseBranch x))) ALTS) with
1135 | T_Leaf None => let case_nil := tt in _
1136 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
1137 | T_Leaf (Some x) =>
1138 match x as X return ND Rule [] [@pcb_judg tc Γ Δ l tbranches atypes
1139 (fst (mkProofCaseBranch X))
1140 (snd (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 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.
1254 apply (fun x => nd_comp e' x).
1260 rewrite <- mapOptionTree_compose.
1262 rewrite <- mapleaves'.
1263 rewrite vec2list_map_list2vec.
1265 rewrite <- vec2list_map_list2vec.
1267 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1268 unfold scbwv_varstypes in z.
1269 rewrite vec2list_map_list2vec in z.
1270 rewrite fst_zip in z.
1273 unfold sac_gamma in *.
1275 Unset Printing Implicit.
1279 set (scbwv_exprvars_distinct scbx) as q'.
1280 rewrite <- leaves_unleaves in q'.
1281 apply (AComp (@factorContextRightAndWeaken'' _ (weakCE' Δ) _ _ (expr2antecedent ex) q')).
1284 set (scbwv_coherent scbx l ξ) as H.
1285 rewrite leaves_unleaves.
1286 unfold scbwv_varstypes.
1288 rewrite <- mapleaves'.
1289 rewrite <- mapleaves'.
1291 rewrite vec2list_map_list2vec.
1294 rewrite <- mapleaves'.
1295 rewrite vec2list_map_list2vec.
1297 unfold scbwv_varstypes.
1303 destruct case_branch.
1304 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1309 destruct case_ECase.
1310 set (@RCase Γ Δ l tc) as q.
1311 rewrite <- case_lemma.
1312 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1313 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1314 rewrite <- mapOptionTree_compose.
1318 destruct case_ELetRec; intros.
1323 apply letRecSubproofsToND'.
1329 End HaskStrongToProof.