Minor reflective changes

6 files changed, 55 insertions, 7 deletions

diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index 7de1cc3a5..83751e4f2 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -71,7 +71,7 @@ Section language.
               (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t
                       (x, x')) G
             -> interpf interp_op x = x')
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+    : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (interp interp_op (inline_const e1))
                                     (interp interp_op e2).
   Proof.
@@ -86,7 +86,7 @@ Section language.
 
   Lemma Interp_InlineConst {t} (e : Expr t)
         (wf : Wf e)
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+    : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (Interp interp_op (InlineConst e))
                                     (Interp interp_op e).
   Proof.
diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v
index ef1168555..c53389b8c 100644
--- a/src/Reflection/InterpWf.v
+++ b/src/Reflection/InterpWf.v
@@ -72,7 +72,7 @@ Section language.
                  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).
+    : interp_type_gen_rel_pointwise (fun _ => eq) (interp e1) (interp e2).
     Proof.
       induction Rwf; simpl; repeat intro; simpl in *; subst; eauto.
       match goal with
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index 1da4ac851..dfc37824d 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -77,7 +77,7 @@ Section language.
   Local Hint Resolve interpf_linearizef.
 
   Lemma interp_linearize {t} e
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+    : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (interp interp_op (linearize (t:=t) e))
                                     (interp interp_op e).
   Proof.
@@ -86,7 +86,7 @@ Section language.
   Qed.
 
   Lemma Interp_Linearize {t} (e : Expr t)
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+    : interp_type_gen_rel_pointwise (fun _ => @eq _)
                                     (Interp interp_op (Linearize e))
                                     (Interp interp_op e).
   Proof.
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 37d585ab1..3d784db0d 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -281,7 +281,7 @@ 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_type_gen_rel_pointwise {_ _} _ {_} _ _.
 Global Arguments interp_flat_type_rel_pointwise {_} _ _ {_} _ _.
 Global Arguments interp_type {_} _ _.
 Global Arguments wff {_ _ _ _ _} G {t} _ _.
diff --git a/src/Reflection/Z/Reify.v b/src/Reflection/Z/Reify.v
index 4fcb16638..9500b2b88 100644
--- a/src/Reflection/Z/Reify.v
+++ b/src/Reflection/Z/Reify.v
@@ -25,4 +25,6 @@ Ltac base_reify_type T ::=
 Ltac Reify' e := Reflection.Reify.Reify' base_type interp_base_type op e.
 Ltac Reify e :=
   let v := Reflection.Reify.Reify base_type interp_base_type op e in
-  constr:((*Inline _*) ((*CSE _*) ((*InlineConst*) (Linearize v)))).
+  constr:((*Inline _*) ((*CSE _*) (InlineConst (Linearize v)))).
+Ltac Reify_rhs :=
+  etransitivity; [ | Reflection.Reify.Reify_rhs base_type interp_base_type op interp_op ].
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v
index 7b87934d6..2d31ec8e2 100644
--- a/src/Reflection/Z/Syntax.v
+++ b/src/Reflection/Z/Syntax.v
@@ -4,6 +4,7 @@ Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.Util.Equality.
 Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.PointedProp.
 Export Syntax.Notations.
 
 Local Set Boolean Equality Schemes.
@@ -45,3 +46,48 @@ Definition interp_op src dst (f : op src dst) : interp_flat_type interp_base_typ
      | Cmovne => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovne x y z w
      | Cmovle => fun xyzw => let '(x, y, z, w) := eta4 xyzw in cmovl x y z w
      end%Z.
+
+Definition base_type_eq_semidec_transparent (t1 t2 : base_type)
+  : option (t1 = t2)
+  := Some (match t1, t2 return t1 = t2 with
+           | TZ, TZ => eq_refl
+           end).
+Lemma base_type_eq_semidec_is_dec t1 t2 : base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2.
+Proof.
+  unfold base_type_eq_semidec_transparent; congruence.
+Qed.
+
+Definition op_beq t1 tR (f g : op t1 tR) : option pointed_Prop
+  := option_pointed_Prop_of_bool match f, g with
+                                 | Add, Add => true
+                                 | Add, _ => false
+                                 | Sub, Sub => true
+                                 | Sub, _ => false
+                                 | Mul, Mul => true
+                                 | Mul, _ => false
+                                 | Shl, Shl => true
+                                 | Shl, _ => false
+                                 | Shr, Shr => true
+                                 | Shr, _ => false
+                                 | Land, Land => true
+                                 | Land, _ => false
+                                 | Lor, Lor => true
+                                 | Lor, _ => false
+                                 | Neg, Neg => true
+                                 | Neg, _ => false
+                                 | Cmovne, Cmovne => true
+                                 | Cmovne, _ => false
+                                 | Cmovle, Cmovle => true
+                                 | Cmovle, _ => false
+                                 end.
+
+Lemma op_beq_bl : forall t1 tR x y, prop_of_option (op_beq t1 tR x y) -> x = y.
+Proof.
+  intros ?? x; destruct x;
+    intro y;
+    refine match y with
+           | Add => _
+           | _ => _
+           end;
+    compute; try (reflexivity || trivial || (intros; exfalso; assumption)).
+Qed.