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 copyAndPivotContext {T} a b c : @Arrange T ((a,,b),,(c,,b)) ((a,,c),,b).
23 eapply RComp; [ idtac | apply (RLeft (a,,c) (RCont b)) ].
24 eapply RComp; [ idtac | apply RCossa ].
25 eapply RComp; [ idtac | apply (RRight b (pivotContext a b c)) ].
29 Context {VV:Type}{eqd_vv:EqDecidable VV}.
31 (* maintenance of Xi *)
32 Fixpoint dropVar (lv:list VV)(v:VV) : ??VV :=
35 | v'::lv' => if eqd_dec v v' then None else dropVar lv' v
38 Fixpoint mapOptionTree' {a b:Type}(f:a->??b)(t:@Tree ??a) : @Tree ??b :=
40 | T_Leaf None => T_Leaf None
41 | T_Leaf (Some x) => T_Leaf (f x)
42 | T_Branch l r => T_Branch (mapOptionTree' f l) (mapOptionTree' f r)
45 (* later: use mapOptionTreeAndFlatten *)
46 Definition stripOutVars (lv:list VV) : Tree ??VV -> Tree ??VV :=
47 mapOptionTree' (dropVar lv).
49 Lemma In_both : forall T (l1 l2:list T) a, In a l1 -> In a (app l1 l2).
61 Lemma In_both' : forall T (l1 l2:list T) a, In a l2 -> In a (app l1 l2).
65 rewrite <- app_comm_cons.
72 Lemma distinct_app : forall T (l1 l2:list T), distinct (app l1 l2) -> distinct l1 /\ distinct l2.
81 set (IHl1 _ H3) as H3'.
84 apply distinct_cons; auto.
90 Lemma mapOptionTree'_compose : forall T A B (t:Tree ??T) (f:T->??A)(g:A->??B),
91 mapOptionTree' g (mapOptionTree' f t)
93 mapOptionTree' (fun x => match f x with None => None | Some x => g x end) t.
97 destruct (f t); reflexivity.
104 Lemma strip_lemma a x t : stripOutVars (a::x) t = stripOutVars (a::nil) (stripOutVars x t).
106 rewrite mapOptionTree'_compose.
114 destruct (eqd_dec v a0).
115 destruct (eqd_dec v a); reflexivity.
124 Lemma strip_nil_lemma t : stripOutVars nil t = t.
127 destruct a; reflexivity.
128 rewrite <- IHt1 at 2.
129 rewrite <- IHt2 at 2.
133 Lemma strip_swap0_lemma : forall a a0 y t,
134 stripOutVars (a :: a0 :: y) t = stripOutVars (a0 :: a :: y) t.
138 destruct a1; simpl; [ idtac | reflexivity ].
139 destruct (eqd_dec v a); subst.
140 destruct (eqd_dec a a0); subst.
143 destruct (eqd_dec v a0); subst.
152 Lemma strip_swap1_lemma : forall a y t,
153 stripOutVars (a :: nil) (stripOutVars y t) =
154 stripOutVars y (stripOutVars (a :: nil) t).
157 rewrite strip_nil_lemma.
158 rewrite strip_nil_lemma.
160 rewrite (strip_lemma a0 y (stripOutVars (a::nil) t)).
163 rewrite <- (strip_lemma a y t).
164 rewrite <- strip_lemma.
165 rewrite <- strip_lemma.
166 apply strip_swap0_lemma.
169 Lemma strip_swap_lemma : forall x y t, stripOutVars x (stripOutVars y t) = stripOutVars y (stripOutVars x t).
174 rewrite strip_nil_lemma.
175 rewrite strip_nil_lemma.
178 rewrite (strip_lemma a x [v]).
181 apply strip_swap1_lemma.
183 unfold stripOutVars in *.
190 Lemma strip_twice_lemma x y t : stripOutVars x (stripOutVars y t) = stripOutVars (app x y) t.
192 apply strip_nil_lemma.
196 rewrite <- strip_lemma.
200 Lemma notin_strip_inert a y : (not (In a (leaves y))) -> stripOutVars (a :: nil) y = y.
203 destruct a0; try reflexivity.
207 destruct (eqd_dec v a).
214 rewrite <- IHy1 at 2.
215 rewrite <- IHy2 at 2.
219 eapply In_both' in H0.
223 eapply In_both in H0.
227 Lemma drop_distinct x v : (not (In v x)) -> dropVar x v = Some v.
232 destruct (eqd_dec v a).
234 assert False. apply H.
244 Lemma in3 {T}(a b c:list T) q : In q (app a c) -> In q (app (app a b) c).
251 rewrite <- app_comm_cons.
254 rewrite <- app_comm_cons in H.
262 Lemma distinct3 {T}(a b c:list T) : distinct (app (app a b) c) -> distinct (app a c).
265 apply distinct_app in H; auto.
267 rewrite <- app_comm_cons.
269 rewrite <- ass_app in H.
270 rewrite <- app_comm_cons in H.
280 rewrite <- ass_app in H.
281 rewrite <- app_comm_cons in H.
287 Lemma notin_strip_inert' y : forall x, distinct (app x (leaves y)) -> stripOutVars x y = y.
292 induction y; try destruct a; auto.
298 apply distinct_app in H; destruct H; auto.
299 apply distinct_app in H; destruct H; auto.
300 rewrite <- app_comm_cons in H.
305 apply notin_strip_inert.
313 Lemma dropvar_lemma v v' y : dropVar y v = Some v' -> v=v'.
321 destruct (eqd_dec v a).
326 Lemma updating_stripped_tree_is_inert'
328 (ξ:VV -> LeveledHaskType Γ ★)
330 mapOptionTree (update_ξ ξ lev lv) (stripOutVars (map (@fst _ _) lv) tree2)
331 = mapOptionTree ξ (stripOutVars (map (@fst _ _) lv) tree2).
334 destruct a; [ idtac | reflexivity ]; simpl.
335 induction lv; [ reflexivity | idtac ]; simpl.
337 set (eqd_dec v v0) as q; destruct q; auto.
338 set (dropVar (map (@fst _ _) lv) v) as b in *.
339 assert (dropVar (map (@fst _ _) lv) v=b). reflexivity.
340 destruct b; [ idtac | reflexivity ].
341 apply dropvar_lemma in H.
346 destruct (eqd_dec v0 v1).
348 assert False. apply n. intros; auto. inversion H.
350 unfold stripOutVars in *.
352 rewrite <- IHtree2_1.
353 rewrite <- IHtree2_2.
357 Lemma distinct_bogus : forall {T}a0 (a:list T), distinct (a0::(app a (a0::nil))) -> False.
358 intros; induction a; auto.
366 rewrite <- app_comm_cons in H.
369 apply distinct_cons; auto.
376 Lemma distinct_swap' : forall {T}a (b:list T), distinct (app b (a::nil)) -> distinct (a::b).
379 induction b; intros; simpl; auto.
380 rewrite <- app_comm_cons in H.
384 inversion H0; subst; auto.
385 apply distinct_bogus in H; inversion H.
386 induction b; intros; simpl; auto.
388 apply distinct_app in H.
392 Lemma in_both : forall {T}(a b:list T) x, In x (app a b) -> In x a \/ In x b.
393 induction a; intros; simpl; auto.
394 rewrite <- app_comm_cons in H.
398 set (IHa _ _ H0) as H'.
404 Lemma distinct_lemma : forall {T} (a b:list T) a0, distinct (app a (a0 :: b)) -> distinct (app a b).
406 induction a; simpl; auto.
409 assert (distinct (app a1 b)) as Q.
413 rewrite <- app_comm_cons in H.
414 inversion H; subst; auto.
415 apply distinct_cons; [ idtac | apply Q ].
419 rewrite <- app_comm_cons in H.
420 inversion H; subst; auto.
423 rewrite <- app_comm_cons in H.
424 inversion H; subst; auto.
426 apply In_both'; auto.
431 Lemma nil_app : forall {T}(a:list T) x, x::a = (app (x::nil) a).
432 induction a; intros; simpl; auto.
435 Lemma distinct_swap : forall {T}(a b:list T), distinct (app a b) -> distinct (app b a).
438 rewrite <- app_nil_end in H; auto.
439 rewrite <- app_comm_cons.
440 set (distinct_lemma _ _ _ H) as H'.
442 apply distinct_cons; [ idtac | apply H'' ].
447 apply distinct_app in H.
451 rewrite nil_app in H.
452 rewrite ass_app in H.
453 apply distinct_app in H.
455 apply distinct_swap' in H.
459 Lemma update_ξ_lemma' `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
461 distinct (map (@fst _ _) (leaves (v1,,(varstypes,,v2)))) ->
462 mapOptionTree (update_ξ ξ lev (leaves (v1,,(varstypes,,v2)))) (mapOptionTree (@fst _ _) varstypes) =
463 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
464 induction varstypes; intros.
465 destruct a; simpl; [ idtac | reflexivity ].
469 induction (leaves v1).
471 destruct (eqd_dec v v); auto.
472 assert False. apply n. auto. inversion H0.
475 destruct (eqd_dec v0 v); subst; auto.
477 rewrite map_app in H.
479 rewrite nil_app in H.
480 apply distinct_swap in H.
481 rewrite app_ass in H.
482 apply distinct_app in H.
484 apply distinct_swap in H0.
494 set (IHvarstypes1 v1 (varstypes2,,v2)) as i1.
495 set (IHvarstypes2 (v1,,varstypes1) v2) as i2.
504 clear i1 i2 IHvarstypes1 IHvarstypes2.
505 repeat rewrite ass_app in *; auto.
506 clear i1 i2 IHvarstypes1 IHvarstypes2.
507 repeat rewrite ass_app in *; auto.
510 Lemma update_ξ_lemma `{EQD_VV:EqDecidable VV} Γ ξ (lev:HaskLevel Γ)(varstypes:Tree ??(VV*_)) :
511 distinct (map (@fst _ _) (leaves varstypes)) ->
512 mapOptionTree (update_ξ ξ lev (leaves varstypes)) (mapOptionTree (@fst _ _) varstypes) =
513 mapOptionTree (fun t => t@@ lev) (mapOptionTree (@snd _ _) varstypes).
514 set (update_ξ_lemma' Γ ξ lev varstypes [] []) as q.
516 rewrite <- app_nil_end in q.
520 Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}(exp:Expr Γ' Δ' ξ' τ') : Tree ??VV :=
521 match exp as E in Expr Γ Δ ξ τ with
522 | EGlobal Γ Δ ξ _ _ _ => []
523 | EVar Γ Δ ξ ev => [ev]
524 | ELit Γ Δ ξ lit lev => []
525 | EApp Γ Δ ξ t1 t2 lev e1 e2 => (expr2antecedent e2),,(expr2antecedent e1)
526 | ELam Γ Δ ξ t1 t2 lev v e => stripOutVars (v::nil) (expr2antecedent e)
527 | ELet Γ Δ ξ tv t lev v ev ebody => ((stripOutVars (v::nil) (expr2antecedent ebody)),,(expr2antecedent ev))
528 | EEsc Γ Δ ξ ec t lev e => expr2antecedent e
529 | EBrak Γ Δ ξ ec t lev e => expr2antecedent e
530 | ECast Γ Δ ξ γ t1 t2 lev e => expr2antecedent e
531 | ENote Γ Δ ξ t n e => expr2antecedent e
532 | ETyLam Γ Δ ξ κ σ l e => expr2antecedent e
533 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => expr2antecedent e
534 | ECoApp Γ Δ κ γ σ₁ σ₂ σ ξ l e => expr2antecedent e
535 | ETyApp Γ Δ κ σ τ ξ l e => expr2antecedent e
536 | ELetRec Γ Δ ξ l τ vars _ branches body =>
537 let branch_context := eLetRecContext branches
538 in let all_contexts := (expr2antecedent body),,branch_context
539 in stripOutVars (leaves (mapOptionTree (@fst _ _ ) vars)) all_contexts
540 | ECase Γ Δ ξ l tc tbranches atypes e' alts =>
541 ((fix varsfromalts (alts:
542 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
544 (sac_Δ sac Γ atypes (weakCK'' Δ))
546 (weakLT' (tbranches@@l)) } }
550 | T_Leaf (Some h) => stripOutVars (vec2list (scbwv_exprvars (projT1 (projT2 h)))) (expr2antecedent (projT2 (projT2 h)))
551 | T_Branch b1 b2 => (varsfromalts b1),,(varsfromalts b2)
552 end) alts),,(expr2antecedent e')
554 with eLetRecContext {Γ}{Δ}{ξ}{lev}{tree}(elrb:ELetRecBindings Γ Δ ξ lev tree) : Tree ??VV :=
556 | ELR_nil Γ Δ ξ lev => []
557 | ELR_leaf Γ Δ ξ lev v t e => expr2antecedent e
558 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecContext b1),,(eLetRecContext b2)
561 Definition mkProofCaseBranch {Γ}{Δ}{ξ}{l}{tc}{tbranches}{atypes}
562 (alt : { sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
564 (sac_Δ sac Γ atypes (weakCK'' Δ))
566 (weakLT' (tbranches@@l)) } })
567 : { sac : _ & ProofCaseBranch tc Γ Δ l tbranches atypes sac }.
571 {| pcb_freevars := mapOptionTree ξ
572 (stripOutVars (vec2list (scbwv_exprvars (projT1 s)))
573 (expr2antecedent (projT2 s)))
578 Fixpoint eLetRecTypes {Γ}{Δ}{ξ}{lev}{τ}(elrb:ELetRecBindings Γ Δ ξ lev τ) : Tree ??(HaskType Γ ★) :=
580 | ELR_nil Γ Δ ξ lev => []
581 | ELR_leaf Γ Δ ξ lev v t e => [t]
582 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => (eLetRecTypes b1),,(eLetRecTypes b2)
585 Lemma stripping_nothing_is_inert
587 (ξ:VV -> LeveledHaskType Γ ★)
589 stripOutVars nil tree = tree.
591 simpl; destruct a; reflexivity.
595 fold (stripOutVars nil).
596 rewrite <- IHtree1 at 2.
597 rewrite <- IHtree2 at 2.
601 Definition arrangeContext
602 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
603 v (* variable to be pivoted, if found *)
604 ctx (* initial context *)
605 (ξ:VV -> LeveledHaskType Γ ★)
608 (* a proof concluding in a context where that variable does not appear *)
610 (mapOptionTree ξ ctx )
611 (mapOptionTree ξ (stripOutVars (v::nil) ctx),,[] ))
613 (* or a proof concluding in a context where that variable appears exactly once in the left branch *)
615 (mapOptionTree ξ ctx )
616 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) )).
620 refine (match a with None => let case_None := tt in _ | Some v' => let case_Some := tt in _ end).
624 unfold stripOutVars in *; simpl.
626 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
628 destruct (eqd_dec v' v); subst.
630 (* where the leaf is v *)
635 (* where the leaf is NOT v *)
641 apply inl; simpl in *.
649 | inr rpf => let case_Both := tt in _
650 | inl rpf => let case_Left := tt in _
654 | inr rpf => let case_Right := tt in _
655 | inl rpf => let case_Neither := tt in _
657 end); clear IHctx1; clear IHctx2.
659 destruct case_Neither.
661 eapply RComp; [idtac | apply RuCanR ].
663 (* order will not matter because these are central as morphisms *)
664 (RRight _ (RComp lpf (RCanR _)))
665 (RLeft _ (RComp rpf (RCanR _)))).
670 fold (stripOutVars (v::nil)).
671 set (RRight (mapOptionTree ξ ctx2) (RComp lpf ((RCanR _)))) as q.
677 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
678 eapply RComp; [ idtac | apply RAssoc ].
684 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
685 fold (stripOutVars (v::nil)).
686 eapply RComp; [ idtac | eapply pivotContext ].
687 set (RComp rpf (RCanR _ )) as rpf'.
688 set (RLeft ((mapOptionTree ξ (stripOutVars (v :: nil) ctx1),, [ξ v])) rpf') as qq.
690 eapply RComp; [ idtac | apply qq ].
692 apply (RRight (mapOptionTree ξ ctx2)).
697 unfold mapOptionTree in *; simpl; fold (mapOptionTree ξ) in *.
698 fold (stripOutVars (v::nil)).
699 eapply RComp; [ idtac | eapply copyAndPivotContext ].
700 (* order will not matter because these are central as morphisms *)
701 exact (RComp (RRight _ lpf) (RLeft _ rpf)).
705 (* same as before, but use RWeak if necessary *)
706 Definition arrangeContextAndWeaken
707 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
708 v (* variable to be pivoted, if found *)
709 ctx (* initial context *)
710 (ξ:VV -> LeveledHaskType Γ ★) :
712 (mapOptionTree ξ ctx )
713 (mapOptionTree ξ ((stripOutVars (v::nil) ctx),,[v]) ).
714 set (arrangeContext Γ Δ v ctx ξ) as q.
716 eapply RComp; [ apply a | idtac ].
717 refine (RLeft _ (RWeak _)).
720 Definition arrangeContextAndWeaken''
721 (Γ:TypeEnv)(Δ:CoercionEnv Γ)
722 v (* variable to be pivoted, if found *)
723 (ξ:VV -> LeveledHaskType Γ ★) : forall ctx,
724 distinct (leaves v) ->
726 ((mapOptionTree ξ ctx) )
727 ((mapOptionTree ξ (stripOutVars (leaves v) ctx)),,(mapOptionTree ξ v)).
731 unfold mapOptionTree in *.
733 fold (mapOptionTree ξ) in *.
735 apply arrangeContextAndWeaken.
738 unfold mapOptionTree; simpl in *.
740 rewrite (@stripping_nothing_is_inert Γ); auto.
743 unfold mapOptionTree in *.
745 fold (mapOptionTree ξ) in *.
746 set (mapOptionTree ξ) as X in *.
748 set (IHv2 ((stripOutVars (leaves v1) ctx),, v1)) as IHv2'.
749 unfold stripOutVars in IHv2'.
751 fold (stripOutVars (leaves v2)) in IHv2'.
752 fold (stripOutVars (leaves v1)) in IHv2'.
754 unfold mapOptionTree in IHv2'.
756 fold (mapOptionTree ξ) in IHv2'.
758 set (distinct_app _ _ _ H) as H'.
759 destruct H' as [H1 H2].
760 set (RComp (IHv1 _ H1) (IHv2' H2)) as qq.
763 clear qq IHv2' IHv2 IHv1.
764 rewrite strip_swap_lemma.
765 rewrite strip_twice_lemma.
766 rewrite (notin_strip_inert' v1 (leaves v2)).
772 Lemma updating_stripped_tree_is_inert {Γ} (ξ:VV -> LeveledHaskType Γ ★) v tree t lev :
773 mapOptionTree (update_ξ ξ lev ((v,t)::nil)) (stripOutVars (v :: nil) tree)
774 = mapOptionTree ξ (stripOutVars (v :: nil) tree).
775 set (@updating_stripped_tree_is_inert' Γ lev ξ ((v,t)::nil)) as p.
781 (* TODO: use multi-conclusion proofs instead *)
782 Inductive LetRecSubproofs Γ Δ ξ lev : forall tree, ELetRecBindings Γ Δ ξ lev tree -> Type :=
783 | lrsp_nil : LetRecSubproofs Γ Δ ξ lev [] (ELR_nil _ _ _ _)
784 | lrsp_leaf : forall v t e ,
785 (ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [t@@lev]]) ->
786 LetRecSubproofs Γ Δ ξ lev [(v, t)] (ELR_leaf _ _ _ _ _ t e)
787 | lrsp_cons : forall t1 t2 b1 b2,
788 LetRecSubproofs Γ Δ ξ lev t1 b1 ->
789 LetRecSubproofs Γ Δ ξ lev t2 b2 ->
790 LetRecSubproofs Γ Δ ξ lev (t1,,t2) (ELR_branch _ _ _ _ _ _ b1 b2).
792 Lemma letRecSubproofsToND Γ Δ ξ lev tree branches :
793 LetRecSubproofs Γ Δ ξ lev tree branches ->
794 ND Rule [] [ Γ > Δ > mapOptionTree ξ (eLetRecContext branches)
795 |- (mapOptionTree (@snd _ _) tree) @@@ lev ].
796 intro X; induction X; intros; simpl in *.
803 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
804 eapply nd_comp; [ apply nd_llecnac | idtac ].
808 Lemma letRecSubproofsToND' Γ Δ ξ lev τ tree :
809 forall branches body (dist:distinct (leaves (mapOptionTree (@fst _ _) tree))),
810 ND Rule [] [Γ > Δ > mapOptionTree (update_ξ ξ lev (leaves tree)) (expr2antecedent body) |- [τ @@ lev]] ->
811 LetRecSubproofs Γ Δ (update_ξ ξ lev (leaves tree)) lev tree branches ->
812 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent (@ELetRec VV _ Γ Δ ξ lev τ tree dist branches body)) |- [τ @@ lev]].
814 (* NOTE: how we interpret stuff here affects the order-of-side-effects *)
821 assert (distinct (leaves (mapOptionTree (@fst _ _) tree))) as disti'.
823 rewrite mapleaves in disti'.
825 set (@update_ξ_lemma _ Γ ξ lev tree disti') as ξlemma.
826 rewrite <- mapOptionTree_compose in ξlemma.
828 set ((update_ξ ξ lev (leaves tree))) as ξ' in *.
829 set ((stripOutVars (leaves (mapOptionTree (@fst _ _) tree)) (eLetRecContext branches))) as ctx.
830 set (mapOptionTree (@fst _ _) tree) as pctx.
831 set (mapOptionTree ξ' pctx) as passback.
832 set (fun a b => @RLetRec Γ Δ a b (mapOptionTree (@snd _ _) tree)) as z.
833 eapply nd_comp; [ idtac | eapply nd_rule; apply z ].
836 set (@arrangeContextAndWeaken'' Γ Δ pctx ξ' (expr2antecedent body,,eLetRecContext branches)) as q'.
837 unfold passback in *; clear passback.
838 unfold pctx in *; clear pctx.
839 set (q' disti) as q''.
842 set (@updating_stripped_tree_is_inert' Γ lev ξ (leaves tree)) as zz.
843 rewrite <- mapleaves in zz.
849 rewrite <- mapOptionTree_compose in q''.
851 eapply nd_comp; [ idtac | eapply nd_rule; apply (RArrange _ _ _ _ _ q'') ].
856 set (letRecSubproofsToND _ _ _ _ _ branches lrsp) as q.
857 eapply nd_comp; [ idtac | eapply nd_rule; apply RJoin ].
858 eapply nd_comp; [ apply nd_llecnac | idtac ].
864 Lemma scbwv_coherent {tc}{Γ}{atypes:IList _ (HaskType Γ) _}{sac} :
865 forall scb:StrongCaseBranchWithVVs _ _ tc atypes sac,
867 vec2list (vec_map (scbwv_ξ scb ξ l) (scbwv_exprvars scb)) =
868 vec2list (vec_map (fun t => t @@ weakL' l) (sac_types sac _ atypes)).
871 unfold scbwv_varstypes.
872 set (@update_ξ_lemma _ _ (weakLT' ○ ξ) (weakL' l)
873 (unleaves (vec2list (vec_zip (scbwv_exprvars scb) (sac_types sac Γ atypes))))
875 rewrite <- mapleaves' in q.
876 rewrite <- mapleaves' in q.
877 rewrite <- mapleaves' in q.
878 rewrite <- mapleaves' in q.
879 set (fun z => unleaves_injective _ _ _ (q z)) as q'.
880 rewrite vec2list_map_list2vec in q'.
881 rewrite fst_zip in q'.
882 rewrite vec2list_map_list2vec in q'.
883 rewrite vec2list_map_list2vec in q'.
884 rewrite snd_zip in q'.
885 rewrite leaves_unleaves in q'.
886 rewrite vec2list_map_list2vec in q'.
887 rewrite vec2list_map_list2vec in q'.
890 apply scbwv_exprvars_distinct.
894 Lemma case_lemma : forall Γ Δ ξ l tc tbranches atypes e
896 ??{sac : StrongAltCon &
897 {scb : StrongCaseBranchWithVVs VV eqd_vv tc atypes sac &
898 Expr (sac_Γ sac Γ) (sac_Δ sac Γ atypes (weakCK'' Δ))
899 (scbwv_ξ scb ξ l) (weakLT' (tbranches @@ l))}}),
901 (mapOptionTreeAndFlatten (fun x => pcb_freevars (projT2 x))
902 (mapOptionTree mkProofCaseBranch alts'))
904 mapOptionTree ξ (expr2antecedent e) =
906 (expr2antecedent (ECase Γ Δ ξ l tc tbranches atypes e alts')).
909 Ltac hack := match goal with [ |- ?A,,?B = ?C,,?D ] => assert (A=C) end.
914 unfold mkProofCaseBranch.
925 Definition expr2proof :
926 forall Γ Δ ξ τ (e:Expr Γ Δ ξ τ),
927 ND Rule [] [Γ > Δ > mapOptionTree ξ (expr2antecedent e) |- [τ]].
929 refine (fix expr2proof Γ' Δ' ξ' τ' (exp:Expr Γ' Δ' ξ' τ') {struct exp}
930 : ND Rule [] [Γ' > Δ' > mapOptionTree ξ' (expr2antecedent exp) |- [τ']] :=
931 match exp as E in Expr Γ Δ ξ τ with
932 | EGlobal Γ Δ ξ g v lev => let case_EGlobal := tt in _
933 | EVar Γ Δ ξ ev => let case_EVar := tt in _
934 | ELit Γ Δ ξ lit lev => let case_ELit := tt in _
935 | EApp Γ Δ ξ t1 t2 lev e1 e2 => let case_EApp := tt in
936 (fun e1' e2' => _) (expr2proof _ _ _ _ e1) (expr2proof _ _ _ _ e2)
937 | ELam Γ Δ ξ t1 t2 lev v e => let case_ELam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
938 | ELet Γ Δ ξ tv t v lev ev ebody => let case_ELet := tt in
939 (fun pf_let pf_body => _) (expr2proof _ _ _ _ ev) (expr2proof _ _ _ _ ebody)
940 | ELetRec Γ Δ ξ lev t tree disti branches ebody =>
941 let ξ' := update_ξ ξ lev (leaves tree) in
942 let case_ELetRec := tt in (fun e' subproofs => _) (expr2proof _ _ _ _ ebody)
943 ((fix subproofs Γ'' Δ'' ξ'' lev'' (tree':Tree ??(VV * HaskType Γ'' ★))
944 (branches':ELetRecBindings Γ'' Δ'' ξ'' lev'' tree')
945 : LetRecSubproofs Γ'' Δ'' ξ'' lev'' tree' branches' :=
946 match branches' as B in ELetRecBindings G D X L T return LetRecSubproofs G D X L T B with
947 | ELR_nil Γ Δ ξ lev => lrsp_nil _ _ _ _
948 | ELR_leaf Γ Δ ξ l v t e => lrsp_leaf Γ Δ ξ l v t e (expr2proof _ _ _ _ e)
949 | ELR_branch Γ Δ ξ lev t1 t2 b1 b2 => lrsp_cons _ _ _ _ _ _ _ _ (subproofs _ _ _ _ _ b1) (subproofs _ _ _ _ _ b2)
951 ) _ _ _ _ tree branches)
952 | EEsc Γ Δ ξ ec t lev e => let case_EEsc := tt in (fun e' => _) (expr2proof _ _ _ _ e)
953 | EBrak Γ Δ ξ ec t lev e => let case_EBrak := tt in (fun e' => _) (expr2proof _ _ _ _ e)
954 | ECast Γ Δ ξ γ t1 t2 lev e => let case_ECast := tt in (fun e' => _) (expr2proof _ _ _ _ e)
955 | ENote Γ Δ ξ t n e => let case_ENote := tt in (fun e' => _) (expr2proof _ _ _ _ e)
956 | ETyLam Γ Δ ξ κ σ l e => let case_ETyLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
957 | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e => let case_ECoLam := tt in (fun e' => _) (expr2proof _ _ _ _ e)
958 | ECoApp Γ Δ κ σ₁ σ₂ σ γ ξ l e => let case_ECoApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
959 | ETyApp Γ Δ κ σ τ ξ l e => let case_ETyApp := tt in (fun e' => _) (expr2proof _ _ _ _ e)
960 | ECase Γ Δ ξ l tc tbranches atypes e alts' =>
963 Tree ??{ sac : _ & { scb : StrongCaseBranchWithVVs _ _ tc atypes sac
965 (sac_Δ sac Γ atypes (weakCK'' Δ))
967 (weakLT' (tbranches@@l)) } })
968 : ND Rule [] (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) alts) :=
969 match alts as ALTS return ND Rule []
970 (mapOptionTree (fun x => pcb_judg (projT2 (mkProofCaseBranch x))) ALTS) with
971 | T_Leaf None => let case_nil := tt in _
972 | T_Branch b1 b2 => let case_branch := tt in (fun b1' b2' => _) (mkdcsp b1) (mkdcsp b2)
974 match x as X return ND Rule [] [pcb_judg (projT2 (mkProofCaseBranch X))] with
975 existT sac (existT scbx ex) =>
976 (fun e' => let case_leaf := tt in _) (expr2proof _ _ _ _ ex)
979 in let case_ECase := tt in (fun e' => _) (expr2proof _ _ _ _ e)
981 ); clear exp ξ' τ' Γ' Δ' expr2proof; try clear mkdcsp.
983 destruct case_EGlobal.
986 apply (RGlobal _ _ _ g).
990 unfold mapOptionTree; simpl.
999 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1000 eapply nd_comp; [ idtac
1002 apply (@RApp _ _ _ _ t2 t1) ].
1003 eapply nd_comp; [ apply nd_llecnac | idtac ].
1004 apply nd_prod; auto.
1006 destruct case_ELam; intros.
1007 unfold mapOptionTree; simpl; fold (mapOptionTree ξ).
1008 eapply nd_comp; [ idtac | eapply nd_rule; apply RLam ].
1009 set (update_ξ ξ lev ((v,t1)::nil)) as ξ'.
1010 set (arrangeContextAndWeaken Γ Δ v (expr2antecedent e) ξ') as pfx.
1011 eapply RArrange in pfx.
1012 unfold mapOptionTree in pfx; simpl in pfx.
1014 rewrite updating_stripped_tree_is_inert in pfx.
1015 unfold update_ξ in pfx.
1016 destruct (eqd_dec v v).
1017 eapply nd_comp; [ idtac | apply (nd_rule pfx) ].
1025 destruct case_ELet; intros; simpl in *.
1026 eapply nd_comp; [ idtac | eapply nd_rule; eapply RLet ].
1027 eapply nd_comp; [ apply nd_llecnac | idtac ].
1031 eapply nd_comp; [ apply pf_body | idtac ].
1033 fold (@mapOptionTree VV).
1034 fold (mapOptionTree ξ).
1035 set (update_ξ ξ v ((lev,tv)::nil)) as ξ'.
1036 set (arrangeContextAndWeaken Γ Δ lev (expr2antecedent ebody) ξ') as n.
1037 unfold mapOptionTree in n; simpl in n; fold (mapOptionTree ξ') in n.
1039 rewrite updating_stripped_tree_is_inert in n.
1040 unfold update_ξ in n.
1041 destruct (eqd_dec lev lev).
1044 eapply RArrange in n.
1046 assert False. apply n0; auto. inversion H.
1049 eapply nd_comp; [ idtac | eapply nd_rule; apply REsc ].
1052 destruct case_EBrak; intros.
1053 eapply nd_comp; [ idtac | eapply nd_rule; apply RBrak ].
1056 destruct case_ECast.
1057 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCast ].
1061 destruct case_ENote.
1063 eapply nd_comp; [ idtac | eapply nd_rule; apply RNote ].
1067 destruct case_ETyApp; simpl in *; intros.
1068 eapply nd_comp; [ idtac | eapply nd_rule; apply RAppT ].
1072 destruct case_ECoLam; simpl in *; intros.
1073 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsCo with (κ:=κ) ].
1076 destruct case_ECoApp; simpl in *; intros.
1077 eapply nd_comp; [ idtac | eapply nd_rule; apply (@RAppCo _ _ (mapOptionTree ξ (expr2antecedent e)) _ σ₁ σ₂ σ γ l) ].
1081 destruct case_ETyLam; intros.
1082 eapply nd_comp; [ idtac | eapply nd_rule; apply RAbsT ].
1083 unfold mapOptionTree in e'.
1084 rewrite mapOptionTree_compose in e'.
1085 unfold mapOptionTree.
1089 clear o x alts alts' e.
1090 eapply nd_comp; [ apply e' | idtac ].
1097 rewrite <- mapOptionTree_compose.
1099 rewrite <- mapleaves'.
1100 rewrite vec2list_map_list2vec.
1102 rewrite <- (scbwv_coherent scbx l ξ).
1103 rewrite <- vec2list_map_list2vec.
1105 set (@arrangeContextAndWeaken'') as q.
1107 set (@updating_stripped_tree_is_inert' _ (weakL' l) (weakLT' ○ ξ) (vec2list (scbwv_varstypes scbx))) as z.
1108 unfold scbwv_varstypes in z.
1109 rewrite vec2list_map_list2vec in z.
1110 rewrite fst_zip in z.
1113 replace (stripOutVars (vec2list (scbwv_exprvars scbx))) with
1114 (stripOutVars (leaves (unleaves (vec2list (scbwv_exprvars scbx))))).
1116 apply (sac_Δ sac Γ atypes (weakCK'' Δ)).
1117 rewrite leaves_unleaves.
1118 apply (scbwv_exprvars_distinct scbx).
1119 rewrite leaves_unleaves.
1125 destruct case_branch.
1126 simpl; eapply nd_comp; [ apply nd_llecnac | idtac ].
1131 destruct case_ECase.
1132 set (@RCase Γ Δ l tc) as q.
1133 rewrite <- case_lemma.
1134 eapply nd_comp; [ idtac | eapply nd_rule; eapply RCase ].
1135 eapply nd_comp; [ apply nd_llecnac | idtac ]; apply nd_prod.
1136 rewrite <- mapOptionTree_compose.
1140 destruct case_ELetRec; intros.
1145 apply letRecSubproofsToND'.
1151 End HaskStrongToProof.