Add Wf proofs about MapInterp

2 files changed, 46 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index e806b3a62..17e3d2467 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -104,6 +104,7 @@ src/Reflection/Linearize.v
 src/Reflection/LinearizeInterp.v
 src/Reflection/LinearizeWf.v
 src/Reflection/MapInterp.v
+src/Reflection/MapInterpWf.v
 src/Reflection/Reify.v
 src/Reflection/Syntax.v
 src/Reflection/TestCase.v
diff --git a/src/Reflection/MapInterpWf.v b/src/Reflection/MapInterpWf.v
new file mode 100644
index 000000000..2bd3f1f82
--- /dev/null
+++ b/src/Reflection/MapInterpWf.v
@@ -0,0 +1,45 @@
+(** * Well-foundedness of changing the interp function on PHOAS Representation of Gallina *)
+Require Import Coq.Strings.String Coq.Classes.RelationClasses.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.MapInterp.
+Require Import Crypto.Reflection.WfRel.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope ctype_scope.
+Local Open Scope expr_scope.
+Section language.
+  Context {base_type_code : Type}
+          {interp_base_type interp_base_type1 interp_base_type2 : base_type_code -> Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          (f1 : forall t, interp_base_type t -> interp_base_type1 t)
+          (f2 : forall t, interp_base_type t -> interp_base_type2 t)
+          (R : forall t, interp_base_type1 t -> interp_base_type2 t -> Prop)
+          (Rf12 : forall t v, R t (f1 t v) (f2 t v)).
+
+  Section with_var.
+    Context {var1 var2 : base_type_code -> Type}.
+
+    Lemma flat_rel_pointwise2_mapf {t} (v : interp_flat_type_gen interp_base_type t)
+      : interp_flat_type_gen_rel_pointwise2
+          R
+          (mapf_interp_flat_type_gen f1 v)
+          (mapf_interp_flat_type_gen f2 v).
+    Proof. induction t; simpl; auto. Qed.
+
+    Lemma wff_mapf_interp {t e1 e2} G
+          (Hwf : @wff base_type_code interp_base_type op var1 var2 G t e1 e2)
+      : rel_wff R G (mapf_interp f1 e1) (mapf_interp f2 e2).
+    Proof. induction Hwf; constructor; auto using flat_rel_pointwise2_mapf. Qed.
+
+    Lemma wf_map_interp {t e1 e2} G
+          (Hwf : @wf base_type_code interp_base_type op var1 var2 G t e1 e2)
+      : rel_wf R G (map_interp f1 e1) (map_interp f2 e2).
+    Proof. induction Hwf; constructor; auto using wff_mapf_interp. Qed.
+  End with_var.
+
+  Lemma WfMapInterp {t e} (Hwf : @Wf base_type_code interp_base_type op t e)
+    : RelWf R (MapInterp f1 e) (MapInterp f2 e).
+  Proof. repeat intro; apply wf_map_interp, Hwf. Qed.
+End language.