From a62576f9cb6379f3d9b5316ca64339353bde0aaa Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 9 Mar 2019 19:28:18 -0500 Subject: Add UnderLets.wf_of_expr --- src/UnderLetsProofs.v | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/UnderLetsProofs.v b/src/UnderLetsProofs.v index 7a59b7c78..7553b2cb1 100644 --- a/src/UnderLetsProofs.v +++ b/src/UnderLetsProofs.v @@ -228,6 +228,13 @@ Module Compilers. intro Hwf; induction Hwf; cbn [to_expr]; [ assumption | constructor; auto ]. Qed. + Lemma wf_of_expr {t} (x : @expr var1 t) (y : @expr var2 t) + G + : expr.wf G x y -> wf (fun G => expr.wf G) G (of_expr x) (of_expr y). + Proof. + intro Hwf; induction Hwf; cbn [of_expr]; repeat constructor; auto. + Qed. + Lemma wf_splice {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} -- cgit v1.2.3