diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-09 17:40:20 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-09 17:40:20 -0400 |
commit | 4d334608f7f8f5be98276c5f1904d7955e1b6f53 (patch) | |
tree | 14c79154a71fca6becdcaed11125d320fd25ae8f | |
parent | f731a49d3d79e63f986ab73f2198051c3ada0c76 (diff) |
Split off ZUtil.Stabilization, finish IsBoundedBy!
-rw-r--r-- | _CoqProject | 1 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 2 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 69 | ||||
-rw-r--r-- | src/Util/ZUtil/Stabilization.v | 121 |
4 files changed, 124 insertions, 69 deletions
diff --git a/_CoqProject b/_CoqProject index dba0fdcf4..e0e88e441 100644 --- a/_CoqProject +++ b/_CoqProject @@ -290,3 +290,4 @@ src/Util/Tactics/TransparentAssert.v src/Util/Tactics/UnifyAbstractReflexivity.v src/Util/Tactics/UniquePose.v src/Util/Tactics/VM.v +src/Util/ZUtil/Stabilization.v diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index 893f1d5d6..ab2a8ef43 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -56,7 +56,7 @@ Module Import Bounds. Definition max_abs_bound (x : t) : Z := Z.max (Z.abs (lower x)) (Z.abs (upper x)). Definition upper_lor_and_bounds (x y : Z) : Z - := 2^(1 + Z.log2_up (Z.max x y)) - 1. + := 2^(1 + Z.log2_up (Z.max x y)). Definition extreme_lor_land_bounds (x y : t) : t := let mx := max_abs_bound x in let my := max_abs_bound y in diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index c66880e46..415c65406 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -8,6 +8,7 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Stabilization. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.Tactics.DestructHead. @@ -118,74 +119,6 @@ Proof. repeat (apply Z.max_case_strong || apply Zabs_ind); omega. Qed. -Local Notation stabilizes_after x l := (exists b, forall n, l < n -> Z.testbit x n = b). - -Lemma stabilizes_after_Proper x - : Proper (Z.le ==> Basics.impl) (fun l => stabilizes_after x l). -Proof. - intros ?? H [b H']; exists b. - intros n H''; apply (H' n); omega. -Qed. - -Lemma stabilization_time (x:Z) : stabilizes_after x (Z.max (Z.log2 (Z.pred (- x))) (Z.log2 x)). -Proof. - destruct (Z_lt_le_dec x 0); eexists; intros; - [ eapply Z.bits_above_log2_neg | eapply Z.bits_above_log2]; lia. -Qed. - -Lemma stabilization_time_weaker (x:Z) : stabilizes_after x (Z.log2_up (Z.abs x)). -Proof. - eapply stabilizes_after_Proper; try apply stabilization_time. - repeat match goal with - | [ |- context[Z.abs _ ] ] => apply Zabs_ind; intro - | [ |- context[Z.log2 ?x] ] - => rewrite (Z.log2_nonpos x) by omega - | [ |- context[Z.log2_up ?x] ] - => rewrite (Z.log2_up_nonpos x) by omega - | _ => rewrite Z.max_r by auto with zarith - | _ => rewrite Z.max_l by auto with zarith - | _ => etransitivity; [ apply Z.le_log2_log2_up | omega ] - | _ => progress Z.replace_all_neg_with_pos - | [ H : 0 <= ?x |- _ ] - => assert (x = 0 \/ x = 1 \/ 1 < x) by omega; clear H; destruct_head' or; subst - | _ => omega - | _ => simpl; omega - | _ => rewrite Z.log2_up_eqn by assumption - | _ => progress change (Z.log2_up 1) with 0 - end. -Qed. - -Lemma land_stabilizes (a b la lb:Z) (Ha:stabilizes_after a la) (Hb:stabilizes_after b lb) : stabilizes_after (Z.land a b) (Z.max la lb). -Proof. - destruct Ha as [ba Hba]. destruct Hb as [bb Hbb]. - exists (andb ba bb); intros n Hn. - rewrite Z.land_spec, Hba, Hbb; trivial; lia. -Qed. - -Lemma lor_stabilizes (a b la lb:Z) (Ha:stabilizes_after a la) (Hb:stabilizes_after b lb) : stabilizes_after (Z.lor a b) (Z.max la lb). -Proof. - destruct Ha as [ba Hba]. destruct Hb as [bb Hbb]. - exists (orb ba bb); intros n Hn. - rewrite Z.lor_spec, Hba, Hbb; trivial; lia. -Qed. - -Local Arguments Z.pow !_ !_. -Local Arguments Z.log2_up !_. -Local Arguments Z.add !_ !_. -Lemma stabilizes_bounded (x l:Z) (H:stabilizes_after x l) (Hl : 0 <= l) : Z.abs x <= 2^(1 + l) - 1. -Proof. - rewrite Z.add_comm. - destruct H as [b H]. - destruct (Z_zerop x); subst; simpl. - { cut (0 < 2^(l + 1)); auto with zarith. } - assert (Hlt : forall n, l < n <-> l + 1 <= n) by (intro; omega). - apply Zabs_ind; intro. - { pose proof (Z.testbit_false_bound x (l + 1)) as Hf. - setoid_rewrite <- Z.le_ngt in Hf. - setoid_rewrite <- Hlt in Hf. - destruct b; specialize_by (omega || assumption); [ | omega ]. -Admitted. (* this theorem statement is just a guess, I don't know what the actual bound is *) - Local Existing Instances Z.log2_up_le_Proper Z.add_le_Proper. Lemma land_upper_lor_land_bounds a b : Z.abs (Z.land a b) <= Bounds.upper_lor_and_bounds (Z.abs a) (Z.abs b). diff --git a/src/Util/ZUtil/Stabilization.v b/src/Util/ZUtil/Stabilization.v new file mode 100644 index 000000000..4df0300da --- /dev/null +++ b/src/Util/ZUtil/Stabilization.v @@ -0,0 +1,121 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.SpecializeBy. + +Local Open Scope Z_scope. + +Local Notation stabilizes_after x l := (exists b, forall n, l < n -> Z.testbit x n = b). + +Lemma stabilizes_after_Proper x + : Proper (Z.le ==> Basics.impl) (fun l => stabilizes_after x l). +Proof. + intros ?? H [b H']; exists b. + intros n H''; apply (H' n); omega. +Qed. + +Lemma stabilization_time (x:Z) : stabilizes_after x (Z.max (Z.log2 (Z.pred (- x))) (Z.log2 x)). +Proof. + destruct (Z_lt_le_dec x 0); eexists; intros; + [ eapply Z.bits_above_log2_neg | eapply Z.bits_above_log2]; lia. +Qed. + +Lemma stabilization_time_weaker (x:Z) : stabilizes_after x (Z.log2_up (Z.abs x)). +Proof. + eapply stabilizes_after_Proper; try apply stabilization_time. + repeat match goal with + | [ |- context[Z.abs _ ] ] => apply Zabs_ind; intro + | [ |- context[Z.log2 ?x] ] + => rewrite (Z.log2_nonpos x) by omega + | [ |- context[Z.log2_up ?x] ] + => rewrite (Z.log2_up_nonpos x) by omega + | _ => rewrite Z.max_r by auto with zarith + | _ => rewrite Z.max_l by auto with zarith + | _ => etransitivity; [ apply Z.le_log2_log2_up | omega ] + | _ => progress Z.replace_all_neg_with_pos + | [ H : 0 <= ?x |- _ ] + => assert (x = 0 \/ x = 1 \/ 1 < x) by omega; clear H; destruct_head' or; subst + | _ => omega + | _ => simpl; omega + | _ => rewrite Z.log2_up_eqn by assumption + | _ => progress change (Z.log2_up 1) with 0 + end. +Qed. + +Lemma land_stabilizes (a b la lb:Z) (Ha:stabilizes_after a la) (Hb:stabilizes_after b lb) : stabilizes_after (Z.land a b) (Z.max la lb). +Proof. + destruct Ha as [ba Hba]. destruct Hb as [bb Hbb]. + exists (andb ba bb); intros n Hn. + rewrite Z.land_spec, Hba, Hbb; trivial; lia. +Qed. + +Lemma lor_stabilizes (a b la lb:Z) (Ha:stabilizes_after a la) (Hb:stabilizes_after b lb) : stabilizes_after (Z.lor a b) (Z.max la lb). +Proof. + destruct Ha as [ba Hba]. destruct Hb as [bb Hbb]. + exists (orb ba bb); intros n Hn. + rewrite Z.lor_spec, Hba, Hbb; trivial; lia. +Qed. + +Local Arguments Z.pow !_ !_. +Local Arguments Z.log2_up !_. +Local Arguments Z.add !_ !_. +Lemma testbit_nonneg_iff x + : (exists l, 0 <= l /\ forall n : Z, l < n -> Z.testbit x n = false) <-> 0 <= x. +Proof. + split; intro H. + { destruct H as [l [Hl H]]. + edestruct Z_lt_le_dec; [ | eassumption ]. + pose proof (fun pf n => Z.bits_above_log2_neg x n pf) as H'. + specialize_by (omega || assumption). + specialize (H (1 + Z.max l (Z.log2 (Z.pred (- x))))). + specialize (H' (1 + Z.max l (Z.log2 (Z.pred (- x))))). + specialize_by (apply Z.max_case_strong; omega). + congruence. } + { pose proof (fun n => Z.bits_above_log2 x n H) as Hf. + eexists; split; [ | eapply Hf ]; auto with zarith. } +Qed. + +Lemma stabilizes_bounded_pos (x l:Z) (H:stabilizes_after x l) (Hl : 0 <= l) (Hx : 0 < x) + : x <= 2^(l + 1) - 1. +Proof. + assert (Hlt : forall l n, l < n <-> l + 1 <= n) by (intros; omega). + destruct H as [b H]. + destruct (proj2 (testbit_nonneg_iff x)) as [l' [H0' H1']]; [ omega | ]. + pose proof (Z.testbit_false_bound x (l' + 1)) as Hf. + pose proof (Z.testbit_false_bound x (l + 1)) as Hf'. + pose proof (fun pf n => Z.bits_above_log2 x n pf) as Hf''. + pose proof (fun pf n => Z.log2_lt_pow2 x n pf) as Hlg. + specialize_by omega. + setoid_rewrite <- Z.le_ngt in Hf. + setoid_rewrite <- Z.le_ngt in Hf'. + setoid_rewrite <- Hlt in Hf; setoid_rewrite <- Hlt in Hf'; clear Hlt. + setoid_rewrite <- Hlg in Hf''; clear Hlg. + destruct b; specialize_by (omega || assumption); [ | omega ]. + specialize (H (1 + Z.max l l')). + specialize (H1' (1 + Z.max l l')). + specialize_by (apply Z.max_case_strong; omega). + congruence. +Qed. + +Lemma stabilizes_bounded (x l:Z) (H:stabilizes_after x l) (Hl : 0 <= l) : Z.abs x <= 2^(1 + l). +Proof. + assert (Hlt : forall l n, l < n <-> l + 1 <= n) by (intros; omega). + rewrite Z.add_comm. + destruct (Z_zerop x); subst; simpl. + { cut (0 < 2^(l + 1)); auto with zarith. } + apply Zabs_ind; intro. + { etransitivity; [ apply stabilizes_bounded_pos; eauto | ]; omega. } + { Z.replace_all_neg_with_pos. + destruct (Z.eq_dec x 1); subst. + { assert (1 < 2^(l+1)) by auto with zarith. + omega. } + { assert (H' : stabilizes_after (Z.pred x) l). + { destruct H as [b H]; exists (negb b). + do 2 let x := fresh in intro x; specialize (H x). + rewrite Z.bits_opp in H by omega. + destruct b; rewrite ?Bool.negb_true_iff, ?Bool.negb_false_iff in H; assumption. } + clear H. + apply stabilizes_bounded_pos in H'; auto; omega. } } +Qed. |