From 44b17c0317ea5afcb554149310a0356cadcc09fc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 5 Nov 2016 14:20:49 -0400 Subject: Add reflect_iff_gen to Bool.v --- src/Util/Bool.v | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/Util/Bool.v') diff --git a/src/Util/Bool.v b/src/Util/Bool.v index 7b94c503e..a59cf53f0 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -51,3 +51,9 @@ Definition pull_bool_if_dep {A B} (f : forall b : bool, A b -> B b) (b : bool) ( Definition pull_bool_if {A B} (f : A -> B) (b : bool) (x : A) (y : A) : (if b then f x else f y) = f (if b then x else y) := @pull_bool_if_dep (fun _ => A) (fun _ => B) (fun _ => f) b x y. + +Definition reflect_iff_gen {P b} : reflect P b -> forall b' : bool, (if b' then P else ~P) <-> b = b'. +Proof. + intros H; apply reflect_iff in H; intro b'; destruct b, b'; + intuition congruence. +Qed. -- cgit v1.2.3