Add more interp lemmas

2 files changed, 37 insertions, 1 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 2a6f33101..fc1c45612 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -650,6 +650,8 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
 
       Section interp.
         Import defaults.
+        Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}.
+        Local Notation interp := (expr.interp (@ident.gen_interp cast_outside_of_range)).
         Lemma interp_reify_list {t} ls : interp (reify_list (t:=t) ls) = List.map interp ls.
         Proof.
           cbv [reify_list]; induction ls as [|l ls IHls]; [ reflexivity | ];
@@ -664,7 +666,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
           { etransitivity; [ | apply map_id ]; apply map_ext; auto. }
         Qed.
 
-        Lemma Interp_Reify_as {t} v : Interp (GallinaReify.base.Reify_as t v) = v.
+        Lemma Interp_Reify_as {t} v : expr.Interp (@ident.gen_interp cast_outside_of_range) (GallinaReify.base.Reify_as t v) = v.
         Proof. apply interp_reify. Qed.
       End interp.
     End invert.
diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index 30422918b..c4c06c0e5 100644
--- a/src/Experiments/NewPipeline/UnderLetsProofs.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -312,6 +312,40 @@ Module Compilers.
                            end ].
         Qed.
       End with_var.
+
+      Section for_interp.
+        Context {base_interp : base_type -> Type}
+                (ident_interp : forall t, ident t -> type.interp base_interp t).
+
+        Local Notation UnderLets := (@UnderLets (type.interp base_interp)).
+
+        Fixpoint interp {T} (v : UnderLets T) : T
+          := match v with
+             | Base v => v
+             | UnderLet A x f => let xv := expr.interp ident_interp x in
+                                 @interp _ (f xv)
+             end.
+
+        Lemma interp_splice {A B} (x : UnderLets A) (e : A -> UnderLets B)
+          : interp (splice x e) = interp (e (interp x)).
+        Proof. induction x; cbn [splice interp]; eauto. Qed.
+
+        Lemma interp_splice_list {A B} (x : list (UnderLets A)) (e : list A -> UnderLets B)
+          : interp (splice_list x e)
+            = interp (e (map interp x)).
+        Proof.
+          revert e; induction x as [|x xs IHx]; intros; cbn [splice_list interp map]; [ reflexivity | ].
+          rewrite interp_splice, IHx; reflexivity.
+        Qed.
+
+        Lemma interp_to_expr {t} (x : UnderLets (expr t))
+          : expr.interp ident_interp (to_expr x) = expr.interp ident_interp (interp x).
+        Proof. induction x; cbn [expr.interp interp to_expr]; cbv [LetIn.Let_In]; eauto. Qed.
+
+        Lemma interp_of_expr {t} (x : expr t)
+          : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x.
+        Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed.
+      End for_interp.
     End with_ident.
 
     Section reify.