From ad1f0354971bdd3ae5e24f154a9fffe034af6c5e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 3 Aug 2018 19:00:01 -0400 Subject: Add wf_splice_list, wf_splice_list_no_order --- src/Experiments/NewPipeline/UnderLetsProofs.v | 75 +++++++++++++++++++++++---- 1 file changed, 65 insertions(+), 10 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index 7d2ba5ba4..30422918b 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -236,26 +236,81 @@ Module Compilers. eauto using (ex_intro _ nil). Qed. - (* Lemma wf_splice_list {A1 B1 A2 B2} - {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {P_parts : nat -> list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {P : list { t : type & var1 t * var2 t }%type -> list A1 -> list A2 -> Prop} {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} G (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (P_parts_Proper_list : forall n G1 G2 a1 a2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> P_parts n G1 a1 a2 -> P_parts n G2 a1 a2) + (HP : forall G' l1 l2, + (exists seg, G' = seg ++ G) -> length l1 = length x1 -> length l2 = length x2 + -> (forall n v1 v2, nth_error l1 n = Some v1 -> nth_error l2 n = Some v2 -> P_parts n G' v1 v2) + -> P G' l1 l2) (Hx_len : length x1 = length x2) - (Hx : forall v1 v2, List.In (v1, v2) (List.combine x1 x2) -> @wf _ _ P G v1 v2) + (Hx : forall n v1 v2, nth_error x1 n = Some v1 -> nth_error x2 n = Some v2 ->@wf _ _ (P_parts n) G v1 v2) (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2) (He : forall G' a1 a2, (exists seg, G' = seg ++ G) -> P G' a1 a2 -> @wf _ _ Q G' (e1 a1) (e2 a2)) : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2). Proof. - induction Hx; cbn [splice]; [ | constructor ]; - eauto using (ex_intro _ nil); intros. - match goal with H : _ |- _ => eapply H end; - intros; destruct_head'_ex; subst. - rewrite ListUtil.app_cons_app_app in *. - eauto using (ex_intro _ nil). + revert dependent P; revert dependent P_parts; revert dependent G; revert dependent e1; revert dependent e2; revert dependent x2; + induction x1 as [|x1 xs1 IHx1], x2 as [|x2 xs2]; + cbn [splice_list length nth_error]; intros; try congruence. + { eapply He; [ exists nil; reflexivity | eapply HP; eauto using (ex_intro _ nil) ]. + intros []; cbn [nth_error]; intros; congruence. } + { inversion Hx_len; clear Hx_len. + pose proof (fun n => Hx (S n)) as Hxs. + specialize (Hx O). + cbn [nth_error] in *. + eapply wf_splice; [ eapply Hx; reflexivity | wf_safe_t ]. + destruct_head'_ex; subst. + lazymatch goal with + | [ |- wf _ _ (splice_list _ (fun _ => ?e1 (?a1 :: _))) (splice_list _ (fun _ => ?e2 (?a2 :: _))) ] + => eapply IHx1 with (P_parts:=fun n => P_parts (S n)) (P:=fun G' l1 l2 => P G' (a1::l1) (a2::l2)) + end; wf_safe_t; destruct_head'_ex; wf_safe_t. + { eapply wf_Proper_list; [ | | eapply Hxs ]; wf_t. } + { eapply HP; cbn [length]; rewrite ?app_assoc; eauto; []. + intros []; cbn [nth_error]; wf_safe_t; inversion_option; wf_safe_t. + { eapply P_parts_Proper_list; [ | eauto ]; wf_t. } + { eapply P_parts_Proper_list; [ | eauto ]; wf_t. } } + { eapply He; eauto; rewrite ?app_assoc; eauto. } } + Qed. + + Lemma wf_splice_list_no_order {A1 B1 A2 B2} + {P : list { t : type & var1 t * var2 t }%type -> A1 -> A2 -> Prop} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (P_Proper_list : forall G1 G2 a1 a2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> P G1 a1 a2 -> P G2 a1 a2) + (Hx_len : length x1 = length x2) + (Hx : forall n v1 v2, nth_error x1 n = Some v1 -> nth_error x2 n = Some v2 ->@wf _ _ P G v1 v2) + (e1 : list A1 -> @UnderLets var1 B1) (e2 : list A2 -> @UnderLets var2 B2) + (He : forall G' a1 a2, (exists seg, G' = seg ++ G) + -> length a1 = length x1 + -> length a2 = length x2 + -> (forall v1 v2, List.In (v1, v2) (combine a1 a2) -> P G' v1 v2) + -> @wf _ _ Q G' (e1 a1) (e2 a2)) + : @wf _ _ Q G (splice_list x1 e1) (splice_list x2 e2). + Proof. + apply @wf_splice_list + with (P_parts := fun _ => P) + (P:=fun G' l1 l2 => length l1 = length x1 /\ length l2 = length x2 + /\ forall v1 v2, List.In (v1, v2) (combine l1 l2) -> P G' v1 v2); + repeat first [ progress wf_safe_t + | apply conj + | progress inversion_option + | progress destruct_head'_ex + | progress break_innermost_match_hyps + | match goal with + | [ H : In _ (combine _ _) |- _ ] => apply ListUtil.In_nth_error_value in H + | [ H : context[nth_error (combine _ _) _] |- _ ] + => rewrite ListUtil.nth_error_combine in H + end ]. Qed. - *) End with_var. End with_ident. -- cgit v1.2.3