diff options
author | Jason Gross <jgross@mit.edu> | 2019-03-04 17:26:45 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-03-04 17:26:45 -0500 |
commit | f9b2da9dd012e0ee0548aa82e8a132abc6429d7d (patch) | |
tree | 7936f3736894a01af07bc7108082c30bc9700b5a /src/Util | |
parent | 9a6b540adee6440f36ce83c826ec291697f0dcf2 (diff) |
Add some minor reflect things
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Bool/Reflect.v | 1 | ||||
-rw-r--r-- | src/Util/ZRange.v | 4 |
2 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/Bool/Reflect.v b/src/Util/Bool/Reflect.v index d9e93fe93..8a5333f0a 100644 --- a/src/Util/Bool/Reflect.v +++ b/src/Util/Bool/Reflect.v @@ -69,6 +69,7 @@ Ltac beq_to_eq beq bl lb := Existing Class reflect. Definition decb (P : Prop) {b : bool} {H : reflect P b} := b. Notation reflect_rel P b := (forall x y, reflect (P x y) (b x y)). +Definition decb_rel {A B} (P : A -> B -> Prop) {b : A -> B -> bool} {H : reflect_rel P b} := b. Lemma decb_true_iff P {b} {H : reflect P b} : @decb P b H = true <-> P. Proof. symmetry; apply reflect_iff, H. Qed. diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index ae3c71ef4..0258e5c8e 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -2,6 +2,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.ZArith.ZArith. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Bool.Reflect. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. @@ -98,6 +99,9 @@ Proof. subst; split; reflexivity. Qed. +Global Instance reflect_zrange_eq : reflect_rel (@eq zrange) zrange_beq | 10. +Proof. apply reflect_of_beq; auto using zrange_bl, zrange_lb. Qed. + Global Instance zrange_rect_Proper {P} : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@zrange_rect (fun _ => P)) | 10. Proof. |