From fa089c9028eca922a4ecf5941fb77cb4a7149532 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 14 Mar 2017 14:17:08 -0400 Subject: Move find_if_eq to Decidable.v, use Decidable in Named --- src/Util/Decidable.v | 13 +++++++++++++ 1 file changed, 13 insertions(+) (limited to 'src/Util/Decidable.v') 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. -- cgit v1.2.3