From 78656baa06ed1daeb7ba90c2d429228516dc8475 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 26 Jun 2018 15:10:24 -0400 Subject: Add a couple of zrange lemmas --- src/Util/ZRange/BasicLemmas.v | 61 +++++++++++++++++++++++++++++++++++-------- src/Util/ZRange/Operations.v | 11 ++++++++ 2 files changed, 61 insertions(+), 11 deletions(-) (limited to 'src/Util/ZRange') diff --git a/src/Util/ZRange/BasicLemmas.v b/src/Util/ZRange/BasicLemmas.v index c5dcaa3d4..b8f9c7c66 100644 --- a/src/Util/ZRange/BasicLemmas.v +++ b/src/Util/ZRange/BasicLemmas.v @@ -1,7 +1,11 @@ Require Import Coq.ZArith.ZArith. +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.SplitMinMax. +Require Import Crypto.Util.Tactics.SpecializeBy. +Require Import Crypto.Util.Tactics.SpecializeAllWays. Require Import Crypto.Util.Notations. Require Import Crypto.Util.Tactics.DestructHead. @@ -11,17 +15,17 @@ Module ZRange. Local Notation eta v := r[ lower v ~> upper v ]. - Local Ltac t := - repeat first [ reflexivity - | progress destruct_head' zrange - | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt] - | progress split_min_max - | match goal with - | [ |- _ = _ :> zrange ] => apply f_equal2 - end - | omega - | solve [ auto ] ]. - + Local Ltac t_step := + first [ reflexivity + | progress destruct_head' zrange + | progress cbv -[Z.min Z.max Z.le Z.lt Z.ge Z.gt andb Z.leb Z.geb] in * + | progress split_min_max + | match goal with + | [ |- _ = _ :> zrange ] => apply f_equal2 + end + | omega + | solve [ auto ] ]. + Local Ltac t := repeat t_step. Lemma flip_flip v : flip (flip v) = v. Proof. destruct v; reflexivity. Qed. @@ -34,4 +38,39 @@ Module ZRange. Definition normalize_or v : normalize v = v \/ normalize v = flip v. Proof. t. Qed. + + Local Ltac t2_step := + first [ t_step + | rewrite !Bool.andb_true_iff + | rewrite !Z.leb_le + | rewrite !Z.leb_gt + | rewrite Bool.andb_true_iff in * + | rewrite Z.leb_le in * + | rewrite Z.leb_gt in * + | progress intros + | match goal with + | [ H : context[andb _ _ = true] |- _ ] => setoid_rewrite Bool.andb_true_iff in H + | [ |- context[andb _ _ = true] ] => setoid_rewrite Bool.andb_true_iff + | [ H : context[Z.leb _ _ = true] |- _ ] => setoid_rewrite Z.leb_le in H + | [ |- context[Z.leb _ _ = true] ] => setoid_rewrite Z.leb_le + | [ H : context[Z.leb _ _ = false] |- _ ] => setoid_rewrite Z.leb_gt in H + | [ |- context[Z.leb _ _ = false] ] => setoid_rewrite Z.leb_gt + | [ |- and _ _ ] => apply conj + | [ |- or _ (true = false) ] => left + | [ |- or _ (false = true) ] => left + | [ |- or _ (?x = ?x) ] => right + | [ H : true = false |- _ ] => exfalso; clear -H; discriminate + end + | progress specialize_by omega + | progress destruct_head'_or ]. + + Lemma is_bounded_by_iff_is_tighter_than r1 r2 + : (forall v, is_bounded_by_bool v r1 = true -> is_bounded_by_bool v r2 = true) + <-> (is_tighter_than_bool r1 r2 = true \/ goodb r1 = false). + Proof. repeat t2_step; specialize_all_ways; repeat t2_step. Qed. + + Lemma is_bounded_by_iff_is_tighter_than_good r1 r2 (Hgood : goodb r1 = true) + : (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. End ZRange. diff --git a/src/Util/ZRange/Operations.v b/src/Util/ZRange/Operations.v index 881a28a31..d17785f77 100644 --- a/src/Util/ZRange/Operations.v +++ b/src/Util/ZRange/Operations.v @@ -78,6 +78,12 @@ Module ZRange. => let (lx, ux) := x in let (ly, uy) := y in {| lower := Z.min 0 (Z.min lx ly) ; upper := Z.max 0 (Z.min ux uy) |}). + Definition lor_bounds : zrange -> zrange -> zrange + := extremization_bounds + (fun x y + => let (lx, ux) := x in + let (ly, uy) := y in + {| lower := Z.max lx ly ; upper := upper_lor_land_bounds ux uy |}). Definition split_bounds (r : zrange) (split_at : BinInt.Z) : zrange * zrange := if upper r