Add InterpWf

3 files changed, 100 insertions, 12 deletions

diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v
new file mode 100644
index 000000000..ef1168555
--- /dev/null
+++ b/src/Reflection/InterpWf.v
@@ -0,0 +1,85 @@
+Require Import Coq.Strings.String Coq.Classes.RelationClasses.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.Prod.
+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 : base_type_code -> Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          (interp_op : forall src dst, op src dst -> interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst).
+
+  Local Notation exprf := (@exprf base_type_code interp_base_type op interp_base_type).
+  Local Notation expr := (@expr base_type_code interp_base_type op interp_base_type).
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+  Local Notation interpf := (@interpf base_type_code interp_base_type op interp_op).
+  Local Notation interp := (@interp base_type_code interp_base_type op interp_op).
+  Local Notation Interp := (@Interp base_type_code interp_base_type op interp_op).
+
+  Lemma eq_in_flatten_binding_list
+        {t x x' T e}
+        (HIn : List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core)
+                       (flatten_binding_list base_type_code (t:=T) e e))
+    : x = x'.
+  Proof.
+    induction T; simpl in *; [ | rewrite List.in_app_iff in HIn ];
+      repeat first [ progress destruct_head or
+                   | progress destruct_head False
+                   | progress destruct_head and
+                   | progress inversion_sigma
+                   | progress inversion_prod
+                   | progress subst
+                   | solve [ eauto ] ].
+  Qed.
+
+
+  Local Hint Resolve List.in_app_or List.in_or_app eq_in_flatten_binding_list.
+
+  Section wf.
+    Lemma interpf_wff
+             {t} {e1 e2 : exprf t}
+             {G}
+             (HG : forall t x x',
+                 List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G
+                 -> x = x')
+             (Rwf : wff G e1 e2)
+    : interpf e1 = interpf e2.
+    Proof.
+      induction Rwf; simpl; auto;
+        specialize_by auto; try congruence.
+      rewrite_hyp !*; auto.
+      repeat match goal with
+             | [ H : context[List.In _ (_ ++ _)] |- _ ]
+               => setoid_rewrite List.in_app_iff in H
+             end.
+      match goal with
+      | [ H : _ |- _ ]
+        => apply H; intros; destruct_head' or; solve [ eauto ]
+      end.
+    Qed.
+
+    Local Hint Resolve interpf_wff.
+
+    Lemma interp_wf
+             {t} {e1 e2 : expr t}
+             {G}
+             (HG : forall t x x',
+                 List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core) G
+                 -> x = x')
+             (Rwf : wf G e1 e2)
+    : interp_type_gen_rel_pointwise2 (fun _ => eq) (interp e1) (interp e2).
+    Proof.
+      induction Rwf; simpl; repeat intro; simpl in *; subst; eauto.
+      match goal with
+      | [ H : _ |- _ ]
+        => apply H; intros; progress destruct_head' or; [ | solve [ eauto ] ]
+      end.
+      inversion_sigma; inversion_prod; repeat subst; simpl; auto.
+    Qed.
+  End wf.
+End language.
diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v
index 450bb14ba..9057e2ba5 100644
--- a/src/Reflection/InterpWfRel.v
+++ b/src/Reflection/InterpWfRel.v
@@ -20,18 +20,18 @@ Section language.
                                             -> interp_flat_type_rel_pointwise2
                                                  R (interp_op1 src dst op sv1) (interp_op2 src dst op sv2)).
 
-  Notation exprf1 := (@exprf base_type_code interp_base_type1 op interp_base_type1).
-  Notation exprf2 := (@exprf base_type_code interp_base_type2 op interp_base_type2).
-  Notation expr1 := (@expr base_type_code interp_base_type1 op interp_base_type1).
-  Notation expr2 := (@expr base_type_code interp_base_type2 op interp_base_type2).
-  Notation Expr1 := (@Expr base_type_code interp_base_type1 op).
-  Notation Expr2 := (@Expr base_type_code interp_base_type2 op).
-  Notation interpf1 := (@interpf base_type_code interp_base_type1 op interp_op1).
-  Notation interpf2 := (@interpf base_type_code interp_base_type2 op interp_op2).
-  Notation interp1 := (@interp base_type_code interp_base_type1 op interp_op1).
-  Notation interp2 := (@interp base_type_code interp_base_type2 op interp_op2).
-  Notation Interp1 := (@Interp base_type_code interp_base_type1 op interp_op1).
-  Notation Interp2 := (@Interp base_type_code interp_base_type2 op interp_op2).
+  Local Notation exprf1 := (@exprf base_type_code interp_base_type1 op interp_base_type1).
+  Local Notation exprf2 := (@exprf base_type_code interp_base_type2 op interp_base_type2).
+  Local Notation expr1 := (@expr base_type_code interp_base_type1 op interp_base_type1).
+  Local Notation expr2 := (@expr base_type_code interp_base_type2 op interp_base_type2).
+  Local Notation Expr1 := (@Expr base_type_code interp_base_type1 op).
+  Local Notation Expr2 := (@Expr base_type_code interp_base_type2 op).
+  Local Notation interpf1 := (@interpf base_type_code interp_base_type1 op interp_op1).
+  Local Notation interpf2 := (@interpf base_type_code interp_base_type2 op interp_op2).
+  Local Notation interp1 := (@interp base_type_code interp_base_type1 op interp_op1).
+  Local Notation interp2 := (@interp base_type_code interp_base_type2 op interp_op2).
+  Local Notation Interp1 := (@Interp base_type_code interp_base_type1 op interp_op1).
+  Local Notation Interp2 := (@Interp base_type_code interp_base_type2 op interp_op2).
 
   Lemma interp_flat_type_rel_pointwise2_flatten_binding_list
         {t x x' T e1 e2}
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index fc390acdb..37d585ab1 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -70,6 +70,8 @@ Section language.
           | Prod _ _ => fun x y => interp_flat_type_rel_pointwise _ (fst x) (fst y)
                                    /\ interp_flat_type_rel_pointwise _ (snd x) (snd y)
           end.
+        Definition interp_type_rel_pointwise
+          := interp_type_gen_rel_pointwise _ interp_flat_type_rel_pointwise.
       End rel.
     End flat_type.
     Section rel_pointwise2.
@@ -278,6 +280,7 @@ Global Arguments interp_flat_type_rel_pointwise2 {_ _ _} R {t} _ _.
 Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _.
 Global Arguments interp_type_gen {_} _ _.
 Global Arguments interp_flat_type {_} _ _.
+Global Arguments interp_type_rel_pointwise {_} _ _ {_} _ _.
 Global Arguments interp_type_gen_rel_pointwise {_} _ _ {_} _ _.
 Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
 Global Arguments interp_type {_} _ _.