diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZAdd.v | 32 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 110 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 35 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 7 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 1908 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivEucl.v | 17 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivFloor.v | 17 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZDivTrunc.v | 15 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZGcd.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZLcm.v | 37 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 16 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZParity.v | 160 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZPow.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 5 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZSgnAbs.v | 38 |
16 files changed, 2152 insertions, 277 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index 2c386a980..f95dcc76f 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -16,23 +16,24 @@ Include ZBaseProp Z. (** Theorems that are either not valid on N or have different proofs on N and Z *) +Hint Rewrite opp_0 : nz. + Theorem add_pred_l : forall n m, P n + m == P (n + m). Proof. intros n m. rewrite <- (succ_pred n) at 2. -rewrite add_succ_l. now rewrite pred_succ. +now rewrite add_succ_l, pred_succ. Qed. Theorem add_pred_r : forall n m, n + P m == P (n + m). Proof. -intros n m; rewrite (add_comm n (P m)), (add_comm n m); -apply add_pred_l. +intros n m; rewrite 2 (add_comm n); apply add_pred_l. Qed. Theorem add_opp_r : forall n m, n + (- m) == n - m. Proof. nzinduct m. -rewrite opp_0; rewrite sub_0_r; now rewrite add_0_r. +now nzsimpl. intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd. Qed. @@ -43,7 +44,7 @@ Qed. Theorem sub_succ_l : forall n m, S n - m == S (n - m). Proof. -intros n m; do 2 rewrite <- add_opp_r; now rewrite add_succ_l. +intros n m; rewrite <- 2 add_opp_r; now rewrite add_succ_l. Qed. Theorem sub_pred_l : forall n m, P n - m == P (n - m). @@ -67,7 +68,7 @@ Qed. Theorem sub_diag : forall n, n - n == 0. Proof. nzinduct n. -now rewrite sub_0_r. +now nzsimpl. intro n. rewrite sub_succ_r, sub_succ_l; now rewrite pred_succ. Qed. @@ -88,20 +89,20 @@ Qed. Theorem add_sub_assoc : forall n m p, n + (m - p) == (n + m) - p. Proof. -intros n m p; do 2 rewrite <- add_opp_r; now rewrite add_assoc. +intros n m p; rewrite <- 2 add_opp_r; now rewrite add_assoc. Qed. Theorem opp_involutive : forall n, - (- n) == n. Proof. nzinduct n. -now do 2 rewrite opp_0. +now nzsimpl. intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd. Qed. Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m). Proof. intros n m; nzinduct n. -rewrite opp_0; now do 2 rewrite add_0_l. +now nzsimpl. intro n. rewrite add_succ_l; do 2 rewrite opp_succ; rewrite add_pred_l. now rewrite pred_inj_wd. Qed. @@ -114,7 +115,7 @@ Qed. Theorem opp_inj : forall n m, - n == - m -> n == m. Proof. -intros n m H. apply opp_wd in H. now do 2 rewrite opp_involutive in H. +intros n m H. apply opp_wd in H. now rewrite 2 opp_involutive in H. Qed. Theorem opp_inj_wd : forall n m, - n == - m <-> n == m. @@ -135,7 +136,7 @@ Qed. Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. Proof. intros n m p; rewrite <- add_opp_r, opp_add_distr, add_assoc. -now do 2 rewrite add_opp_r. +now rewrite 2 add_opp_r. Qed. Theorem sub_sub_distr : forall n m p, n - (m - p) == (n - m) + p. @@ -146,7 +147,7 @@ Qed. Theorem sub_opp_l : forall n m, - n - m == - m - n. Proof. -intros n m. do 2 rewrite <- add_opp_r. now rewrite add_comm. +intros n m. rewrite <- 2 add_opp_r. now rewrite add_comm. Qed. Theorem sub_opp_r : forall n m, n - (- m) == n + m. @@ -163,7 +164,7 @@ Qed. Theorem sub_cancel_l : forall n m p, n - m == n - p <-> m == p. Proof. intros n m p. rewrite <- (add_cancel_l (n - m) (n - p) (- n)). -do 2 rewrite add_sub_assoc. rewrite add_opp_diag_l; do 2 rewrite sub_0_l. +rewrite 2 add_sub_assoc. rewrite add_opp_diag_l; rewrite 2 sub_0_l. apply opp_inj_wd. Qed. @@ -250,6 +251,11 @@ Proof. intros; now rewrite <- sub_sub_distr, sub_diag, sub_0_r. Qed. +Theorem sub_add : forall n m, m - n + n == m. +Proof. + intros. now rewrite <- add_sub_swap, add_simpl_r. +Qed. + (** Now we have two sums or differences; the name includes the two operators and the position of the terms being canceled *) diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index b5ca908b4..423cdf585 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -18,173 +18,163 @@ Include ZOrderProp Z. Theorem add_neg_neg : forall n m, n < 0 -> m < 0 -> n + m < 0. Proof. -intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_mono. +intros. rewrite <- (add_0_l 0). now apply add_lt_mono. Qed. Theorem add_neg_nonpos : forall n m, n < 0 -> m <= 0 -> n + m < 0. Proof. -intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_lt_le_mono. +intros. rewrite <- (add_0_l 0). now apply add_lt_le_mono. Qed. Theorem add_nonpos_neg : forall n m, n <= 0 -> m < 0 -> n + m < 0. Proof. -intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_lt_mono. +intros. rewrite <- (add_0_l 0). now apply add_le_lt_mono. Qed. Theorem add_nonpos_nonpos : forall n m, n <= 0 -> m <= 0 -> n + m <= 0. Proof. -intros n m H1 H2. rewrite <- (add_0_l 0). now apply add_le_mono. +intros. rewrite <- (add_0_l 0). now apply add_le_mono. Qed. (** Sub and order *) Theorem lt_0_sub : forall n m, 0 < m - n <-> n < m. Proof. -intros n m. stepl (0 + n < m - n + n) by symmetry; apply add_lt_mono_r. -rewrite add_0_l; now rewrite sub_simpl_r. +intros n m. now rewrite (add_lt_mono_r _ _ n), add_0_l, sub_simpl_r. Qed. Notation sub_pos := lt_0_sub (only parsing). Theorem le_0_sub : forall n m, 0 <= m - n <-> n <= m. Proof. -intros n m; stepl (0 + n <= m - n + n) by symmetry; apply add_le_mono_r. -rewrite add_0_l; now rewrite sub_simpl_r. +intros n m. now rewrite (add_le_mono_r _ _ n), add_0_l, sub_simpl_r. Qed. Notation sub_nonneg := le_0_sub (only parsing). Theorem lt_sub_0 : forall n m, n - m < 0 <-> n < m. Proof. -intros n m. stepl (n - m + m < 0 + m) by symmetry; apply add_lt_mono_r. -rewrite add_0_l; now rewrite sub_simpl_r. +intros n m. now rewrite (add_lt_mono_r _ _ m), add_0_l, sub_simpl_r. Qed. Notation sub_neg := lt_sub_0 (only parsing). Theorem le_sub_0 : forall n m, n - m <= 0 <-> n <= m. Proof. -intros n m. stepl (n - m + m <= 0 + m) by symmetry; apply add_le_mono_r. -rewrite add_0_l; now rewrite sub_simpl_r. +intros n m. now rewrite (add_le_mono_r _ _ m), add_0_l, sub_simpl_r. Qed. Notation sub_nonpos := le_sub_0 (only parsing). Theorem opp_lt_mono : forall n m, n < m <-> - m < - n. Proof. -intros n m. stepr (m + - m < m + - n) by symmetry; apply add_lt_mono_l. -do 2 rewrite add_opp_r. rewrite sub_diag. symmetry; apply lt_0_sub. +intros n m. now rewrite <- lt_0_sub, <- add_opp_l, <- sub_opp_r, lt_0_sub. Qed. Theorem opp_le_mono : forall n m, n <= m <-> - m <= - n. Proof. -intros n m. stepr (m + - m <= m + - n) by symmetry; apply add_le_mono_l. -do 2 rewrite add_opp_r. rewrite sub_diag. symmetry; apply le_0_sub. +intros n m. now rewrite <- le_0_sub, <- add_opp_l, <- sub_opp_r, le_0_sub. Qed. Theorem opp_pos_neg : forall n, 0 < - n <-> n < 0. Proof. -intro n; rewrite (opp_lt_mono n 0); now rewrite opp_0. +intro n; now rewrite (opp_lt_mono n 0), opp_0. Qed. Theorem opp_neg_pos : forall n, - n < 0 <-> 0 < n. Proof. -intro n. rewrite (opp_lt_mono 0 n). now rewrite opp_0. +intro n. now rewrite (opp_lt_mono 0 n), opp_0. Qed. Theorem opp_nonneg_nonpos : forall n, 0 <= - n <-> n <= 0. Proof. -intro n; rewrite (opp_le_mono n 0); now rewrite opp_0. +intro n; now rewrite (opp_le_mono n 0), opp_0. Qed. Theorem opp_nonpos_nonneg : forall n, - n <= 0 <-> 0 <= n. Proof. -intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0. +intro n. now rewrite (opp_le_mono 0 n), opp_0. Qed. -Theorem lt_m1_0 : -(1) < 0. +Theorem lt_m1_0 : -1 < 0. Proof. apply opp_neg_pos, lt_0_1. Qed. Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n. Proof. -intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l. -apply opp_lt_mono. +intros. now rewrite <- 2 add_opp_r, <- add_lt_mono_l, opp_lt_mono. Qed. Theorem sub_lt_mono_r : forall n m p, n < m <-> n - p < m - p. Proof. -intros n m p; do 2 rewrite <- add_opp_r; apply add_lt_mono_r. +intros. now rewrite <- 2 add_opp_r, add_lt_mono_r. Qed. Theorem sub_lt_mono : forall n m p q, n < m -> q < p -> n - p < m - q. Proof. intros n m p q H1 H2. apply lt_trans with (m - p); -[now apply -> sub_lt_mono_r | now apply -> sub_lt_mono_l]. +[now apply sub_lt_mono_r | now apply sub_lt_mono_l]. Qed. Theorem sub_le_mono_l : forall n m p, n <= m <-> p - m <= p - n. Proof. -intros n m p; do 2 rewrite <- add_opp_r; rewrite <- add_le_mono_l; -apply opp_le_mono. +intros. now rewrite <- 2 add_opp_r, <- add_le_mono_l, opp_le_mono. Qed. Theorem sub_le_mono_r : forall n m p, n <= m <-> n - p <= m - p. Proof. -intros n m p; do 2 rewrite <- add_opp_r; apply add_le_mono_r. +intros. now rewrite <- 2 add_opp_r, add_le_mono_r. Qed. Theorem sub_le_mono : forall n m p q, n <= m -> q <= p -> n - p <= m - q. Proof. intros n m p q H1 H2. apply le_trans with (m - p); -[now apply -> sub_le_mono_r | now apply -> sub_le_mono_l]. +[now apply sub_le_mono_r | now apply sub_le_mono_l]. Qed. Theorem sub_lt_le_mono : forall n m p q, n < m -> q <= p -> n - p < m - q. Proof. intros n m p q H1 H2. apply lt_le_trans with (m - p); -[now apply -> sub_lt_mono_r | now apply -> sub_le_mono_l]. +[now apply sub_lt_mono_r | now apply sub_le_mono_l]. Qed. Theorem sub_le_lt_mono : forall n m p q, n <= m -> q < p -> n - p < m - q. Proof. intros n m p q H1 H2. apply le_lt_trans with (m - p); -[now apply -> sub_le_mono_r | now apply -> sub_lt_mono_l]. +[now apply sub_le_mono_r | now apply sub_lt_mono_l]. Qed. Theorem le_lt_sub_lt : forall n m p q, n <= m -> p - n < q - m -> p < q. Proof. intros n m p q H1 H2. apply (le_lt_add_lt (- m) (- n)); -[now apply -> opp_le_mono | now do 2 rewrite add_opp_r]. +[now apply -> opp_le_mono | now rewrite 2 add_opp_r]. Qed. Theorem lt_le_sub_lt : forall n m p q, n < m -> p - n <= q - m -> p < q. Proof. intros n m p q H1 H2. apply (lt_le_add_lt (- m) (- n)); -[now apply -> opp_lt_mono | now do 2 rewrite add_opp_r]. +[now apply -> opp_lt_mono | now rewrite 2 add_opp_r]. Qed. Theorem le_le_sub_lt : forall n m p q, n <= m -> p - n <= q - m -> p <= q. Proof. intros n m p q H1 H2. apply (le_le_add_le (- m) (- n)); -[now apply -> opp_le_mono | now do 2 rewrite add_opp_r]. +[now apply -> opp_le_mono | now rewrite 2 add_opp_r]. Qed. Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p. Proof. -intros n m p. stepl (n + p - p < m - p) by symmetry; apply sub_lt_mono_r. -now rewrite add_simpl_r. +intros n m p. now rewrite (sub_lt_mono_r _ _ p), add_simpl_r. Qed. Theorem le_add_le_sub_r : forall n m p, n + p <= m <-> n <= m - p. Proof. -intros n m p. stepl (n + p - p <= m - p) by symmetry; apply sub_le_mono_r. -now rewrite add_simpl_r. +intros n m p. now rewrite (sub_le_mono_r _ _ p), add_simpl_r. Qed. Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n. @@ -199,14 +189,12 @@ Qed. Theorem lt_sub_lt_add_r : forall n m p, n - p < m <-> n < m + p. Proof. -intros n m p. stepl (n - p + p < m + p) by symmetry; apply add_lt_mono_r. -now rewrite sub_simpl_r. +intros n m p. now rewrite (add_lt_mono_r _ _ p), sub_simpl_r. Qed. Theorem le_sub_le_add_r : forall n m p, n - p <= m <-> n <= m + p. Proof. -intros n m p. stepl (n - p + p <= m + p) by symmetry; apply add_le_mono_r. -now rewrite sub_simpl_r. +intros n m p. now rewrite (add_le_mono_r _ _ p), sub_simpl_r. Qed. Theorem lt_sub_lt_add_l : forall n m p, n - m < p <-> n < m + p. @@ -221,74 +209,68 @@ Qed. Theorem lt_sub_lt_add : forall n m p q, n - m < p - q <-> n + q < m + p. Proof. -intros n m p q. rewrite lt_sub_lt_add_l. rewrite add_sub_assoc. -now rewrite <- lt_add_lt_sub_r. +intros n m p q. now rewrite lt_sub_lt_add_l, add_sub_assoc, <- lt_add_lt_sub_r. Qed. Theorem le_sub_le_add : forall n m p q, n - m <= p - q <-> n + q <= m + p. Proof. -intros n m p q. rewrite le_sub_le_add_l. rewrite add_sub_assoc. -now rewrite <- le_add_le_sub_r. +intros n m p q. now rewrite le_sub_le_add_l, add_sub_assoc, <- le_add_le_sub_r. Qed. Theorem lt_sub_pos : forall n m, 0 < m <-> n - m < n. Proof. -intros n m. stepr (n - m < n - 0) by now rewrite sub_0_r. apply sub_lt_mono_l. +intros n m. now rewrite (sub_lt_mono_l _ _ n), sub_0_r. Qed. Theorem le_sub_nonneg : forall n m, 0 <= m <-> n - m <= n. Proof. -intros n m. stepr (n - m <= n - 0) by now rewrite sub_0_r. apply sub_le_mono_l. +intros n m. now rewrite (sub_le_mono_l _ _ n), sub_0_r. Qed. Theorem sub_lt_cases : forall n m p q, n - m < p - q -> n < m \/ q < p. Proof. -intros n m p q H. rewrite lt_sub_lt_add in H. now apply add_lt_cases. +intros. now apply add_lt_cases, lt_sub_lt_add. Qed. Theorem sub_le_cases : forall n m p q, n - m <= p - q -> n <= m \/ q <= p. Proof. -intros n m p q H. rewrite le_sub_le_add in H. now apply add_le_cases. +intros. now apply add_le_cases, le_sub_le_add. Qed. Theorem sub_neg_cases : forall n m, n - m < 0 -> n < 0 \/ 0 < m. Proof. -intros n m H; rewrite <- add_opp_r in H. -setoid_replace (0 < m) with (- m < 0) using relation iff by (symmetry; apply opp_neg_pos). -now apply add_neg_cases. +intros. +rewrite <- (opp_neg_pos m). apply add_neg_cases. now rewrite add_opp_r. Qed. Theorem sub_pos_cases : forall n m, 0 < n - m -> 0 < n \/ m < 0. Proof. -intros n m H; rewrite <- add_opp_r in H. -setoid_replace (m < 0) with (0 < - m) using relation iff by (symmetry; apply opp_pos_neg). -now apply add_pos_cases. +intros. +rewrite <- (opp_pos_neg m). apply add_pos_cases. now rewrite add_opp_r. Qed. Theorem sub_nonpos_cases : forall n m, n - m <= 0 -> n <= 0 \/ 0 <= m. Proof. -intros n m H; rewrite <- add_opp_r in H. -setoid_replace (0 <= m) with (- m <= 0) using relation iff by (symmetry; apply opp_nonpos_nonneg). -now apply add_nonpos_cases. +intros. +rewrite <- (opp_nonpos_nonneg m). apply add_nonpos_cases. now rewrite add_opp_r. Qed. Theorem sub_nonneg_cases : forall n m, 0 <= n - m -> 0 <= n \/ m <= 0. Proof. -intros n m H; rewrite <- add_opp_r in H. -setoid_replace (m <= 0) with (0 <= - m) using relation iff by (symmetry; apply opp_nonneg_nonpos). -now apply add_nonneg_cases. +intros. +rewrite <- (opp_nonneg_nonpos m). apply add_nonneg_cases. now rewrite add_opp_r. Qed. Section PosNeg. Variable P : Z.t -> Prop. -Hypothesis P_wd : Proper (Z.eq ==> iff) P. +Hypothesis P_wd : Proper (eq ==> iff) P. Theorem zero_pos_neg : P 0 -> (forall n, 0 < n -> P n /\ P (- n)) -> forall n, P n. Proof. intros H1 H2 n. destruct (lt_trichotomy n 0) as [H3 | [H3 | H3]]. -apply <- opp_pos_neg in H3. apply H2 in H3. destruct H3 as [_ H3]. +apply opp_pos_neg, H2 in H3. destruct H3 as [_ H3]. now rewrite opp_involutive in H3. now rewrite H3. apply H2 in H3; now destruct H3. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index f177755fa..237ac93ef 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -9,7 +9,7 @@ (************************************************************************) Require Export NZAxioms. -Require Import NZPow NZSqrt NZLog NZGcd NZDiv. +Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits. (** We obtain integers by postulating that successor of predecessor is identity. *) @@ -38,8 +38,15 @@ Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z). Axiom opp_succ : forall n, - (S n) == P (- n). End IsOpp. +Module Type OppCstNotation (Import A : NZAxiomsSig)(Import B : Opp A). + Notation "- 1" := (opp one). + Notation "- 2" := (opp two). +End OppCstNotation. + Module Type ZAxiomsMiniSig := NZOrdAxiomsSig <+ ZAxiom <+ Opp <+ IsOpp. -Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp. +Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp + <+ OppCstNotation. + (** Other functions and their specifications *) @@ -57,19 +64,9 @@ Module Type HasSgn (Import Z : ZAxiomsMiniSig'). Parameter Inline sgn : t -> t. Axiom sgn_null : forall n, n==0 -> sgn n == 0. Axiom sgn_pos : forall n, 0<n -> sgn n == 1. - Axiom sgn_neg : forall n, n<0 -> sgn n == -(1). + Axiom sgn_neg : forall n, n<0 -> sgn n == -1. End HasSgn. -(** Parity functions *) - -Module Type Parity (Import Z : ZAxiomsMiniSig'). - Parameter Inline even odd : t -> bool. - Definition Even n := exists m, n == 2*m. - Definition Odd n := exists m, n == 2*m+1. - Axiom even_spec : forall n, even n = true <-> Even n. - Axiom odd_spec : forall n, odd n = true <-> Odd n. -End Parity. - (** Divisions *) (** First, the usual Coq convention of Truncated-Toward-Bottom @@ -110,16 +107,18 @@ End QuotRemSpec. Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z. Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z. -(** For pow sqrt log2 gcd, the NZ axiomatizations are enough. *) +(** For all other functions, the NZ axiomatizations are enough. *) (** Let's group everything *) Module Type ZAxiomsSig := - ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity + ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn + <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd - <+ ZDiv <+ ZQuot. + <+ ZDiv <+ ZQuot <+ NZBits.NZBits. Module Type ZAxiomsSig' := - ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity + ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn + <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' - <+ ZDiv' <+ ZQuot'. + <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index f9bd8dba3..4afc10201 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -19,7 +19,7 @@ Include NZProp Z. Theorem pred_inj : forall n m, P n == P m -> n == m. Proof. -intros n m H. apply succ_wd in H. now do 2 rewrite succ_pred in H. +intros n m H. apply succ_wd in H. now rewrite 2 succ_pred in H. Qed. Theorem pred_inj_wd : forall n1 n2, P n1 == P n2 <-> n1 == n2. @@ -27,5 +27,10 @@ Proof. intros n1 n2; split; [apply pred_inj | apply pred_wd]. Qed. +Lemma succ_m1 : S (-1) == 0. +Proof. + now rewrite one_succ, opp_succ, opp_0, succ_pred. +Qed. + End ZBaseProp. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v new file mode 100644 index 000000000..44cd08e67 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -0,0 +1,1908 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import + Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog. + +(** Derived properties of bitwise operations *) + +Module Type ZBitsProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZParityProp A B) + (Import D : ZSgnAbsProp A B) + (Import E : ZPowProp A B C D) + (Import F : ZDivProp A B D) + (Import G : NZLog2Prop A A A B E). + +Include BoolEqualityFacts A. + +Ltac order_nz := try apply pow_nonzero; order'. +Ltac order_pos' := try apply abs_nonneg; order_pos. +Hint Rewrite div_0_l mod_0_l div_1_r mod_1_r : nz. + +(** Some properties of power and division *) + +Lemma pow_sub_r : forall a b c, a~=0 -> 0<=c<=b -> a^(b-c) == a^b / a^c. +Proof. + intros a b c Ha (H,H'). rewrite <- (sub_simpl_r b c) at 2. + rewrite pow_add_r; trivial. + rewrite div_mul. reflexivity. + now apply pow_nonzero. + now apply le_0_sub. +Qed. + +Lemma pow_div_l : forall a b c, b~=0 -> 0<=c -> a mod b == 0 -> + (a/b)^c == a^c / b^c. +Proof. + intros a b c Hb Hc H. rewrite (div_mod a b Hb) at 2. + rewrite H, add_0_r, pow_mul_l, mul_comm, div_mul. reflexivity. + now apply pow_nonzero. +Qed. + +(** An injection from bits [true] and [false] to numbers 1 and 0. + We declare it as a (local) coercion for shorter statements. *) + +Definition b2z (b:bool) := if b then 1 else 0. +Local Coercion b2z : bool >-> t. + +(** Alternative caracterisations of [testbit] *) + +Lemma testbit_spec' : forall a n, 0<=n -> a.[n] == (a / 2^n) mod 2. +Proof. + intros a n Hn. + destruct (testbit_spec a n Hn) as (l & h & H & EQ). fold (b2z a.[n]) in EQ. + apply mod_unique with h. left. destruct a.[n]; split; simpl; order'. + symmetry. apply div_unique with l. now left. + now rewrite add_comm, mul_comm, (add_comm (2*h)). +Qed. + +Lemma testbit_true : forall a n, 0<=n -> + (a.[n] = true <-> (a / 2^n) mod 2 == 1). +Proof. + intros a n Hn. + rewrite <- testbit_spec' by trivial. + destruct a.[n]; split; simpl; now try order'. +Qed. + +Lemma testbit_false : forall a n, 0<=n -> + (a.[n] = false <-> (a / 2^n) mod 2 == 0). +Proof. + intros a n Hn. + rewrite <- testbit_spec' by trivial. + destruct a.[n]; split; simpl; now try order'. +Qed. + +Lemma testbit_eqb : forall a n, 0<=n -> + a.[n] = eqb ((a / 2^n) mod 2) 1. +Proof. + intros a n Hn. + apply eq_true_iff_eq. now rewrite testbit_true, eqb_eq. +Qed. + +(** testbit is hence a morphism *) + +Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. +Proof. + intros a a' Ha n n' Hn. + destruct (le_gt_cases 0 n), (le_gt_cases 0 n'); try order. + now rewrite 2 testbit_eqb, Ha, Hn by trivial. + now rewrite 2 testbit_neg_r by trivial. +Qed. + +(** Results about the injection [b2z] *) + +Lemma b2z_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0. +Proof. + intros [|] [|]; simpl; trivial; order'. +Qed. + +Lemma add_b2z_double_div2 : forall (a0:bool) a, (a0+2*a)/2 == a. +Proof. + intros a0 a. rewrite mul_comm, div_add by order'. + now rewrite div_small, add_0_l by (destruct a0; split; simpl; order'). +Qed. + +Lemma add_b2z_double_bit0 : forall (a0:bool) a, (a0+2*a).[0] = a0. +Proof. + intros a0 a. apply b2z_inj. + rewrite testbit_spec' by order. + nzsimpl. rewrite mul_comm, mod_add by order'. + now rewrite mod_small by (destruct a0; split; simpl; order'). +Qed. + +Lemma b2z_div2 : forall (a0:bool), a0/2 == 0. +Proof. + intros a0. rewrite <- (add_b2z_double_div2 a0 0). now nzsimpl. +Qed. + +Lemma b2z_bit0 : forall (a0:bool), a0.[0] = a0. +Proof. + intros a0. rewrite <- (add_b2z_double_bit0 a0 0) at 2. now nzsimpl. +Qed. + +(** The initial specification of testbit is complete *) + +Lemma testbit_unique : forall a n (a0:bool) l h, + 0<=l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0. +Proof. + intros a n a0 l h Hl EQ. + assert (0<=n). + destruct (le_gt_cases 0 n) as [Hn|Hn]; trivial. + rewrite pow_neg_r in Hl by trivial. destruct Hl; order. + apply b2z_inj. rewrite testbit_spec' by trivial. + symmetry. apply mod_unique with h. + left; destruct a0; simpl; split; order'. + symmetry. apply div_unique with l. + now left. + now rewrite add_comm, (add_comm _ a0), mul_comm. +Qed. + +(** All bits of number 0 are 0 *) + +Lemma bits_0 : forall n, 0.[n] = false. +Proof. + intros n. + destruct (le_gt_cases 0 n). + apply testbit_false; trivial. nzsimpl; order_nz. + now apply testbit_neg_r. +Qed. + +(** For negative numbers, we are actually doing two's complement *) + +Lemma bits_opp : forall a n, 0<=n -> (-a).[n] = negb (P a).[n]. +Proof. + intros a n Hn. + destruct (testbit_spec (-a) n Hn) as (l & h & Hl & EQ). + fold (b2z (-a).[n]) in EQ. + apply negb_sym. + apply testbit_unique with (2^n-l-1) (-h-1). + split. + apply lt_succ_r. rewrite sub_1_r, succ_pred. now apply lt_0_sub. + apply le_succ_l. rewrite sub_1_r, succ_pred. apply le_sub_le_add_r. + rewrite <- (add_0_r (2^n)) at 1. now apply add_le_mono_l. + rewrite <- add_sub_swap, sub_1_r. apply pred_wd. + apply opp_inj. rewrite opp_add_distr, opp_sub_distr. + rewrite (add_comm _ l), <- add_assoc. + rewrite EQ at 1. apply add_cancel_l. + rewrite <- opp_add_distr. + rewrite <- (mul_1_l (2^n)) at 2. rewrite <- mul_add_distr_r. + rewrite <- mul_opp_l. + apply mul_wd; try reflexivity. + rewrite !opp_add_distr. + rewrite <- mul_opp_r. + rewrite opp_sub_distr, opp_involutive. + rewrite (add_comm h). + rewrite mul_add_distr_l. + rewrite !add_assoc. + apply add_cancel_r. + rewrite mul_1_r. + rewrite add_comm, add_assoc, !add_opp_r, sub_1_r, two_succ, pred_succ. + destruct (-a).[n]; simpl. now rewrite sub_0_r. now nzsimpl'. +Qed. + +(** All bits of number (-1) are 1 *) + +Lemma bits_m1 : forall n, 0<=n -> (-1).[n] = true. +Proof. + intros. now rewrite bits_opp, one_succ, pred_succ, bits_0. +Qed. + +(** Various ways to refer to the lowest bit of a number *) + +Lemma bit0_mod : forall a, a.[0] == a mod 2. +Proof. + intros a. rewrite testbit_spec' by order. now nzsimpl. +Qed. + +Lemma bit0_eqb : forall a, a.[0] = eqb (a mod 2) 1. +Proof. + intros a. rewrite testbit_eqb by order. now nzsimpl. +Qed. + +Lemma bit0_odd : forall a, a.[0] = odd a. +Proof. + intros. rewrite bit0_eqb by order. + apply eq_true_iff_eq. rewrite eqb_eq, odd_spec. split. + intros H. exists (a/2). rewrite <- H. apply div_mod. order'. + intros (b,H). + rewrite H, add_comm, mul_comm, mod_add, mod_small; try split; order'. +Qed. + +(** Hence testing a bit is equivalent to shifting and testing parity *) + +Lemma testbit_odd : forall a n, a.[n] = odd (a>>n). +Proof. + intros. now rewrite <- bit0_odd, shiftr_spec, add_0_l. +Qed. + +(** [log2] gives the highest nonzero bit of positive numbers *) + +Lemma bit_log2 : forall a, 0<a -> a.[log2 a] = true. +Proof. + intros a Ha. + assert (Ha' := log2_nonneg a). + destruct (log2_spec_alt a Ha) as (r & EQ & Hr). + rewrite EQ at 1. + rewrite testbit_true, add_comm by trivial. + rewrite <- (mul_1_l (2^log2 a)) at 1. + rewrite div_add by order_nz. + rewrite div_small; trivial. + rewrite add_0_l. apply mod_small. split; order'. +Qed. + +Lemma bits_above_log2 : forall a n, 0<=a -> log2 a < n -> + a.[n] = false. +Proof. + intros a n Ha H. + assert (Hn : 0<=n). + transitivity (log2 a). apply log2_nonneg. order'. + rewrite testbit_false by trivial. + rewrite div_small. nzsimpl; order'. + split. order. apply log2_lt_cancel. now rewrite log2_pow2. +Qed. + +(** Hence the number of bits of [a] is [1+log2 a] + (see [Psize] and [Psize_pos]). +*) + +(** For negative numbers, things are the other ways around: + log2 gives the highest zero bit (for numbers below -1). +*) + +Lemma bit_log2_neg : forall a, a < -1 -> a.[log2 (P (-a))] = false. +Proof. + intros a Ha. + rewrite <- (opp_involutive a) at 1. + rewrite bits_opp. + apply negb_false_iff. + apply bit_log2. + apply opp_lt_mono in Ha. rewrite opp_involutive in Ha. + apply lt_succ_lt_pred. now rewrite <- one_succ. + apply log2_nonneg. +Qed. + +Lemma bits_above_log2_neg : forall a n, a < 0 -> log2 (P (-a)) < n -> + a.[n] = true. +Proof. + intros a n Ha H. + assert (Hn : 0<=n). + transitivity (log2 (P (-a))). apply log2_nonneg. order'. + rewrite <- (opp_involutive a), bits_opp, negb_true_iff by trivial. + apply bits_above_log2; trivial. + now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. +Qed. + +(** Accesing a high enough bit of a number gives its sign *) + +Lemma bits_iff_nonneg : forall a n, log2 (abs a) < n -> + (0<=a <-> a.[n] = false). +Proof. + intros a n Hn. split; intros H. + rewrite abs_eq in Hn; trivial. now apply bits_above_log2. + destruct (le_gt_cases 0 a); trivial. + rewrite abs_neq in Hn by order. + rewrite bits_above_log2_neg in H; try easy. + apply le_lt_trans with (log2 (-a)); trivial. + apply log2_le_mono. apply le_pred_l. +Qed. + +Lemma bits_iff_nonneg' : forall a, + 0<=a <-> a.[S (log2 (abs a))] = false. +Proof. + intros. apply bits_iff_nonneg. apply lt_succ_diag_r. +Qed. + +Lemma bits_iff_nonneg_ex : forall a, + 0<=a <-> (exists k, forall m, k<m -> a.[m] = false). +Proof. + intros a. split. + intros Ha. exists (log2 a). intros m Hm. now apply bits_above_log2. + intros (k,Hk). destruct (le_gt_cases k (log2 (abs a))). + now apply bits_iff_nonneg', Hk, lt_succ_r. + apply (bits_iff_nonneg a (S k)). + now apply lt_succ_r, lt_le_incl. + apply Hk. apply lt_succ_diag_r. +Qed. + +Lemma bits_iff_neg : forall a n, log2 (abs a) < n -> + (a<0 <-> a.[n] = true). +Proof. + intros a n Hn. + now rewrite lt_nge, <- not_false_iff_true, (bits_iff_nonneg a n). +Qed. + +Lemma bits_iff_neg' : forall a, a<0 <-> a.[S (log2 (abs a))] = true. +Proof. + intros. apply bits_iff_neg. apply lt_succ_diag_r. +Qed. + +Lemma bits_iff_neg_ex : forall a, + a<0 <-> (exists k, forall m, k<m -> a.[m] = true). +Proof. + intros a. split. + intros Ha. exists (log2 (P (-a))). intros m Hm. now apply bits_above_log2_neg. + intros (k,Hk). destruct (le_gt_cases k (log2 (abs a))). + now apply bits_iff_neg', Hk, lt_succ_r. + apply (bits_iff_neg a (S k)). + now apply lt_succ_r, lt_le_incl. + apply Hk. apply lt_succ_diag_r. +Qed. + +(** Testing bits after division or multiplication by a power of two *) + +Lemma div2_bits : forall a n, 0<=n -> (a/2).[n] = a.[S n]. +Proof. + intros a n Hn. + apply eq_true_iff_eq. rewrite 2 testbit_true by order_pos. + rewrite pow_succ_r by trivial. + now rewrite div_div by order_pos. +Qed. + +Lemma div_pow2_bits : forall a n m, 0<=n -> 0<=m -> (a/2^n).[m] = a.[m+n]. +Proof. + intros a n m Hn. revert a m. apply le_ind with (4:=Hn). + solve_predicate_wd. + intros a m Hm. now nzsimpl. + clear n Hn. intros n Hn IH a m Hm. nzsimpl; trivial. + rewrite <- div_div by order_pos. + now rewrite IH, div2_bits by order_pos. +Qed. + +Lemma double_bits_succ : forall a n, (2*a).[S n] = a.[n]. +Proof. + intros a n. + destruct (le_gt_cases 0 n) as [Hn|Hn]. + now rewrite <- div2_bits, mul_comm, div_mul by order'. + rewrite (testbit_neg_r a n Hn). + apply le_succ_l, le_lteq in Hn. destruct Hn as [Hn|Hn]. + now rewrite testbit_neg_r. + now rewrite Hn, bit0_odd, odd_mul, odd_2. +Qed. + +Lemma double_bits : forall a n, (2*a).[n] = a.[P n]. +Proof. + intros a n. rewrite <- (succ_pred n) at 1. apply double_bits_succ. +Qed. + +Lemma mul_pow2_bits_add : forall a n m, 0<=n -> (a*2^n).[n+m] = a.[m]. +Proof. + intros a n m Hn. revert a m. apply le_ind with (4:=Hn). + solve_predicate_wd. + intros a m. now nzsimpl. + clear n Hn. intros n Hn IH a m. nzsimpl; trivial. + rewrite mul_assoc, (mul_comm _ 2), <- mul_assoc. + now rewrite double_bits_succ. +Qed. + +Lemma mul_pow2_bits : forall a n m, 0<=n -> (a*2^n).[m] = a.[m-n]. +Proof. + intros. + rewrite <- (add_simpl_r m n) at 1. rewrite add_sub_swap, add_comm. + now apply mul_pow2_bits_add. +Qed. + +Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false. +Proof. + intros. + destruct (le_gt_cases 0 n). + rewrite mul_pow2_bits by trivial. + apply testbit_neg_r. now apply lt_sub_0. + now rewrite pow_neg_r, mul_0_r, bits_0. +Qed. + +(** Selecting the low part of a number can be done by a modulo *) + +Lemma mod_pow2_bits_high : forall a n m, 0<=n<=m -> + (a mod 2^n).[m] = false. +Proof. + intros a n m (Hn,H). + destruct (mod_pos_bound a (2^n)) as [LE LT]. order_pos. + apply le_lteq in LE; destruct LE as [LT'|EQ]. + apply bits_above_log2; try order. + apply lt_le_trans with n; trivial. + apply log2_lt_pow2; trivial. + now rewrite <-EQ, bits_0. +Qed. + +Lemma mod_pow2_bits_low : forall a n m, m<n -> + (a mod 2^n).[m] = a.[m]. +Proof. + intros a n m H. + destruct (le_gt_cases 0 m) as [Hm|Hm]; [|now rewrite !testbit_neg_r]. + rewrite testbit_eqb; trivial. + rewrite <- (mod_add _ (2^(P (n-m))*(a/2^n))) by order'. + rewrite <- div_add by order_nz. + rewrite (mul_comm _ 2), mul_assoc, <- pow_succ_r, succ_pred. + rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add; trivial. + rewrite add_comm, <- div_mod by order_nz. + symmetry. apply testbit_eqb; trivial. + apply le_0_sub; order. + now apply lt_le_pred, lt_0_sub. +Qed. + +(** We now prove that having the same bits implies equality. + For that we use a notion of equality over functional + streams of bits. *) + +Definition eqf (f g:t -> bool) := forall n:t, f n = g n. + +Instance eqf_equiv : Equivalence eqf. +Proof. + split; congruence. +Qed. + +Local Infix "===" := eqf (at level 70, no associativity). + +Instance testbit_eqf : Proper (eq==>eqf) testbit. +Proof. + intros a a' Ha n. now rewrite Ha. +Qed. + +(** Only zero corresponds to the always-false stream. *) + +Lemma bits_inj_0 : + forall a, (forall n, a.[n] = false) -> a == 0. +Proof. + intros a H. destruct (lt_trichotomy a 0) as [Ha|[Ha|Ha]]; trivial. + apply (bits_above_log2_neg a (S (log2 (P (-a))))) in Ha. + now rewrite H in Ha. + apply lt_succ_diag_r. + apply bit_log2 in Ha. now rewrite H in Ha. +Qed. + +(** If two numbers produce the same stream of bits, they are equal. *) + +Lemma bits_inj : forall a b, testbit a === testbit b -> a == b. +Proof. + assert (AUX : forall n, 0<=n -> forall a b, + 0<=a<2^n -> testbit a === testbit b -> a == b). + intros n Hn. apply le_ind with (4:=Hn). + solve_predicate_wd. + intros a b Ha H. rewrite pow_0_r, one_succ, lt_succ_r in Ha. + assert (Ha' : a == 0) by (destruct Ha; order). + rewrite Ha' in *. + symmetry. apply bits_inj_0. + intros m. now rewrite <- H, bits_0. + clear n Hn. intros n Hn IH a b (Ha,Ha') H. + rewrite (div_mod a 2), (div_mod b 2) by order'. + apply add_wd; [ | now rewrite <- 2 bit0_mod, H]. + apply mul_wd. reflexivity. + apply IH. + split. apply div_pos; order'. + apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r. + intros m. + destruct (le_gt_cases 0 m). + rewrite 2 div2_bits by trivial. apply H. + now rewrite 2 testbit_neg_r. + intros a b H. + destruct (le_gt_cases 0 a) as [Ha|Ha]. + apply (AUX a); trivial. split; trivial. + apply pow_gt_lin_r; order'. + apply succ_inj, opp_inj. + assert (0 <= - S a). + apply opp_le_mono. now rewrite opp_involutive, opp_0, le_succ_l. + apply (AUX (-(S a))); trivial. split; trivial. + apply pow_gt_lin_r; order'. + intros m. destruct (le_gt_cases 0 m). + now rewrite 2 bits_opp, 2 pred_succ, H. + now rewrite 2 testbit_neg_r. +Qed. + +Lemma bits_inj_iff : forall a b, testbit a === testbit b <-> a == b. +Proof. + split. apply bits_inj. intros EQ; now rewrite EQ. +Qed. + +(** In fact, checking the bits at positive indexes is enough. *) + +Lemma bits_inj' : forall a b, + (forall n, 0<=n -> a.[n] = b.[n]) -> a == b. +Proof. + intros a b H. apply bits_inj. + intros n. destruct (le_gt_cases 0 n). + now apply H. + now rewrite 2 testbit_neg_r. +Qed. + +Lemma bits_inj_iff' : forall a b, (forall n, 0<=n -> a.[n] = b.[n]) <-> a == b. +Proof. + split. apply bits_inj'. intros EQ n Hn; now rewrite EQ. +Qed. + +Ltac bitwise := apply bits_inj'; intros ?m ?Hm; autorewrite with bitwise. + +Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. + +(** The streams of bits that correspond to a numbers are + exactly the ones which are stationary after some point. *) + +Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f -> + ((exists n, forall m, 0<=m -> f m = n.[m]) <-> + (exists k, forall m, k<=m -> f m = f k)). +Proof. + intros f Hf. split. + intros (a,H). + destruct (le_gt_cases 0 a). + exists (S (log2 a)). intros m Hm. apply le_succ_l in Hm. + rewrite 2 H, 2 bits_above_log2; trivial using lt_succ_diag_r. + order_pos. apply le_trans with (log2 a); order_pos. + exists (S (log2 (P (-a)))). intros m Hm. apply le_succ_l in Hm. + rewrite 2 H, 2 bits_above_log2_neg; trivial using lt_succ_diag_r. + order_pos. apply le_trans with (log2 (P (-a))); order_pos. + intros (k,Hk). + destruct (lt_ge_cases k 0) as [LT|LE]. + case_eq (f 0); intros H0. + exists (-1). intros m Hm. rewrite bits_m1, Hk by order. + symmetry; rewrite <- H0. apply Hk; order. + exists 0. intros m Hm. rewrite bits_0, Hk by order. + symmetry; rewrite <- H0. apply Hk; order. + revert f Hf Hk. apply le_ind with (4:=LE). + (* compat : solve_predicat_wd fails here *) + apply proper_sym_impl_iff. exact eq_sym. + clear k LE. intros k k' Hk IH f Hf H. apply IH; trivial. + now setoid_rewrite Hk. + (* /compat *) + intros f Hf H0. destruct (f 0). + exists (-1). intros m Hm. now rewrite bits_m1, H0. + exists 0. intros m Hm. now rewrite bits_0, H0. + clear k LE. intros k LE IH f Hf Hk. + destruct (IH (fun m => f (S m))) as (n, Hn). + solve_predicate_wd. + intros m Hm. apply Hk. now rewrite <- succ_le_mono. + exists (f 0 + 2*n). intros m Hm. + apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + rewrite <- (succ_pred m), Hn, <- div2_bits. + rewrite mul_comm, div_add, b2z_div2, add_0_l; trivial. order'. + now rewrite <- lt_succ_r, succ_pred. + now rewrite <- lt_succ_r, succ_pred. + rewrite <- Hm. + symmetry. apply add_b2z_double_bit0. +Qed. + +(** * Properties of shifts *) + +(** First, a unified specification for [shiftl] : the [shiftl_spec] + below (combined with [testbit_neg_r]) is equivalent to + [shiftl_spec_low] and [shiftl_spec_high]. *) + +Lemma shiftl_spec : forall a n m, 0<=m -> (a << n).[m] = a.[m-n]. +Proof. + intros. + destruct (le_gt_cases n m). + now apply shiftl_spec_high. + rewrite shiftl_spec_low, testbit_neg_r; trivial. now apply lt_sub_0. +Qed. + +(** A shiftl by a negative number is a shiftr, and vice-versa *) + +Lemma shiftr_opp_r : forall a n, a >> (-n) == a << n. +Proof. + intros. bitwise. now rewrite shiftr_spec, shiftl_spec, add_opp_r. +Qed. + +Lemma shiftl_opp_r : forall a n, a << (-n) == a >> n. +Proof. + intros. bitwise. now rewrite shiftr_spec, shiftl_spec, sub_opp_r. +Qed. + +(** Shifts correspond to multiplication or division by a power of two *) + +Lemma shiftr_div_pow2 : forall a n, 0<=n -> a >> n == a / 2^n. +Proof. + intros. bitwise. now rewrite shiftr_spec, div_pow2_bits. +Qed. + +Lemma shiftr_mul_pow2 : forall a n, n<=0 -> a >> n == a * 2^(-n). +Proof. + intros. bitwise. rewrite shiftr_spec, mul_pow2_bits; trivial. + now rewrite sub_opp_r. + now apply opp_nonneg_nonpos. +Qed. + +Lemma shiftl_mul_pow2 : forall a n, 0<=n -> a << n == a * 2^n. +Proof. + intros. bitwise. now rewrite shiftl_spec, mul_pow2_bits. +Qed. + +Lemma shiftl_div_pow2 : forall a n, n<=0 -> a << n == a / 2^(-n). +Proof. + intros. bitwise. rewrite shiftl_spec, div_pow2_bits; trivial. + now rewrite add_opp_r. + now apply opp_nonneg_nonpos. +Qed. + +(** Shifts are morphisms *) + +Instance shiftr_wd : Proper (eq==>eq==>eq) shiftr. +Proof. + intros a a' Ha n n' Hn. + destruct (le_ge_cases n 0) as [H|H]; assert (H':=H); rewrite Hn in H'. + now rewrite 2 shiftr_mul_pow2, Ha, Hn. + now rewrite 2 shiftr_div_pow2, Ha, Hn. +Qed. + +Instance shiftl_wd : Proper (eq==>eq==>eq) shiftl. +Proof. + intros a a' Ha n n' Hn. now rewrite <- 2 shiftr_opp_r, Ha, Hn. +Qed. + +(** We could also have specified shiftl with an addition on the left. *) + +Lemma shiftl_spec_alt : forall a n m, 0<=n -> (a << n).[m+n] = a.[m]. +Proof. + intros. now rewrite shiftl_mul_pow2, mul_pow2_bits, add_simpl_r. +Qed. + +(** Chaining several shifts. The only case for which + there isn't any simple expression is a true shiftr + followed by a true shiftl. +*) + +Lemma shiftl_shiftl : forall a n m, 0<=n -> + (a << n) << m == a << (n+m). +Proof. + intros a n p Hn. bitwise. + rewrite 2 (shiftl_spec _ _ m) by trivial. + rewrite add_comm, sub_add_distr. + destruct (le_gt_cases 0 (m-p)) as [H|H]. + now rewrite shiftl_spec. + rewrite 2 testbit_neg_r; trivial. + apply lt_sub_0. now apply lt_le_trans with 0. +Qed. + +Lemma shiftr_shiftl_l : forall a n m, 0<=n -> + (a << n) >> m == a << (n-m). +Proof. + intros. now rewrite <- shiftl_opp_r, shiftl_shiftl, add_opp_r. +Qed. + +Lemma shiftr_shiftl_r : forall a n m, 0<=n -> + (a << n) >> m == a >> (m-n). +Proof. + intros. now rewrite <- 2 shiftl_opp_r, shiftl_shiftl, opp_sub_distr, add_comm. +Qed. + +Lemma shiftr_shiftr : forall a n m, 0<=n -> 0<=m -> + (a >> n) >> m == a >> (n+m). +Proof. + intros a n m Hn Hm. + now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_pos. +Qed. + +(** shifts and constants *) + +Lemma shiftl_1_l : forall n, 1 << n == 2^n. +Proof. + intros n. destruct (le_gt_cases 0 n). + now rewrite shiftl_mul_pow2, mul_1_l. + rewrite shiftl_div_pow2, div_1_l, pow_neg_r; try order. + apply pow_gt_1. order'. now apply opp_pos_neg. +Qed. + +Lemma shiftl_0_r : forall a, a << 0 == a. +Proof. + intros. rewrite shiftl_mul_pow2 by order. now nzsimpl. +Qed. + +Lemma shiftr_0_r : forall a, a >> 0 == a. +Proof. + intros. now rewrite <- shiftl_opp_r, opp_0, shiftl_0_r. +Qed. + +Lemma shiftl_0_l : forall n, 0 << n == 0. +Proof. + intros. + destruct (le_ge_cases 0 n). + rewrite shiftl_mul_pow2 by trivial. now nzsimpl. + rewrite shiftl_div_pow2 by trivial. + rewrite <- opp_nonneg_nonpos in H. nzsimpl; order_nz. +Qed. + +Lemma shiftr_0_l : forall n, 0 >> n == 0. +Proof. + intros. now rewrite <- shiftl_opp_r, shiftl_0_l. +Qed. + +Lemma shiftl_eq_0_iff : forall a n, 0<=n -> (a << n == 0 <-> a == 0). +Proof. + intros a n Hn. + rewrite shiftl_mul_pow2 by trivial. rewrite eq_mul_0. split. + intros [H | H]; trivial. contradict H; order_nz. + intros H. now left. +Qed. + +Lemma shiftr_eq_0_iff : forall a n, + a >> n == 0 <-> a==0 \/ (0<a /\ log2 a < n). +Proof. + intros a n. + destruct (le_gt_cases 0 n) as [Hn|Hn]. + rewrite shiftr_div_pow2, div_small_iff by order_nz. + destruct (lt_trichotomy a 0) as [LT|[EQ|LT]]. + split. + intros [(H,_)|(H,H')]. order. generalize (pow_nonneg 2 n le_0_2); order. + intros [H|(H,H')]; order. + rewrite EQ. split. now left. intros _; left. split; order_pos. + split. intros [(H,H')|(H,H')]; right. split; trivial. + apply log2_lt_pow2; trivial. + generalize (pow_nonneg 2 n le_0_2); order. + intros [H|(H,H')]. order. left. + split. order. now apply log2_lt_pow2. + rewrite shiftr_mul_pow2 by order. rewrite eq_mul_0. + split; intros [H|H]. + now left. + elim (pow_nonzero 2 (-n)); try apply opp_nonneg_nonpos; order'. + now left. + destruct H. generalize (log2_nonneg a); order. +Qed. + +Lemma shiftr_eq_0 : forall a n, 0<=a -> log2 a < n -> a >> n == 0. +Proof. + intros a n Ha H. + apply shiftr_eq_0_iff. + apply le_lteq in Ha. destruct Ha as [Ha|Ha]. + right. now split. now left. +Qed. + +(** Properties of [div2]. *) + +Lemma div2_div : forall a, div2 a == a/2. +Proof. + intros. rewrite div2_spec, shiftr_div_pow2. now nzsimpl. order'. +Qed. + +Instance div2_wd : Proper (eq==>eq) div2. +Proof. + intros a a' Ha. now rewrite 2 div2_div, Ha. +Qed. + +Lemma div2_odd : forall a, a == 2*(div2 a) + odd a. +Proof. + intros a. rewrite div2_div, <- bit0_odd, bit0_mod. + apply div_mod. order'. +Qed. + +(** Properties of [lxor] and others, directly deduced + from properties of [xorb] and others. *) + +Instance lxor_wd : Proper (eq ==> eq ==> eq) lxor. +Proof. + intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb. +Qed. + +Instance land_wd : Proper (eq ==> eq ==> eq) land. +Proof. + intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb. +Qed. + +Instance lor_wd : Proper (eq ==> eq ==> eq) lor. +Proof. + intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb. +Qed. + +Instance ldiff_wd : Proper (eq ==> eq ==> eq) ldiff. +Proof. + intros a a' Ha b b' Hb. bitwise. now rewrite Ha, Hb. +Qed. + +Lemma lxor_eq : forall a a', lxor a a' == 0 -> a == a'. +Proof. + intros a a' H. bitwise. apply xorb_eq. + now rewrite <- lxor_spec, H, bits_0. +Qed. + +Lemma lxor_nilpotent : forall a, lxor a a == 0. +Proof. + intros. bitwise. apply xorb_nilpotent. +Qed. + +Lemma lxor_eq_0_iff : forall a a', lxor a a' == 0 <-> a == a'. +Proof. + split. apply lxor_eq. intros EQ; rewrite EQ; apply lxor_nilpotent. +Qed. + +Lemma lxor_0_l : forall a, lxor 0 a == a. +Proof. + intros. bitwise. apply xorb_false_l. +Qed. + +Lemma lxor_0_r : forall a, lxor a 0 == a. +Proof. + intros. bitwise. apply xorb_false_r. +Qed. + +Lemma lxor_comm : forall a b, lxor a b == lxor b a. +Proof. + intros. bitwise. apply xorb_comm. +Qed. + +Lemma lxor_assoc : + forall a b c, lxor (lxor a b) c == lxor a (lxor b c). +Proof. + intros. bitwise. apply xorb_assoc. +Qed. + +Lemma lor_0_l : forall a, lor 0 a == a. +Proof. + intros. bitwise. trivial. +Qed. + +Lemma lor_0_r : forall a, lor a 0 == a. +Proof. + intros. bitwise. apply orb_false_r. +Qed. + +Lemma lor_comm : forall a b, lor a b == lor b a. +Proof. + intros. bitwise. apply orb_comm. +Qed. + +Lemma lor_assoc : + forall a b c, lor a (lor b c) == lor (lor a b) c. +Proof. + intros. bitwise. apply orb_assoc. +Qed. + +Lemma lor_diag : forall a, lor a a == a. +Proof. + intros. bitwise. apply orb_diag. +Qed. + +Lemma lor_eq_0_l : forall a b, lor a b == 0 -> a == 0. +Proof. + intros a b H. bitwise. + apply (orb_false_iff a.[m] b.[m]). + now rewrite <- lor_spec, H, bits_0. +Qed. + +Lemma lor_eq_0_iff : forall a b, lor a b == 0 <-> a == 0 /\ b == 0. +Proof. + intros a b. split. + split. now apply lor_eq_0_l in H. + rewrite lor_comm in H. now apply lor_eq_0_l in H. + intros (EQ,EQ'). now rewrite EQ, lor_0_l. +Qed. + +Lemma land_0_l : forall a, land 0 a == 0. +Proof. + intros. bitwise. trivial. +Qed. + +Lemma land_0_r : forall a, land a 0 == 0. +Proof. + intros. bitwise. apply andb_false_r. +Qed. + +Lemma land_comm : forall a b, land a b == land b a. +Proof. + intros. bitwise. apply andb_comm. +Qed. + +Lemma land_assoc : + forall a b c, land a (land b c) == land (land a b) c. +Proof. + intros. bitwise. apply andb_assoc. +Qed. + +Lemma land_diag : forall a, land a a == a. +Proof. + intros. bitwise. apply andb_diag. +Qed. + +Lemma ldiff_0_l : forall a, ldiff 0 a == 0. +Proof. + intros. bitwise. trivial. +Qed. + +Lemma ldiff_0_r : forall a, ldiff a 0 == a. +Proof. + intros. bitwise. now rewrite andb_true_r. +Qed. + +Lemma ldiff_diag : forall a, ldiff a a == 0. +Proof. + intros. bitwise. apply andb_negb_r. +Qed. + +Lemma lor_land_distr_l : forall a b c, + lor (land a b) c == land (lor a c) (lor b c). +Proof. + intros. bitwise. apply orb_andb_distrib_l. +Qed. + +Lemma lor_land_distr_r : forall a b c, + lor a (land b c) == land (lor a b) (lor a c). +Proof. + intros. bitwise. apply orb_andb_distrib_r. +Qed. + +Lemma land_lor_distr_l : forall a b c, + land (lor a b) c == lor (land a c) (land b c). +Proof. + intros. bitwise. apply andb_orb_distrib_l. +Qed. + +Lemma land_lor_distr_r : forall a b c, + land a (lor b c) == lor (land a b) (land a c). +Proof. + intros. bitwise. apply andb_orb_distrib_r. +Qed. + +Lemma ldiff_ldiff_l : forall a b c, + ldiff (ldiff a b) c == ldiff a (lor b c). +Proof. + intros. bitwise. now rewrite negb_orb, andb_assoc. +Qed. + +Lemma lor_ldiff_and : forall a b, + lor (ldiff a b) (land a b) == a. +Proof. + intros. bitwise. + now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r. +Qed. + +Lemma land_ldiff : forall a b, + land (ldiff a b) b == 0. +Proof. + intros. bitwise. + now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r. +Qed. + +(** Properties of [setbit] and [clearbit] *) + +Definition setbit a n := lor a (1 << n). +Definition clearbit a n := ldiff a (1 << n). + +Lemma setbit_spec' : forall a n, setbit a n == lor a (2^n). +Proof. + intros. unfold setbit. now rewrite shiftl_1_l. +Qed. + +Lemma clearbit_spec' : forall a n, clearbit a n == ldiff a (2^n). +Proof. + intros. unfold clearbit. now rewrite shiftl_1_l. +Qed. + +Instance setbit_wd : Proper (eq==>eq==>eq) setbit. +Proof. + intros a a' Ha n n' Hn. unfold setbit. now rewrite Ha, Hn. +Qed. + +Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit. +Proof. + intros a a' Ha n n' Hn. unfold clearbit. now rewrite Ha, Hn. +Qed. + +Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true. +Proof. + intros. rewrite <- (mul_1_l (2^n)). + now rewrite mul_pow2_bits, sub_diag, bit0_odd, odd_1. +Qed. + +Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false. +Proof. + intros. + destruct (le_gt_cases 0 n); [|now rewrite pow_neg_r, bits_0]. + destruct (le_gt_cases n m). + rewrite <- (mul_1_l (2^n)), mul_pow2_bits; trivial. + rewrite <- (succ_pred (m-n)), <- div2_bits. + now rewrite div_small, bits_0 by (split; order'). + rewrite <- lt_succ_r, succ_pred, lt_0_sub. order. + rewrite <- (mul_1_l (2^n)), mul_pow2_bits_low; trivial. +Qed. + +Lemma pow2_bits_eqb : forall n m, 0<=n -> (2^n).[m] = eqb n m. +Proof. + intros n m Hn. apply eq_true_iff_eq. rewrite eqb_eq. split. + destruct (eq_decidable n m) as [H|H]. trivial. + now rewrite (pow2_bits_false _ _ H). + intros EQ. rewrite EQ. apply pow2_bits_true; order. +Qed. + +Lemma setbit_eqb : forall a n m, 0<=n -> + (setbit a n).[m] = eqb n m || a.[m]. +Proof. + intros. now rewrite setbit_spec', lor_spec, pow2_bits_eqb, orb_comm. +Qed. + +Lemma setbit_iff : forall a n m, 0<=n -> + ((setbit a n).[m] = true <-> n==m \/ a.[m] = true). +Proof. + intros. now rewrite setbit_eqb, orb_true_iff, eqb_eq. +Qed. + +Lemma setbit_eq : forall a n, 0<=n -> (setbit a n).[n] = true. +Proof. + intros. apply setbit_iff; trivial. now left. +Qed. + +Lemma setbit_neq : forall a n m, 0<=n -> n~=m -> + (setbit a n).[m] = a.[m]. +Proof. + intros a n m Hn H. rewrite setbit_eqb; trivial. + rewrite <- eqb_eq in H. apply not_true_is_false in H. now rewrite H. +Qed. + +Lemma clearbit_eqb : forall a n m, + (clearbit a n).[m] = a.[m] && negb (eqb n m). +Proof. + intros. + destruct (le_gt_cases 0 m); [| now rewrite 2 testbit_neg_r]. + rewrite clearbit_spec', ldiff_spec. f_equal. f_equal. + destruct (le_gt_cases 0 n) as [Hn|Hn]. + now apply pow2_bits_eqb. + symmetry. rewrite pow_neg_r, bits_0, <- not_true_iff_false, eqb_eq; order. +Qed. + +Lemma clearbit_iff : forall a n m, + (clearbit a n).[m] = true <-> a.[m] = true /\ n~=m. +Proof. + intros. rewrite clearbit_eqb, andb_true_iff, <- eqb_eq. + now rewrite negb_true_iff, not_true_iff_false. +Qed. + +Lemma clearbit_eq : forall a n, (clearbit a n).[n] = false. +Proof. + intros. rewrite clearbit_eqb, (proj2 (eqb_eq _ _) (eq_refl n)). + apply andb_false_r. +Qed. + +Lemma clearbit_neq : forall a n m, n~=m -> + (clearbit a n).[m] = a.[m]. +Proof. + intros a n m H. rewrite clearbit_eqb. + rewrite <- eqb_eq in H. apply not_true_is_false in H. rewrite H. + apply andb_true_r. +Qed. + +(** Shifts of bitwise operations *) + +Lemma shiftl_lxor : forall a b n, + (lxor a b) << n == lxor (a << n) (b << n). +Proof. + intros. bitwise. now rewrite !shiftl_spec, lxor_spec. +Qed. + +Lemma shiftr_lxor : forall a b n, + (lxor a b) >> n == lxor (a >> n) (b >> n). +Proof. + intros. bitwise. now rewrite !shiftr_spec, lxor_spec. +Qed. + +Lemma shiftl_land : forall a b n, + (land a b) << n == land (a << n) (b << n). +Proof. + intros. bitwise. now rewrite !shiftl_spec, land_spec. +Qed. + +Lemma shiftr_land : forall a b n, + (land a b) >> n == land (a >> n) (b >> n). +Proof. + intros. bitwise. now rewrite !shiftr_spec, land_spec. +Qed. + +Lemma shiftl_lor : forall a b n, + (lor a b) << n == lor (a << n) (b << n). +Proof. + intros. bitwise. now rewrite !shiftl_spec, lor_spec. +Qed. + +Lemma shiftr_lor : forall a b n, + (lor a b) >> n == lor (a >> n) (b >> n). +Proof. + intros. bitwise. now rewrite !shiftr_spec, lor_spec. +Qed. + +Lemma shiftl_ldiff : forall a b n, + (ldiff a b) << n == ldiff (a << n) (b << n). +Proof. + intros. bitwise. now rewrite !shiftl_spec, ldiff_spec. +Qed. + +Lemma shiftr_ldiff : forall a b n, + (ldiff a b) >> n == ldiff (a >> n) (b >> n). +Proof. + intros. bitwise. now rewrite !shiftr_spec, ldiff_spec. +Qed. + +(** For integers, we do have a binary complement function *) + +Definition lnot a := P (-a). + +Instance lnot_wd : Proper (eq==>eq) lnot. +Proof. intros a a' Ha; unfold lnot; now rewrite Ha. Qed. + +Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n]. +Proof. + intros. unfold lnot. rewrite <- (opp_involutive a) at 2. + rewrite bits_opp, negb_involutive; trivial. +Qed. + +Lemma lnot_involutive : forall a, lnot (lnot a) == a. +Proof. + intros a. bitwise. now rewrite 2 lnot_spec, negb_involutive. +Qed. + +Lemma lnot_0 : lnot 0 == -1. +Proof. + unfold lnot. now rewrite opp_0, <- sub_1_r, sub_0_l. +Qed. + +Lemma lnot_m1 : lnot (-1) == 0. +Proof. + unfold lnot. now rewrite opp_involutive, one_succ, pred_succ. +Qed. + +(** Complement and other operations *) + +Lemma lor_m1_r : forall a, lor a (-1) == -1. +Proof. + intros. bitwise. now rewrite bits_m1, orb_true_r. +Qed. + +Lemma lor_m1_l : forall a, lor (-1) a == -1. +Proof. + intros. now rewrite lor_comm, lor_m1_r. +Qed. + +Lemma land_m1_r : forall a, land a (-1) == a. +Proof. + intros. bitwise. now rewrite bits_m1, andb_true_r. +Qed. + +Lemma land_m1_l : forall a, land (-1) a == a. +Proof. + intros. now rewrite land_comm, land_m1_r. +Qed. + +Lemma ldiff_m1_r : forall a, ldiff a (-1) == 0. +Proof. + intros. bitwise. now rewrite bits_m1, andb_false_r. +Qed. + +Lemma ldiff_m1_l : forall a, ldiff (-1) a == lnot a. +Proof. + intros. bitwise. now rewrite lnot_spec, bits_m1. +Qed. + +Lemma lor_lnot_diag : forall a, lor a (lnot a) == -1. +Proof. + intros a. bitwise. rewrite lnot_spec, bits_m1; trivial. + now destruct a.[m]. +Qed. + +Lemma add_lnot_diag : forall a, a + lnot a == -1. +Proof. + intros a. unfold lnot. + now rewrite add_pred_r, add_opp_r, sub_diag, one_succ, opp_succ, opp_0. +Qed. + +Lemma ldiff_land : forall a b, ldiff a b == land a (lnot b). +Proof. + intros. bitwise. now rewrite lnot_spec. +Qed. + +Lemma land_lnot_diag : forall a, land a (lnot a) == 0. +Proof. + intros. now rewrite <- ldiff_land, ldiff_diag. +Qed. + +Lemma lnot_lor : forall a b, lnot (lor a b) == land (lnot a) (lnot b). +Proof. + intros a b. bitwise. now rewrite !lnot_spec, lor_spec, negb_orb. +Qed. + +Lemma lnot_land : forall a b, lnot (land a b) == lor (lnot a) (lnot b). +Proof. + intros a b. bitwise. now rewrite !lnot_spec, land_spec, negb_andb. +Qed. + +Lemma lnot_ldiff : forall a b, lnot (ldiff a b) == lor (lnot a) b. +Proof. + intros a b. bitwise. + now rewrite !lnot_spec, ldiff_spec, negb_andb, negb_involutive. +Qed. + +Lemma lxor_lnot_lnot : forall a b, lxor (lnot a) (lnot b) == lxor a b. +Proof. + intros a b. bitwise. now rewrite !lnot_spec, xorb_negb_negb. +Qed. + +Lemma lnot_lxor_l : forall a b, lnot (lxor a b) == lxor (lnot a) b. +Proof. + intros a b. bitwise. now rewrite !lnot_spec, !lxor_spec, negb_xorb_l. +Qed. + +Lemma lnot_lxor_r : forall a b, lnot (lxor a b) == lxor a (lnot b). +Proof. + intros a b. bitwise. now rewrite !lnot_spec, !lxor_spec, negb_xorb_r. +Qed. + +Lemma lxor_m1_r : forall a, lxor a (-1) == lnot a. +Proof. + intros. now rewrite <- (lxor_0_r (lnot a)), <- lnot_m1, lxor_lnot_lnot. +Qed. + +Lemma lxor_m1_l : forall a, lxor (-1) a == lnot a. +Proof. + intros. now rewrite lxor_comm, lxor_m1_r. +Qed. + +Lemma lxor_lor : forall a b, land a b == 0 -> + lxor a b == lor a b. +Proof. + intros a b H. bitwise. + assert (a.[m] && b.[m] = false) + by now rewrite <- land_spec, H, bits_0. + now destruct a.[m], b.[m]. +Qed. + +Lemma lnot_shiftr : forall a n, 0<=n -> lnot (a >> n) == (lnot a) >> n. +Proof. + intros a n Hn. bitwise. + now rewrite lnot_spec, 2 shiftr_spec, lnot_spec by order_pos. +Qed. + +(** [(ones n)] is [2^n-1], the number with [n] digits 1 *) + +Definition ones n := P (1<<n). + +Instance ones_wd : Proper (eq==>eq) ones. +Proof. intros a a' Ha; unfold ones; now rewrite Ha. Qed. + +Lemma ones_equiv : forall n, ones n == P (2^n). +Proof. + intros. unfold ones. + destruct (le_gt_cases 0 n). + now rewrite shiftl_mul_pow2, mul_1_l. + apply pred_wd. rewrite pow_neg_r; trivial. + rewrite <- shiftr_opp_r. apply shiftr_eq_0_iff. right; split. + order'. rewrite log2_1. now apply opp_pos_neg. +Qed. + +Lemma ones_add : forall n m, 0<=n -> 0<=m -> + ones (m+n) == 2^m * ones n + ones m. +Proof. + intros n m Hn Hm. rewrite !ones_equiv. + rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r by trivial. + rewrite add_sub_assoc, sub_add. reflexivity. +Qed. + +Lemma ones_div_pow2 : forall n m, 0<=m<=n -> ones n / 2^m == ones (n-m). +Proof. + intros n m (Hm,H). symmetry. apply div_unique with (ones m). + left. rewrite ones_equiv. split. + rewrite <- lt_succ_r, succ_pred. order_pos. + now rewrite <- le_succ_l, succ_pred. + rewrite <- (sub_add m n) at 1. rewrite (add_comm _ m). + apply ones_add; trivial. now apply le_0_sub. +Qed. + +Lemma ones_mod_pow2 : forall n m, 0<=m<=n -> (ones n) mod (2^m) == ones m. +Proof. + intros n m (Hm,H). symmetry. apply mod_unique with (ones (n-m)). + left. rewrite ones_equiv. split. + rewrite <- lt_succ_r, succ_pred. order_pos. + now rewrite <- le_succ_l, succ_pred. + rewrite <- (sub_add m n) at 1. rewrite (add_comm _ m). + apply ones_add; trivial. now apply le_0_sub. +Qed. + +Lemma ones_spec_low : forall n m, 0<=m<n -> (ones n).[m] = true. +Proof. + intros n m (Hm,H). apply testbit_true; trivial. + rewrite ones_div_pow2 by (split; order). + rewrite <- (pow_1_r 2). rewrite ones_mod_pow2. + rewrite ones_equiv. now nzsimpl'. + split. order'. apply le_add_le_sub_r. nzsimpl. now apply le_succ_l. +Qed. + +Lemma ones_spec_high : forall n m, 0<=n<=m -> (ones n).[m] = false. +Proof. + intros n m (Hn,H). apply le_lteq in Hn. destruct Hn as [Hn|Hn]. + apply bits_above_log2; rewrite ones_equiv. + rewrite <-lt_succ_r, succ_pred; order_pos. + rewrite log2_pred_pow2; trivial. now rewrite <-le_succ_l, succ_pred. + rewrite ones_equiv. now rewrite <- Hn, pow_0_r, one_succ, pred_succ, bits_0. +Qed. + +Lemma ones_spec_iff : forall n m, 0<=n -> + ((ones n).[m] = true <-> 0<=m<n). +Proof. + intros n m Hn. split. intros H. + destruct (lt_ge_cases m 0) as [Hm|Hm]. + now rewrite testbit_neg_r in H. + split; trivial. apply lt_nge. intro H'. rewrite ones_spec_high in H. + discriminate. now split. + apply ones_spec_low. +Qed. + +Lemma lor_ones_low : forall a n, 0<=a -> log2 a < n -> + lor a (ones n) == ones n. +Proof. + intros a n Ha H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, bits_above_log2; try split; trivial. + now apply lt_le_trans with n. + apply le_trans with (log2 a); order_pos. + rewrite ones_spec_low, orb_true_r; try split; trivial. +Qed. + +Lemma land_ones : forall a n, 0<=n -> land a (ones n) == a mod 2^n. +Proof. + intros a n Hn. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r; + try split; trivial. + rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r; + try split; trivial. +Qed. + +Lemma land_ones_low : forall a n, 0<=a -> log2 a < n -> + land a (ones n) == a. +Proof. + intros a n Ha H. + assert (Hn : 0<=n) by (generalize (log2_nonneg a); order). + rewrite land_ones; trivial. apply mod_small. + split; trivial. + apply log2_lt_cancel. now rewrite log2_pow2. +Qed. + +Lemma ldiff_ones_r : forall a n, 0<=n -> + ldiff a (ones n) == (a >> n) << n. +Proof. + intros a n Hn. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, shiftl_spec_high, shiftr_spec; trivial. + rewrite sub_add; trivial. apply andb_true_r. + now apply le_0_sub. + now split. + rewrite ones_spec_low, shiftl_spec_low, andb_false_r; + try split; trivial. +Qed. + +Lemma ldiff_ones_r_low : forall a n, 0<=a -> log2 a < n -> + ldiff a (ones n) == 0. +Proof. + intros a n Ha H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + split; trivial. now apply le_trans with (log2 a); order_pos. + rewrite ones_spec_low, andb_false_r; try split; trivial. +Qed. + +Lemma ldiff_ones_l_low : forall a n, 0<=a -> log2 a < n -> + ldiff (ones n) a == lxor a (ones n). +Proof. + intros a n Ha H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + split; trivial. now apply le_trans with (log2 a); order_pos. + rewrite ones_spec_low, xorb_true_r; try split; trivial. +Qed. + +(** Bitwise operations and sign *) + +Lemma shiftl_nonneg : forall a n, 0 <= (a << n) <-> 0 <= a. +Proof. + intros a n. + destruct (le_ge_cases 0 n) as [Hn|Hn]. + (* 0<=n *) + rewrite 2 bits_iff_nonneg_ex. split; intros (k,Hk). + exists (k-n). intros m Hm. + destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. + rewrite <- (add_simpl_r m n), <- (shiftl_spec a n) by order_pos. + apply Hk. now apply lt_sub_lt_add_r. + exists (k+n). intros m Hm. + destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. + rewrite shiftl_spec by trivial. apply Hk. now apply lt_add_lt_sub_r. + (* n<=0*) + rewrite <- shiftr_opp_r, 2 bits_iff_nonneg_ex. split; intros (k,Hk). + destruct (le_gt_cases 0 k). + exists (k-n). intros m Hm. apply lt_sub_lt_add_r in Hm. + rewrite <- (add_simpl_r m n), <- add_opp_r, <- (shiftr_spec a (-n)). + now apply Hk. order. + assert (EQ : a >> (-n) == 0). + apply bits_inj'. intros m Hm. rewrite bits_0. apply Hk; order. + apply shiftr_eq_0_iff in EQ. + rewrite <- bits_iff_nonneg_ex. destruct EQ as [EQ|[LT _]]; order. + exists (k+n). intros m Hm. + destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. + rewrite shiftr_spec by trivial. apply Hk. + rewrite add_opp_r. now apply lt_add_lt_sub_r. +Qed. + +Lemma shiftl_neg : forall a n, (a << n) < 0 <-> a < 0. +Proof. + intros a n. now rewrite 2 lt_nge, shiftl_nonneg. +Qed. + +Lemma shiftr_nonneg : forall a n, 0 <= (a >> n) <-> 0 <= a. +Proof. + intros. rewrite <- shiftl_opp_r. apply shiftl_nonneg. +Qed. + +Lemma shiftr_neg : forall a n, (a >> n) < 0 <-> a < 0. +Proof. + intros a n. now rewrite 2 lt_nge, shiftr_nonneg. +Qed. + +Lemma div2_nonneg : forall a, 0 <= div2 a <-> 0 <= a. +Proof. + intros. rewrite div2_spec. apply shiftr_nonneg. +Qed. + +Lemma div2_neg : forall a, div2 a < 0 <-> a < 0. +Proof. + intros a. now rewrite 2 lt_nge, div2_nonneg. +Qed. + +Lemma lor_nonneg : forall a b, 0 <= lor a b <-> 0<=a /\ 0<=b. +Proof. + intros a b. + rewrite 3 bits_iff_nonneg_ex. split. intros (k,Hk). + split; exists k; intros m Hm; apply (orb_false_elim a.[m] b.[m]); + rewrite <- lor_spec; now apply Hk. + intros ((k,Hk),(k',Hk')). + destruct (le_ge_cases k k'); [ exists k' | exists k ]; + intros m Hm; rewrite lor_spec, Hk, Hk'; trivial; order. +Qed. + +Lemma lor_neg : forall a b, lor a b < 0 <-> a < 0 \/ b < 0. +Proof. + intros a b. rewrite 3 lt_nge, lor_nonneg. split. + apply not_and. apply le_decidable. + now intros [H|H] (H',H''). +Qed. + +Lemma lnot_nonneg : forall a, 0 <= lnot a <-> a < 0. +Proof. + intros a; unfold lnot. + now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. +Qed. + +Lemma lnot_neg : forall a, lnot a < 0 <-> 0 <= a. +Proof. + intros a. now rewrite le_ngt, lt_nge, lnot_nonneg. +Qed. + +Lemma land_nonneg : forall a b, 0 <= land a b <-> 0<=a \/ 0<=b. +Proof. + intros a b. + now rewrite <- (lnot_involutive (land a b)), lnot_land, lnot_nonneg, + lor_neg, !lnot_neg. +Qed. + +Lemma land_neg : forall a b, land a b < 0 <-> a < 0 /\ b < 0. +Proof. + intros a b. + now rewrite <- (lnot_involutive (land a b)), lnot_land, lnot_neg, + lor_nonneg, !lnot_nonneg. +Qed. + +Lemma ldiff_nonneg : forall a b, 0 <= ldiff a b <-> 0<=a \/ b<0. +Proof. + intros. now rewrite ldiff_land, land_nonneg, lnot_nonneg. +Qed. + +Lemma ldiff_neg : forall a b, ldiff a b < 0 <-> a<0 /\ 0<=b. +Proof. + intros. now rewrite ldiff_land, land_neg, lnot_neg. +Qed. + +Lemma lxor_nonneg : forall a b, 0 <= lxor a b <-> (0<=a <-> 0<=b). +Proof. + assert (H : forall a b, 0<=a -> 0<=b -> 0<=lxor a b). + intros a b. rewrite 3 bits_iff_nonneg_ex. intros (k,Hk) (k', Hk'). + destruct (le_ge_cases k k'); [ exists k' | exists k]; + intros m Hm; rewrite lxor_spec, Hk, Hk'; trivial; order. + assert (H' : forall a b, 0<=a -> b<0 -> lxor a b<0). + intros a b. rewrite bits_iff_nonneg_ex, 2 bits_iff_neg_ex. + intros (k,Hk) (k', Hk'). + destruct (le_ge_cases k k'); [ exists k' | exists k]; + intros m Hm; rewrite lxor_spec, Hk, Hk'; trivial; order. + intros a b. + split. + intros Hab. split. + intros Ha. destruct (le_gt_cases 0 b) as [Hb|Hb]; trivial. + generalize (H' _ _ Ha Hb). order. + intros Hb. destruct (le_gt_cases 0 a) as [Ha|Ha]; trivial. + generalize (H' _ _ Hb Ha). rewrite lxor_comm. order. + intros E. + destruct (le_gt_cases 0 a) as [Ha|Ha]. apply H; trivial. apply E; trivial. + destruct (le_gt_cases 0 b) as [Hb|Hb]. apply H; trivial. apply E; trivial. + rewrite <- lxor_lnot_lnot. apply H; now apply lnot_nonneg. +Qed. + +(** Bitwise operations and log2 *) + +Lemma log2_bits_unique : forall a n, + a.[n] = true -> + (forall m, n<m -> a.[m] = false) -> + log2 a == n. +Proof. + intros a n H H'. + destruct (lt_trichotomy a 0) as [Ha|[Ha|Ha]]. + (* a < 0 *) + destruct (proj1 (bits_iff_neg_ex a) Ha) as (k,Hk). + destruct (le_gt_cases n k). + specialize (Hk (S k) (lt_succ_diag_r _)). + rewrite H' in Hk. discriminate. apply lt_succ_r; order. + specialize (H' (S n) (lt_succ_diag_r _)). + rewrite Hk in H'. discriminate. apply lt_succ_r; order. + (* a = 0 *) + now rewrite Ha, bits_0 in H. + (* 0 < a *) + apply le_antisymm; apply le_ngt; intros LT. + specialize (H' _ LT). now rewrite bit_log2 in H'. + now rewrite bits_above_log2 in H by order. +Qed. + +Lemma log2_shiftr : forall a n, 0<a -> log2 (a >> n) == max 0 (log2 a - n). +Proof. + intros a n Ha. + destruct (le_gt_cases 0 (log2 a - n)); + [rewrite max_r | rewrite max_l]; try order. + apply log2_bits_unique. + now rewrite shiftr_spec, sub_add, bit_log2. + intros m Hm. + destruct (le_gt_cases 0 m); [|now rewrite testbit_neg_r]. + rewrite shiftr_spec; trivial. apply bits_above_log2; try order. + now apply lt_sub_lt_add_r. + rewrite lt_sub_lt_add_r, add_0_l in H. + apply log2_nonpos. apply le_lteq; right. + apply shiftr_eq_0_iff. right. now split. +Qed. + +Lemma log2_shiftl : forall a n, 0<a -> 0<=n -> log2 (a << n) == log2 a + n. +Proof. + intros a n Ha Hn. + rewrite shiftl_mul_pow2, add_comm by trivial. + now apply log2_mul_pow2. +Qed. + +Lemma log2_shiftl' : forall a n, 0<a -> log2 (a << n) == max 0 (log2 a + n). +Proof. + intros a n Ha. + rewrite <- shiftr_opp_r, log2_shiftr by trivial. + destruct (le_gt_cases 0 (log2 a + n)); + [rewrite 2 max_r | rewrite 2 max_l]; rewrite ?sub_opp_r; try order. +Qed. + +Lemma log2_lor : forall a b, 0<=a -> 0<=b -> + log2 (lor a b) == max (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lor a b) == log2 b). + intros a b Ha H. + apply le_lteq in Ha; destruct Ha as [Ha|Ha]; [|now rewrite <- Ha, lor_0_l]. + apply log2_bits_unique. + now rewrite lor_spec, bit_log2, orb_true_r by order. + intros m Hm. assert (H' := log2_le_mono _ _ H). + now rewrite lor_spec, 2 bits_above_log2 by order. + (* main *) + intros a b Ha Hb. destruct (le_ge_cases a b) as [H|H]. + rewrite max_r by now apply log2_le_mono. + now apply AUX. + rewrite max_l by now apply log2_le_mono. + rewrite lor_comm. now apply AUX. +Qed. + +Lemma log2_land : forall a b, 0<=a -> 0<=b -> + log2 (land a b) <= min (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, 0<=a -> a<=b -> log2 (land a b) <= log2 a). + intros a b Ha Hb. + apply le_ngt. intros H'. + assert (LE : 0 <= land a b) by (apply land_nonneg; now left). + apply le_lteq in LE. destruct LE as [LT|EQ]. + generalize (bit_log2 (land a b) LT). + now rewrite land_spec, bits_above_log2. + rewrite <- EQ in H'. apply log2_lt_cancel in H'; order. + (* main *) + intros a b Ha Hb. + destruct (le_ge_cases a b) as [H|H]. + rewrite min_l by now apply log2_le_mono. now apply AUX. + rewrite min_r by now apply log2_le_mono. rewrite land_comm. now apply AUX. +Qed. + +Lemma log2_lxor : forall a b, 0<=a -> 0<=b -> + log2 (lxor a b) <= max (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, 0<=a -> a<=b -> log2 (lxor a b) <= log2 b). + intros a b Ha Hb. + apply le_ngt. intros H'. + assert (LE : 0 <= lxor a b) by (apply lxor_nonneg; split; order). + apply le_lteq in LE. destruct LE as [LT|EQ]. + generalize (bit_log2 (lxor a b) LT). + rewrite lxor_spec, 2 bits_above_log2; try order. discriminate. + apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. + rewrite <- EQ in H'. apply log2_lt_cancel in H'; order. + (* main *) + intros a b Ha Hb. + destruct (le_ge_cases a b) as [H|H]. + rewrite max_r by now apply log2_le_mono. now apply AUX. + rewrite max_l by now apply log2_le_mono. rewrite lxor_comm. now apply AUX. +Qed. + +(** Bitwise operations and arithmetical operations *) + +Local Notation xor3 a b c := (xorb (xorb a b) c). +Local Notation lxor3 a b c := (lxor (lxor a b) c). +Local Notation nextcarry a b c := ((a&&b) || (c && (a||b))). +Local Notation lnextcarry a b c := (lor (land a b) (land c (lor a b))). + +Lemma add_bit0 : forall a b, (a+b).[0] = xorb a.[0] b.[0]. +Proof. + intros. now rewrite !bit0_odd, odd_add. +Qed. + +Lemma add3_bit0 : forall a b c, + (a+b+c).[0] = xor3 a.[0] b.[0] c.[0]. +Proof. + intros. now rewrite !add_bit0. +Qed. + +Lemma add3_bits_div2 : forall (a0 b0 c0 : bool), + (a0 + b0 + c0)/2 == nextcarry a0 b0 c0. +Proof. + assert (H : 1+1 == 2) by now nzsimpl'. + intros [|] [|] [|]; simpl; rewrite ?add_0_l, ?add_0_r, ?H; + (apply div_same; order') || (apply div_small; split; order') || idtac. + symmetry. apply div_unique with 1. left; split; order'. now nzsimpl'. +Qed. + +Lemma add_carry_div2 : forall a b (c0:bool), + (a + b + c0)/2 == a/2 + b/2 + nextcarry a.[0] b.[0] c0. +Proof. + intros. + rewrite <- add3_bits_div2. + rewrite (add_comm ((a/2)+_)). + rewrite <- div_add by order'. + apply div_wd; try easy. + rewrite <- !div2_div, mul_comm, mul_add_distr_l. + rewrite (div2_odd a), <- bit0_odd at 1. + rewrite (div2_odd b), <- bit0_odd at 1. + rewrite add_shuffle1. + rewrite <-(add_assoc _ _ c0). apply add_comm. +Qed. + +(** The main result concerning addition: we express the bits of the sum + in term of bits of [a] and [b] and of some carry stream which is also + recursively determined by another equation. +*) + +Lemma add_carry_bits_aux : forall n, 0<=n -> + forall a b (c0:bool), -(2^n) <= a < 2^n -> -(2^n) <= b < 2^n -> + exists c, + a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0. +Proof. + intros n Hn. apply le_ind with (4:=Hn). + solve_predicate_wd. + (* base *) + intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r, <- !one_succ. + intros (Ha1,Ha2) (Hb1,Hb2). + apply le_lteq in Ha1; apply le_lteq in Hb1. + rewrite <- le_succ_l, succ_m1 in Ha1, Hb1. + destruct Ha1 as [Ha1|Ha1]; destruct Hb1 as [Hb1|Hb1]. + (* base, a = 0, b = 0 *) + exists c0. + rewrite (le_antisymm _ _ Ha2 Ha1), (le_antisymm _ _ Hb2 Hb1). + rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r. + rewrite b2z_div2, b2z_bit0; now repeat split. + (* base, a = 0, b = -1 *) + exists (-c0). rewrite <- Hb1, (le_antisymm _ _ Ha2 Ha1). repeat split. + rewrite add_0_l, lxor_0_l, lxor_m1_l. + unfold lnot. now rewrite opp_involutive, add_comm, add_opp_r, sub_1_r. + rewrite land_0_l, !lor_0_l, land_m1_r. + symmetry. apply div_unique with c0. left; destruct c0; simpl; split; order'. + now rewrite two_succ, mul_succ_l, mul_1_l, add_opp_r, sub_add. + rewrite bit0_odd, odd_opp; destruct c0; simpl; apply odd_1 || apply odd_0. + (* base, a = -1, b = 0 *) + exists (-c0). rewrite <- Ha1, (le_antisymm _ _ Hb2 Hb1). repeat split. + rewrite add_0_r, lxor_0_r, lxor_m1_l. + unfold lnot. now rewrite opp_involutive, add_comm, add_opp_r, sub_1_r. + rewrite land_0_r, lor_0_r, lor_0_l, land_m1_r. + symmetry. apply div_unique with c0. left; destruct c0; simpl; split; order'. + now rewrite two_succ, mul_succ_l, mul_1_l, add_opp_r, sub_add. + rewrite bit0_odd, odd_opp; destruct c0; simpl; apply odd_1 || apply odd_0. + (* base, a = -1, b = -1 *) + exists (c0 + 2*(-1)). rewrite <- Ha1, <- Hb1. repeat split. + rewrite lxor_m1_l, lnot_m1, lxor_0_l. + now rewrite two_succ, mul_succ_l, mul_1_l, add_comm, add_assoc. + rewrite land_m1_l, lor_m1_l. + apply add_b2z_double_div2. + apply add_b2z_double_bit0. + (* step *) + clear n Hn. intros n Hn IH a b c0 Ha Hb. + set (c1:=nextcarry a.[0] b.[0] c0). + destruct (IH (a/2) (b/2) c1) as (c & IH1 & IH2 & Hc); clear IH. + split. + apply div_le_lower_bound. order'. now rewrite mul_opp_r, <- pow_succ_r. + apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r. + split. + apply div_le_lower_bound. order'. now rewrite mul_opp_r, <- pow_succ_r. + apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r. + exists (c0 + 2*c). repeat split. + (* step, add *) + bitwise. + apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + rewrite <- (succ_pred m), lt_succ_r in Hm. + rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial. + apply testbit_wd; try easy. + rewrite add_b2z_double_div2, <- IH1. apply add_carry_div2. + rewrite <- Hm. + now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0. + (* step, carry *) + rewrite add_b2z_double_div2. + bitwise. + apply le_lteq in Hm. destruct Hm as [Hm|Hm]. + rewrite <- (succ_pred m), lt_succ_r in Hm. + rewrite <- (succ_pred m), <- !div2_bits, IH2 by trivial. + autorewrite with bitwise. now rewrite add_b2z_double_div2. + rewrite <- Hm. + now rewrite add_b2z_double_bit0. + (* step, carry0 *) + apply add_b2z_double_bit0. +Qed. + +Lemma add_carry_bits : forall a b (c0:bool), exists c, + a+b+c0 == lxor3 a b c /\ c/2 == lnextcarry a b c /\ c.[0] = c0. +Proof. + intros a b c0. + set (n := max (abs a) (abs b)). + apply (add_carry_bits_aux n). + (* positivity *) + unfold n. + destruct (le_ge_cases (abs a) (abs b)); + [rewrite max_r|rewrite max_l]; order_pos'. + (* bound for a *) + assert (Ha : abs a < 2^n). + apply lt_le_trans with (2^(abs a)). apply pow_gt_lin_r; order_pos'. + apply pow_le_mono_r. order'. unfold n. + destruct (le_ge_cases (abs a) (abs b)); + [rewrite max_r|rewrite max_l]; try order. + apply abs_lt in Ha. destruct Ha; split; order. + (* bound for b *) + assert (Hb : abs b < 2^n). + apply lt_le_trans with (2^(abs b)). apply pow_gt_lin_r; order_pos'. + apply pow_le_mono_r. order'. unfold n. + destruct (le_ge_cases (abs a) (abs b)); + [rewrite max_r|rewrite max_l]; try order. + apply abs_lt in Hb. destruct Hb; split; order. +Qed. + +(** Particular case : the second bit of an addition *) + +Lemma add_bit1 : forall a b, + (a+b).[1] = xor3 a.[1] b.[1] (a.[0] && b.[0]). +Proof. + intros a b. + destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc). + simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1. + autorewrite with bitwise. f_equal. + rewrite one_succ, <- div2_bits, EQ2 by order. + autorewrite with bitwise. + rewrite Hc. simpl. apply orb_false_r. +Qed. + +(** In an addition, there will be no carries iff there is + no common bits in the numbers to add *) + +Lemma nocarry_equiv : forall a b c, + c/2 == lnextcarry a b c -> c.[0] = false -> + (c == 0 <-> land a b == 0). +Proof. + intros a b c H H'. + split. intros EQ; rewrite EQ in *. + rewrite div_0_l in H by order'. + symmetry in H. now apply lor_eq_0_l in H. + intros EQ. rewrite EQ, lor_0_l in H. + apply bits_inj'. intros n Hn. rewrite bits_0. + apply le_ind with (4:=Hn). + solve_predicate_wd. + trivial. + clear n Hn. intros n Hn IH. + rewrite <- div2_bits, H; trivial. + autorewrite with bitwise. + now rewrite IH. +Qed. + +(** When there is no common bits, the addition is just a xor *) + +Lemma add_nocarry_lxor : forall a b, land a b == 0 -> + a+b == lxor a b. +Proof. + intros a b H. + destruct (add_carry_bits a b false) as (c & EQ1 & EQ2 & Hc). + simpl in EQ1; rewrite add_0_r in EQ1. rewrite EQ1. + apply (nocarry_equiv a b c) in H; trivial. + rewrite H. now rewrite lxor_0_r. +Qed. + +(** A null [ldiff] implies being smaller *) + +Lemma ldiff_le : forall a b, 0<=b -> ldiff a b == 0 -> 0 <= a <= b. +Proof. + assert (AUX : forall n, 0<=n -> + forall a b, 0 <= a < 2^n -> 0<=b -> ldiff a b == 0 -> a <= b). + intros n Hn. apply le_ind with (4:=Hn); clear n Hn. + solve_predicate_wd. + intros a b Ha Hb _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. + setoid_replace a with 0 by (destruct Ha; order'); trivial. + intros n Hn IH a b (Ha,Ha') Hb H. + assert (NEQ : 2 ~= 0) by order'. + rewrite (div_mod a 2 NEQ), (div_mod b 2 NEQ). + apply add_le_mono. + apply mul_le_mono_pos_l; try order'. + apply IH. + split. apply div_pos; order'. + apply div_lt_upper_bound; try order'. now rewrite <- pow_succ_r. + apply div_pos; order'. + rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2 by order'. + rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l; order'. + rewrite <- 2 bit0_mod. + apply bits_inj_iff in H. specialize (H 0). + rewrite ldiff_spec, bits_0 in H. + destruct a.[0], b.[0]; try discriminate; simpl; order'. + (* main *) + intros a b Hb Hd. + assert (Ha : 0<=a). + apply le_ngt; intros Ha'. apply (lt_irrefl 0). rewrite <- Hd at 1. + apply ldiff_neg. now split. + split; trivial. apply (AUX a); try split; trivial. apply pow_gt_lin_r; order'. +Qed. + +(** Subtraction can be a ldiff when the opposite ldiff is null. *) + +Lemma sub_nocarry_ldiff : forall a b, ldiff b a == 0 -> + a-b == ldiff a b. +Proof. + intros a b H. + apply add_cancel_r with b. + rewrite sub_add. + symmetry. + rewrite add_nocarry_lxor; trivial. + bitwise. + apply bits_inj_iff in H. specialize (H m). + rewrite ldiff_spec, bits_0 in H. + now destruct a.[m], b.[m]. + apply land_ldiff. +Qed. + +(** Adding numbers with no common bits cannot lead to a much bigger number *) + +Lemma add_nocarry_lt_pow2 : forall a b n, land a b == 0 -> + a < 2^n -> b < 2^n -> a+b < 2^n. +Proof. + intros a b n H Ha Hb. + destruct (le_gt_cases a 0) as [Ha'|Ha']. + apply le_lt_trans with (0+b). now apply add_le_mono_r. now nzsimpl. + destruct (le_gt_cases b 0) as [Hb'|Hb']. + apply le_lt_trans with (a+0). now apply add_le_mono_l. now nzsimpl. + rewrite add_nocarry_lxor by order. + destruct (lt_ge_cases 0 (lxor a b)); [|apply le_lt_trans with 0; order_pos]. + apply log2_lt_pow2; trivial. + apply log2_lt_pow2 in Ha; trivial. + apply log2_lt_pow2 in Hb; trivial. + apply le_lt_trans with (max (log2 a) (log2 b)). + apply log2_lxor; order. + destruct (le_ge_cases (log2 a) (log2 b)); + [rewrite max_r|rewrite max_l]; order. +Qed. + +Lemma add_nocarry_mod_lt_pow2 : forall a b n, 0<=n -> land a b == 0 -> + a mod 2^n + b mod 2^n < 2^n. +Proof. + intros a b n Hn H. + apply add_nocarry_lt_pow2. + bitwise. + destruct (le_gt_cases n m). + rewrite mod_pow2_bits_high; now split. + now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. + apply mod_pos_bound; order_pos. + apply mod_pos_bound; order_pos. +Qed. + +End ZBitsProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 070003972..c8fd29a54 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -575,6 +575,23 @@ Proof. apply div_mod; order. Qed. +(** Similarly, the following result doesn't always hold for negative + [b] and [c]. For instance [3 mod (-2*-2)) = 3] while + [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. +*) + +Lemma mod_mul_r : forall a b c, 0<b -> 0<c -> + a mod (b*c) == a mod b + b*((a/b) mod c). +Proof. + intros a b c Hb Hc. + apply add_cancel_l with (b*c*(a/(b*c))). + rewrite <- div_mod by (apply neq_mul_0; split; order). + rewrite <- div_div by trivial. + rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l. + rewrite <- div_mod by order. + apply div_mod; order. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index 5f52f046f..017f995cc 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -618,6 +618,23 @@ Proof. apply div_mod; order. Qed. +(** Similarly, the following result doesn't always hold for negative + [b] and [c]. For instance [3 mod (-2*-2)) = 3] while + [3 mod (-2) + (-2)*((3/-2) mod -2) = -1]. +*) + +Lemma rem_mul_r : forall a b c, 0<b -> 0<c -> + a mod (b*c) == a mod b + b*((a/b) mod c). +Proof. + intros a b c Hb Hc. + apply add_cancel_l with (b*c*(a/(b*c))). + rewrite <- div_mod by (apply neq_mul_0; split; order). + rewrite <- div_div by trivial. + rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l. + rewrite <- div_mod by order. + apply div_mod; order. +Qed. + (** A last inequality: *) Theorem div_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index e33265762..09f9e023e 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -584,8 +584,7 @@ destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. Qed. - -(** Conversely, the following result needs less restrictions here. *) +(** Conversely, the following results need less restrictions here. *) Lemma quot_quot : forall a b c, b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c). @@ -605,6 +604,18 @@ apply opp_inj. rewrite <- 3 quot_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0. tauto. Qed. +Lemma mod_mul_r : forall a b c, b~=0 -> c~=0 -> + a rem (b*c) == a rem b + b*((a÷b) rem c). +Proof. + intros a b c Hb Hc. + apply add_cancel_l with (b*c*(a÷(b*c))). + rewrite <- quot_rem by (apply neq_mul_0; split; order). + rewrite <- quot_quot by trivial. + rewrite add_assoc, add_shuffle0, <- mul_assoc, <- mul_add_distr_l. + rewrite <- quot_rem by order. + apply quot_rem; order. +Qed. + (** A last inequality: *) Theorem quot_mul_le: diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v index 6b1d4675e..8e128215d 100644 --- a/theories/Numbers/Integer/Abstract/ZGcd.v +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -51,7 +51,7 @@ Proof. now apply divide_abs_l. Qed. -Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-(1). +Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1. Proof. intros n (m,Hm). now apply eq_mul_1 with m. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 27bd5962c..bbf7d893a 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -43,6 +43,43 @@ Proof. apply quot_rem. order. Qed. +(** We can use the sign rule to have an relation between divisions. *) + +Lemma quot_div : forall a b, b~=0 -> + a÷b == (sgn a)*(sgn b)*(abs a / abs b). +Proof. + assert (AUX : forall a b, 0<b -> a÷b == (sgn a)*(sgn b)*(abs a / abs b)). + intros a b Hb. rewrite (sgn_pos b), (abs_eq b), mul_1_r by order. + destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]]. + rewrite sgn_pos, abs_eq, mul_1_l, quot_div_nonneg; order. + rewrite <- Ha, abs_0, sgn_0, quot_0_l, div_0_l, mul_0_l; order. + rewrite sgn_neg, abs_neq, mul_opp_l, mul_1_l, eq_opp_r, <-quot_opp_l + by order. + apply quot_div_nonneg; trivial. apply opp_nonneg_nonpos; order. + (* main *) + intros a b Hb. + apply neg_pos_cases in Hb. destruct Hb as [Hb|Hb]; [|now apply AUX]. + rewrite <- (opp_involutive b) at 1. rewrite quot_opp_r. + rewrite AUX, abs_opp, sgn_opp, mul_opp_r, mul_opp_l, opp_involutive. + reflexivity. + now apply opp_pos_neg. + rewrite eq_opp_l, opp_0; order. +Qed. + +Lemma rem_mod : forall a b, b~=0 -> + a rem b == (sgn a) * ((abs a) mod (abs b)). +Proof. + intros a b Hb. + rewrite <- rem_abs_r by trivial. + assert (Hb' := proj2 (abs_pos b) Hb). + destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]]. + rewrite (abs_eq a), sgn_pos, mul_1_l, rem_mod_nonneg; order. + rewrite <- Ha, abs_0, sgn_0, mod_0_l, rem_0_l, mul_0_l; order. + rewrite sgn_neg, (abs_neq a), mul_opp_l, mul_1_l, eq_opp_r, <-rem_opp_l + by order. + apply rem_mod_nonneg; trivial. apply opp_nonneg_nonpos; order. +Qed. + (** Modulo and remainder are null at the same place, and this correspond to the divisibility relation. *) diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 23eac0e69..5431b4a10 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -121,10 +121,10 @@ Proof. intro; apply lt_neq; apply lt_pred_l. Qed. -Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1). +Theorem lt_m1_r : forall n m, n < m -> m < 0 -> n < -1. Proof. intros n m H1 H2. apply -> lt_le_pred in H2. -setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m. +setoid_replace (P 0) with (-1) in H2. now apply lt_le_trans with m. apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 1010a0f2f..4c0a9a2ca 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -13,8 +13,6 @@ Require Export ZAddOrder. Module Type ZMulOrderProp (Import Z : ZAxiomsMiniSig'). Include ZAddOrderProp Z. -Local Notation "- 1" := (-(1)). - Theorem mul_lt_mono_nonpos : forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. Proof. @@ -135,18 +133,18 @@ now apply lt_1_l with (- m). assumption. Qed. -Theorem lt_mul_n1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1. +Theorem lt_mul_m1_neg : forall n m, 1 < n -> m < 0 -> n * m < -1. Proof. intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1. -rewrite mul_1_l in H1. now apply lt_n1_r with m. +rewrite mul_1_l in H1. now apply lt_m1_r with m. assumption. Qed. -Theorem lt_mul_n1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1. +Theorem lt_mul_m1_pos : forall n m, n < -1 -> 0 < m -> n * m < -1. Proof. intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1. rewrite mul_opp_l, mul_1_l in H1. -apply <- opp_neg_pos in H2. now apply lt_n1_r with (- m). +apply <- opp_neg_pos in H2. now apply lt_m1_r with (- m). assumption. Qed. @@ -154,18 +152,18 @@ Theorem lt_1_mul_l : forall n m, 1 < n -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. Proof. intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]]. -left. now apply lt_mul_n1_neg. +left. now apply lt_mul_m1_neg. right; left; now rewrite H1, mul_0_r. right; right; now apply lt_1_mul_pos. Qed. -Theorem lt_n1_mul_r : forall n m, n < -1 -> +Theorem lt_m1_mul_r : forall n m, n < -1 -> n * m < -1 \/ n * m == 0 \/ 1 < n * m. Proof. intros n m H; destruct (lt_trichotomy m 0) as [H1 | [H1 | H1]]. right; right. now apply lt_1_mul_neg. right; left; now rewrite H1, mul_0_r. -left. now apply lt_mul_n1_pos. +left. now apply lt_mul_m1_pos. Qed. Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 4c752043c..5c7e9eb14 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -6,167 +6,23 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Bool ZMulOrder. +Require Import Bool ZMulOrder NZParity. -(** Properties of [even] and [odd]. *) - -(** NB: most parts of [NParity] and [ZParity] are common, - but it is difficult to share them in NZ, since - initial proofs [Even_or_Odd] and [Even_Odd_False] must - be proved differently *) +(** Some more properties of [even] and [odd]. *) Module Type ZParityProp (Import Z : ZAxiomsSig') (Import ZP : ZMulOrderProp Z). -Instance Even_wd : Proper (eq==>iff) Even. -Proof. unfold Even. solve_predicate_wd. Qed. - -Instance Odd_wd : Proper (eq==>iff) Odd. -Proof. unfold Odd. solve_predicate_wd. Qed. - -Instance even_wd : Proper (eq==>Logic.eq) even. -Proof. - intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd. -Qed. - -Instance odd_wd : Proper (eq==>Logic.eq) odd. -Proof. - intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd. -Qed. - -Lemma Even_or_Odd : forall x, Even x \/ Odd x. -Proof. - nzinduct x. - left. exists 0. now nzsimpl. - intros x. - split; intros [(y,H)|(y,H)]. - right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl'. - right. exists (P y). rewrite <- succ_inj_wd. rewrite H. - nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. - left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. -Qed. - -Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. -Proof. - intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. -Qed. - -Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m. -Proof. - intros. nzsimpl'. - rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. - apply add_le_mono; now apply le_succ_l. -Qed. - -Lemma Even_Odd_False : forall x, Even x -> Odd x -> False. -Proof. -intros x (y,E) (z,O). rewrite O in E; clear O. -destruct (le_gt_cases y z) as [LE|GT]. -generalize (double_below _ _ LE); order. -generalize (double_above _ _ GT); order. -Qed. - -Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. -Proof. - intros. - destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. -Qed. - -Lemma negb_odd_even : forall n, negb (odd n) = even n. -Proof. - intros. - generalize (Even_or_Odd n) (Even_Odd_False n). - rewrite <- even_spec, <- odd_spec. - destruct (odd n), (even n); simpl; intuition. -Qed. - -Lemma negb_even_odd : forall n, negb (even n) = odd n. -Proof. - intros. rewrite <- negb_odd_even. apply negb_involutive. -Qed. - -Lemma even_0 : even 0 = true. -Proof. - rewrite even_spec. exists 0. now nzsimpl. -Qed. - -Lemma odd_1 : odd 1 = true. -Proof. - rewrite odd_spec. exists 0. now nzsimpl'. -Qed. - -Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n. -Proof. - split; intros (m,H). - exists m. apply succ_inj. now rewrite add_1_r in H. - exists m. rewrite add_1_r. now apply succ_wd. -Qed. - -Lemma odd_succ_even : forall n, odd (S n) = even n. -Proof. - intros. apply eq_iff_eq_true. rewrite even_spec, odd_spec. - apply Odd_succ_Even. -Qed. - -Lemma even_succ_odd : forall n, even (S n) = odd n. -Proof. - intros. now rewrite <- negb_odd_even, odd_succ_even, negb_even_odd. -Qed. - -Lemma Even_succ_Odd : forall n, Even (S n) <-> Odd n. -Proof. - intros. now rewrite <- even_spec, even_succ_odd, odd_spec. -Qed. - -Lemma odd_pred_even : forall n, odd (P n) = even n. -Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ_odd. -Qed. - -Lemma even_pred_odd : forall n, even (P n) = odd n. -Proof. - intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ_even. -Qed. - -Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m). -Proof. - intros. - case_eq (even n); case_eq (even m); - rewrite <- ?negb_true_iff, ?negb_even_odd, ?odd_spec, ?even_spec; - intros (m',Hm) (n',Hn). - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. - exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. -Qed. - -Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). -Proof. - intros. rewrite <- !negb_even_odd. rewrite even_add. - now destruct (even n), (even m). -Qed. +Include NZParityProp Z Z ZP. -Lemma even_mul : forall n m, even (mul n m) = even n || even m. +Lemma odd_pred : forall n, odd (P n) = even n. Proof. - intros. - case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. - intros (m',Hm). exists (n*m'). now rewrite Hm, !mul_assoc, (mul_comm 2). - (* odd / odd *) - rewrite <- !negb_true_iff, !negb_even_odd, !odd_spec. - intros (m',Hm) (n',Hn). exists (n'*2*m' +n'+m'). - rewrite Hn,Hm, !mul_add_distr_l, !mul_add_distr_r, !mul_1_l, !mul_1_r. - now rewrite add_shuffle1, add_assoc, !mul_assoc. + intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. Qed. -Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. +Lemma even_pred : forall n, even (P n) = odd n. Proof. - intros. rewrite <- !negb_even_odd. rewrite even_mul. - now destruct (even n), (even m). + intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. Qed. Lemma even_opp : forall n, even (-n) = even n. @@ -180,7 +36,7 @@ Qed. Lemma odd_opp : forall n, odd (-n) = odd n. Proof. - intros. rewrite <- !negb_even_odd. now rewrite even_opp. + intros. rewrite <- !negb_even. now rewrite even_opp. Qed. Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m). diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 8ea012250..682c680cc 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -30,7 +30,7 @@ Qed. Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a. Proof. - intros. now rewrite <- !negb_even_odd, even_pow. + intros. now rewrite <- !negb_even, even_pow. Qed. (** Properties of power of negative numbers *) @@ -80,8 +80,7 @@ Proof. rewrite <- EQ'. nzsimpl. destruct (le_gt_cases 0 b). apply pow_0_l. - assert (b~=0) by - (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0). + assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0). order. now rewrite pow_neg_r. rewrite abs_neq by order. @@ -95,8 +94,7 @@ Proof. destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. apply sgn_pos. apply pow_pos_nonneg; trivial. rewrite <- EQ'. rewrite pow_0_l. apply sgn_0. - assert (b~=0) by - (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0). + assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0). order. apply sgn_neg. rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial. @@ -105,4 +103,22 @@ Proof. now apply opp_pos_neg. Qed. +Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b. +Proof. + intros a b. + destruct (Even_or_Odd b). + rewrite pow_even_abs by trivial. + apply abs_eq, pow_nonneg, abs_nonneg. + rewrite pow_odd_abs_sgn by trivial. + rewrite abs_mul. + destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]]. + rewrite (sgn_pos a), (abs_eq 1), mul_1_l by order'. + apply abs_eq, pow_nonneg, abs_nonneg. + rewrite <- Ha, sgn_0, abs_0, mul_0_l. + symmetry. apply pow_0_l'. intro Hb. rewrite Hb in H. + apply (Even_Odd_False 0); trivial. exists 0; now nzsimpl. + rewrite (sgn_neg a), abs_opp, (abs_eq 1), mul_1_l by order'. + apply abs_eq, pow_nonneg, abs_nonneg. +Qed. + End ZPowProp. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index d04443d9c..c04551960 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -7,7 +7,7 @@ (************************************************************************) Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor - ZGcd ZLcm NZLog NZSqrt. + ZGcd ZLcm NZLog NZSqrt ZBits. (** This functor summarizes all known facts about Z. *) @@ -15,4 +15,5 @@ Module Type ZProp (Z:ZAxiomsSig) := ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z - <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z. + <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z + <+ ZBitsProp Z. diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index 6d90bc0fd..b2f6cc84d 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -37,12 +37,12 @@ Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare. Module Type GenericSgn (Import Z : ZDecAxiomsSig') (Import ZP : ZMulOrderProp Z) <: HasSgn Z. Definition sgn n := - match compare 0 n with Eq => 0 | Lt => 1 | Gt => -(1) end. + match compare 0 n with Eq => 0 | Lt => 1 | Gt => -1 end. Lemma sgn_null : forall n, n==0 -> sgn n == 0. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. Lemma sgn_pos : forall n, 0<n -> sgn n == 1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. - Lemma sgn_neg : forall n, n<0 -> sgn n == -(1). + Lemma sgn_neg : forall n, n<0 -> sgn n == -1. Proof. unfold sgn; intros. destruct (compare_spec 0 n); order. Qed. End GenericSgn. @@ -168,6 +168,28 @@ Proof. rewrite EQn, EQ, opp_inj_wd, eq_opp_l, or_comm. apply abs_eq_or_opp. Qed. +Lemma abs_lt : forall a b, abs a < b <-> -b < a < b. +Proof. + intros a b. + destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ. + split; try split; try destruct 1; try order. + apply lt_le_trans with 0; trivial. apply opp_neg_pos; order. + rewrite opp_lt_mono, opp_involutive. + split; try split; try destruct 1; try order. + apply lt_le_trans with 0; trivial. apply opp_nonpos_nonneg; order. +Qed. + +Lemma abs_le : forall a b, abs a <= b <-> -b <= a <= b. +Proof. + intros a b. + destruct (abs_spec a) as [[LE EQ]|[LT EQ]]; rewrite EQ; clear EQ. + split; try split; try destruct 1; try order. + apply le_trans with 0; trivial. apply opp_nonpos_nonneg; order. + rewrite opp_le_mono, opp_involutive. + split; try split; try destruct 1; try order. + apply le_trans with 0. order. apply opp_nonpos_nonneg; order. +Qed. + (** Triangular inequality *) Lemma abs_triangle : forall n m, abs (n + m) <= abs n + abs m. @@ -234,7 +256,7 @@ Qed. Lemma sgn_spec : forall n, 0 < n /\ sgn n == 1 \/ 0 == n /\ sgn n == 0 \/ - 0 > n /\ sgn n == -(1). + 0 > n /\ sgn n == -1. Proof. intros n. destruct_sgn n; [left|right;left|right;right]; auto with relations. @@ -249,7 +271,7 @@ Lemma sgn_pos_iff : forall n, sgn n == 1 <-> 0<n. Proof. split; try apply sgn_pos. destruct_sgn n; auto. intros. elim (lt_neq 0 1); auto. apply lt_0_1. - intros. elim (lt_neq (-(1)) 1); auto. + intros. elim (lt_neq (-1) 1); auto. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. Qed. @@ -257,16 +279,16 @@ Lemma sgn_null_iff : forall n, sgn n == 0 <-> n==0. Proof. split; try apply sgn_null. destruct_sgn n; auto with relations. intros. elim (lt_neq 0 1); auto with relations. apply lt_0_1. - intros. elim (lt_neq (-(1)) 0); auto. + intros. elim (lt_neq (-1) 0); auto. rewrite opp_neg_pos. apply lt_0_1. Qed. -Lemma sgn_neg_iff : forall n, sgn n == -(1) <-> n<0. +Lemma sgn_neg_iff : forall n, sgn n == -1 <-> n<0. Proof. split; try apply sgn_neg. destruct_sgn n; auto with relations. - intros. elim (lt_neq (-(1)) 1); auto with relations. + intros. elim (lt_neq (-1) 1); auto with relations. apply lt_trans with 0. rewrite opp_neg_pos. apply lt_0_1. apply lt_0_1. - intros. elim (lt_neq (-(1)) 0); auto with relations. + intros. elim (lt_neq (-1) 0); auto with relations. rewrite opp_neg_pos. apply lt_0_1. Qed. |