diff options
author | Jason Gross <jgross@mit.edu> | 2019-02-02 16:09:06 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2019-02-02 16:09:06 -0500 |
commit | cd1d339aa57c09abc716ef30a5a153ac5aadb563 (patch) | |
tree | d8aca7ff46b94860a49e5e4f0ccc6758f7ccd4d5 /src/Util/ZRange.v | |
parent | d26139a5ce27c5dd661df4ebaaa6526472f1bdd2 (diff) |
Add zrange_rect{,_Proper,_Proper_dep}
Diffstat (limited to 'src/Util/ZRange.v')
-rw-r--r-- | src/Util/ZRange.v | 16 |
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. |