diff options
author | Jason Gross <jgross@mit.edu> | 2017-03-14 14:17:08 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-03-14 14:17:08 -0400 |
commit | fa089c9028eca922a4ecf5941fb77cb4a7149532 (patch) | |
tree | ec7c6d2ad3c44e290123ecaafa76972fb521ad18 /src | |
parent | 7a3740e056dcd0ca644eea443d7d87fb72df5aee (diff) |
Move find_if_eq to Decidable.v, use Decidable in Named
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Named/ContextDefinitions.v | 28 | ||||
-rw-r--r-- | src/Reflection/Named/ContextProperties.v | 13 | ||||
-rw-r--r-- | src/Util/Decidable.v | 13 |
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. |