Add zrange_rect{,_Proper,_Proper_dep}

1 files changed, 16 insertions, 0 deletions

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.