From f9b2da9dd012e0ee0548aa82e8a132abc6429d7d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 4 Mar 2019 17:26:45 -0500 Subject: Add some minor reflect things --- src/Util/ZRange.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/ZRange.v') 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. -- cgit v1.2.3