diff options
| -rw-r--r-- | src/Util/Bool/Reflect.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index 0d31853fe..d4a0df069 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -234,12 +234,17 @@ Global Instance reflect_match_pair {A B} {P : A -> B -> Prop} {Pb : A -> B -> bo : reflect (let '(a, b) := x in P a b) (let '(a, b) := x in Pb a b) | 1. Proof. edestruct (_ : _ * _); assumption. Qed. -Global Instance reflect_if_bool {x : bool} {A B a b} {HA : reflect A a} {HB : reflect B b} - : reflect (if x then A else B) (if x then a else b) | 10 +Definition reflect_if_bool {x : bool} {A B a b} {HA : reflect A a} {HB : reflect B b} + : reflect (if x then A else B) (if x then a else b) := if x return reflect (if x then A else B) (if x then a else b) then HA else HB. +Hint Extern 1 (reflect _ (match ?x with true => ?a | false => ?b end)) +=> eapply (@reflect_if_bool x _ _ a b) : typeclass_instances. +Hint Extern 1 (reflect (match ?x with true => ?A | false => ?B end) _) +=> eapply (@reflect_if_bool x A B) : typeclass_instances. + Global Instance reflect_ex_forall_not : forall T (P:T->Prop) (exPb:bool) {d:reflect (exists b, P b) exPb}, reflect (forall b, ~ P b) (negb exPb). Proof. intros T P exPb d; destruct d; constructor; firstorder. |