From a786c992c387567431e7b82a7e5c0c55f653031d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 31 Jul 2018 11:20:50 -0400 Subject: Add wf_Proper_list, wf_splice_list --- src/Experiments/NewPipeline/UnderLetsProofs.v | 42 +++++++++++++++++++++++---- 1 file changed, 37 insertions(+), 5 deletions(-) (limited to 'src') diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v index c284e5e23..bc97dd809 100644 --- a/src/Experiments/NewPipeline/UnderLetsProofs.v +++ b/src/Experiments/NewPipeline/UnderLetsProofs.v @@ -1,5 +1,6 @@ Require Import Coq.Lists.List. Require Import Coq.Classes.Morphisms. +Require Import Coq.Lists.SetoidList. Require Import Crypto.Experiments.NewPipeline.Language. Require Import Crypto.Experiments.NewPipeline.LanguageInversion. Require Import Crypto.Experiments.NewPipeline.LanguageWf. @@ -172,16 +173,16 @@ Module Compilers. -> wf G (UnderLet x1 f1) (UnderLet x2 f2). Global Arguments wf {T1 T2} P _ _ _. - Lemma wf_Proper_list {T1 T2} - {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} + Lemma wf_Proper_list_impl {T1 T2} + (P1 P2 : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop) (HP : forall G1 G2, (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) - -> forall v1 v2, P G1 v1 v2 -> P G2 v1 v2) + -> forall v1 v2, P1 G1 v1 v2 -> P2 G2 v1 v2) G1 G2 (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) e1 e2 - (Hwf : @wf T1 T2 P G1 e1 e2) - : @wf T1 T2 P G2 e1 e2. + (Hwf : @wf T1 T2 P1 G1 e1 e2) + : @wf T1 T2 P2 G2 e1 e2. Proof. revert dependent G2; induction Hwf; constructor; repeat first [ progress cbn in * @@ -195,6 +196,18 @@ Module Compilers. | wf_unsafe_t_step ]. Qed. + Lemma wf_Proper_list {T1 T2} + {P : list { t : type & var1 t * var2 t }%type -> T1 -> T2 -> Prop} + (HP : forall G1 G2, + (forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + -> forall v1 v2, P G1 v1 v2 -> P G2 v1 v2) + G1 G2 + (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2) + e1 e2 + (Hwf : @wf T1 T2 P G1 e1 e2) + : @wf T1 T2 P G2 e1 e2. + Proof. eapply wf_Proper_list_impl; eassumption. Qed. + Lemma wf_to_expr {t} (x : @UnderLets var1 (@expr var1 t)) (y : @UnderLets var2 (@expr var2 t)) G : wf (fun G => expr.wf G) G x y -> expr.wf G (to_expr x) (to_expr y). @@ -218,6 +231,25 @@ Module Compilers. rewrite ListUtil.app_cons_app_app in *. 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} + {Q : list { t : type & var1 t * var2 t }%type -> B1 -> B2 -> Prop} + G + (x1 : list (@UnderLets var1 A1)) (x2 : list (@UnderLets var2 A2)) + (Hx_len : length x1 = length x2) + (Hx : forall v1 v2, List.In (v1, v2) (List.combine x1 x2) -> @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) -> 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). + Qed. End with_var. End with_ident. -- cgit v1.2.3