From cd1d339aa57c09abc716ef30a5a153ac5aadb563 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 2 Feb 2019 16:09:06 -0500 Subject: Add zrange_rect{,_Proper,_Proper_dep} --- src/Util/ZRange.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/Util') diff --git a/src/Util/ZRange.v b/src/Util/ZRange.v index 8badcb492..ae3c71ef4 100644 --- a/src/Util/ZRange.v +++ b/src/Util/ZRange.v @@ -1,9 +1,12 @@ +Require Import Coq.Classes.Morphisms. Require Import Coq.ZArith.ZArith. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. Delimit Scope zrange_scope with zrange. +Local Set Nonrecursive Elimination Schemes. (* COQBUG(https://github.com/coq/coq/issues/7835) *) (* Local Set Boolean Equality Schemes. @@ -95,6 +98,19 @@ Proof. subst; split; reflexivity. Qed. +Global Instance zrange_rect_Proper {P} + : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq) (@zrange_rect (fun _ => P)) | 10. +Proof. + cbv [pointwise_relation zrange_rect]; repeat intro; subst; break_innermost_match; eauto. +Qed. + +Global Instance zrange_rect_Proper_dep {P} + : Proper (forall_relation (fun _ => forall_relation (fun _ => eq)) ==> forall_relation (fun _ => eq)) + (@zrange_rect P) | 10. +Proof. + cbv [forall_relation zrange_rect]; repeat intro; subst; break_innermost_match; eauto. +Qed. + Module Export Notations. Delimit Scope zrange_scope with zrange. Notation "r[ l ~> u ]" := {| lower := l ; upper := u |} : zrange_scope. -- cgit v1.2.3