diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
18 files changed, 3832 insertions, 574 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v index d9624ea3..647ab0ac 100644 --- a/theories/Numbers/Integer/Abstract/ZAdd.v +++ b/theories/Numbers/Integer/Abstract/ZAdd.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,34 +8,33 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZBase. -Module ZAddPropFunct (Import Z : ZAxiomsSig'). -Include ZBasePropFunct Z. +Module ZAddProp (Import Z : ZAxiomsMiniSig'). +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. -intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd. +now nzsimpl. +intro m. rewrite opp_succ, sub_succ_r, add_pred_r. now rewrite pred_inj_wd. Qed. Theorem sub_0_l : forall n, 0 - n == - n. @@ -45,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). @@ -69,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. @@ -90,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. -intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd. +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. @@ -116,12 +115,12 @@ 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. Proof. -intros n m; split; [apply opp_inj | apply opp_wd]. +intros n m; split; [apply opp_inj | intros; now f_equiv]. Qed. Theorem eq_opp_l : forall n m, - n == m <-> n == - m. @@ -137,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. @@ -148,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. @@ -165,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. @@ -252,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 *) @@ -289,5 +293,5 @@ Qed. (** Of course, there are many other variants *) -End ZAddPropFunct. +End ZAddProp. diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index 6ce54f88..423cdf58 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,180 +8,173 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZAddOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZLt. -Module ZAddOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZOrderPropFunct Z. +Module ZAddOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZOrderProp Z. (** Theorems that are either not valid on N or have different proofs on N and 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. +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. @@ -196,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. @@ -218,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. @@ -295,6 +280,6 @@ End PosNeg. Ltac zero_pos_neg n := induction_maker n ltac:(apply zero_pos_neg). -End ZAddOrderPropFunct. +End ZAddOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index fd14cff0..fd20ce72 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,11 +8,19 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NZAxioms. +Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits. + +(** We obtain integers by postulating that successor of predecessor + is identity. *) + +Module Type ZAxiom (Import Z : NZAxiomsSig'). + Axiom succ_pred : forall n, S (P n) == n. +End ZAxiom. -Set Implicit Arguments. +(** For historical reasons, ZAxiomsMiniSig isn't just NZ + ZAxiom, + we also add an [opp] function, that can be seen as a shortcut + for [sub 0]. *) Module Type Opp (Import T:Typ). Parameter Inline opp : t -> t. @@ -24,15 +32,91 @@ End OppNotation. Module Type Opp' (T:Typ) := Opp T <+ OppNotation T. -(** We obtain integers by postulating that every number has a predecessor. *) - Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z). Declare Instance opp_wd : Proper (eq==>eq) opp. - Axiom succ_pred : forall n, S (P n) == n. Axiom opp_0 : - 0 == 0. Axiom opp_succ : forall n, - (S n) == P (- n). End IsOpp. -Module Type ZAxiomsSig := NZOrdAxiomsSig <+ Opp <+ IsOpp. -Module Type ZAxiomsSig' := NZOrdAxiomsSig' <+ Opp' <+ 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 + <+ OppCstNotation. + + +(** Other functions and their specifications *) + +(** Absolute value *) + +Module Type HasAbs(Import Z : ZAxiomsMiniSig'). + Parameter Inline abs : t -> t. + Axiom abs_eq : forall n, 0<=n -> abs n == n. + Axiom abs_neq : forall n, n<=0 -> abs n == -n. +End HasAbs. + +(** A sign function *) + +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. +End HasSgn. + +(** Divisions *) + +(** First, the usual Coq convention of Truncated-Toward-Bottom + (a.k.a Floor). We simply extend the NZ signature. *) + +Module Type ZDivSpecific (Import A:ZAxiomsMiniSig')(Import B : DivMod' A). + Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. + Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. +End ZDivSpecific. + +Module Type ZDiv (Z:ZAxiomsMiniSig) := NZDiv.NZDiv Z <+ ZDivSpecific Z. +Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z. + +(** Then, the Truncated-Toward-Zero convention. + For not colliding with Floor operations, we use different names +*) + +Module Type QuotRem (Import A : Typ). + Parameters Inline quot rem : t -> t -> t. +End QuotRem. + +Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A). + Infix "÷" := quot (at level 40, left associativity). + Infix "rem" := rem (at level 40, no associativity). +End QuotRemNotation. + +Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A. + +Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A). + Declare Instance quot_wd : Proper (eq==>eq==>eq) quot. + Declare Instance rem_wd : Proper (eq==>eq==>eq) B.rem. + Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b). + Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b. + Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b). + Axiom rem_opp_r : forall a b, b ~= 0 -> a rem (-b) == a rem b. +End QuotRemSpec. + +Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z. +Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z. + +(** For all other functions, the NZ axiomatizations are enough. *) + +(** Let's group everything *) + +Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions + <+ HasAbs <+ HasSgn <+ NZParity.NZParity + <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd + <+ ZDiv <+ ZQuot <+ NZBits.NZBits <+ NZSquare. +Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions' + <+ HasAbs <+ HasSgn <+ NZParity.NZParity + <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' + <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits' <+ NZSquare. diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index aa7979ae..51054852 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,26 +8,29 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Decidable. Require Export ZAxioms. Require Import NZProperties. -Module ZBasePropFunct (Import Z : ZAxiomsSig'). -Include NZPropFunct Z. +Module ZBaseProp (Import Z : ZAxiomsMiniSig'). +Include NZProp Z. (* Theorems that are true for integers but not for natural numbers *) 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. Proof. -intros n1 n2; split; [apply pred_inj | apply pred_wd]. +intros n1 n2; split; [apply pred_inj | intros; now f_equiv]. +Qed. + +Lemma succ_m1 : S (-1) == 0. +Proof. + now rewrite one_succ, opp_succ, opp_0, succ_pred. Qed. -End ZBasePropFunct. +End ZBaseProp. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v new file mode 100644 index 00000000..92afbcb5 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -0,0 +1,1947 @@ +(************************************************************************) +(* 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. + +Instance b2z_wd : Proper (Logic.eq ==> eq) b2z := _. + +Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. +Proof. + elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. + exists a'. exists false. now nzsimpl. + exists a'. exists true. now simpl. +Qed. + +(** We can compact [testbit_odd_0] [testbit_even_0] + [testbit_even_succ] [testbit_odd_succ] in only two lemmas. *) + +Lemma testbit_0_r a (b:bool) : testbit (2*a+b) 0 = b. +Proof. + destruct b; simpl; rewrite ?add_0_r. + apply testbit_odd_0. + apply testbit_even_0. +Qed. + +Lemma testbit_succ_r a (b:bool) n : 0<=n -> + testbit (2*a+b) (succ n) = testbit a n. +Proof. + destruct b; simpl; rewrite ?add_0_r. + now apply testbit_odd_succ. + now apply testbit_even_succ. +Qed. + +(** Alternative caracterisations of [testbit] *) + +(** This concise equation could have been taken as specification + for testbit in the interface, but it would have been hard to + implement with little initial knowledge about div and mod *) + +Lemma testbit_spec' a n : 0<=n -> a.[n] == (a / 2^n) mod 2. +Proof. + intro Hn. revert a. apply le_ind with (4:=Hn). + solve_proper. + intros a. nzsimpl. + destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. + rewrite testbit_0_r. apply mod_unique with a'; trivial. + left. destruct b; split; simpl; order'. + clear n Hn. intros n Hn IH a. + destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. + rewrite testbit_succ_r, IH by trivial. f_equiv. + rewrite pow_succ_r, <- div_div by order_pos. f_equiv. + apply div_unique with b; trivial. + left. destruct b; split; simpl; order'. +Qed. + +(** This caracterisation that uses only basic operations and + power was initially taken as specification for testbit. + We describe [a] as having a low part and a high part, with + the corresponding bit in the middle. This caracterisation + is moderatly complex to implement, but also moderately + usable... *) + +Lemma testbit_spec a n : 0<=n -> + exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n. +Proof. + intro Hn. exists (a mod 2^n). exists (a / 2^n / 2). split. + apply mod_pos_bound; order_pos. + rewrite add_comm, mul_comm, (add_comm a.[n]). + rewrite (div_mod a (2^n)) at 1 by order_nz. do 2 f_equiv. + rewrite testbit_spec' by trivial. apply div_mod. order'. +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. + +(** 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 specification of testbit by low and high parts 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. f_equiv. + 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. + f_equiv. + 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_odd : forall a, a.[0] = odd a. +Proof. + intros. symmetry. + destruct (exists_div2 a) as (a' & b & EQ). + rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2. + destruct b; simpl; apply odd_1 || apply odd_0. +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_mod : forall a, a.[0] == a mod 2. +Proof. + intros a. rewrite testbit_spec' by order. now nzsimpl. +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_proper. + 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 in Hn. le_elim 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_proper. + 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. + le_elim LE. + apply bits_above_log2; try order. + apply lt_le_trans with n; trivial. + apply log2_lt_pow2; trivial. + now rewrite <- LE, 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_proper. + 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'. + f_equiv; [ | now rewrite <- 2 bit0_mod, H]. + f_equiv. + 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_proper 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_proper. + intros m Hm. apply Hk. now rewrite <- succ_le_mono. + exists (f 0 + 2*n). intros m Hm. + le_elim 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<=m -> + (a >> n) >> m == a >> (n+m). +Proof. + intros a n p Hn. bitwise. + rewrite 3 shiftr_spec; trivial. + now rewrite (add_comm n p), add_assoc. + now apply add_nonneg_nonneg. +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. + le_elim 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. unfold setbit. solve_proper. Qed. + +Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit. +Proof. unfold clearbit. solve_proper. 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. unfold lnot. solve_proper. 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. unfold ones. solve_proper. 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. + f_equiv. 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). le_elim 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. + le_elim 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 LT. + assert (H : 0 <= land a b) by (apply land_nonneg; now left). + le_elim H. + generalize (bit_log2 (land a b) H). + now rewrite land_spec, bits_above_log2. + rewrite <- H in LT. apply log2_lt_cancel in LT; 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 LT. + assert (H : 0 <= lxor a b) by (apply lxor_nonneg; split; order). + le_elim H. + generalize (bit_log2 (lxor a b) H). + rewrite lxor_spec, 2 bits_above_log2; try order. discriminate. + apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. + rewrite <- H in LT. apply log2_lt_cancel in LT; 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'. + f_equiv. + 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_proper. + (* base *) + intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r, <- !one_succ. + intros (Ha1,Ha2) (Hb1,Hb2). + le_elim Ha1; rewrite <- ?le_succ_l, ?succ_m1 in Ha1; + le_elim Hb1; rewrite <- ?le_succ_l, ?succ_m1 in 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. + le_elim Hm. + rewrite <- (succ_pred m), lt_succ_r in Hm. + rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial. + f_equiv. + 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. + le_elim 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_proper. + 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_proper. + 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 4555e733..fe951a75 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -1,11 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem @@ -19,37 +21,29 @@ Vol. 14, No.2, pp. 127-144, April 1992. See files [ZDivTrunc] and [ZDivFloor] for others conventions. -*) - -Require Import ZAxioms ZProperties NZDiv. -Module Type ZDivSpecific (Import Z : ZAxiomsExtSig')(Import DM : DivMod' Z). - Axiom mod_always_pos : forall a b, 0 <= a mod b < abs b. -End ZDivSpecific. - -Module Type ZDiv (Z:ZAxiomsExtSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. + We simply extend NZDiv with a bound for modulo that holds + regardless of the sign of a and b. This new specification + subsume mod_bound_pos, which nonetheless stays there for + subtyping. Note also that ZAxiomSig now already contain + a div and a modulo (that follow the Floor convention). + We just ignore them here. +*) -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +End EuclidSpec. -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. +Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. -(** We benefit from what already exists for NZ *) +Module ZEuclidProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B) + (Import D : ZEuclid' A). - Module ZD <: NZDiv Z. - Definition div := div. - Definition modulo := modulo. - Definition div_wd := div_wd. - Definition mod_wd := mod_wd. - Definition div_mod := div_mod. - Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Proof. - intros. rewrite <- (abs_eq b) at 3 by now apply lt_le_incl. - apply mod_always_pos. - Qed. - End ZD. - Module Import NZDivP := NZDivPropFunct Z ZP ZD. + Module Import Private_NZDiv := Nop <+ NZDivProp A D B. (** Another formulation of the main equation *) @@ -117,7 +111,7 @@ Lemma div_opp_r : forall a b, b~=0 -> a/(-b) == -(a/b). Proof. intros. symmetry. apply div_unique with (a mod b). -rewrite abs_opp; apply mod_always_pos. +rewrite abs_opp; now apply mod_always_pos. rewrite mul_opp_opp; now apply div_mod. Qed. @@ -125,7 +119,7 @@ Lemma mod_opp_r : forall a b, b~=0 -> a mod (-b) == a mod b. Proof. intros. symmetry. apply mod_unique with (-(a/b)). -rewrite abs_opp; apply mod_always_pos. +rewrite abs_opp; now apply mod_always_pos. rewrite mul_opp_opp; now apply div_mod. Qed. @@ -274,6 +268,11 @@ Proof. intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag. Qed. +Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b. +Proof. + intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul. +Qed. + (** * Order results about mod and div *) (** A modulo cannot grow beyond its starting point. *) @@ -296,7 +295,7 @@ intros a b Hb. split. intros EQ. rewrite (div_mod a b Hb), EQ; nzsimpl. -apply mod_always_pos. +now apply mod_always_pos. intros. pos_or_neg b. apply div_small. now rewrite <- (abs_eq b). @@ -365,7 +364,7 @@ intros. nzsimpl. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. -destruct (mod_always_pos a b). +destruct (mod_always_pos a b). order. rewrite abs_eq in *; order. Qed. @@ -375,7 +374,7 @@ intros a b Hb. rewrite mul_pred_r, <- add_opp_r. rewrite (div_mod a b) at 1; try order. rewrite <- add_lt_mono_l. -destruct (mod_always_pos a b). +destruct (mod_always_pos a b). order. rewrite <- opp_pos_neg in Hb. rewrite abs_neq' in *; order. Qed. @@ -469,7 +468,7 @@ apply div_unique with ((a mod b)*c). (* ineqs *) rewrite abs_mul, (abs_eq c) by order. rewrite <-(mul_0_l c), <-mul_lt_mono_pos_r, <-mul_le_mono_pos_r by trivial. -apply mod_always_pos. +now apply mod_always_pos. (* equation *) rewrite (div_mod a b) at 1 by order. rewrite mul_add_distr_r. @@ -556,17 +555,18 @@ Proof. Qed. (** With the current convention, the following result isn't always - true for negative divisors. For instance - [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *) + true with a negative intermediate divisor. For instance + [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ] and + [ 3/(-2)/2 = -1 <> 0 = 3 / (-2*2) ]. *) -Lemma div_div : forall a b c, 0<b -> 0<c -> +Lemma div_div : forall a b c, 0<b -> c~=0 -> (a/b)/c == a/(b*c). Proof. intros a b c Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b). (* begin 0<= ... <abs(b*c) *) rewrite abs_mul. - destruct (mod_always_pos (a/b) c), (mod_always_pos a b). + destruct (mod_always_pos (a/b) c), (mod_always_pos a b); try order. split. apply add_nonneg_nonneg; trivial. apply mul_nonneg_nonneg; order. @@ -581,6 +581,22 @@ Proof. apply div_mod; order. Qed. +(** Similarly, the following result doesn't always hold when [b<0]. + 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 -> c~=0 -> + 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: @@ -590,16 +606,13 @@ Proof. exact div_mul_le. Qed. (** mod is related to divisibility *) Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). + (a mod b == 0 <-> (b|a)). Proof. intros a b Hb. split. -intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. - rewrite Hab; now nzsimpl. -intros (c,Hc). -rewrite Hc, mul_comm. -now apply mod_mul. +intros Hab. exists (a/b). rewrite mul_comm. + rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl. +intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. - -End ZDivPropFunct. +End ZEuclidProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v index efefab81..14003d89 100644 --- a/theories/Numbers/Integer/Abstract/ZDivFloor.v +++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v @@ -1,11 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers (Floor convention) We use here the convention known as Floor, or Round-Toward-Bottom, @@ -24,33 +26,13 @@ See files [ZDivTrunc] and [ZDivEucl] for others conventions. *) -Require Import ZAxioms ZProperties NZDiv. - -Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). - Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b. - Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0. -End ZDivSpecific. - -Module Type ZDiv (Z:ZAxiomsSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. - -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. - -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module Type ZDivProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B). (** We benefit from what already exists for NZ *) - - Module ZD <: NZDiv Z. - Definition div := div. - Definition modulo := modulo. - Definition div_wd := div_wd. - Definition mod_wd := mod_wd. - Definition div_mod := div_mod. - Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Proof. intros. now apply mod_pos_bound. Qed. - End ZD. - Module Import NZDivP := NZDivPropFunct Z ZP ZD. +Module Import Private_NZDiv := Nop <+ NZDivProp A A B. (** Another formulation of the main equation *) @@ -62,6 +44,18 @@ rewrite <- add_move_l. symmetry. now apply div_mod. Qed. +(** We have a general bound for absolute values *) + +Lemma mod_bound_abs : + forall a b, b~=0 -> abs (a mod b) < abs b. +Proof. +intros. +destruct (abs_spec b) as [(LE,EQ)|(LE,EQ)]; rewrite EQ. +destruct (mod_pos_bound a b). order. now rewrite abs_eq. +destruct (mod_neg_bound a b). order. rewrite abs_neq; trivial. +now rewrite <- opp_lt_mono. +Qed. + (** Uniqueness theorems *) Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, @@ -94,7 +88,7 @@ Theorem div_unique_pos: Proof. intros; apply div_unique with r; auto. Qed. Theorem div_unique_neg: - forall a b q r, 0<=r<b -> a == b*q + r -> q == a/b. + forall a b q r, b<r<=0 -> a == b*q + r -> q == a/b. Proof. intros; apply div_unique with r; auto. Qed. Theorem mod_unique: @@ -230,11 +224,26 @@ rewrite mod_opp_opp, mod_opp_l_nz by trivial. now rewrite opp_sub_distr, add_comm, add_opp_r. Qed. -(** The sign of [a mod b] is the one of [b] *) +(** The sign of [a mod b] is the one of [b] (when it isn't null) *) + +Lemma mod_sign_nz : forall a b, b~=0 -> a mod b ~= 0 -> + sgn (a mod b) == sgn b. +Proof. +intros a b Hb H. destruct (lt_ge_cases 0 b) as [Hb'|Hb']. +destruct (mod_pos_bound a b Hb'). rewrite 2 sgn_pos; order. +destruct (mod_neg_bound a b). order. rewrite 2 sgn_neg; order. +Qed. -(* TODO: a proper sgn function and theory *) +Lemma mod_sign : forall a b, b~=0 -> sgn (a mod b) ~= -sgn b. +Proof. +intros a b Hb H. +destruct (eq_decidable (a mod b) 0) as [EQ|NEQ]. +apply Hb, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0. +apply Hb, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'. +apply add_move_0_l. rewrite <- H. symmetry. now apply mod_sign_nz. +Qed. -Lemma mod_sign : forall a b, b~=0 -> (0 <= (a mod b) * b). +Lemma mod_sign_mul : forall a b, b~=0 -> 0 <= (a mod b) * b. Proof. intros. destruct (lt_ge_cases 0 b). apply mul_nonneg_nonneg; destruct (mod_pos_bound a b); order. @@ -307,6 +316,11 @@ Proof. intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag. Qed. +Theorem div_unique_exact a b q: b~=0 -> a == b*q -> q == a/b. +Proof. + intros Hb H. rewrite H, mul_comm. symmetry. now apply div_mul. +Qed. + (** * Order results about mod and div *) (** A modulo cannot grow beyond its starting point. *) @@ -585,15 +599,25 @@ Proof. Qed. (** With the current convention, the following result isn't always - true for negative divisors. For instance - [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ]. *) + true with a negative last divisor. For instance + [ 3/(-2)/(-2) = 1 <> 0 = 3 / (-2*-2) ], or + [ 5/2/(-2) = -1 <> -2 = 5 / (2*-2) ]. *) -Lemma div_div : forall a b c, 0<b -> 0<c -> +Lemma div_div : forall a b c, b~=0 -> 0<c -> (a/b)/c == a/(b*c). Proof. intros a b c Hb Hc. apply div_unique with (b*((a/b) mod c) + a mod b). (* begin 0<= ... <b*c \/ ... *) + apply neg_pos_cases in Hb. destruct Hb as [Hb|Hb]. + right. + destruct (mod_pos_bound (a/b) c), (mod_neg_bound a b); trivial. + split. + apply le_lt_trans with (b*((a/b) mod c) + b). + now rewrite <- mul_succ_r, <- mul_le_mono_neg_l, le_succ_l. + now rewrite <- add_lt_mono_l. + apply add_nonpos_nonpos; trivial. + apply mul_nonpos_nonneg; order. left. destruct (mod_pos_bound (a/b) c), (mod_pos_bound a b); trivial. split. @@ -609,24 +633,27 @@ Proof. apply div_mod; order. Qed. +(** Similarly, the following result doesn't always hold when [c<0]. + 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, b~=0 -> 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: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. exact div_mul_le. Qed. -(** mod is related to divisibility *) - -Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). -Proof. -intros a b Hb. split. -intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. - rewrite Hab. now nzsimpl. -intros (c,Hc). -rewrite Hc, mul_comm. -now apply mod_mul. -Qed. - -End ZDivPropFunct. - +End ZDivProp. diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v index 069d8a8d..bd8b6ce2 100644 --- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v +++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v @@ -1,11 +1,13 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 ZAxioms ZMulOrder ZSgnAbs NZDiv. + (** * Euclidean Division for integers (Trunc convention) We use here the convention known as Trunc, or Round-Toward-Zero, @@ -24,25 +26,24 @@ See files [ZDivFloor] and [ZDivEucl] for others conventions. *) -Require Import ZAxioms ZProperties NZDiv. - -Module Type ZDivSpecific (Import Z:ZAxiomsSig')(Import DM : DivMod' Z). - Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. - Axiom mod_opp_l : forall a b, b ~= 0 -> (-a) mod b == - (a mod b). - Axiom mod_opp_r : forall a b, b ~= 0 -> a mod (-b) == a mod b. -End ZDivSpecific. - -Module Type ZDiv (Z:ZAxiomsSig) - := DivMod Z <+ NZDivCommon Z <+ ZDivSpecific Z. - -Module Type ZDivSig := ZAxiomsExtSig <+ ZDiv. -Module Type ZDivSig' := ZAxiomsExtSig' <+ ZDiv <+ DivModNotation. - -Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z). +Module Type ZQuotProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B). (** We benefit from what already exists for NZ *) - Module Import NZDivP := NZDivPropFunct Z ZP Z. + Module Import Private_Div. + Module Quot2Div <: NZDiv A. + Definition div := quot. + Definition modulo := A.rem. + Definition div_wd := quot_wd. + Definition mod_wd := rem_wd. + Definition div_mod := quot_rem. + Definition mod_bound_pos := rem_bound_pos. + End Quot2Div. + Module NZQuot := Nop <+ NZDivProp A Quot2Div B. + End Private_Div. Ltac pos_or_neg a := let LT := fresh "LT" in @@ -51,175 +52,274 @@ Ltac pos_or_neg a := (** Another formulation of the main equation *) -Lemma mod_eq : - forall a b, b~=0 -> a mod b == a - b*(a/b). +Lemma rem_eq : + forall a b, b~=0 -> a rem b == a - b*(a÷b). Proof. intros. rewrite <- add_move_l. -symmetry. now apply div_mod. +symmetry. now apply quot_rem. Qed. (** A few sign rules (simple ones) *) -Lemma mod_opp_opp : forall a b, b ~= 0 -> (-a) mod (-b) == - (a mod b). -Proof. intros. now rewrite mod_opp_r, mod_opp_l. Qed. +Lemma rem_opp_opp : forall a b, b ~= 0 -> (-a) rem (-b) == - (a rem b). +Proof. intros. now rewrite rem_opp_r, rem_opp_l. Qed. -Lemma div_opp_l : forall a b, b ~= 0 -> (-a)/b == -(a/b). +Lemma quot_opp_l : forall a b, b ~= 0 -> (-a)÷b == -(a÷b). Proof. intros. rewrite <- (mul_cancel_l _ _ b) by trivial. -rewrite <- (add_cancel_r _ _ ((-a) mod b)). -now rewrite <- div_mod, mod_opp_l, mul_opp_r, <- opp_add_distr, <- div_mod. +rewrite <- (add_cancel_r _ _ ((-a) rem b)). +now rewrite <- quot_rem, rem_opp_l, mul_opp_r, <- opp_add_distr, <- quot_rem. Qed. -Lemma div_opp_r : forall a b, b ~= 0 -> a/(-b) == -(a/b). +Lemma quot_opp_r : forall a b, b ~= 0 -> a÷(-b) == -(a÷b). Proof. intros. assert (-b ~= 0) by (now rewrite eq_opp_l, opp_0). rewrite <- (mul_cancel_l _ _ (-b)) by trivial. -rewrite <- (add_cancel_r _ _ (a mod (-b))). -now rewrite <- div_mod, mod_opp_r, mul_opp_opp, <- div_mod. -Qed. - -Lemma div_opp_opp : forall a b, b ~= 0 -> (-a)/(-b) == a/b. -Proof. intros. now rewrite div_opp_r, div_opp_l, opp_involutive. Qed. - -(** The sign of [a mod b] is the one of [a] *) - -(* TODO: a proper sgn function and theory *) - -Lemma mod_sign : forall a b, b~=0 -> 0 <= (a mod b) * a. -Proof. -assert (Aux : forall a b, 0<b -> 0 <= (a mod b) * a). - intros. pos_or_neg a. - apply mul_nonneg_nonneg; trivial. now destruct (mod_bound a b). - rewrite <- mul_opp_opp, <- mod_opp_l by order. - apply mul_nonneg_nonneg; try order. destruct (mod_bound (-a) b); order. -intros. pos_or_neg b. apply Aux; order. -rewrite <- mod_opp_r by order. apply Aux; order. +rewrite <- (add_cancel_r _ _ (a rem (-b))). +now rewrite <- quot_rem, rem_opp_r, mul_opp_opp, <- quot_rem. Qed. +Lemma quot_opp_opp : forall a b, b ~= 0 -> (-a)÷(-b) == a÷b. +Proof. intros. now rewrite quot_opp_r, quot_opp_l, opp_involutive. Qed. (** Uniqueness theorems *) -Theorem div_mod_unique : forall b q1 q2 r1 r2 : t, +Theorem quot_rem_unique : forall b q1 q2 r1 r2 : t, (0<=r1<b \/ b<r1<=0) -> (0<=r2<b \/ b<r2<=0) -> b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. Proof. intros b q1 q2 r1 r2 Hr1 Hr2 EQ. destruct Hr1; destruct Hr2; try (intuition; order). -apply div_mod_unique with b; trivial. +apply NZQuot.div_mod_unique with b; trivial. rewrite <- (opp_inj_wd r1 r2). -apply div_mod_unique with (-b); trivial. +apply NZQuot.div_mod_unique with (-b); trivial. rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. rewrite <- opp_lt_mono, opp_nonneg_nonpos; tauto. now rewrite 2 mul_opp_l, <- 2 opp_add_distr, opp_inj_wd. Qed. -Theorem div_unique: - forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a/b. -Proof. intros; now apply div_unique with r. Qed. +Theorem quot_unique: + forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> q == a÷b. +Proof. intros; now apply NZQuot.div_unique with r. Qed. -Theorem mod_unique: - forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a mod b. -Proof. intros; now apply mod_unique with q. Qed. +Theorem rem_unique: + forall a b q r, 0<=a -> 0<=r<b -> a == b*q + r -> r == a rem b. +Proof. intros; now apply NZQuot.mod_unique with q. Qed. (** A division by itself returns 1 *) -Lemma div_same : forall a, a~=0 -> a/a == 1. +Lemma quot_same : forall a, a~=0 -> a÷a == 1. Proof. -intros. pos_or_neg a. apply div_same; order. -rewrite <- div_opp_opp by trivial. now apply div_same. +intros. pos_or_neg a. apply NZQuot.div_same; order. +rewrite <- quot_opp_opp by trivial. now apply NZQuot.div_same. Qed. -Lemma mod_same : forall a, a~=0 -> a mod a == 0. +Lemma rem_same : forall a, a~=0 -> a rem a == 0. Proof. -intros. rewrite mod_eq, div_same by trivial. nzsimpl. apply sub_diag. +intros. rewrite rem_eq, quot_same by trivial. nzsimpl. apply sub_diag. Qed. (** A division of a small number by a bigger one yields zero. *) -Theorem div_small: forall a b, 0<=a<b -> a/b == 0. -Proof. exact div_small. Qed. +Theorem quot_small: forall a b, 0<=a<b -> a÷b == 0. +Proof. exact NZQuot.div_small. Qed. -(** Same situation, in term of modulo: *) +(** Same situation, in term of remulo: *) -Theorem mod_small: forall a b, 0<=a<b -> a mod b == a. -Proof. exact mod_small. Qed. +Theorem rem_small: forall a b, 0<=a<b -> a rem b == a. +Proof. exact NZQuot.mod_small. Qed. (** * Basic values of divisions and modulo. *) -Lemma div_0_l: forall a, a~=0 -> 0/a == 0. +Lemma quot_0_l: forall a, a~=0 -> 0÷a == 0. Proof. -intros. pos_or_neg a. apply div_0_l; order. -rewrite <- div_opp_opp, opp_0 by trivial. now apply div_0_l. +intros. pos_or_neg a. apply NZQuot.div_0_l; order. +rewrite <- quot_opp_opp, opp_0 by trivial. now apply NZQuot.div_0_l. Qed. -Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0. +Lemma rem_0_l: forall a, a~=0 -> 0 rem a == 0. Proof. -intros; rewrite mod_eq, div_0_l; now nzsimpl. +intros; rewrite rem_eq, quot_0_l; now nzsimpl. Qed. -Lemma div_1_r: forall a, a/1 == a. +Lemma quot_1_r: forall a, a÷1 == a. Proof. -intros. pos_or_neg a. now apply div_1_r. -apply opp_inj. rewrite <- div_opp_l. apply div_1_r; order. +intros. pos_or_neg a. now apply NZQuot.div_1_r. +apply opp_inj. rewrite <- quot_opp_l. apply NZQuot.div_1_r; order. intro EQ; symmetry in EQ; revert EQ; apply lt_neq, lt_0_1. Qed. -Lemma mod_1_r: forall a, a mod 1 == 0. +Lemma rem_1_r: forall a, a rem 1 == 0. Proof. -intros. rewrite mod_eq, div_1_r; nzsimpl; auto using sub_diag. +intros. rewrite rem_eq, quot_1_r; nzsimpl; auto using sub_diag. intro EQ; symmetry in EQ; revert EQ; apply lt_neq; apply lt_0_1. Qed. -Lemma div_1_l: forall a, 1<a -> 1/a == 0. -Proof. exact div_1_l. Qed. +Lemma quot_1_l: forall a, 1<a -> 1÷a == 0. +Proof. exact NZQuot.div_1_l. Qed. + +Lemma rem_1_l: forall a, 1<a -> 1 rem a == 1. +Proof. exact NZQuot.mod_1_l. Qed. -Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. -Proof. exact mod_1_l. Qed. +Lemma quot_mul : forall a b, b~=0 -> (a*b)÷b == a. +Proof. +intros. pos_or_neg a; pos_or_neg b. apply NZQuot.div_mul; order. +rewrite <- quot_opp_opp, <- mul_opp_r by order. apply NZQuot.div_mul; order. +rewrite <- opp_inj_wd, <- quot_opp_l, <- mul_opp_l by order. +apply NZQuot.div_mul; order. +rewrite <- opp_inj_wd, <- quot_opp_r, <- mul_opp_opp by order. +apply NZQuot.div_mul; order. +Qed. -Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a. +Lemma rem_mul : forall a b, b~=0 -> (a*b) rem b == 0. Proof. -intros. pos_or_neg a; pos_or_neg b. apply div_mul; order. -rewrite <- div_opp_opp, <- mul_opp_r by order. apply div_mul; order. -rewrite <- opp_inj_wd, <- div_opp_l, <- mul_opp_l by order. apply div_mul; order. -rewrite <- opp_inj_wd, <- div_opp_r, <- mul_opp_opp by order. apply div_mul; order. +intros. rewrite rem_eq, quot_mul by trivial. rewrite mul_comm; apply sub_diag. Qed. -Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0. +Theorem quot_unique_exact a b q: b~=0 -> a == b*q -> q == a÷b. Proof. -intros. rewrite mod_eq, div_mul by trivial. rewrite mul_comm; apply sub_diag. + intros Hb H. rewrite H, mul_comm. symmetry. now apply quot_mul. Qed. -(** * Order results about mod and div *) +(** The sign of [a rem b] is the one of [a] (when it's not null) *) + +Lemma rem_nonneg : forall a b, b~=0 -> 0 <= a -> 0 <= a rem b. +Proof. + intros. pos_or_neg b. destruct (rem_bound_pos a b); order. + rewrite <- rem_opp_r; trivial. + destruct (rem_bound_pos a (-b)); trivial. +Qed. + +Lemma rem_nonpos : forall a b, b~=0 -> a <= 0 -> a rem b <= 0. +Proof. + intros a b Hb Ha. + apply opp_nonneg_nonpos. apply opp_nonneg_nonpos in Ha. + rewrite <- rem_opp_l by trivial. now apply rem_nonneg. +Qed. + +Lemma rem_sign_mul : forall a b, b~=0 -> 0 <= (a rem b) * a. +Proof. +intros a b Hb. destruct (le_ge_cases 0 a). + apply mul_nonneg_nonneg; trivial. now apply rem_nonneg. + apply mul_nonpos_nonpos; trivial. now apply rem_nonpos. +Qed. + +Lemma rem_sign_nz : forall a b, b~=0 -> a rem b ~= 0 -> + sgn (a rem b) == sgn a. +Proof. +intros a b Hb H. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. +rewrite 2 sgn_pos; try easy. + generalize (rem_nonneg a b Hb (lt_le_incl _ _ LT)). order. +now rewrite <- EQ, rem_0_l, sgn_0. +rewrite 2 sgn_neg; try easy. + generalize (rem_nonpos a b Hb (lt_le_incl _ _ LT)). order. +Qed. + +Lemma rem_sign : forall a b, a~=0 -> b~=0 -> sgn (a rem b) ~= -sgn a. +Proof. +intros a b Ha Hb H. +destruct (eq_decidable (a rem b) 0) as [EQ|NEQ]. +apply Ha, sgn_null_iff, opp_inj. now rewrite <- H, opp_0, EQ, sgn_0. +apply Ha, sgn_null_iff. apply eq_mul_0_l with 2; try order'. nzsimpl'. +apply add_move_0_l. rewrite <- H. symmetry. now apply rem_sign_nz. +Qed. + +(** Operations and absolute value *) + +Lemma rem_abs_l : forall a b, b ~= 0 -> (abs a) rem b == abs (a rem b). +Proof. +intros a b Hb. destruct (le_ge_cases 0 a) as [LE|LE]. +rewrite 2 abs_eq; try easy. now apply rem_nonneg. +rewrite 2 abs_neq, rem_opp_l; try easy. now apply rem_nonpos. +Qed. + +Lemma rem_abs_r : forall a b, b ~= 0 -> a rem (abs b) == a rem b. +Proof. +intros a b Hb. destruct (le_ge_cases 0 b). +now rewrite abs_eq. now rewrite abs_neq, ?rem_opp_r. +Qed. + +Lemma rem_abs : forall a b, b ~= 0 -> (abs a) rem (abs b) == abs (a rem b). +Proof. +intros. now rewrite rem_abs_r, rem_abs_l. +Qed. + +Lemma quot_abs_l : forall a b, b ~= 0 -> (abs a)÷b == (sgn a)*(a÷b). +Proof. +intros a b Hb. destruct (lt_trichotomy 0 a) as [LT|[EQ|LT]]. +rewrite abs_eq, sgn_pos by order. now nzsimpl. +rewrite <- EQ, abs_0, quot_0_l; trivial. now nzsimpl. +rewrite abs_neq, quot_opp_l, sgn_neg by order. + rewrite mul_opp_l. now nzsimpl. +Qed. + +Lemma quot_abs_r : forall a b, b ~= 0 -> a÷(abs b) == (sgn b)*(a÷b). +Proof. +intros a b Hb. destruct (lt_trichotomy 0 b) as [LT|[EQ|LT]]. +rewrite abs_eq, sgn_pos by order. now nzsimpl. +order. +rewrite abs_neq, quot_opp_r, sgn_neg by order. + rewrite mul_opp_l. now nzsimpl. +Qed. + +Lemma quot_abs : forall a b, b ~= 0 -> (abs a)÷(abs b) == abs (a÷b). +Proof. +intros a b Hb. +pos_or_neg a; [rewrite (abs_eq a)|rewrite (abs_neq a)]; + try apply opp_nonneg_nonpos; try order. +pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; + try apply opp_nonneg_nonpos; try order. +rewrite abs_eq; try easy. apply NZQuot.div_pos; order. +rewrite <- abs_opp, <- quot_opp_r, abs_eq; try easy. + apply NZQuot.div_pos; order. +pos_or_neg b; [rewrite (abs_eq b)|rewrite (abs_neq b)]; + try apply opp_nonneg_nonpos; try order. +rewrite <- (abs_opp (_÷_)), <- quot_opp_l, abs_eq; try easy. + apply NZQuot.div_pos; order. +rewrite <- (quot_opp_opp a b), abs_eq; try easy. + apply NZQuot.div_pos; order. +Qed. + +(** We have a general bound for absolute values *) + +Lemma rem_bound_abs : + forall a b, b~=0 -> abs (a rem b) < abs b. +Proof. +intros. rewrite <- rem_abs; trivial. +apply rem_bound_pos. apply abs_nonneg. now apply abs_pos. +Qed. + +(** * Order results about rem and quot *) (** A modulo cannot grow beyond its starting point. *) -Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. -Proof. exact mod_le. Qed. +Theorem rem_le: forall a b, 0<=a -> 0<b -> a rem b <= a. +Proof. exact NZQuot.mod_le. Qed. -Theorem div_pos : forall a b, 0<=a -> 0<b -> 0<= a/b. -Proof. exact div_pos. Qed. +Theorem quot_pos : forall a b, 0<=a -> 0<b -> 0<= a÷b. +Proof. exact NZQuot.div_pos. Qed. -Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b. -Proof. exact div_str_pos. Qed. +Lemma quot_str_pos : forall a b, 0<b<=a -> 0 < a÷b. +Proof. exact NZQuot.div_str_pos. Qed. -Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> abs a < abs b). +Lemma quot_small_iff : forall a b, b~=0 -> (a÷b==0 <-> abs a < abs b). Proof. intros. pos_or_neg a; pos_or_neg b. -rewrite div_small_iff; try order. rewrite 2 abs_eq; intuition; order. -rewrite <- opp_inj_wd, opp_0, <- div_opp_r, div_small_iff by order. +rewrite NZQuot.div_small_iff; try order. rewrite 2 abs_eq; intuition; order. +rewrite <- opp_inj_wd, opp_0, <- quot_opp_r, NZQuot.div_small_iff by order. rewrite (abs_eq a), (abs_neq' b); intuition; order. -rewrite <- opp_inj_wd, opp_0, <- div_opp_l, div_small_iff by order. +rewrite <- opp_inj_wd, opp_0, <- quot_opp_l, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_eq b); intuition; order. -rewrite <- div_opp_opp, div_small_iff by order. +rewrite <- quot_opp_opp, NZQuot.div_small_iff by order. rewrite (abs_neq' a), (abs_neq' b); intuition; order. Qed. -Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> abs a < abs b). +Lemma rem_small_iff : forall a b, b~=0 -> (a rem b == a <-> abs a < abs b). Proof. -intros. rewrite mod_eq, <- div_small_iff by order. +intros. rewrite rem_eq, <- quot_small_iff by order. rewrite sub_move_r, <- (add_0_r a) at 1. rewrite add_cancel_l. rewrite eq_sym_iff, eq_mul_0. tauto. Qed. @@ -227,306 +327,306 @@ Qed. (** As soon as the divisor is strictly greater than 1, the division is strictly decreasing. *) -Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. -Proof. exact div_lt. Qed. +Lemma quot_lt : forall a b, 0<a -> 1<b -> a÷b < a. +Proof. exact NZQuot.div_lt. Qed. (** [le] is compatible with a positive division. *) -Lemma div_le_mono : forall a b c, 0<c -> a<=b -> a/c <= b/c. +Lemma quot_le_mono : forall a b c, 0<c -> a<=b -> a÷c <= b÷c. Proof. -intros. pos_or_neg a. apply div_le_mono; auto. +intros. pos_or_neg a. apply NZQuot.div_le_mono; auto. pos_or_neg b. apply le_trans with 0. - rewrite <- opp_nonneg_nonpos, <- div_opp_l by order. - apply div_pos; order. - apply div_pos; order. -rewrite opp_le_mono in *. rewrite <- 2 div_opp_l by order. - apply div_le_mono; intuition; order. + rewrite <- opp_nonneg_nonpos, <- quot_opp_l by order. + apply quot_pos; order. + apply quot_pos; order. +rewrite opp_le_mono in *. rewrite <- 2 quot_opp_l by order. + apply NZQuot.div_le_mono; intuition; order. Qed. (** With this choice of division, - rounding of div is always done toward zero: *) + rounding of quot is always done toward zero: *) -Lemma mul_div_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a/b) <= a. +Lemma mul_quot_le : forall a b, 0<=a -> b~=0 -> 0 <= b*(a÷b) <= a. Proof. intros. pos_or_neg b. split. -apply mul_nonneg_nonneg; [|apply div_pos]; order. -apply mul_div_le; order. -rewrite <- mul_opp_opp, <- div_opp_r by order. +apply mul_nonneg_nonneg; [|apply quot_pos]; order. +apply NZQuot.mul_div_le; order. +rewrite <- mul_opp_opp, <- quot_opp_r by order. split. -apply mul_nonneg_nonneg; [|apply div_pos]; order. -apply mul_div_le; order. +apply mul_nonneg_nonneg; [|apply quot_pos]; order. +apply NZQuot.mul_div_le; order. Qed. -Lemma mul_div_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a/b) <= 0. +Lemma mul_quot_ge : forall a b, a<=0 -> b~=0 -> a <= b*(a÷b) <= 0. Proof. intros. -rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-div_opp_l by order. +rewrite <- opp_nonneg_nonpos, opp_le_mono, <-mul_opp_r, <-quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. -destruct (mul_div_le (-a) b); tauto. +destruct (mul_quot_le (-a) b); tauto. Qed. -(** For positive numbers, considering [S (a/b)] leads to an upper bound for [a] *) +(** For positive numbers, considering [S (a÷b)] leads to an upper bound for [a] *) -Lemma mul_succ_div_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). -Proof. exact mul_succ_div_gt. Qed. +Lemma mul_succ_quot_gt: forall a b, 0<=a -> 0<b -> a < b*(S (a÷b)). +Proof. exact NZQuot.mul_succ_div_gt. Qed. (** Similar results with negative numbers *) -Lemma mul_pred_div_lt: forall a b, a<=0 -> 0<b -> b*(P (a/b)) < a. +Lemma mul_pred_quot_lt: forall a b, a<=0 -> 0<b -> b*(P (a÷b)) < a. Proof. intros. -rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- div_opp_l by order. +rewrite opp_lt_mono, <- mul_opp_r, opp_pred, <- quot_opp_l by order. rewrite <- opp_nonneg_nonpos in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -Lemma mul_pred_div_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a/b)). +Lemma mul_pred_quot_gt: forall a b, 0<=a -> b<0 -> a < b*(P (a÷b)). Proof. intros. -rewrite <- mul_opp_opp, opp_pred, <- div_opp_r by order. +rewrite <- mul_opp_opp, opp_pred, <- quot_opp_r by order. rewrite <- opp_pos_neg in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -Lemma mul_succ_div_lt: forall a b, a<=0 -> b<0 -> b*(S (a/b)) < a. +Lemma mul_succ_quot_lt: forall a b, a<=0 -> b<0 -> b*(S (a÷b)) < a. Proof. intros. -rewrite opp_lt_mono, <- mul_opp_l, <- div_opp_opp by order. +rewrite opp_lt_mono, <- mul_opp_l, <- quot_opp_opp by order. rewrite <- opp_nonneg_nonpos, <- opp_pos_neg in *. -now apply mul_succ_div_gt. +now apply mul_succ_quot_gt. Qed. -(** Inequality [mul_div_le] is exact iff the modulo is zero. *) +(** Inequality [mul_quot_le] is exact iff the modulo is zero. *) -Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). +Lemma quot_exact : forall a b, b~=0 -> (a == b*(a÷b) <-> a rem b == 0). Proof. -intros. rewrite mod_eq by order. rewrite sub_move_r; nzsimpl; tauto. +intros. rewrite rem_eq by order. rewrite sub_move_r; nzsimpl; tauto. Qed. -(** Some additionnal inequalities about div. *) +(** Some additionnal inequalities about quot. *) -Theorem div_lt_upper_bound: - forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. -Proof. exact div_lt_upper_bound. Qed. +Theorem quot_lt_upper_bound: + forall a b q, 0<=a -> 0<b -> a < b*q -> a÷b < q. +Proof. exact NZQuot.div_lt_upper_bound. Qed. -Theorem div_le_upper_bound: - forall a b q, 0<b -> a <= b*q -> a/b <= q. +Theorem quot_le_upper_bound: + forall a b q, 0<b -> a <= b*q -> a÷b <= q. Proof. intros. -rewrite <- (div_mul q b) by order. -apply div_le_mono; trivial. now rewrite mul_comm. +rewrite <- (quot_mul q b) by order. +apply quot_le_mono; trivial. now rewrite mul_comm. Qed. -Theorem div_le_lower_bound: - forall a b q, 0<b -> b*q <= a -> q <= a/b. +Theorem quot_le_lower_bound: + forall a b q, 0<b -> b*q <= a -> q <= a÷b. Proof. intros. -rewrite <- (div_mul q b) by order. -apply div_le_mono; trivial. now rewrite mul_comm. +rewrite <- (quot_mul q b) by order. +apply quot_le_mono; trivial. now rewrite mul_comm. Qed. (** A division respects opposite monotonicity for the divisor *) -Lemma div_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p/r <= p/q. -Proof. exact div_le_compat_l. Qed. +Lemma quot_le_compat_l: forall p q r, 0<=p -> 0<q<=r -> p÷r <= p÷q. +Proof. exact NZQuot.div_le_compat_l. Qed. -(** * Relations between usual operations and mod and div *) +(** * Relations between usual operations and rem and quot *) (** Unlike with other division conventions, some results here aren't always valid, and need to be restricted. For instance - [(a+b*c) mod c <> a mod c] for [a=9,b=-5,c=2] *) + [(a+b*c) rem c <> a rem c] for [a=9,b=-5,c=2] *) -Lemma mod_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> - (a + b * c) mod c == a mod c. +Lemma rem_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> + (a + b * c) rem c == a rem c. Proof. -assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) mod c == a mod c). - intros. pos_or_neg c. apply mod_add; order. - rewrite <- (mod_opp_r a), <- (mod_opp_r (a+b*c)) by order. +assert (forall a b c, c~=0 -> 0<=a -> 0<=a+b*c -> (a+b*c) rem c == a rem c). + intros. pos_or_neg c. apply NZQuot.mod_add; order. + rewrite <- (rem_opp_r a), <- (rem_opp_r (a+b*c)) by order. rewrite <- mul_opp_opp in *. - apply mod_add; order. + apply NZQuot.mod_add; order. intros a b c Hc Habc. destruct (le_0_mul _ _ Habc) as [(Habc',Ha)|(Habc',Ha)]. auto. apply opp_inj. revert Ha Habc'. rewrite <- 2 opp_nonneg_nonpos. -rewrite <- 2 mod_opp_l, opp_add_distr, <- mul_opp_l by order. auto. +rewrite <- 2 rem_opp_l, opp_add_distr, <- mul_opp_l by order. auto. Qed. -Lemma div_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> - (a + b * c) / c == a / c + b. +Lemma quot_add : forall a b c, c~=0 -> 0 <= (a+b*c)*a -> + (a + b * c) ÷ c == a ÷ c + b. Proof. intros. rewrite <- (mul_cancel_l _ _ c) by trivial. -rewrite <- (add_cancel_r _ _ ((a+b*c) mod c)). -rewrite <- div_mod, mod_add by trivial. -now rewrite mul_add_distr_l, add_shuffle0, <-div_mod, mul_comm. +rewrite <- (add_cancel_r _ _ ((a+b*c) rem c)). +rewrite <- quot_rem, rem_add by trivial. +now rewrite mul_add_distr_l, add_shuffle0, <-quot_rem, mul_comm. Qed. -Lemma div_add_l: forall a b c, b~=0 -> 0 <= (a*b+c)*c -> - (a * b + c) / b == a + c / b. +Lemma quot_add_l: forall a b c, b~=0 -> 0 <= (a*b+c)*c -> + (a * b + c) ÷ b == a + c ÷ b. Proof. - intros a b c. rewrite add_comm, (add_comm a). now apply div_add. + intros a b c. rewrite add_comm, (add_comm a). now apply quot_add. Qed. (** Cancellations. *) -Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> - (a*c)/(b*c) == a/b. +Lemma quot_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> + (a*c)÷(b*c) == a÷b. Proof. -assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)/(b*c) == a/b). - intros. pos_or_neg c. apply div_mul_cancel_r; order. - rewrite <- div_opp_opp, <- 2 mul_opp_r. apply div_mul_cancel_r; order. +assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a*c)÷(b*c) == a÷b). + intros. pos_or_neg c. apply NZQuot.div_mul_cancel_r; order. + rewrite <- quot_opp_opp, <- 2 mul_opp_r. apply NZQuot.div_mul_cancel_r; order. rewrite <- neq_mul_0; intuition order. -assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)/(b*c) == a/b). +assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a*c)÷(b*c) == a÷b). intros. pos_or_neg b. apply Aux1; order. - apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_l; try order. apply Aux1; order. + apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_l; try order. apply Aux1; order. rewrite <- neq_mul_0; intuition order. intros. pos_or_neg a. apply Aux2; order. -apply opp_inj. rewrite <- 2 div_opp_l, <- mul_opp_l; try order. apply Aux2; order. +apply opp_inj. rewrite <- 2 quot_opp_l, <- mul_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0; intuition order. Qed. -Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> - (c*a)/(c*b) == a/b. +Lemma quot_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> + (c*a)÷(c*b) == a÷b. Proof. -intros. rewrite !(mul_comm c); now apply div_mul_cancel_r. +intros. rewrite !(mul_comm c); now apply quot_mul_cancel_r. Qed. -Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 -> - (a*c) mod (b*c) == (a mod b) * c. +Lemma mul_rem_distr_r: forall a b c, b~=0 -> c~=0 -> + (a*c) rem (b*c) == (a rem b) * c. Proof. intros. assert (b*c ~= 0) by (rewrite <- neq_mul_0; tauto). -rewrite ! mod_eq by trivial. -rewrite div_mul_cancel_r by order. -now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a/b) c). +rewrite ! rem_eq by trivial. +rewrite quot_mul_cancel_r by order. +now rewrite mul_sub_distr_r, <- !mul_assoc, (mul_comm (a÷b) c). Qed. -Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 -> - (c*a) mod (c*b) == c * (a mod b). +Lemma mul_rem_distr_l: forall a b c, b~=0 -> c~=0 -> + (c*a) rem (c*b) == c * (a rem b). Proof. -intros; rewrite !(mul_comm c); now apply mul_mod_distr_r. +intros; rewrite !(mul_comm c); now apply mul_rem_distr_r. Qed. (** Operations modulo. *) -Theorem mod_mod: forall a n, n~=0 -> - (a mod n) mod n == a mod n. +Theorem rem_rem: forall a n, n~=0 -> + (a rem n) rem n == a rem n. Proof. -intros. pos_or_neg a; pos_or_neg n. apply mod_mod; order. -rewrite <- ! (mod_opp_r _ n) by trivial. apply mod_mod; order. -apply opp_inj. rewrite <- !mod_opp_l by order. apply mod_mod; order. -apply opp_inj. rewrite <- !mod_opp_opp by order. apply mod_mod; order. +intros. pos_or_neg a; pos_or_neg n. apply NZQuot.mod_mod; order. +rewrite <- ! (rem_opp_r _ n) by trivial. apply NZQuot.mod_mod; order. +apply opp_inj. rewrite <- !rem_opp_l by order. apply NZQuot.mod_mod; order. +apply opp_inj. rewrite <- !rem_opp_opp by order. apply NZQuot.mod_mod; order. Qed. -Lemma mul_mod_idemp_l : forall a b n, n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n. +Lemma mul_rem_idemp_l : forall a b n, n~=0 -> + ((a rem n)*b) rem n == (a*b) rem n. Proof. assert (Aux1 : forall a b n, 0<=a -> 0<=b -> n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n). - intros. pos_or_neg n. apply mul_mod_idemp_l; order. - rewrite <- ! (mod_opp_r _ n) by order. apply mul_mod_idemp_l; order. + ((a rem n)*b) rem n == (a*b) rem n). + intros. pos_or_neg n. apply NZQuot.mul_mod_idemp_l; order. + rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.mul_mod_idemp_l; order. assert (Aux2 : forall a b n, 0<=a -> n~=0 -> - ((a mod n)*b) mod n == (a*b) mod n). + ((a rem n)*b) rem n == (a*b) rem n). intros. pos_or_neg b. now apply Aux1. - apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_r by order. + apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_r by order. apply Aux1; order. intros a b n Hn. pos_or_neg a. now apply Aux2. -apply opp_inj. rewrite <-2 mod_opp_l, <-2 mul_opp_l, <-mod_opp_l by order. +apply opp_inj. rewrite <-2 rem_opp_l, <-2 mul_opp_l, <-rem_opp_l by order. apply Aux2; order. Qed. -Lemma mul_mod_idemp_r : forall a b n, n~=0 -> - (a*(b mod n)) mod n == (a*b) mod n. +Lemma mul_rem_idemp_r : forall a b n, n~=0 -> + (a*(b rem n)) rem n == (a*b) rem n. Proof. -intros. rewrite !(mul_comm a). now apply mul_mod_idemp_l. +intros. rewrite !(mul_comm a). now apply mul_rem_idemp_l. Qed. -Theorem mul_mod: forall a b n, n~=0 -> - (a * b) mod n == ((a mod n) * (b mod n)) mod n. +Theorem mul_rem: forall a b n, n~=0 -> + (a * b) rem n == ((a rem n) * (b rem n)) rem n. Proof. -intros. now rewrite mul_mod_idemp_l, mul_mod_idemp_r. +intros. now rewrite mul_rem_idemp_l, mul_rem_idemp_r. Qed. (** addition and modulo Generally speaking, unlike with other conventions, we don't have - [(a+b) mod n = (a mod n + b mod n) mod n] + [(a+b) rem n = (a rem n + b rem n) rem n] for any a and b. - For instance, take (8 + (-10)) mod 3 = -2 whereas - (8 mod 3 + (-10 mod 3)) mod 3 = 1. + For instance, take (8 + (-10)) rem 3 = -2 whereas + (8 rem 3 + (-10 rem 3)) rem 3 = 1. *) -Lemma add_mod_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> - ((a mod n)+b) mod n == (a+b) mod n. +Lemma add_rem_idemp_l : forall a b n, n~=0 -> 0 <= a*b -> + ((a rem n)+b) rem n == (a+b) rem n. Proof. assert (Aux : forall a b n, 0<=a -> 0<=b -> n~=0 -> - ((a mod n)+b) mod n == (a+b) mod n). - intros. pos_or_neg n. apply add_mod_idemp_l; order. - rewrite <- ! (mod_opp_r _ n) by order. apply add_mod_idemp_l; order. + ((a rem n)+b) rem n == (a+b) rem n). + intros. pos_or_neg n. apply NZQuot.add_mod_idemp_l; order. + rewrite <- ! (rem_opp_r _ n) by order. apply NZQuot.add_mod_idemp_l; order. intros a b n Hn Hab. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]. now apply Aux. -apply opp_inj. rewrite <-2 mod_opp_l, 2 opp_add_distr, <-mod_opp_l by order. +apply opp_inj. rewrite <-2 rem_opp_l, 2 opp_add_distr, <-rem_opp_l by order. rewrite <- opp_nonneg_nonpos in *. now apply Aux. Qed. -Lemma add_mod_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> - (a+(b mod n)) mod n == (a+b) mod n. +Lemma add_rem_idemp_r : forall a b n, n~=0 -> 0 <= a*b -> + (a+(b rem n)) rem n == (a+b) rem n. Proof. -intros. rewrite !(add_comm a). apply add_mod_idemp_l; trivial. +intros. rewrite !(add_comm a). apply add_rem_idemp_l; trivial. now rewrite mul_comm. Qed. -Theorem add_mod: forall a b n, n~=0 -> 0 <= a*b -> - (a+b) mod n == (a mod n + b mod n) mod n. +Theorem add_rem: forall a b n, n~=0 -> 0 <= a*b -> + (a+b) rem n == (a rem n + b rem n) rem n. Proof. -intros a b n Hn Hab. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. +intros a b n Hn Hab. rewrite add_rem_idemp_l, add_rem_idemp_r; trivial. reflexivity. destruct (le_0_mul _ _ Hab) as [(Ha,Hb)|(Ha,Hb)]; - destruct (le_0_mul _ _ (mod_sign b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; + destruct (le_0_mul _ _ (rem_sign_mul b n Hn)) as [(Hb',Hm)|(Hb',Hm)]; auto using mul_nonneg_nonneg, mul_nonpos_nonpos. - setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order. - setoid_replace b with 0 by order. rewrite mod_0_l by order. nzsimpl; order. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. + setoid_replace b with 0 by order. rewrite rem_0_l by order. nzsimpl; order. Qed. +(** Conversely, the following results need less restrictions here. *) -(** Conversely, the following result needs less restrictions here. *) - -Lemma div_div : forall a b c, b~=0 -> c~=0 -> - (a/b)/c == a/(b*c). +Lemma quot_quot : forall a b c, b~=0 -> c~=0 -> + (a÷b)÷c == a÷(b*c). Proof. -assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a/b)/c == a/(b*c)). - intros. pos_or_neg c. apply div_div; order. - apply opp_inj. rewrite <- 2 div_opp_r, <- mul_opp_r; trivial. - apply div_div; order. +assert (Aux1 : forall a b c, 0<=a -> 0<b -> c~=0 -> (a÷b)÷c == a÷(b*c)). + intros. pos_or_neg c. apply NZQuot.div_div; order. + apply opp_inj. rewrite <- 2 quot_opp_r, <- mul_opp_r; trivial. + apply NZQuot.div_div; order. rewrite <- neq_mul_0; intuition order. -assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a/b)/c == a/(b*c)). +assert (Aux2 : forall a b c, 0<=a -> b~=0 -> c~=0 -> (a÷b)÷c == a÷(b*c)). intros. pos_or_neg b. apply Aux1; order. - apply opp_inj. rewrite <- div_opp_l, <- 2 div_opp_r, <- mul_opp_l; trivial. + apply opp_inj. rewrite <- quot_opp_l, <- 2 quot_opp_r, <- mul_opp_l; trivial. apply Aux1; trivial. rewrite <- neq_mul_0; intuition order. intros. pos_or_neg a. apply Aux2; order. -apply opp_inj. rewrite <- 3 div_opp_l; try order. apply Aux2; order. +apply opp_inj. rewrite <- 3 quot_opp_l; try order. apply Aux2; order. rewrite <- neq_mul_0. tauto. Qed. -(** A last inequality: *) - -Theorem div_mul_le: - forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. -Proof. exact div_mul_le. Qed. - -(** mod is related to divisibility *) - -Lemma mod_divides : forall a b, b~=0 -> - (a mod b == 0 <-> exists c, a == b*c). +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 Hb. split. - intros Hab. exists (a/b). rewrite (div_mod a b Hb) at 1. - rewrite Hab; now nzsimpl. - intros (c,Hc). rewrite Hc, mul_comm. now apply mod_mul. + 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. -End ZDivPropFunct. +(** A last inequality: *) + +Theorem quot_mul_le: + forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a÷b) <= (c*a)÷b. +Proof. exact NZQuot.div_mul_le. Qed. + +End ZQuotProp. diff --git a/theories/Numbers/Integer/Abstract/ZGcd.v b/theories/Numbers/Integer/Abstract/ZGcd.v new file mode 100644 index 00000000..404fc0c4 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZGcd.v @@ -0,0 +1,274 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Properties of the greatest common divisor *) + +Require Import ZAxioms ZMulOrder ZSgnAbs NZGcd. + +Module Type ZGcdProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B). + + Include NZGcdProp A A B. + +(** Results concerning divisibility*) + +Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m). +Proof. + intros n m. split; intros (p,Hp); exists (-p); rewrite Hp. + now rewrite mul_opp_l, mul_opp_r. + now rewrite mul_opp_opp. +Qed. + +Lemma divide_opp_r : forall n m, (n | -m) <-> (n | m). +Proof. + intros n m. split; intros (p,Hp); exists (-p). + now rewrite mul_opp_l, <- Hp, opp_involutive. + now rewrite Hp, mul_opp_l. +Qed. + +Lemma divide_abs_l : forall n m, (abs n | m) <-> (n | m). +Proof. + intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply divide_opp_l. +Qed. + +Lemma divide_abs_r : forall n m, (n | abs m) <-> (n | m). +Proof. + intros n m. destruct (abs_eq_or_opp m) as [H|H]; rewrite H. + easy. apply divide_opp_r. +Qed. + +Lemma divide_1_r_abs : forall n, (n | 1) -> abs n == 1. +Proof. + intros n Hn. apply divide_1_r_nonneg. apply abs_nonneg. + now apply divide_abs_l. +Qed. + +Lemma divide_1_r : forall n, (n | 1) -> n==1 \/ n==-1. +Proof. + intros n (m,H). rewrite mul_comm in H. now apply eq_mul_1 with m. +Qed. + +Lemma divide_antisym_abs : forall n m, + (n | m) -> (m | n) -> abs n == abs m. +Proof. + intros. apply divide_antisym_nonneg; try apply abs_nonneg. + now apply divide_abs_l, divide_abs_r. + now apply divide_abs_l, divide_abs_r. +Qed. + +Lemma divide_antisym : forall n m, + (n | m) -> (m | n) -> n == m \/ n == -m. +Proof. + intros. now apply abs_eq_cases, divide_antisym_abs. +Qed. + +Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p). +Proof. + intros n m p H H'. rewrite <- add_opp_r. + apply divide_add_r; trivial. now apply divide_opp_r. +Qed. + +Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p). +Proof. + intros n m p H H'. rewrite <- (add_simpl_l m p). now apply divide_sub_r. +Qed. + +(** Properties of gcd *) + +Lemma gcd_opp_l : forall n m, gcd (-n) m == gcd n m. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. rewrite divide_opp_r. apply gcd_divide_iff. +Qed. + +Lemma gcd_opp_r : forall n m, gcd n (-m) == gcd n m. +Proof. + intros. now rewrite gcd_comm, gcd_opp_l, gcd_comm. +Qed. + +Lemma gcd_abs_l : forall n m, gcd (abs n) m == gcd n m. +Proof. + intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply gcd_opp_l. +Qed. + +Lemma gcd_abs_r : forall n m, gcd n (abs m) == gcd n m. +Proof. + intros. now rewrite gcd_comm, gcd_abs_l, gcd_comm. +Qed. + +Lemma gcd_0_l : forall n, gcd 0 n == abs n. +Proof. + intros. rewrite <- gcd_abs_r. apply gcd_0_l_nonneg, abs_nonneg. +Qed. + +Lemma gcd_0_r : forall n, gcd n 0 == abs n. +Proof. + intros. now rewrite gcd_comm, gcd_0_l. +Qed. + +Lemma gcd_diag : forall n, gcd n n == abs n. +Proof. + intros. rewrite <- gcd_abs_l, <- gcd_abs_r. + apply gcd_diag_nonneg, abs_nonneg. +Qed. + +Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. +Proof. + intros. apply gcd_unique_alt; try apply gcd_nonneg. + intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial. + apply divide_add_r; trivial. now apply divide_mul_r. + apply divide_add_cancel_r with (p*n); trivial. + now apply divide_mul_r. now rewrite add_comm. +Qed. + +Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m. +Proof. + intros n m. rewrite <- (mul_1_l n) at 2. apply gcd_add_mult_diag_r. +Qed. + +Lemma gcd_sub_diag_r : forall n m, gcd n (m-n) == gcd n m. +Proof. + intros n m. rewrite <- (mul_1_l n) at 2. + rewrite <- add_opp_r, <- mul_opp_l. apply gcd_add_mult_diag_r. +Qed. + +Definition Bezout n m p := exists a b, a*n + b*m == p. + +Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout. +Proof. + unfold Bezout. intros x x' Hx y y' Hy z z' Hz. + setoid_rewrite Hx. setoid_rewrite Hy. now setoid_rewrite Hz. +Qed. + +Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1. +Proof. + intros n m (q & r & H). + apply gcd_unique; trivial using divide_1_l, le_0_1. + intros p Hn Hm. + rewrite <- H. apply divide_add_r; now apply divide_mul_r. +Qed. + +Lemma gcd_bezout : forall n m p, gcd n m == p -> Bezout n m p. +Proof. + (* First, a version restricted to natural numbers *) + assert (aux : forall n, 0<=n -> forall m, 0<=m -> Bezout n m (gcd n m)). + intros n Hn; pattern n. + apply strong_right_induction with (z:=0); trivial. + unfold Bezout. solve_proper. + clear n Hn. intros n Hn IHn. + apply le_lteq in Hn; destruct Hn as [Hn|Hn]. + intros m Hm; pattern m. + apply strong_right_induction with (z:=0); trivial. + unfold Bezout. solve_proper. + clear m Hm. intros m Hm IHm. + destruct (lt_trichotomy n m) as [LT|[EQ|LT]]. + (* n < m *) + destruct (IHm (m-n)) as (a & b & EQ). + apply sub_nonneg; order. + now apply lt_sub_pos. + exists (a-b). exists b. + rewrite gcd_sub_diag_r in EQ. rewrite <- EQ. + rewrite mul_sub_distr_r, mul_sub_distr_l. + now rewrite add_sub_assoc, add_sub_swap. + (* n = m *) + rewrite EQ. rewrite gcd_diag_nonneg; trivial. + exists 1. exists 0. now nzsimpl. + (* m < n *) + destruct (IHn m Hm LT n) as (a & b & EQ). order. + exists b. exists a. now rewrite gcd_comm, <- EQ, add_comm. + (* n = 0 *) + intros m Hm. rewrite <- Hn, gcd_0_l_nonneg; trivial. + exists 0. exists 1. now nzsimpl. + (* Then we relax the positivity condition on n *) + assert (aux' : forall n m, 0<=m -> Bezout n m (gcd n m)). + intros n m Hm. + destruct (le_ge_cases 0 n). now apply aux. + assert (Hn' : 0 <= -n) by now apply opp_nonneg_nonpos. + destruct (aux (-n) Hn' m Hm) as (a & b & EQ). + exists (-a). exists b. now rewrite <- gcd_opp_l, <- EQ, mul_opp_r, mul_opp_l. + (* And finally we do the same for m *) + intros n m p Hp. rewrite <- Hp; clear Hp. + destruct (le_ge_cases 0 m). now apply aux'. + assert (Hm' : 0 <= -m) by now apply opp_nonneg_nonpos. + destruct (aux' n (-m) Hm') as (a & b & EQ). + exists a. exists (-b). now rewrite <- gcd_opp_r, <- EQ, mul_opp_r, mul_opp_l. +Qed. + +Lemma gcd_mul_mono_l : + forall n m p, gcd (p * n) (p * m) == abs p * gcd n m. +Proof. + intros n m p. + apply gcd_unique. + apply mul_nonneg_nonneg; trivial using gcd_nonneg, abs_nonneg. + destruct (gcd_divide_l n m) as (q,Hq). + rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. + rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. + destruct (gcd_divide_r n m) as (q,Hq). + rewrite Hq at 2. rewrite mul_assoc. apply mul_divide_mono_r. + rewrite <- (abs_sgn p) at 2. rewrite <- mul_assoc. apply divide_factor_l. + intros q H H'. + destruct (gcd_bezout n m (gcd n m) (eq_refl _)) as (a & b & EQ). + rewrite <- EQ, <- sgn_abs, mul_add_distr_l. apply divide_add_r. + rewrite mul_shuffle2. now apply divide_mul_l. + rewrite mul_shuffle2. now apply divide_mul_l. +Qed. + +Lemma gcd_mul_mono_l_nonneg : + forall n m p, 0<=p -> gcd (p*n) (p*m) == p * gcd n m. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_l. +Qed. + +Lemma gcd_mul_mono_r : + forall n m p, gcd (n * p) (m * p) == gcd n m * abs p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), gcd_mul_mono_l, mul_comm. +Qed. + +Lemma gcd_mul_mono_r_nonneg : + forall n m p, 0<=p -> gcd (n*p) (m*p) == gcd n m * p. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply gcd_mul_mono_r. +Qed. + +Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). +Proof. + intros n m p H G. + destruct (gcd_bezout n m 1 G) as (a & b & EQ). + rewrite <- (mul_1_l p), <- EQ, mul_add_distr_r. + apply divide_add_r. rewrite mul_shuffle0. apply divide_factor_r. + rewrite <- mul_assoc. now apply divide_mul_r. +Qed. + +Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) -> + exists q r, n == q*r /\ (q | m) /\ (r | p). +Proof. + intros n m p Hn H. + assert (G := gcd_nonneg n m). + apply le_lteq in G; destruct G as [G|G]. + destruct (gcd_divide_l n m) as (q,Hq). + exists (gcd n m). exists q. + split. now rewrite mul_comm. + split. apply gcd_divide_r. + destruct (gcd_divide_r n m) as (r,Hr). + rewrite Hr in H. rewrite Hq in H at 1. + rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order]. + apply gauss with r; trivial. + apply mul_cancel_r with (gcd n m); [order|]. + rewrite mul_1_l. + rewrite <- gcd_mul_mono_r_nonneg, <- Hq, <- Hr; order. + symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. +Qed. + +(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *) + +End ZGcdProp. diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v new file mode 100644 index 00000000..06af04d1 --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -0,0 +1,471 @@ +(************************************************************************) +(* 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 ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor. + +(** * Least Common Multiple *) + +(** Unlike other functions around, we will define lcm below instead of + axiomatizing it. Indeed, there is no "prior art" about lcm in the + standard library to be compliant with, and the generic definition + of lcm via gcd is quite reasonable. + + By the way, we also state here some combined properties of div/mod + and quot/rem and gcd. +*) + +Module Type ZLcmProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZSgnAbsProp A B) + (Import D : ZDivProp A B C) + (Import E : ZQuotProp A B C) + (Import F : ZGcdProp A B C). + +(** The two notions of division are equal on non-negative numbers *) + +Lemma quot_div_nonneg : forall a b, 0<=a -> 0<b -> a÷b == a/b. +Proof. + intros. apply div_unique_pos with (a rem b). + now apply rem_bound_pos. + apply quot_rem. order. +Qed. + +Lemma rem_mod_nonneg : forall a b, 0<=a -> 0<b -> a rem b == a mod b. +Proof. + intros. apply mod_unique_pos with (a÷b). + now apply rem_bound_pos. + 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. *) + +Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)). +Proof. + intros a b Hb. split. + intros Hab. exists (a/b). rewrite mul_comm. + rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite Hc. now apply mod_mul. +Qed. + +Lemma rem_divide : forall a b, b~=0 -> (a rem b == 0 <-> (b|a)). +Proof. + intros a b Hb. split. + intros Hab. exists (a÷b). rewrite mul_comm. + rewrite (quot_rem a b Hb) at 1. rewrite Hab; now nzsimpl. + intros (c,Hc). rewrite Hc. now apply rem_mul. +Qed. + +Lemma rem_mod_eq_0 : forall a b, b~=0 -> (a rem b == 0 <-> a mod b == 0). +Proof. + intros a b Hb. now rewrite mod_divide, rem_divide. +Qed. + +(** When division is exact, div and quot agree *) + +Lemma quot_div_exact : forall a b, b~=0 -> (b|a) -> a÷b == a/b. +Proof. + intros a b Hb H. + apply mul_cancel_l with b; trivial. + assert (H':=H). + apply rem_divide, quot_exact in H; trivial. + apply mod_divide, div_exact in H'; trivial. + now rewrite <-H,<-H'. +Qed. + +Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) -> + (c*a)/b == c*(a/b). +Proof. + intros a b c Hb H. + apply mul_cancel_l with b; trivial. + rewrite mul_assoc, mul_shuffle0. + assert (H':=H). apply mod_divide, div_exact in H'; trivial. + rewrite <- H', (mul_comm a c). + symmetry. apply div_exact; trivial. + apply mod_divide; trivial. + now apply divide_mul_r. +Qed. + +Lemma divide_quot_mul_exact : forall a b c, b~=0 -> (b|a) -> + (c*a)÷b == c*(a÷b). +Proof. + intros a b c Hb H. + rewrite 2 quot_div_exact; trivial. + apply divide_div_mul_exact; trivial. + now apply divide_mul_r. +Qed. + +(** Gcd of divided elements, for exact divisions *) + +Lemma gcd_div_factor : forall a b c, 0<c -> (c|a) -> (c|b) -> + gcd (a/c) (b/c) == (gcd a b)/c. +Proof. + intros a b c Hc Ha Hb. + apply mul_cancel_l with c; try order. + assert (H:=gcd_greatest _ _ _ Ha Hb). + apply mod_divide, div_exact in H; try order. + rewrite <- H. + rewrite <- gcd_mul_mono_l_nonneg; try order. + f_equiv; symmetry; apply div_exact; try order; + apply mod_divide; trivial; try order. +Qed. + +Lemma gcd_quot_factor : forall a b c, 0<c -> (c|a) -> (c|b) -> + gcd (a÷c) (b÷c) == (gcd a b)÷c. +Proof. + intros a b c Hc Ha Hb. rewrite !quot_div_exact; trivial; try order. + now apply gcd_div_factor. now apply gcd_greatest. +Qed. + +Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b -> + gcd (a/g) (b/g) == 1. +Proof. + intros a b g NZ EQ. rewrite gcd_div_factor. + now rewrite <- EQ, div_same. + generalize (gcd_nonneg a b); order. + rewrite EQ; apply gcd_divide_l. + rewrite EQ; apply gcd_divide_r. +Qed. + +Lemma gcd_quot_gcd : forall a b g, g~=0 -> g == gcd a b -> + gcd (a÷g) (b÷g) == 1. +Proof. + intros a b g NZ EQ. rewrite !quot_div_exact; trivial. + now apply gcd_div_gcd. + rewrite EQ; apply gcd_divide_r. + rewrite EQ; apply gcd_divide_l. +Qed. + +(** The following equality is crucial for Euclid algorithm *) + +Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a. +Proof. + intros a b Hb. rewrite mod_eq; trivial. + rewrite <- add_opp_r, mul_comm, <- mul_opp_l. + rewrite (gcd_comm _ b). + apply gcd_add_mult_diag_r. +Qed. + +Lemma gcd_rem : forall a b, b~=0 -> gcd (a rem b) b == gcd b a. +Proof. + intros a b Hb. rewrite rem_eq; trivial. + rewrite <- add_opp_r, mul_comm, <- mul_opp_l. + rewrite (gcd_comm _ b). + apply gcd_add_mult_diag_r. +Qed. + +(** We now define lcm thanks to gcd: + + lcm a b = a * (b / gcd a b) + = (a / gcd a b) * b + = (a*b) / gcd a b + + We had an abs in order to have an always-nonnegative lcm, + in the spirit of gcd. Nota: [lcm 0 0] should be 0, which + isn't garantee with the third equation above. +*) + +Definition lcm a b := abs (a*(b/gcd a b)). + +Instance lcm_wd : Proper (eq==>eq==>eq) lcm. +Proof. unfold lcm. solve_proper. Qed. + +Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 -> + a * (b / gcd a b) == (a*b)/gcd a b. +Proof. + intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r. +Qed. + +Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 -> + (a / gcd a b) * b == (a*b)/gcd a b. +Proof. + intros a b H. rewrite 2 (mul_comm _ b). + rewrite divide_div_mul_exact; try easy. apply gcd_divide_l. +Qed. + +Lemma gcd_div_swap : forall a b, + (a / gcd a b) * b == a * (b / gcd a b). +Proof. + intros a b. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl. + now rewrite lcm_equiv1, <-lcm_equiv2. +Qed. + +Lemma divide_lcm_l : forall a b, (a | lcm a b). +Proof. + unfold lcm. intros a b. apply divide_abs_r, divide_factor_l. +Qed. + +Lemma divide_lcm_r : forall a b, (b | lcm a b). +Proof. + unfold lcm. intros a b. apply divide_abs_r. rewrite <- gcd_div_swap. + apply divide_factor_r. +Qed. + +Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a). +Proof. + intros a b c Ha Hb (c',Hc). exists c'. + now rewrite <- divide_div_mul_exact, <- Hc. +Qed. + +Lemma lcm_least : forall a b c, + (a | c) -> (b | c) -> (lcm a b | c). +Proof. + intros a b c Ha Hb. unfold lcm. apply divide_abs_l. + destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ]. + apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl. + assert (Ga := gcd_divide_l a b). + assert (Gb := gcd_divide_r a b). + set (g:=gcd a b) in *. + assert (Ha' := divide_div g a c NEQ Ga Ha). + assert (Hb' := divide_div g b c NEQ Gb Hb). + destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'. + apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm]. + destruct Hb' as (b',Hb'). + exists b'. + rewrite mul_shuffle3, <- Hb'. + rewrite (proj2 (div_exact c g NEQ)). + rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv. + symmetry. apply div_exact; trivial. + apply mod_divide; trivial. + apply mod_divide; trivial. transitivity a; trivial. +Qed. + +Lemma lcm_nonneg : forall a b, 0 <= lcm a b. +Proof. + intros a b. unfold lcm. apply abs_nonneg. +Qed. + +Lemma lcm_comm : forall a b, lcm a b == lcm b a. +Proof. + intros a b. unfold lcm. rewrite (gcd_comm b), (mul_comm b). + now rewrite <- gcd_div_swap. +Qed. + +Lemma lcm_divide_iff : forall n m p, + (lcm n m | p) <-> (n | p) /\ (m | p). +Proof. + intros. split. split. + transitivity (lcm n m); trivial using divide_lcm_l. + transitivity (lcm n m); trivial using divide_lcm_r. + intros (H,H'). now apply lcm_least. +Qed. + +Lemma lcm_unique : forall n m p, + 0<=p -> (n|p) -> (m|p) -> + (forall q, (n|q) -> (m|q) -> (p|q)) -> + lcm n m == p. +Proof. + intros n m p Hp Hn Hm H. + apply divide_antisym_nonneg; trivial. apply lcm_nonneg. + now apply lcm_least. + apply H. apply divide_lcm_l. apply divide_lcm_r. +Qed. + +Lemma lcm_unique_alt : forall n m p, 0<=p -> + (forall q, (p|q) <-> (n|q) /\ (m|q)) -> + lcm n m == p. +Proof. + intros n m p Hp H. + apply lcm_unique; trivial. + apply H, divide_refl. + apply H, divide_refl. + intros. apply H. now split. +Qed. + +Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p. +Proof. + intros. apply lcm_unique_alt; try apply lcm_nonneg. + intros. now rewrite !lcm_divide_iff, and_assoc. +Qed. + +Lemma lcm_0_l : forall n, lcm 0 n == 0. +Proof. + intros. apply lcm_unique; trivial. order. + apply divide_refl. + apply divide_0_r. +Qed. + +Lemma lcm_0_r : forall n, lcm n 0 == 0. +Proof. + intros. now rewrite lcm_comm, lcm_0_l. +Qed. + +Lemma lcm_1_l_nonneg : forall n, 0<=n -> lcm 1 n == n. +Proof. + intros. apply lcm_unique; trivial using divide_1_l, le_0_1, divide_refl. +Qed. + +Lemma lcm_1_r_nonneg : forall n, 0<=n -> lcm n 1 == n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l_nonneg. +Qed. + +Lemma lcm_diag_nonneg : forall n, 0<=n -> lcm n n == n. +Proof. + intros. apply lcm_unique; trivial using divide_refl. +Qed. + +Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0. +Proof. + intros. split. + intros EQ. + apply eq_mul_0. + apply divide_0_l. rewrite <- EQ. apply lcm_least. + apply divide_factor_l. apply divide_factor_r. + destruct 1 as [EQ|EQ]; rewrite EQ. apply lcm_0_l. apply lcm_0_r. +Qed. + +Lemma divide_lcm_eq_r : forall n m, 0<=m -> (n|m) -> lcm n m == m. +Proof. + intros n m Hm H. apply lcm_unique_alt; trivial. + intros q. split. split; trivial. now transitivity m. + now destruct 1. +Qed. + +Lemma divide_lcm_iff : forall n m, 0<=m -> ((n|m) <-> lcm n m == m). +Proof. + intros n m Hn. split. now apply divide_lcm_eq_r. + intros EQ. rewrite <- EQ. apply divide_lcm_l. +Qed. + +Lemma lcm_opp_l : forall n m, lcm (-n) m == lcm n m. +Proof. + intros. apply lcm_unique_alt; try apply lcm_nonneg. + intros. rewrite divide_opp_l. apply lcm_divide_iff. +Qed. + +Lemma lcm_opp_r : forall n m, lcm n (-m) == lcm n m. +Proof. + intros. now rewrite lcm_comm, lcm_opp_l, lcm_comm. +Qed. + +Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m. +Proof. + intros. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. + easy. apply lcm_opp_l. +Qed. + +Lemma lcm_abs_r : forall n m, lcm n (abs m) == lcm n m. +Proof. + intros. now rewrite lcm_comm, lcm_abs_l, lcm_comm. +Qed. + +Lemma lcm_1_l : forall n, lcm 1 n == abs n. +Proof. + intros. rewrite <- lcm_abs_r. apply lcm_1_l_nonneg, abs_nonneg. +Qed. + +Lemma lcm_1_r : forall n, lcm n 1 == abs n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l. +Qed. + +Lemma lcm_diag : forall n, lcm n n == abs n. +Proof. + intros. rewrite <- lcm_abs_l, <- lcm_abs_r. + apply lcm_diag_nonneg, abs_nonneg. +Qed. + +Lemma lcm_mul_mono_l : + forall n m p, lcm (p * n) (p * m) == abs p * lcm n m. +Proof. + intros n m p. + destruct (eq_decidable p 0) as [Hp|Hp]. + rewrite Hp. nzsimpl. rewrite lcm_0_l, abs_0. now nzsimpl. + destruct (eq_decidable (gcd n m) 0) as [Hg|Hg]. + apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm. + nzsimpl. rewrite lcm_0_l. now nzsimpl. + unfold lcm. + rewrite gcd_mul_mono_l. + rewrite !abs_mul, mul_assoc. f_equiv. + rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc. + rewrite div_mul_cancel_l; trivial. + rewrite divide_div_mul_exact; trivial. rewrite abs_mul. + rewrite <- (sgn_abs (sgn p)), sgn_sgn. + destruct (sgn_spec p) as [(_,EQ)|[(EQ,_)|(_,EQ)]]. + rewrite EQ. now nzsimpl. order. + rewrite EQ. rewrite mul_opp_l, mul_opp_r, opp_involutive. now nzsimpl. + apply gcd_divide_r. + contradict Hp. now apply abs_0_iff. +Qed. + +Lemma lcm_mul_mono_l_nonneg : + forall n m p, 0<=p -> lcm (p*n) (p*m) == p * lcm n m. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_l. +Qed. + +Lemma lcm_mul_mono_r : + forall n m p, lcm (n * p) (m * p) == lcm n m * abs p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm. +Qed. + +Lemma lcm_mul_mono_r_nonneg : + forall n m p, 0<=p -> lcm (n*p) (m*p) == lcm n m * p. +Proof. + intros. rewrite <- (abs_eq p) at 3; trivial. apply lcm_mul_mono_r. +Qed. + +Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> + (gcd n m == 1 <-> lcm n m == abs (n*m)). +Proof. + intros n m Hn Hm. split; intros H. + unfold lcm. rewrite H. now rewrite div_1_r. + unfold lcm in *. + rewrite !abs_mul in H. apply mul_cancel_l in H; [|now rewrite abs_0_iff]. + assert (H' := gcd_divide_r n m). + assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). + apply mod_divide in H'; trivial. apply div_exact in H'; trivial. + assert (m / gcd n m ~=0) by (contradict Hm; rewrite H', Hm; now nzsimpl). + rewrite <- (mul_1_l (abs (_/_))) in H. + rewrite H' in H at 3. rewrite abs_mul in H. + apply mul_cancel_r in H; [|now rewrite abs_0_iff]. + rewrite abs_eq in H. order. apply gcd_nonneg. +Qed. + +End ZLcmProp. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 57be0f0e..3a8e1f38 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,12 +8,10 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZLt.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZMul. -Module ZOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZMulPropFunct Z. +Module ZOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZMulProp Z. (** Instances of earlier theorems for m == 0 *) @@ -70,12 +68,12 @@ Qed. Theorem lt_lt_pred : forall n m, n < m -> P n < m. Proof. -intros; apply <- lt_pred_le; now apply lt_le_incl. +intros; apply lt_pred_le; now apply lt_le_incl. Qed. Theorem le_le_pred : forall n m, n <= m -> P n <= m. Proof. -intros; apply lt_le_incl; now apply <- lt_pred_le. +intros; apply lt_le_incl; now apply lt_pred_le. Qed. Theorem lt_pred_lt : forall n m, n < P m -> n < m. @@ -85,7 +83,7 @@ Qed. Theorem le_pred_lt : forall n m, n <= P m -> n <= m. Proof. -intros; apply lt_le_incl; now apply <- lt_le_pred. +intros; apply lt_le_incl; now apply lt_le_pred. Qed. Theorem pred_lt_mono : forall n m, n < m <-> P n < P m. @@ -123,12 +121,12 @@ 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. -apply <- eq_opp_r. now rewrite opp_pred, opp_0. +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. +apply eq_opp_r. now rewrite one_succ, opp_pred, opp_0. Qed. -End ZOrderPropFunct. +End ZOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZMaxMin.v b/theories/Numbers/Integer/Abstract/ZMaxMin.v new file mode 100644 index 00000000..4e653fee --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZMaxMin.v @@ -0,0 +1,179 @@ +(************************************************************************) +(* 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 ZAxioms ZMulOrder GenericMinMax. + +(** * Properties of minimum and maximum specific to integer numbers *) + +Module Type ZMaxMinProp (Import Z : ZAxiomsMiniSig'). +Include ZMulOrderProp Z. + +(** The following results are concrete instances of [max_monotone] + and similar lemmas. *) + +(** Succ *) + +Lemma succ_max_distr : forall n m, S (max n m) == max (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?succ_le_mono. +Qed. + +Lemma succ_min_distr : forall n m, S (min n m) == min (S n) (S m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?succ_le_mono. +Qed. + +(** Pred *) + +Lemma pred_max_distr : forall n m, P (max n m) == max (P n) (P m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?pred_le_mono. +Qed. + +Lemma pred_min_distr : forall n m, P (min n m) == min (P n) (P m). +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?pred_le_mono. +Qed. + +(** Add *) + +Lemma add_max_distr_l : forall n m p, max (p + n) (p + m) == p + max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_max_distr_r : forall n m p, max (n + p) (m + p) == max n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; now rewrite <- ?add_le_mono_r. +Qed. + +Lemma add_min_distr_l : forall n m p, min (p + n) (p + m) == p + min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_l. +Qed. + +Lemma add_min_distr_r : forall n m p, min (n + p) (m + p) == min n m + p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; now rewrite <- ?add_le_mono_r. +Qed. + +(** Opp *) + +Lemma opp_max_distr : forall n m, -(max n m) == min (-n) (-m). +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. symmetry. apply min_r. now rewrite <- opp_le_mono. + rewrite max_l by trivial. symmetry. apply min_l. now rewrite <- opp_le_mono. +Qed. + +Lemma opp_min_distr : forall n m, -(min n m) == max (-n) (-m). +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. symmetry. apply max_l. now rewrite <- opp_le_mono. + rewrite min_r by trivial. symmetry. apply max_r. now rewrite <- opp_le_mono. +Qed. + +(** Sub *) + +Lemma sub_max_distr_l : forall n m p, max (p - n) (p - m) == p - min n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. apply max_l. now rewrite <- sub_le_mono_l. + rewrite min_r by trivial. apply max_r. now rewrite <- sub_le_mono_l. +Qed. + +Lemma sub_max_distr_r : forall n m p, max (n - p) (m - p) == max n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply sub_le_mono_r. +Qed. + +Lemma sub_min_distr_l : forall n m p, min (p - n) (p - m) == p - max n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. apply min_r. now rewrite <- sub_le_mono_l. + rewrite max_l by trivial. apply min_l. now rewrite <- sub_le_mono_l. +Qed. + +Lemma sub_min_distr_r : forall n m p, min (n - p) (m - p) == min n m - p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply sub_le_mono_r. +Qed. + +(** Mul *) + +Lemma mul_max_distr_nonneg_l : forall n m p, 0 <= p -> + max (p * n) (p * m) == p * max n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_l. +Qed. + +Lemma mul_max_distr_nonneg_r : forall n m p, 0 <= p -> + max (n * p) (m * p) == max n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 max_r | rewrite 2 max_l]; try order; now apply mul_le_mono_nonneg_r. +Qed. + +Lemma mul_min_distr_nonneg_l : forall n m p, 0 <= p -> + min (p * n) (p * m) == p * min n m. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_l. +Qed. + +Lemma mul_min_distr_nonneg_r : forall n m p, 0 <= p -> + min (n * p) (m * p) == min n m * p. +Proof. + intros. destruct (le_ge_cases n m); + [rewrite 2 min_l | rewrite 2 min_r]; try order; now apply mul_le_mono_nonneg_r. +Qed. + +Lemma mul_max_distr_nonpos_l : forall n m p, p <= 0 -> + max (p * n) (p * m) == p * min n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_l. + rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_l. +Qed. + +Lemma mul_max_distr_nonpos_r : forall n m p, p <= 0 -> + max (n * p) (m * p) == min n m * p. +Proof. + intros. destruct (le_ge_cases n m). + rewrite min_l by trivial. rewrite max_l. reflexivity. now apply mul_le_mono_nonpos_r. + rewrite min_r by trivial. rewrite max_r. reflexivity. now apply mul_le_mono_nonpos_r. +Qed. + +Lemma mul_min_distr_nonpos_l : forall n m p, p <= 0 -> + min (p * n) (p * m) == p * max n m. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_l. + rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_l. +Qed. + +Lemma mul_min_distr_nonpos_r : forall n m p, p <= 0 -> + min (n * p) (m * p) == max n m * p. +Proof. + intros. destruct (le_ge_cases n m). + rewrite max_r by trivial. rewrite min_r. reflexivity. now apply mul_le_mono_nonpos_r. + rewrite max_l by trivial. rewrite min_l. reflexivity. now apply mul_le_mono_nonpos_r. +Qed. + +End ZMaxMinProp. diff --git a/theories/Numbers/Integer/Abstract/ZMul.v b/theories/Numbers/Integer/Abstract/ZMul.v index 83dc0e10..36f9c3d5 100644 --- a/theories/Numbers/Integer/Abstract/ZMul.v +++ b/theories/Numbers/Integer/Abstract/ZMul.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,12 +8,10 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZMul.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZAdd. -Module ZMulPropFunct (Import Z : ZAxiomsSig'). -Include ZAddPropFunct Z. +Module ZMulProp (Import Z : ZAxiomsMiniSig'). +Include ZAddProp Z. (** A note on naming: right (correspondingly, left) distributivity happens when the sum is multiplied by a number on the right @@ -41,7 +39,7 @@ Qed. Theorem mul_opp_l : forall n m, (- n) * m == - (n * m). Proof. -intros n m. apply -> add_move_0_r. +intros n m. apply add_move_0_r. now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l. Qed. @@ -55,6 +53,11 @@ Proof. intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive. Qed. +Theorem mul_opp_comm : forall n m, (- n) * m == n * (- m). +Proof. +intros n m. now rewrite mul_opp_l, <- mul_opp_r. +Qed. + Theorem mul_sub_distr_l : forall n m p, n * (m - p) == n * m - n * p. Proof. intros n m p. do 2 rewrite <- add_opp_r. rewrite mul_add_distr_l. @@ -67,6 +70,6 @@ intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p); now apply mul_sub_distr_l. Qed. -End ZMulPropFunct. +End ZMulProp. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 06a5d168..d0d64faa 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) @@ -8,14 +8,10 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZMulOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export ZAddOrder. -Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig'). -Include ZAddOrderPropFunct Z. - -Local Notation "- 1" := (-(1)). +Module Type ZMulOrderProp (Import Z : ZAxiomsMiniSig'). +Include ZAddOrderProp Z. Theorem mul_lt_mono_nonpos : forall n m p q, m <= 0 -> n < m -> q <= 0 -> p < q -> m * q < n * p. @@ -94,18 +90,11 @@ Qed. Notation mul_nonpos := le_mul_0 (only parsing). -Theorem le_0_square : forall n, 0 <= n * n. -Proof. -intro n; destruct (neg_nonneg_cases n). -apply lt_le_incl; now apply mul_neg_neg. -now apply mul_nonneg_nonneg. -Qed. - -Notation square_nonneg := le_0_square (only parsing). +Notation le_0_square := square_nonneg (only parsing). Theorem nlt_square_0 : forall n, ~ n * n < 0. Proof. -intros n H. apply -> lt_nge in H. apply H. apply square_nonneg. +intros n H. apply lt_nge in H. apply H. apply square_nonneg. Qed. Theorem square_lt_mono_nonpos : forall n m, n <= 0 -> m < n -> n * n < m * m. @@ -120,42 +109,38 @@ Qed. Theorem square_lt_simpl_nonpos : forall n m, m <= 0 -> n * n < m * m -> m < n. Proof. -intros n m H1 H2. destruct (le_gt_cases n 0). -destruct (lt_ge_cases m n). -assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonpos. -apply -> le_ngt in F. false_hyp H2 F. -now apply le_lt_trans with 0. +intros n m H1 H2. destruct (le_gt_cases n 0); [|order]. +destruct (lt_ge_cases m n) as [LE|GT]; trivial. +apply square_le_mono_nonpos in GT; order. Qed. Theorem square_le_simpl_nonpos : forall n m, m <= 0 -> n * n <= m * m -> m <= n. Proof. -intros n m H1 H2. destruct (le_gt_cases n 0). -destruct (le_gt_cases m n). -assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonpos. -apply -> lt_nge in F. false_hyp H2 F. -apply lt_le_incl; now apply le_lt_trans with 0. +intros n m H1 H2. destruct (le_gt_cases n 0); [|order]. +destruct (le_gt_cases m n) as [LE|GT]; trivial. +apply square_lt_mono_nonpos in GT; order. Qed. Theorem lt_1_mul_neg : forall n m, n < -1 -> m < 0 -> 1 < n * m. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_neg_r m) in H1. -apply <- opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1. +intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1. +apply opp_pos_neg in H2. rewrite mul_opp_l, mul_1_l in H1. 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. +intros n m H1 H2. apply (mul_lt_mono_neg_r m) in H1. +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. +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. @@ -163,39 +148,33 @@ 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. Proof. -assert (F : ~ 1 < -1). -intro H. -assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r. -assert (H2 : 1 < 0) by now apply lt_trans with (-1). -false_hyp H2 nlt_succ_diag_l. +assert (F := lt_m1_0). zero_pos_neg n. -intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r. -intros n H; split; apply <- le_succ_l in H; le_elim H. -intros m H1; apply (lt_1_mul_l n m) in H. -rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl. -intros; now left. -intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1; -apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H. -false_hyp H neq_succ_diag_l. false_hyp H F. -intros; right; symmetry; now apply opp_wd. +(* n = 0 *) +intros m. nzsimpl. now left. +(* 0 < n, proving P n /\ P (-n) *) +intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. +le_elim Hn; split; intros m H. +destruct (lt_1_mul_l n m) as [|[|]]; order'. +rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'. +now left. +intros; right. now f_equiv. Qed. Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n). @@ -229,5 +208,9 @@ apply mul_lt_mono_nonneg. now apply lt_le_incl. assumption. apply le_0_1. assumption. Qed. -End ZMulOrderPropFunct. +(** Alternative name : *) + +Definition mul_eq_1 := eq_mul_1. + +End ZMulOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v new file mode 100644 index 00000000..b364ec3f --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -0,0 +1,52 @@ +(************************************************************************) +(* 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 ZMulOrder NZParity. + +(** Some more properties of [even] and [odd]. *) + +Module Type ZParityProp (Import Z : ZAxiomsSig') + (Import ZP : ZMulOrderProp Z). + +Include NZParityProp Z Z ZP. + +Lemma odd_pred : forall n, odd (P n) = even n. +Proof. + intros. rewrite <- (succ_pred n) at 2. symmetry. apply even_succ. +Qed. + +Lemma even_pred : forall n, even (P n) = odd n. +Proof. + intros. rewrite <- (succ_pred n) at 2. symmetry. apply odd_succ. +Qed. + +Lemma even_opp : forall n, even (-n) = even n. +Proof. + assert (H : forall n, Even n -> Even (-n)). + intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv. + intros. rewrite eq_iff_eq_true, !even_spec. + split. rewrite <- (opp_involutive n) at 2. apply H. + apply H. +Qed. + +Lemma odd_opp : forall n, odd (-n) = odd n. +Proof. + intros. rewrite <- !negb_even. now rewrite even_opp. +Qed. + +Lemma even_sub : forall n m, even (n-m) = Bool.eqb (even n) (even m). +Proof. + intros. now rewrite <- add_opp_r, even_add, even_opp. +Qed. + +Lemma odd_sub : forall n m, odd (n-m) = xorb (odd n) (odd m). +Proof. + intros. now rewrite <- add_opp_r, odd_add, odd_opp. +Qed. + +End ZParityProp. diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v new file mode 100644 index 00000000..53d84dce --- /dev/null +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -0,0 +1,124 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Properties of the power function *) + +Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow. + +Module Type ZPowProp + (Import A : ZAxiomsSig') + (Import B : ZMulOrderProp A) + (Import C : ZParityProp A B) + (Import D : ZSgnAbsProp A B). + + Include NZPowProp A A B. + +(** Parity of power *) + +Lemma even_pow : forall a b, 0<b -> even (a^b) = even a. +Proof. + intros a b Hb. apply lt_ind with (4:=Hb). solve_proper. + now nzsimpl. + clear b Hb. intros b Hb IH. nzsimpl; [|order]. + rewrite even_mul, IH. now destruct (even a). +Qed. + +Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a. +Proof. + intros. now rewrite <- !negb_even, even_pow. +Qed. + +(** Properties of power of negative numbers *) + +Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b. +Proof. + intros a b (c,H). rewrite H. + destruct (le_gt_cases 0 c). + rewrite 2 pow_mul_r by order'. + rewrite 2 pow_2_r. + now rewrite mul_opp_opp. + assert (2*c < 0) by (apply mul_pos_neg; order'). + now rewrite !pow_neg_r. +Qed. + +Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b). +Proof. + intros a b (c,H). rewrite H. + destruct (le_gt_cases 0 c) as [LE|GT]. + assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order'). + rewrite add_1_r, !pow_succ_r; trivial. + rewrite pow_opp_even by (now exists c). + apply mul_opp_l. + apply double_above in GT. rewrite mul_0_r in GT. + rewrite !pow_neg_r by trivial. now rewrite opp_0. +Qed. + +Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b. +Proof. + intros. destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ. + reflexivity. + symmetry. now apply pow_opp_even. +Qed. + +Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a^b. +Proof. + intros. rewrite pow_even_abs by trivial. + apply pow_nonneg, abs_nonneg. +Qed. + +Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b. +Proof. + intros a b H. + destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + nzsimpl. + rewrite abs_eq; order. + rewrite <- EQ'. nzsimpl. + destruct (le_gt_cases 0 b). + apply pow_0_l. + assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0). + order. + now rewrite pow_neg_r. + rewrite abs_neq by order. + rewrite pow_opp_odd; trivial. + now rewrite mul_opp_opp, mul_1_l. +Qed. + +Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a. +Proof. + intros a b Hb H. + 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, odd_0). + order. + apply sgn_neg. + rewrite <- (opp_involutive a). rewrite pow_opp_odd by trivial. + apply opp_neg_pos. + apply pow_pos_nonneg; trivial. + 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 ae7c3209..c0455196 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -1,24 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 *) (************************************************************************) -(*i $Id: ZProperties.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor + ZGcd ZLcm NZLog NZSqrt ZBits. -Require Export ZAxioms ZMulOrder ZSgnAbs. - -(** This functor summarizes all known facts about Z. - For the moment it is only an alias to [ZMulOrderPropFunct], which - subsumes all others, plus properties of [sgn] and [abs]. -*) - -Module Type ZPropSig (Z:ZAxiomsExtSig) := - ZMulOrderPropFunct Z <+ ZSgnAbsPropSig Z. - -Module ZPropFunct (Z:ZAxiomsExtSig) <: ZPropSig Z. - Include ZPropSig Z. -End ZPropFunct. +(** This functor summarizes all known facts about Z. *) +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 + <+ ZBitsProp Z. diff --git a/theories/Numbers/Integer/Abstract/ZSgnAbs.v b/theories/Numbers/Integer/Abstract/ZSgnAbs.v index cecaa6a3..b2f6cc84 100644 --- a/theories/Numbers/Integer/Abstract/ZSgnAbs.v +++ b/theories/Numbers/Integer/Abstract/ZSgnAbs.v @@ -1,25 +1,19 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <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 Export ZMulOrder. +(** Properties of [abs] and [sgn] *) -(** An axiomatization of [abs]. *) - -Module Type HasAbs(Import Z : ZAxiomsSig'). - Parameter Inline abs : t -> t. - Axiom abs_eq : forall n, 0<=n -> abs n == n. - Axiom abs_neq : forall n, n<=0 -> abs n == -n. -End HasAbs. +Require Import ZMulOrder. (** Since we already have [max], we could have defined [abs]. *) -Module GenericAbs (Import Z : ZAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasAbs Z. +Module GenericAbs (Import Z : ZAxiomsMiniSig') + (Import ZP : ZMulOrderProp Z) <: HasAbs Z. Definition abs n := max n (-n). Lemma abs_eq : forall n, 0<=n -> abs n == n. Proof. @@ -35,37 +29,28 @@ Module GenericAbs (Import Z : ZAxiomsSig') Qed. End GenericAbs. -(** An Axiomatization of [sgn]. *) - -Module Type HasSgn (Import Z : ZAxiomsSig'). - 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). -End HasSgn. - (** We can deduce a [sgn] function from a [compare] function *) -Module Type ZDecAxiomsSig := ZAxiomsSig <+ HasCompare. -Module Type ZDecAxiomsSig' := ZAxiomsSig' <+ HasCompare. +Module Type ZDecAxiomsSig := ZAxiomsMiniSig <+ HasCompare. +Module Type ZDecAxiomsSig' := ZAxiomsMiniSig' <+ HasCompare. Module Type GenericSgn (Import Z : ZDecAxiomsSig') - (Import ZP : ZMulOrderPropFunct Z) <: HasSgn Z. + (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. -Module Type ZAxiomsExtSig := ZAxiomsSig <+ HasAbs <+ HasSgn. -Module Type ZAxiomsExtSig' := ZAxiomsSig' <+ HasAbs <+ HasSgn. -Module Type ZSgnAbsPropSig (Import Z : ZAxiomsExtSig') - (Import ZP : ZMulOrderPropFunct Z). +(** Derived properties of [abs] and [sgn] *) + +Module Type ZSgnAbsProp (Import Z : ZAxiomsSig') + (Import ZP : ZMulOrderProp Z). Ltac destruct_max n := destruct (le_ge_cases 0 n); @@ -183,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. @@ -249,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. @@ -264,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. @@ -272,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. @@ -343,6 +350,15 @@ Proof. rewrite eq_opp_l. apply abs_neq. now apply lt_le_incl. Qed. -End ZSgnAbsPropSig. +Lemma sgn_sgn : forall x, sgn (sgn x) == sgn x. +Proof. + intros. + destruct (sgn_spec x) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ. + apply sgn_pos, lt_0_1. + now apply sgn_null. + apply sgn_neg. rewrite opp_neg_pos. apply lt_0_1. +Qed. + +End ZSgnAbsProp. |