diff options
| author |  Jason Gross <jagro@google.com> | 2018-06-27 18:57:07 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-06-27 18:57:07 -0400 |
| commit | 0e65b08ae341df1a270c9f0cb68fcd65463355d6 (patch) | |
| tree | 38d1dd2859e9621974db0114bac62fb3a5c63d5b /src/Util/ZRange | |
| parent | b6c63111a6e84f2affee3c162436722dcd6bcc43 (diff) | |
Add is_tighter_than_bool lemmas
Diffstat (limited to 'src/Util/ZRange')
| -rw-r--r-- | src/Util/ZRange/BasicLemmas.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index b8f9c7c66..e8565bcf3 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -1,8 +1,10 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.RelationClasses. Require Import Coq.omega.Omega. Require Import Coq.micromega.Lia. Require Import Crypto.Util.ZRange. Require Import Crypto.Util.ZRange.Operations. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.SplitMinMax. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SpecializeAllWays. @@ -12,6 +14,7 @@ Require Import Crypto.Util.Tactics.DestructHead. Module ZRange. Import Operations.ZRange. Local Open Scope zrange_scope. + Local Coercion is_true : bool >-> Sortclass. Local Notation eta v := r[ lower v ~> upper v ]. @@ -73,4 +76,15 @@ Module ZRange. : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true) <-> (is_tighter_than_bool r1 r2 = true). Proof. rewrite is_bounded_by_iff_is_tighter_than; intuition (congruence || auto). Qed. + + Global Instance is_tighter_than_bool_Reflexive : Reflexive is_tighter_than_bool. + Proof. + cbv [is_tighter_than_bool is_true]; cbn [lower upper]; repeat intro. + rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; reflexivity. + Qed. + Global Instance is_tighter_than_bool_Transitive : Transitive is_tighter_than_bool. + Proof. + cbv [is_tighter_than_bool is_true]; cbn [lower upper]; repeat intro. + rewrite ?Bool.andb_true_iff, ?Z.leb_le_iff in *; repeat apply conj; etransitivity; destruct_head'_and; eassumption. + Qed. End ZRange. |