Move find_if_eq to Decidable.v, use Decidable in Named

3 files changed, 28 insertions, 26 deletions

diff --git a/src/Reflection/Named/ContextDefinitions.v b/src/Reflection/Named/ContextDefinitions.v
index 186e19b37..c63142de6 100644
--- a/src/Reflection/Named/ContextDefinitions.v
+++ b/src/Reflection/Named/ContextDefinitions.v
@@ -1,17 +1,18 @@
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Decidable.
 
 Section with_context.
   Context {base_type_code Name var} (Context : @Context base_type_code Name var)
-          (base_type_code_dec : forall x y : base_type_code, {x = y} + {x <> y})
-          (Name_dec : forall x y : Name, {x = y} + {x <> y}).
+          (base_type_code_dec : DecidableRel (@eq base_type_code))
+          (Name_dec : DecidableRel (@eq Name)).
 
   Fixpoint find_Name n
            {T : flat_type base_type_code}
     : interp_flat_type (fun _ => Name) T -> option base_type_code
     := match T with
-       | Tbase t' => fun n' : Name => if Name_dec n n' then Some t' else None
+       | Tbase t' => fun n' : Name => if dec (n = n') then Some t' else None
        | Unit => fun _ => None
        | Prod A B
          => fun ab : interp_flat_type _ A * interp_flat_type _ B
@@ -22,25 +23,14 @@ Section with_context.
                end
        end.
 
-  Definition cast_if_eq {var'} t t' (v : var' t) : option (var' t')
-    := match base_type_code_dec t t', base_type_code_dec t' t' with
-       | left pf, left pf' => Some (eq_rect _ var' v _ (eq_trans pf (eq_sym pf')))
-       | _, right pf' => match pf' eq_refl with end
-       | right pf, _ => None
-       end.
-
-  Lemma cast_if_eq_refl {var'} t v : @cast_if_eq var' t t v = Some v.
-  Proof.
-    compute; clear; break_match; reflexivity.
-  Qed.
-
-  Fixpoint find_Name_and_val {var'} t n
+  Fixpoint find_Name_and_val {var'} t (n : Name)
            {T : flat_type base_type_code}
     : interp_flat_type (fun _ => Name) T -> interp_flat_type var' T -> option (var' t) -> option (var' t)
     := match T with
-       | Tbase t' => fun n' v default => if Name_dec n n'
-                                         then cast_if_eq t' t v
-                                         else default
+       | Tbase t' => fun (n' : Name) v default
+                     => if dec (n = n')
+                        then cast_if_eq t' t v
+                        else default
        | Unit => fun _ _ default => default
        | Prod A B
          => fun (ab : interp_flat_type _ A * interp_flat_type _ B)
diff --git a/src/Reflection/Named/ContextProperties.v b/src/Reflection/Named/ContextProperties.v
index ace3a1115..d9bca2683 100644
--- a/src/Reflection/Named/ContextProperties.v
+++ b/src/Reflection/Named/ContextProperties.v
@@ -7,6 +7,7 @@ Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.ContextDefinitions.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Logic.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Tactics.SplitInContext.
@@ -16,12 +17,11 @@ Require Import Crypto.Util.Tactics.RewriteHyp.
 
 Section with_context.
   Context {base_type_code Name var} (Context : @Context base_type_code Name var)
-          (base_type_code_dec : forall x y : base_type_code, {x = y} + {x <> y})
-          (Name_dec : forall x y : Name, {x = y} + {x <> y})
+          (base_type_code_dec : DecidableRel (@eq base_type_code))
+          (Name_dec : DecidableRel (@eq Name))
           (ContextOk : ContextOk Context).
 
   Local Notation find_Name := (@find_Name base_type_code Name Name_dec).
-  Local Notation cast_if_eq := (@cast_if_eq base_type_code base_type_code_dec).
   Local Notation find_Name_and_val := (@find_Name_and_val base_type_code Name base_type_code_dec Name_dec).
 
   Let base_type_UIP_refl : forall t (p : t = t :> base_type_code), p = eq_refl.
@@ -199,10 +199,9 @@ Section with_context.
         {var' t n T N V default}
     : @find_Name_and_val var' t n T N V default
       = match @find_Name n T N with
-        | Some t' => match base_type_code_dec t t' with
-                     | left _ => @find_Name_and_val var' t n T N V None
-                     | right _ => None
-                     end
+        | Some t' => if dec (t = t')
+                     then @find_Name_and_val var' t n T N V None
+                     else None
         | None => default
         end.
   Proof.
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v
index b01fe3627..5801a1c57 100644
--- a/src/Util/Decidable.v
+++ b/src/Util/Decidable.v
@@ -156,3 +156,16 @@ Ltac lazy_decide := abstract lazy_decide_no_check.
 
 (** For dubious compatibility with [eauto using]. *)
 Hint Extern 2 (Decidable _) => progress unfold Decidable : typeclass_instances core.
+
+Definition cast_if_eq {T} `{DecidableRel (@eq T)} {P} (t t' : T) (v : P t) : option (P t')
+  := match dec (t = t'), dec (t' = t') with
+     | left pf, left pf' => Some (eq_rect _ P v _ (eq_trans pf (eq_sym pf')))
+     | _, right pf' => match pf' eq_refl with end
+     | right pf, _ => None
+     end.
+
+Lemma cast_if_eq_refl {T H P} t v : @cast_if_eq T H P t t v = Some v.
+Proof.
+  compute; clear; destruct (H t t) as [ [] |e];
+    [ reflexivity | destruct (e eq_refl) ].
+Qed.