diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
20 files changed, 2687 insertions, 306 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 4185de95..72e09f15 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.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: NAdd.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NBase. -Module NAddPropFunct (Import N : NAxiomsSig'). -Include NBasePropFunct N. +Module NAddProp (Import N : NAxiomsMiniSig'). +Include NBaseProp N. (** For theorems about [add] that are both valid for [N] and [Z], see [NZAdd] *) (** Now comes theorems valid for natural numbers but not for Z *) @@ -24,9 +22,9 @@ intros n m; induct n. nzsimpl; intuition. intros n IH. nzsimpl. setoid_replace (S (n + m) == 0) with False by - (apply -> neg_false; apply neq_succ_0). + (apply neg_false; apply neq_succ_0). setoid_replace (S n == 0) with False by - (apply -> neg_false; apply neq_succ_0). tauto. + (apply neg_false; apply neq_succ_0). tauto. Qed. Theorem eq_add_succ : @@ -47,13 +45,13 @@ Qed. Theorem eq_add_1 : forall n m, n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. -intros n m H. +intros n m. rewrite one_succ. intro H. assert (H1 : exists p, n + m == S p) by now exists 0. -apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +apply eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H. -apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. +apply eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. Qed. Theorem succ_add_discr : forall n m, m ~= S (n + m). @@ -77,5 +75,5 @@ intros n m H; rewrite (add_comm n (P m)); rewrite (add_comm n m); now apply add_pred_l. Qed. -End NAddPropFunct. +End NAddProp. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 0282a6b8..da41886f 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.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: NAddOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NOrder. -Module NAddOrderPropFunct (Import N : NAxiomsSig'). -Include NOrderPropFunct N. +Module NAddOrderProp (Import N : NAxiomsMiniSig'). +Include NOrderProp N. (** Theorems true for natural numbers, not for integers *) @@ -45,4 +43,4 @@ Proof. intros; apply add_nonneg_pos. apply le_0_l. assumption. Qed. -End NAddOrderPropFunct. +End NAddOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index d1cc9972..ca6ccc1b 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.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,32 +8,60 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NAxioms.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Export Bool NZAxioms NZParity NZPow NZSqrt NZLog NZDiv NZGcd NZBits. -Require Export NZAxioms. +(** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *) -Set Implicit Arguments. +Module Type NAxiom (Import NZ : NZDomainSig'). + Axiom pred_0 : P 0 == 0. +End NAxiom. -Module Type NAxioms (Import NZ : NZDomainSig'). +Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom. +Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom. -Axiom pred_0 : P 0 == 0. +(** Let's now add some more functions and their specification *) -Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A. -Implicit Arguments recursion [A]. +(** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon, + and add to that a N-specific constraint. *) -Declare Instance recursion_wd (A : Type) (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). +Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N). + Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. +End NDivSpecific. + +(** For all other functions, the NZ axiomatizations are enough. *) + +(** We now group everything together. *) + +Module Type NAxiomsSig := NAxiomsMiniSig <+ OrderFunctions + <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 + <+ NZGcd.NZGcd <+ NZDiv.NZDiv <+ NZBits.NZBits <+ NZSquare. + +Module Type NAxiomsSig' := NAxiomsMiniSig' <+ OrderFunctions' + <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 + <+ NZGcd.NZGcd' <+ NZDiv.NZDiv' <+ NZBits.NZBits' <+ NZSquare. + + +(** It could also be interesting to have a constructive recursor function. *) + +Module Type NAxiomsRec (Import NZ : NZDomainSig'). + +Parameter Inline recursion : forall {A : Type}, A -> (t -> A -> A) -> t -> A. + +Declare Instance recursion_wd {A : Type} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. Axiom recursion_0 : - forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a. + forall {A} (a : A) (f : t -> A -> A), recursion a f 0 = a. Axiom recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A), + forall {A} (Aeq : relation A) (a : A) (f : t -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)). -End NAxioms. +End NAxiomsRec. -Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms. -Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms. +Module Type NAxiomsRecSig := NAxiomsMiniSig <+ NAxiomsRec. +Module Type NAxiomsRecSig' := NAxiomsMiniSig' <+ NAxiomsRec. +Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec. +Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index efaba960..ac8a0522 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.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,48 +8,23 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NBase.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export Decidable. Require Export NAxioms. Require Import NZProperties. -Module NBasePropFunct (Import N : NAxiomsSig'). +Module NBaseProp (Import N : NAxiomsMiniSig'). (** First, we import all known facts about both natural numbers and integers. *) -Include NZPropFunct N. - -(** We prove that the successor of a number is not zero by defining a -function (by recursion) that maps 0 to false and the successor to true *) - -Definition if_zero (A : Type) (a b : A) (n : N.t) : A := - recursion a (fun _ _ => b) n. - -Implicit Arguments if_zero [A]. - -Instance if_zero_wd (A : Type) : - Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). -Proof. -intros; unfold if_zero. -repeat red; intros. apply recursion_wd; auto. repeat red; auto. -Qed. - -Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a. -Proof. -unfold if_zero; intros; now rewrite recursion_0. -Qed. +Include NZProp N. -Theorem if_zero_succ : - forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b. -Proof. -intros; unfold if_zero. -now rewrite recursion_succ. -Qed. +(** From [pred_0] and order facts, we can prove that 0 isn't a successor. *) Theorem neq_succ_0 : forall n, S n ~= 0. Proof. -intros n H. -generalize (Logic.eq_refl (if_zero false true 0)). -rewrite <- H at 1. rewrite if_zero_0, if_zero_succ; discriminate. + intros n EQ. + assert (EQ' := pred_succ n). + rewrite EQ, pred_0 in EQ'. + rewrite <- EQ' in EQ. + now apply (neq_succ_diag_l 0). Qed. Theorem neq_0_succ : forall n, 0 ~= S n. @@ -66,7 +41,7 @@ nzinduct n. now apply eq_le_incl. intro n; split. apply le_le_succ_r. -intro H; apply -> le_succ_r in H; destruct H as [H | H]. +intro H; apply le_succ_r in H; destruct H as [H | H]. assumption. symmetry in H; false_hyp H neq_succ_0. Qed. @@ -119,12 +94,11 @@ Qed. Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1. Proof. cases n. -rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. -split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. +rewrite pred_0. now split; [left|]. intro n. rewrite pred_succ. -setoid_replace (S n == 0) with False using relation iff by - (apply -> neg_false; apply neq_succ_0). -rewrite succ_inj_wd. tauto. +split. intros H; right. now rewrite H, one_succ. +intros [H|H]. elim (neq_succ_0 _ H). +apply succ_inj_wd. now rewrite <- one_succ. Qed. Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n. @@ -155,6 +129,7 @@ Theorem pair_induction : A 0 -> A 1 -> (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. Proof. +rewrite one_succ. intros until 3. assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. induct n; [ | intros n [IH1 IH2]]; auto. @@ -204,7 +179,7 @@ Ltac double_induct n m := try intros until n; try intros until m; pattern n, m; apply double_induction; clear n m; - [solve_relation_wd | | | ]. + [solve_proper | | | ]. -End NBasePropFunct. +End NBaseProp. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v new file mode 100644 index 00000000..c66f003e --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -0,0 +1,1463 @@ +(************************************************************************) +(* 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 NAxioms NSub NPow NDiv NParity NLog. + +(** Derived properties of bitwise operations *) + +Module Type NBitsProp + (Import A : NAxiomsSig') + (Import B : NSubProp A) + (Import C : NParityProp A B) + (Import D : NPowProp A B C) + (Import E : NDivProp A B) + (Import F : NLog2Prop A B C D). + +Include BoolEqualityFacts A. + +Ltac order_nz := try apply pow_nonzero; order'. +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 -> c<=b -> a^(b-c) == a^b / a^c. +Proof. + intros a b c Ha H. + apply div_unique with 0. + generalize (pow_nonzero a c Ha) (le_0_l (a^c)); order'. + nzsimpl. now rewrite <- pow_add_r, add_comm, sub_add. +Qed. + +Lemma pow_div_l : forall a b c, b~=0 -> a mod b == 0 -> + (a/b)^c == a^c / b^c. +Proof. + intros a b c Hb H. + apply div_unique with 0. + generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'. + nzsimpl. rewrite <- pow_mul_l. f_equiv. now apply div_exact. +Qed. + +(** An injection from bits [true] and [false] to numbers 1 and 0. + We declare it as a (local) coercion for shorter statements. *) + +Definition b2n (b:bool) := if b then 1 else 0. +Local Coercion b2n : bool >-> t. + +Instance b2n_proper : Proper (Logic.eq ==> eq) b2n. +Proof. solve_proper. Qed. + +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 : + testbit (2*a+b) (succ n) = testbit a n. +Proof. + destruct b; simpl; rewrite ?add_0_r. + apply testbit_odd_succ, le_0_l. + apply testbit_even_succ, le_0_l. +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 : a.[n] == (a / 2^n) mod 2. +Proof. + revert a. induct n. + 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. + destruct b; order'. + intros n IH a. + destruct (exists_div2 a) as (a' & b & H). rewrite H at 1. + rewrite testbit_succ_r, IH. f_equiv. + rewrite pow_succ_r', <- div_div by order_nz. f_equiv. + apply div_unique with b; trivial. + destruct b; 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 : + exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n. +Proof. + exists (a mod 2^n). exists (a / 2^n / 2). split. + split; [apply le_0_l | apply mod_upper_bound; order_nz]. + 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'. apply div_mod. order'. +Qed. + +Lemma testbit_true : forall a n, + a.[n] = true <-> (a / 2^n) mod 2 == 1. +Proof. + intros a n. + rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'. +Qed. + +Lemma testbit_false : forall a n, + a.[n] = false <-> (a / 2^n) mod 2 == 0. +Proof. + intros a n. + rewrite <- testbit_spec'; destruct a.[n]; split; simpl; now try order'. +Qed. + +Lemma testbit_eqb : forall a n, + a.[n] = eqb ((a / 2^n) mod 2) 1. +Proof. + intros a n. + apply eq_true_iff_eq. now rewrite testbit_true, eqb_eq. +Qed. + +(** Results about the injection [b2n] *) + +Lemma b2n_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0. +Proof. + intros [|] [|]; simpl; trivial; order'. +Qed. + +Lemma add_b2n_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; order'). +Qed. + +Lemma add_b2n_double_bit0 : forall (a0:bool) a, (a0+2*a).[0] = a0. +Proof. + intros a0 a. apply b2n_inj. + rewrite testbit_spec'. nzsimpl. rewrite mul_comm, mod_add by order'. + now rewrite mod_small by (destruct a0; order'). +Qed. + +Lemma b2n_div2 : forall (a0:bool), a0/2 == 0. +Proof. + intros a0. rewrite <- (add_b2n_double_div2 a0 0). now nzsimpl. +Qed. + +Lemma b2n_bit0 : forall (a0:bool), a0.[0] = a0. +Proof. + intros a0. rewrite <- (add_b2n_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, + l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0. +Proof. + intros a n a0 l h Hl EQ. + apply b2n_inj. rewrite testbit_spec' by trivial. + symmetry. apply mod_unique with h. destruct a0; simpl; order'. + symmetry. apply div_unique with l; trivial. + 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. apply testbit_false. nzsimpl; order_nz. +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. now nzsimpl. +Qed. + +Lemma bit0_mod : forall a, a.[0] == a mod 2. +Proof. + intros a. rewrite testbit_spec'. 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 *) + +Lemma bit_log2 : forall a, a~=0 -> a.[log2 a] = true. +Proof. + intros a Ha. + assert (Ha' : 0 < a) by (generalize (le_0_l a); order). + destruct (log2_spec_alt a Ha') as (r & EQ & (_,Hr)). + rewrite EQ at 1. + rewrite testbit_true, add_comm. + rewrite <- (mul_1_l (2^log2 a)) at 1. + rewrite div_add by order_nz. + rewrite div_small by trivial. + rewrite add_0_l. apply mod_small. order'. +Qed. + +Lemma bits_above_log2 : forall a n, log2 a < n -> + a.[n] = false. +Proof. + intros a n H. + rewrite testbit_false. + rewrite div_small. nzsimpl; order'. + apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l. +Qed. + +(** Hence the number of bits of [a] is [1+log2 a] + (see [Psize] and [Psize_pos]). +*) + +(** Testing bits after division or multiplication by a power of two *) + +Lemma div2_bits : forall a n, (a/2).[n] = a.[S n]. +Proof. + intros. apply eq_true_iff_eq. + rewrite 2 testbit_true. + rewrite pow_succ_r by apply le_0_l. + now rewrite div_div by order_nz. +Qed. + +Lemma div_pow2_bits : forall a n m, (a/2^n).[m] = a.[m+n]. +Proof. + intros a n. revert a. induct n. + intros a m. now nzsimpl. + intros n IH a m. nzsimpl; try apply le_0_l. + rewrite <- div_div by order_nz. + now rewrite IH, div2_bits. +Qed. + +Lemma double_bits_succ : forall a n, (2*a).[S n] = a.[n]. +Proof. + intros. rewrite <- div2_bits. now rewrite mul_comm, div_mul by order'. +Qed. + +Lemma mul_pow2_bits_add : forall a n m, (a*2^n).[m+n] = a.[m]. +Proof. + intros. rewrite <- div_pow2_bits. now rewrite div_mul by order_nz. +Qed. + +Lemma mul_pow2_bits_high : forall a n m, n<=m -> (a*2^n).[m] = a.[m-n]. +Proof. + intros. + rewrite <- (sub_add n m) at 1 by order'. + now rewrite mul_pow2_bits_add. +Qed. + +Lemma mul_pow2_bits_low : forall a n m, m<n -> (a*2^n).[m] = false. +Proof. + intros. apply testbit_false. + rewrite <- (sub_add m n) by order'. rewrite pow_add_r, mul_assoc. + rewrite div_mul by order_nz. + rewrite <- (succ_pred (n-m)). rewrite pow_succ_r. + now rewrite (mul_comm 2), mul_assoc, mod_mul by order'. + apply lt_le_pred. + apply sub_gt in H. generalize (le_0_l (n-m)); order. + now apply sub_gt. +Qed. + +(** Selecting the low part of a number can be done by a modulo *) + +Lemma mod_pow2_bits_high : forall a n m, n<=m -> + (a mod 2^n).[m] = false. +Proof. + intros a n m H. + destruct (eq_0_gt_0_cases (a mod 2^n)) as [EQ|LT]. + now rewrite EQ, bits_0. + apply bits_above_log2. + apply lt_le_trans with n; trivial. + apply log2_lt_pow2; trivial. + apply mod_upper_bound; order_nz. +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. + rewrite testbit_eqb. + 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 + by now apply sub_gt. + rewrite mul_comm, mul_assoc, <- pow_add_r, (add_comm m), sub_add + by order. + rewrite add_comm, <- div_mod by order_nz. + symmetry. apply testbit_eqb. +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 (eq_decidable a 0) as [EQ|NEQ]; trivial. + apply bit_log2 in NEQ. now rewrite H in NEQ. +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. + intros a. pattern a. + apply strong_right_induction with 0;[solve_proper|clear a|apply le_0_l]. + intros a _ IH b H. + destruct (eq_0_gt_0_cases a) as [EQ|LT]. + rewrite EQ in H |- *. symmetry. apply bits_inj_0. + intros n. now rewrite <- H, bits_0. + rewrite (div_mod a 2), (div_mod b 2) by order'. + f_equiv; [ | now rewrite <- 2 bit0_mod, H]. + f_equiv. + apply IH; trivial using le_0_l. + apply div_lt; order'. + intro n. rewrite 2 div2_bits. apply H. +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. + +Hint Rewrite lxor_spec lor_spec land_spec ldiff_spec bits_0 : bitwise. + +Ltac bitwise := apply bits_inj; intros ?m; autorewrite with bitwise. + +(** The streams of bits that correspond to a natural numbers are + exactly the ones that are always 0 after some point *) + +Lemma are_bits : forall (f:t->bool), Proper (eq==>Logic.eq) f -> + ((exists n, f === testbit n) <-> + (exists k, forall m, k<=m -> f m = false)). +Proof. + intros f Hf. split. + intros (a,H). + exists (S (log2 a)). intros m Hm. apply le_succ_l in Hm. + rewrite H, bits_above_log2; trivial using lt_succ_diag_r. + intros (k,Hk). + revert f Hf Hk. induct k. + intros f Hf H0. + exists 0. intros m. rewrite bits_0, H0; trivial. apply le_0_l. + intros k 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. + destruct (zero_or_succ m) as [Hm|(m', Hm)]; rewrite Hm. + symmetry. apply add_b2n_double_bit0. + rewrite Hn, <- div2_bits. + rewrite mul_comm, div_add, b2n_div2, add_0_l; trivial. order'. +Qed. + +(** Properties of shifts *) + +Lemma shiftr_spec' : forall a n m, (a >> n).[m] = a.[m+n]. +Proof. + intros. apply shiftr_spec. apply le_0_l. +Qed. + +Lemma shiftl_spec_high' : forall a n m, n<=m -> (a << n).[m] = a.[m-n]. +Proof. + intros. apply shiftl_spec_high; trivial. apply le_0_l. +Qed. + +Lemma shiftr_div_pow2 : forall a n, a >> n == a / 2^n. +Proof. + intros. bitwise. rewrite shiftr_spec'. + symmetry. apply div_pow2_bits. +Qed. + +Lemma shiftl_mul_pow2 : forall a n, a << n == a * 2^n. +Proof. + intros. bitwise. + destruct (le_gt_cases n m) as [H|H]. + now rewrite shiftl_spec_high', mul_pow2_bits_high. + now rewrite shiftl_spec_low, mul_pow2_bits_low. +Qed. + +Lemma shiftl_spec_alt : forall a n m, (a << n).[m+n] = a.[m]. +Proof. + intros. now rewrite shiftl_mul_pow2, mul_pow2_bits_add. +Qed. + +Instance shiftr_wd : Proper (eq==>eq==>eq) shiftr. +Proof. + intros a a' Ha b b' Hb. now rewrite 2 shiftr_div_pow2, Ha, Hb. +Qed. + +Instance shiftl_wd : Proper (eq==>eq==>eq) shiftl. +Proof. + intros a a' Ha b b' Hb. now rewrite 2 shiftl_mul_pow2, Ha, Hb. +Qed. + +Lemma shiftl_shiftl : forall a n m, + (a << n) << m == a << (n+m). +Proof. + intros. now rewrite !shiftl_mul_pow2, pow_add_r, mul_assoc. +Qed. + +Lemma shiftr_shiftr : forall a n m, + (a >> n) >> m == a >> (n+m). +Proof. + intros. + now rewrite !shiftr_div_pow2, pow_add_r, div_div by order_nz. +Qed. + +Lemma shiftr_shiftl_l : forall a n m, m<=n -> + (a << n) >> m == a << (n-m). +Proof. + intros. + rewrite shiftr_div_pow2, !shiftl_mul_pow2. + rewrite <- (sub_add m n) at 1 by trivial. + now rewrite pow_add_r, mul_assoc, div_mul by order_nz. +Qed. + +Lemma shiftr_shiftl_r : forall a n m, n<=m -> + (a << n) >> m == a >> (m-n). +Proof. + intros. + rewrite !shiftr_div_pow2, shiftl_mul_pow2. + rewrite <- (sub_add n m) at 1 by trivial. + rewrite pow_add_r, (mul_comm (2^(m-n))). + now rewrite <- div_div, div_mul by order_nz. +Qed. + +(** shifts and constants *) + +Lemma shiftl_1_l : forall n, 1 << n == 2^n. +Proof. + intros. now rewrite shiftl_mul_pow2, mul_1_l. +Qed. + +Lemma shiftl_0_r : forall a, a << 0 == a. +Proof. + intros. rewrite shiftl_mul_pow2. now nzsimpl. +Qed. + +Lemma shiftr_0_r : forall a, a >> 0 == a. +Proof. + intros. rewrite shiftr_div_pow2. now nzsimpl. +Qed. + +Lemma shiftl_0_l : forall n, 0 << n == 0. +Proof. + intros. rewrite shiftl_mul_pow2. now nzsimpl. +Qed. + +Lemma shiftr_0_l : forall n, 0 >> n == 0. +Proof. + intros. rewrite shiftr_div_pow2. nzsimpl; order_nz. +Qed. + +Lemma shiftl_eq_0_iff : forall a n, a << n == 0 <-> a == 0. +Proof. + intros a n. rewrite shiftl_mul_pow2. 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. + rewrite shiftr_div_pow2, div_small_iff by order_nz. + destruct (eq_0_gt_0_cases a) as [EQ|LT]. + rewrite EQ. split. now left. intros _. + assert (H : 2~=0) by order'. + generalize (pow_nonzero 2 n H) (le_0_l (2^n)); order. + rewrite log2_lt_pow2; trivial. + split. right; split; trivial. intros [H|[_ H]]; now order. +Qed. + +Lemma shiftr_eq_0 : forall a n, log2 a < n -> a >> n == 0. +Proof. + intros a n H. rewrite shiftr_eq_0_iff. + destruct (eq_0_gt_0_cases a) as [EQ|LT]. now left. right; now split. +Qed. + +(** Properties of [div2]. *) + +Lemma div2_div : forall a, div2 a == a/2. +Proof. + intros. rewrite div2_spec, shiftr_div_pow2. now nzsimpl. +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, (2^n).[n] = true. +Proof. + intros. rewrite <- (mul_1_l (2^n)). rewrite <- (add_0_l n) at 2. + now rewrite mul_pow2_bits_add, bit0_odd, odd_1. +Qed. + +Lemma pow2_bits_false : forall n m, n~=m -> (2^n).[m] = false. +Proof. + intros. + rewrite <- (mul_1_l (2^n)). + destruct (le_gt_cases n m). + rewrite mul_pow2_bits_high; trivial. + rewrite <- (succ_pred (m-n)) by (apply sub_gt; order). + now rewrite <- div2_bits, div_small, bits_0 by order'. + rewrite mul_pow2_bits_low; trivial. +Qed. + +Lemma pow2_bits_eqb : forall n m, (2^n).[m] = eqb n m. +Proof. + intros. 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. +Qed. + +Lemma setbit_eqb : forall a n m, + (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, + (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, (setbit a n).[n] = true. +Proof. + intros. apply setbit_iff. now left. +Qed. + +Lemma setbit_neq : forall a n m, n~=m -> + (setbit a n).[m] = a.[m]. +Proof. + intros a n m H. rewrite setbit_eqb. + 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. now rewrite clearbit_spec', ldiff_spec, pow2_bits_eqb. +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. + destruct (le_gt_cases n m). + now rewrite !shiftl_spec_high', lxor_spec. + now rewrite !shiftl_spec_low. +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. + destruct (le_gt_cases n m). + now rewrite !shiftl_spec_high', land_spec. + now rewrite !shiftl_spec_low. +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. + destruct (le_gt_cases n m). + now rewrite !shiftl_spec_high', lor_spec. + now rewrite !shiftl_spec_low. +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. + destruct (le_gt_cases n m). + now rewrite !shiftl_spec_high', ldiff_spec. + now rewrite !shiftl_spec_low. +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. + +(** We cannot have a function complementing all bits of a number, + otherwise it would have an infinity of bit 1. Nonetheless, + we can design a bounded complement *) + +Definition ones n := P (1 << n). + +Definition lnot a n := lxor a (ones n). + +Instance ones_wd : Proper (eq==>eq) ones. +Proof. unfold ones. solve_proper. Qed. + +Instance lnot_wd : Proper (eq==>eq==>eq) lnot. +Proof. unfold lnot. solve_proper. Qed. + +Lemma ones_equiv : forall n, ones n == P (2^n). +Proof. + intros; unfold ones; now rewrite shiftl_1_l. +Qed. + +Lemma ones_add : forall n m, ones (m+n) == 2^m * ones n + ones m. +Proof. + intros n m. rewrite !ones_equiv. + rewrite <- !sub_1_r, mul_sub_distr_l, mul_1_r, <- pow_add_r. + rewrite add_sub_assoc, sub_add. reflexivity. + apply pow_le_mono_r. order'. + rewrite <- (add_0_r m) at 1. apply add_le_mono_l, le_0_l. + rewrite <- (pow_0_r 2). apply pow_le_mono_r. order'. apply le_0_l. +Qed. + +Lemma ones_div_pow2 : forall n m, m<=n -> ones n / 2^m == ones (n-m). +Proof. + intros n m H. symmetry. apply div_unique with (ones m). + rewrite ones_equiv. + apply le_succ_l. rewrite succ_pred; order_nz. + rewrite <- (sub_add m n H) at 1. rewrite (add_comm _ m). + apply ones_add. +Qed. + +Lemma ones_mod_pow2 : forall n m, m<=n -> (ones n) mod (2^m) == ones m. +Proof. + intros n m H. symmetry. apply mod_unique with (ones (n-m)). + rewrite ones_equiv. + apply le_succ_l. rewrite succ_pred; order_nz. + rewrite <- (sub_add m n H) at 1. rewrite (add_comm _ m). + apply ones_add. +Qed. + +Lemma ones_spec_low : forall n m, m<n -> (ones n).[m] = true. +Proof. + intros. apply testbit_true. rewrite ones_div_pow2 by order. + rewrite <- (pow_1_r 2). rewrite ones_mod_pow2. + rewrite ones_equiv. now nzsimpl'. + apply le_add_le_sub_r. nzsimpl. now apply le_succ_l. +Qed. + +Lemma ones_spec_high : forall n m, n<=m -> (ones n).[m] = false. +Proof. + intros. + destruct (eq_0_gt_0_cases n) as [EQ|LT]; rewrite ones_equiv. + now rewrite EQ, pow_0_r, one_succ, pred_succ, bits_0. + apply bits_above_log2. + rewrite log2_pred_pow2; trivial. rewrite <-le_succ_l, succ_pred; order. +Qed. + +Lemma ones_spec_iff : forall n m, (ones n).[m] = true <-> m<n. +Proof. + intros. split. intros H. + apply lt_nge. intro H'. apply ones_spec_high in H'. + rewrite H in H'; discriminate. + apply ones_spec_low. +Qed. + +Lemma lnot_spec_low : forall a n m, m<n -> + (lnot a n).[m] = negb a.[m]. +Proof. + intros. unfold lnot. now rewrite lxor_spec, ones_spec_low. +Qed. + +Lemma lnot_spec_high : forall a n m, n<=m -> + (lnot a n).[m] = a.[m]. +Proof. + intros. unfold lnot. now rewrite lxor_spec, ones_spec_high, xorb_false_r. +Qed. + +Lemma lnot_involutive : forall a n, lnot (lnot a n) n == a. +Proof. + intros a n. bitwise. + destruct (le_gt_cases n m). + now rewrite 2 lnot_spec_high. + now rewrite 2 lnot_spec_low, negb_involutive. +Qed. + +Lemma lnot_0_l : forall n, lnot 0 n == ones n. +Proof. + intros. unfold lnot. apply lxor_0_l. +Qed. + +Lemma lnot_ones : forall n, lnot (ones n) n == 0. +Proof. + intros. unfold lnot. apply lxor_nilpotent. +Qed. + +(** Bounded complement and other operations *) + +Lemma lor_ones_low : forall a n, log2 a < n -> + lor a (ones n) == ones n. +Proof. + intros a n H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + now rewrite ones_spec_low, orb_true_r. +Qed. + +Lemma land_ones : forall a n, land a (ones n) == a mod 2^n. +Proof. + intros a n. bitwise. destruct (le_gt_cases n m). + now rewrite ones_spec_high, mod_pow2_bits_high, andb_false_r. + now rewrite ones_spec_low, mod_pow2_bits_low, andb_true_r. +Qed. + +Lemma land_ones_low : forall a n, log2 a < n -> + land a (ones n) == a. +Proof. + intros; rewrite land_ones. apply mod_small. + apply log2_lt_cancel. rewrite log2_pow2; trivial using le_0_l. +Qed. + +Lemma ldiff_ones_r : forall a n, + ldiff a (ones n) == (a >> n) << n. +Proof. + intros a n. 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 rewrite ones_spec_low, shiftl_spec_low, andb_false_r. +Qed. + +Lemma ldiff_ones_r_low : forall a n, log2 a < n -> + ldiff a (ones n) == 0. +Proof. + intros a n H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + now rewrite ones_spec_low, andb_false_r. +Qed. + +Lemma ldiff_ones_l_low : forall a n, log2 a < n -> + ldiff (ones n) a == lnot a n. +Proof. + intros a n H. bitwise. destruct (le_gt_cases n m). + rewrite ones_spec_high, lnot_spec_high, bits_above_log2; trivial. + now apply lt_le_trans with n. + now rewrite ones_spec_low, lnot_spec_low. +Qed. + +Lemma lor_lnot_diag : forall a n, + lor a (lnot a n) == lor a (ones n). +Proof. + intros a n. bitwise. + destruct (le_gt_cases n m). + rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. + rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. +Qed. + +Lemma lor_lnot_diag_low : forall a n, log2 a < n -> + lor a (lnot a n) == ones n. +Proof. + intros a n H. now rewrite lor_lnot_diag, lor_ones_low. +Qed. + +Lemma land_lnot_diag : forall a n, + land a (lnot a n) == ldiff a (ones n). +Proof. + intros a n. bitwise. + destruct (le_gt_cases n m). + rewrite lnot_spec_high, ones_spec_high; trivial. now destruct a.[m]. + rewrite lnot_spec_low, ones_spec_low; trivial. now destruct a.[m]. +Qed. + +Lemma land_lnot_diag_low : forall a n, log2 a < n -> + land a (lnot a n) == 0. +Proof. + intros. now rewrite land_lnot_diag, ldiff_ones_r_low. +Qed. + +Lemma lnot_lor_low : forall a b n, log2 a < n -> log2 b < n -> + lnot (lor a b) n == land (lnot a n) (lnot b n). +Proof. + intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high, lor_spec, !bits_above_log2; trivial. + now apply lt_le_trans with n. + now apply lt_le_trans with n. + now rewrite !lnot_spec_low, lor_spec, negb_orb. +Qed. + +Lemma lnot_land_low : forall a b n, log2 a < n -> log2 b < n -> + lnot (land a b) n == lor (lnot a n) (lnot b n). +Proof. + intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high, land_spec, !bits_above_log2; trivial. + now apply lt_le_trans with n. + now apply lt_le_trans with n. + now rewrite !lnot_spec_low, land_spec, negb_andb. +Qed. + +Lemma ldiff_land_low : forall a b n, log2 a < n -> + ldiff a b == land a (lnot b n). +Proof. + intros a b n Ha. bitwise. destruct (le_gt_cases n m). + rewrite (bits_above_log2 a m). trivial. + now apply lt_le_trans with n. + rewrite !lnot_spec_low; trivial. +Qed. + +Lemma lnot_ldiff_low : forall a b n, log2 a < n -> log2 b < n -> + lnot (ldiff a b) n == lor (lnot a n) b. +Proof. + intros a b n Ha Hb. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high, ldiff_spec, !bits_above_log2; trivial. + now apply lt_le_trans with n. + now apply lt_le_trans with n. + now rewrite !lnot_spec_low, ldiff_spec, negb_andb, negb_involutive. +Qed. + +Lemma lxor_lnot_lnot : forall a b n, + lxor (lnot a n) (lnot b n) == lxor a b. +Proof. + intros a b n. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high; trivial. + rewrite !lnot_spec_low, xorb_negb_negb; trivial. +Qed. + +Lemma lnot_lxor_l : forall a b n, + lnot (lxor a b) n == lxor (lnot a n) b. +Proof. + intros a b n. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high, lxor_spec; trivial. + rewrite !lnot_spec_low, lxor_spec, negb_xorb_l; trivial. +Qed. + +Lemma lnot_lxor_r : forall a b n, + lnot (lxor a b) n == lxor a (lnot b n). +Proof. + intros a b n. bitwise. destruct (le_gt_cases n m). + rewrite !lnot_spec_high, lxor_spec; trivial. + rewrite !lnot_spec_low, lxor_spec, negb_xorb_r; trivial. +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. + +(** 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 (eq_0_gt_0_cases a) as [Ha|Ha]. + now rewrite Ha, bits_0 in H. + apply le_antisymm; apply le_ngt; intros LT. + specialize (H' _ LT). now rewrite bit_log2 in H' by order. + now rewrite bits_above_log2 in H by order. +Qed. + +Lemma log2_shiftr : forall a n, log2 (a >> n) == log2 a - n. +Proof. + intros a n. + destruct (eq_0_gt_0_cases a) as [Ha|Ha]. + now rewrite Ha, shiftr_0_l, log2_nonpos, sub_0_l by order. + destruct (lt_ge_cases (log2 a) n). + rewrite shiftr_eq_0, log2_nonpos by order. + symmetry. rewrite sub_0_le; order. + apply log2_bits_unique. + now rewrite shiftr_spec', sub_add, bit_log2 by order. + intros m Hm. + rewrite shiftr_spec'; trivial. apply bits_above_log2; try order. + now apply lt_sub_lt_add_r. +Qed. + +Lemma log2_shiftl : forall a n, a~=0 -> log2 (a << n) == log2 a + n. +Proof. + intros a n Ha. + rewrite shiftl_mul_pow2, add_comm by trivial. + apply log2_mul_pow2. generalize (le_0_l a); order. apply le_0_l. +Qed. + +Lemma log2_lor : forall a b, + log2 (lor a b) == max (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, a<=b -> log2 (lor a b) == log2 b). + intros a b H. + destruct (eq_0_gt_0_cases a) as [Ha|Ha]. now rewrite Ha, lor_0_l. + apply log2_bits_unique. + now rewrite lor_spec, bit_log2, orb_true_r by order. + intros m Hm. assert (H' := log2_le_mono _ _ H). + now rewrite lor_spec, 2 bits_above_log2 by order. + (* main *) + intros a b. 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, + log2 (land a b) <= min (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, a<=b -> log2 (land a b) <= log2 a). + intros a b H. + apply le_ngt. intros H'. + destruct (eq_decidable (land a b) 0) as [EQ|NEQ]. + rewrite EQ in H'. apply log2_lt_cancel in H'. generalize (le_0_l a); order. + generalize (bit_log2 (land a b) NEQ). + now rewrite land_spec, bits_above_log2. + (* main *) + intros a b. + 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, + log2 (lxor a b) <= max (log2 a) (log2 b). +Proof. + assert (AUX : forall a b, a<=b -> log2 (lxor a b) <= log2 b). + intros a b H. + apply le_ngt. intros H'. + destruct (eq_decidable (lxor a b) 0) as [EQ|NEQ]. + rewrite EQ in H'. apply log2_lt_cancel in H'. generalize (le_0_l a); order. + generalize (bit_log2 (lxor a b) NEQ). + rewrite lxor_spec, 2 bits_above_log2; try order. discriminate. + apply le_lt_trans with (log2 b); trivial. now apply log2_le_mono. + (* main *) + intros a b. + 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; order') || idtac. + symmetry. apply div_unique with 1. 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. fold (b2n a.[0]). + rewrite (div2_odd b), <- bit0_odd at 1. fold (b2n b.[0]). + 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 : 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. + (* induction over some n such that [a<2^n] and [b<2^n] *) + set (n:=max a b). + assert (Ha : a<2^n). + apply lt_le_trans with (2^a). apply pow_gt_lin_r, lt_1_2. + apply pow_le_mono_r. order'. unfold n. + destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'. + assert (Hb : b<2^n). + apply lt_le_trans with (2^b). apply pow_gt_lin_r, lt_1_2. + apply pow_le_mono_r. order'. unfold n. + destruct (le_ge_cases a b); [rewrite max_r|rewrite max_l]; order'. + clearbody n. + revert a b c0 Ha Hb. induct n. + (*base*) + intros a b c0. rewrite !pow_0_r, !one_succ, !lt_succ_r. intros Ha Hb. + exists c0. + setoid_replace a with 0 by (generalize (le_0_l a); order'). + setoid_replace b with 0 by (generalize (le_0_l b); order'). + rewrite !add_0_l, !lxor_0_l, !lor_0_r, !land_0_r, !lor_0_r. + rewrite b2n_div2, b2n_bit0; now repeat split. + (*step*) + intros n 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. + apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'. + apply div_lt_upper_bound; trivial. order'. now rewrite <- pow_succ_r'. + exists (c0 + 2*c). repeat split. + (* - add *) + bitwise. + destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. + now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0. + rewrite <- !div2_bits, <- 2 lxor_spec. + f_equiv. + rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2. + (* - carry *) + rewrite add_b2n_double_div2. + bitwise. + destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ. + now rewrite add_b2n_double_bit0. + rewrite <- !div2_bits, IH2. autorewrite with bitwise. + now rewrite add_b2n_double_div2. + (* - carry0 *) + apply add_b2n_double_bit0. +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. + 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_0. + induct n. trivial. + intros n IH. + rewrite <- div2_bits, H. + 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, ldiff a b == 0 -> a <= b. +Proof. + cut (forall n a b, a < 2^n -> ldiff a b == 0 -> a <= b). + intros H a b. apply (H a), pow_gt_lin_r; order'. + induct n. + intros a b Ha _. rewrite pow_0_r, one_succ, lt_succ_r in Ha. + assert (Ha' : a == 0) by (generalize (le_0_l a); order'). + rewrite Ha'. apply le_0_l. + intros n IH a b Ha 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_l. + apply IH. + apply div_lt_upper_bound; trivial. now rewrite <- pow_succ_r'. + rewrite <- (pow_1_r 2), <- 2 shiftr_div_pow2. + now rewrite <- shiftr_ldiff, H, shiftr_div_pow2, pow_1_r, div_0_l. + 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'. +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. + 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. + now apply ldiff_le. +Qed. + +(** We can express lnot in term of subtraction *) + +Lemma add_lnot_diag_low : forall a n, log2 a < n -> + a + lnot a n == ones n. +Proof. + intros a n H. + assert (H' := land_lnot_diag_low a n H). + rewrite add_nocarry_lxor, lxor_lor by trivial. + now apply lor_lnot_diag_low. +Qed. + +Lemma lnot_sub_low : forall a n, log2 a < n -> + lnot a n == ones n - a. +Proof. + intros a n H. + now rewrite <- (add_lnot_diag_low a n H), add_comm, add_sub. +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. + rewrite add_nocarry_lxor by trivial. + apply div_small_iff. order_nz. + rewrite <- shiftr_div_pow2, shiftr_lxor, !shiftr_div_pow2. + rewrite 2 div_small by trivial. + apply lxor_0_l. +Qed. + +Lemma add_nocarry_mod_lt_pow2 : forall a b n, land a b == 0 -> + a mod 2^n + b mod 2^n < 2^n. +Proof. + intros a b n H. + apply add_nocarry_lt_pow2. + bitwise. + destruct (le_gt_cases n m). + now rewrite mod_pow2_bits_high. + now rewrite !mod_pow2_bits_low, <- land_spec, H, bits_0. + apply mod_upper_bound; order_nz. + apply mod_upper_bound; order_nz. +Qed. + +End NBitsProp. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 7b38c148..ad7a9f3a 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.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,41 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NDefOps.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Bool. (* To get the orb and negb function *) Require Import RelationPairs. Require Export NStrongRec. -Module NdefOpsPropFunct (Import N : NAxiomsSig'). -Include NStrongRecPropFunct N. +(** In this module, we derive generic implementations of usual operators + just via the use of a [recursion] function. *) + +Module NdefOpsProp (Import N : NAxiomsRecSig'). +Include NStrongRecProp N. + +(** Nullity Test *) + +Definition if_zero (A : Type) (a b : A) (n : N.t) : A := + recursion a (fun _ _ => b) n. + +Arguments if_zero [A] a b n. + +Instance if_zero_wd (A : Type) : + Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A). +Proof. +unfold if_zero. (* TODO : solve_proper : SLOW + BUG *) +f_equiv'. +Qed. + +Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a. +Proof. +unfold if_zero; intros; now rewrite recursion_0. +Qed. + +Theorem if_zero_succ : + forall (A : Type) (a b : A) (n : N.t), if_zero a b (S n) = b. +Proof. +intros; unfold if_zero. +now rewrite recursion_succ. +Qed. (*****************************************************) (** Addition *) @@ -24,17 +51,9 @@ Definition def_add (x y : N.t) := recursion y (fun _ => S) x. Local Infix "+++" := def_add (at level 50, left associativity). -Instance def_add_prewd : Proper (N.eq==>N.eq==>N.eq) (fun _ => S). -Proof. -intros _ _ _ p p' Epp'; now rewrite Epp'. -Qed. - Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add. Proof. -intros x x' Exx' y y' Eyy'. unfold def_add. -(* TODO: why rewrite Exx' don't work here (or verrrry slowly) ? *) -apply recursion_wd with (Aeq := N.eq); auto with *. -apply def_add_prewd. +unfold def_add. f_equiv'. Qed. Theorem def_add_0_l : forall y, 0 +++ y == y. @@ -45,7 +64,7 @@ Qed. Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y). Proof. intros x y; unfold def_add. -rewrite recursion_succ; auto with *. +rewrite recursion_succ; f_equiv'. Qed. Theorem def_add_add : forall n m, n +++ m == n + m. @@ -62,18 +81,10 @@ Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y. Local Infix "**" := def_mul (at level 40, left associativity). -Instance def_mul_prewd : - Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun x _ p => p +++ x). -Proof. -repeat red; intros; now apply def_add_wd. -Qed. - Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul. Proof. -unfold def_mul. -intros x x' Exx' y y' Eyy'. -apply recursion_wd; auto with *. -now apply def_mul_prewd. +unfold def_mul. (* TODO : solve_proper SLOW + BUG *) +f_equiv'. Qed. Theorem def_mul_0_r : forall x, x ** 0 == 0. @@ -85,7 +96,7 @@ Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x. Proof. intros x y; unfold def_mul. rewrite recursion_succ; auto with *. -now apply def_mul_prewd. +f_equiv'. Qed. Theorem def_mul_mul : forall n m, n ** m == n * m. @@ -106,25 +117,9 @@ recursion Local Infix "<<" := ltb (at level 70, no associativity). -Instance ltb_prewd1 : Proper (N.eq==>Logic.eq) (if_zero false true). -Proof. -red; intros; apply if_zero_wd; auto. -Qed. - -Instance ltb_prewd2 : Proper (N.eq==>(N.eq==>Logic.eq)==>N.eq==>Logic.eq) - (fun _ f n => recursion false (fun n' _ => f n') n). -Proof. -repeat red; intros; simpl. -apply recursion_wd; auto with *. -repeat red; auto. -Qed. - Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb. Proof. -unfold ltb. -intros n n' Hn m m' Hm. -apply f_equiv; auto with *. -apply recursion_wd; auto; [ apply ltb_prewd1 | apply ltb_prewd2 ]. +unfold ltb. f_equiv'. Qed. Theorem ltb_base : forall n, 0 << n = if_zero false true n. @@ -136,11 +131,9 @@ Theorem ltb_step : forall m n, S m << n = recursion false (fun n' _ => m << n') n. Proof. intros m n; unfold ltb at 1. -apply f_equiv; auto with *. -rewrite recursion_succ by (apply ltb_prewd1||apply ltb_prewd2). -fold (ltb m). -repeat red; intros. apply recursion_wd; auto. -repeat red; intros; now apply ltb_wd. +f_equiv. +rewrite recursion_succ; f_equiv'. +reflexivity. Qed. (* Above, we rewrite applications of function. Is it possible to rewrite @@ -162,8 +155,7 @@ Qed. Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m). Proof. intros n m. -rewrite ltb_step. rewrite recursion_succ; try reflexivity. -repeat red; intros; now apply ltb_wd. +rewrite ltb_step. rewrite recursion_succ; f_equiv'. Qed. Theorem ltb_lt : forall n m, n << m = true <-> n < m. @@ -188,9 +180,7 @@ Definition even (x : N.t) := recursion true (fun _ p => negb p) x. Instance even_wd : Proper (N.eq==>Logic.eq) even. Proof. -intros n n' Hn. unfold even. -apply recursion_wd; auto. -congruence. +unfold even. f_equiv'. Qed. Theorem even_0 : even 0 = true. @@ -202,19 +192,12 @@ Qed. Theorem even_succ : forall x, even (S x) = negb (even x). Proof. unfold even. -intro x; rewrite recursion_succ; try reflexivity. -congruence. +intro x; rewrite recursion_succ; f_equiv'. Qed. (*****************************************************) (** Division by 2 *) -Local Notation "a <= b <= c" := (a<=b /\ b<=c). -Local Notation "a <= b < c" := (a<=b /\ b<c). -Local Notation "a < b <= c" := (a<b /\ b<=c). -Local Notation "a < b < c" := (a<b /\ b<c). -Local Notation "2" := (S 1). - Definition half_aux (x : N.t) : N.t * N.t := recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x. @@ -223,14 +206,14 @@ Definition half (x : N.t) := snd (half_aux x). Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux. Proof. intros x x' Hx. unfold half_aux. -apply recursion_wd; auto with *. +f_equiv; trivial. intros y y' Hy (u,v) (u',v') (Hu,Hv). compute in *. rewrite Hu, Hv; auto with *. Qed. Instance half_wd : Proper (N.eq==>N.eq) half. Proof. -intros x x' Hx. unfold half. rewrite Hx; auto with *. +unfold half. f_equiv'. Qed. Lemma half_aux_0 : half_aux 0 = (0,0). @@ -245,8 +228,7 @@ intros. remember (half_aux x) as h. destruct h as (f,s); simpl in *. unfold half_aux in *. -rewrite recursion_succ, <- Heqh; simpl; auto. -repeat red; intros; subst; auto. +rewrite recursion_succ, <- Heqh; simpl; f_equiv'. Qed. Theorem half_aux_spec : forall n, @@ -258,7 +240,7 @@ rewrite half_aux_0; simpl; rewrite add_0_l; auto with *. intros. rewrite half_aux_succ. simpl. rewrite add_succ_l, add_comm; auto. -apply succ_wd; auto. +now f_equiv. Qed. Theorem half_aux_spec2 : forall n, @@ -271,7 +253,7 @@ rewrite half_aux_0; simpl. auto with *. intros. rewrite half_aux_succ; simpl. destruct H; auto with *. -right; apply succ_wd; auto with *. +right; now f_equiv. Qed. Theorem half_0 : half 0 == 0. @@ -281,14 +263,14 @@ Qed. Theorem half_1 : half 1 == 0. Proof. -unfold half. rewrite half_aux_succ, half_aux_0; simpl; auto with *. +unfold half. rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *. Qed. Theorem half_double : forall n, n == 2 * half n \/ n == 1 + 2 * half n. Proof. intros. unfold half. -nzsimpl. +nzsimpl'. destruct (half_aux_spec2 n) as [H|H]; [left|right]. rewrite <- H at 1. apply half_aux_spec. rewrite <- add_succ_l. rewrite <- H at 1. apply half_aux_spec. @@ -319,24 +301,23 @@ assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. destruct (half_double n) as [E|E]; rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT. -destruct (nlt_0_r _ LT). -rewrite <- succ_lt_mono in LT. -destruct (nlt_0_r _ LT). +order'. +order. Qed. Theorem half_decrease : forall n, 0 < n -> half n < n. Proof. intros n LT. -destruct (half_double n) as [E|E]; rewrite E at 2; - rewrite ?mul_succ_l, ?mul_0_l, ?add_0_l, ?add_assoc. +destruct (half_double n) as [E|E]; rewrite E at 2; nzsimpl'. rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. assert (LE : 0 <= half n) by apply le_0_l. le_elim LE; auto. rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT). +rewrite <- add_succ_l. rewrite <- add_0_l at 1. rewrite <- add_lt_mono_r. -rewrite add_succ_l. apply lt_0_succ. +apply lt_0_succ. Qed. @@ -347,17 +328,9 @@ Definition pow (n m : N.t) := recursion 1 (fun _ r => n*r) m. Local Infix "^^" := pow (at level 30, right associativity). -Instance pow_prewd : - Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun n _ r => n*r). -Proof. -intros n n' Hn x x' Hx y y' Hy. rewrite Hn, Hy; auto with *. -Qed. - Instance pow_wd : Proper (N.eq==>N.eq==>N.eq) pow. Proof. -intros n n' Hn m m' Hm. unfold pow. -apply recursion_wd; auto with *. -now apply pow_prewd. +unfold pow. f_equiv'. Qed. Lemma pow_0 : forall n, n^^0 == 1. @@ -367,8 +340,7 @@ Qed. Lemma pow_succ : forall n m, n^^(S m) == n*(n^^m). Proof. -intros. unfold pow. rewrite recursion_succ; auto with *. -now apply pow_prewd. +intros. unfold pow. rewrite recursion_succ; f_equiv'. Qed. @@ -389,15 +361,13 @@ Proof. intros g g' Hg n n' Hn. rewrite Hn. destruct (n' << 2); auto with *. -apply succ_wd. -apply Hg. rewrite Hn; auto with *. +f_equiv. apply Hg. now f_equiv. Qed. Instance log_wd : Proper (N.eq==>N.eq) log. Proof. intros x x' Exx'. unfold log. -apply strong_rec_wd; auto with *. -apply log_prewd. +apply strong_rec_wd; f_equiv'. Qed. Lemma log_good_step : forall n h1 h2, @@ -408,9 +378,9 @@ Proof. intros n h1 h2 E. destruct (n<<2) as [ ]_eqn:H. auto with *. -apply succ_wd, E, half_decrease. -rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. -apply lt_succ_l; auto. +f_equiv. apply E, half_decrease. +rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. +order'. Qed. Hint Resolve log_good_step. @@ -441,14 +411,14 @@ intros n IH k Hk1 Hk2. destruct (lt_ge_cases k 2) as [LT|LE]. (* base *) rewrite log_init, pow_0 by auto. -rewrite <- le_succ_l in Hk2. +rewrite <- le_succ_l, <- one_succ in Hk2. le_elim Hk2. -rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto. +rewrite two_succ, <- nle_gt, le_succ_l in LT. destruct LT; auto. rewrite <- Hk2. rewrite half_1; auto using lt_0_1, le_refl. (* step *) rewrite log_step, pow_succ by auto. -rewrite le_succ_l in LE. +rewrite two_succ, le_succ_l in LE. destruct (IH (half k)) as (IH1,IH2). rewrite <- lt_succ_r. apply lt_le_trans with k; auto. now apply half_decrease. @@ -458,22 +428,13 @@ split. rewrite <- le_succ_l in IH1. apply mul_le_mono_l with (p:=2) in IH1. eapply lt_le_trans; eauto. -nzsimpl. +nzsimpl'. rewrite lt_succ_r. eapply le_trans; [ eapply half_lower_bound | ]. -nzsimpl; apply le_refl. +nzsimpl'; apply le_refl. eapply le_trans; [ | eapply half_upper_bound ]. apply mul_le_mono_l; auto. Qed. -(** Later: - -Theorem log_mul : forall n m, 0 < n -> 0 < m -> - log (n*m) == log n + log m. - -Theorem log_pow2 : forall n, log (2^^n) = n. - -*) - -End NdefOpsPropFunct. +End NdefOpsProp. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v index 171530f0..6db8e448 100644 --- a/theories/Numbers/Natural/Abstract/NDiv.v +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -1,40 +1,36 @@ (************************************************************************) (* 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 *) (************************************************************************) -(** Euclidean Division *) +Require Import NAxioms NSub NZDiv. -Require Import NAxioms NProperties NZDiv. +(** Properties of Euclidean Division *) -Module Type NDivSpecific (Import N : NAxiomsSig')(Import DM : DivMod' N). - Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. -End NDivSpecific. +Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N). -Module Type NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific. -Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. +(** We benefit from what already exists for NZ *) +Module Import Private_NZDiv := Nop <+ NZDivProp N N NP. -Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N). +Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. -(** We benefit from what already exists for NZ *) +(** Let's now state again theorems, but without useless hypothesis. *) - Module ND <: NZDiv N. - 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. split. apply le_0_l. apply mod_upper_bound. order. Qed. - End ND. - Module Import NZDivP := NZDivPropFunct N NP ND. +Lemma mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. +Proof. intros. apply mod_bound_pos; auto'. Qed. - Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. +(** Another formulation of the main equation *) -(** Let's now state again theorems, but without useless hypothesis. *) +Lemma mod_eq : + forall a b, b~=0 -> a mod b == a - b*(a/b). +Proof. +intros. +symmetry. apply add_sub_eq_l. symmetry. +now apply div_mod. +Qed. (** Uniqueness theorems *) @@ -51,6 +47,9 @@ Theorem mod_unique: forall a b q r, r<b -> a == b*q + r -> r == a mod b. Proof. intros. apply mod_unique with q; auto'. Qed. +Theorem div_unique_exact: forall a b q, b~=0 -> a == b*q -> q == a/b. +Proof. intros. apply div_unique_exact; auto'. Qed. + (** A division by itself returns 1 *) Lemma div_same : forall a, a~=0 -> a/a == 1. @@ -223,6 +222,10 @@ Lemma div_div : forall a b c, b~=0 -> c~=0 -> (a/b)/c == a/(b*c). Proof. intros. apply div_div; auto'. Qed. +Lemma mod_mul_r : forall a b c, b~=0 -> c~=0 -> + a mod (b*c) == a mod b + b*((a/b) mod c). +Proof. intros. apply mod_mul_r; auto'. Qed. + (** A last inequality: *) Theorem div_mul_le: @@ -235,5 +238,4 @@ Lemma mod_divides : forall a b, b~=0 -> (a mod b == 0 <-> exists c, a == b*c). Proof. intros. apply mod_divides; auto'. Qed. -End NDivPropFunct. - +End NDivProp. diff --git a/theories/Numbers/Natural/Abstract/NGcd.v b/theories/Numbers/Natural/Abstract/NGcd.v new file mode 100644 index 00000000..ece369d8 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NGcd.v @@ -0,0 +1,213 @@ +(************************************************************************) +(* 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 NAxioms NSub NZGcd. + +Module Type NGcdProp + (Import A : NAxiomsSig') + (Import B : NSubProp A). + + Include NZGcdProp A A B. + +(** Results concerning divisibility*) + +Definition divide_1_r n : (n | 1) -> n == 1 + := divide_1_r_nonneg n (le_0_l n). + +Definition divide_antisym n m : (n | m) -> (m | n) -> n == m + := divide_antisym_nonneg n m (le_0_l n) (le_0_l m). + +Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p). +Proof. + intros n m p (q,Hq) (r,Hr). + exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr. + now rewrite add_comm, add_sub. +Qed. + +Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p). +Proof. + intros n m p H H'. + destruct (le_ge_cases m p) as [LE|LE]. + apply sub_0_le in LE. rewrite LE. apply divide_0_r. + apply divide_add_cancel_r with p; trivial. + now rewrite add_comm, sub_add. +Qed. + +(** Properties of gcd *) + +Definition gcd_0_l n : gcd 0 n == n := gcd_0_l_nonneg n (le_0_l n). +Definition gcd_0_r n : gcd n 0 == n := gcd_0_r_nonneg n (le_0_l n). +Definition gcd_diag n : gcd n n == n := gcd_diag_nonneg n (le_0_l n). +Definition gcd_unique' n m p := gcd_unique n m p (le_0_l p). +Definition gcd_unique_alt' n m p := gcd_unique_alt n m p (le_0_l p). +Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n). + +Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m. +Proof. + intros. apply gcd_unique_alt'. + 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, n<=m -> gcd n (m-n) == gcd n m. +Proof. + intros n m H. symmetry. + rewrite <- (sub_add n m H) at 1. apply gcd_add_diag_r. +Qed. + +(** On natural numbers, we should use a particular form + for the Bezout identity, since we don't have full subtraction. *) + +Definition Bezout n m p := exists a b, a*n == p + b*m. + +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. + apply divide_add_cancel_r with (r*m). + now apply divide_mul_r. + rewrite add_comm, <- H. now apply divide_mul_r. +Qed. + +(** For strictly positive numbers, we have Bezout in the two directions. *) + +Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m -> + Bezout n m (gcd n m) /\ Bezout m n (gcd n m). +Proof. + intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. + pattern n. apply strong_right_induction with (z:=1); trivial. + unfold Bezout. solve_proper. + clear n Hn. intros n Hn IHn. + intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm. + pattern m. apply strong_right_induction with (z:=1); 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), (a' & b' & EQ')). + rewrite one_succ, le_succ_l. + apply lt_add_lt_sub_l; now nzsimpl. + apply sub_lt; order'. + split. + exists (a+b). exists b. + rewrite mul_add_distr_r, EQ, mul_sub_distr_l, <- add_assoc. + rewrite gcd_sub_diag_r by order. + rewrite sub_add. reflexivity. apply mul_le_mono_l; order. + exists a'. exists (a'+b'). + rewrite gcd_sub_diag_r in EQ' by order. + rewrite (add_comm a'), mul_add_distr_r, add_assoc, <- EQ'. + rewrite mul_sub_distr_l, sub_add. reflexivity. apply mul_le_mono_l; order. + (* n = m *) + rewrite EQ. rewrite gcd_diag. + split. + exists 1. exists 0. now nzsimpl. + exists 1. exists 0. now nzsimpl. + (* m < n *) + rewrite gcd_comm, and_comm. + apply IHn; trivial. + now rewrite <- le_succ_l, <- one_succ. +Qed. + +Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m). +Proof. + intros n m Hn. + destruct (eq_0_gt_0_cases m) as [EQ|LT]. + rewrite EQ, gcd_0_r. exists 1. exists 0. now nzsimpl. + now apply gcd_bezout_pos_pos. +Qed. + +(** For arbitrary natural numbers, we could only say that at least + one of the Bezout identities holds. *) + +Lemma gcd_bezout : forall n m, + Bezout n m (gcd n m) \/ Bezout m n (gcd n m). +Proof. + intros n m. + destruct (eq_0_gt_0_cases n) as [EQ|LT]. + right. rewrite EQ, gcd_0_l. exists 1. exists 0. now nzsimpl. + left. now apply gcd_bezout_pos. +Qed. + +Lemma gcd_mul_mono_l : + forall n m p, gcd (p * n) (p * m) == p * gcd n m. +Proof. + intros n m p. + apply gcd_unique'. + apply mul_divide_mono_l, gcd_divide_l. + apply mul_divide_mono_l, gcd_divide_r. + intros q H H'. + destruct (eq_0_gt_0_cases n) as [EQ|LT]. + rewrite EQ in *. now rewrite gcd_0_l. + destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial. + apply divide_add_cancel_r with (p*m*b). + now apply divide_mul_l. + rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ. + rewrite (mul_comm a), mul_assoc. + now apply divide_mul_l. +Qed. + +Lemma gcd_mul_mono_r : + forall n m p, gcd (n*p) (m*p) == gcd n m * p. +Proof. + intros. rewrite !(mul_comm _ p). apply gcd_mul_mono_l. +Qed. + +Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p). +Proof. + intros n m p H G. + destruct (eq_0_gt_0_cases n) as [EQ|LT]. + rewrite EQ in *. rewrite gcd_0_l in G. now rewrite <- (mul_1_l p), <- G. + destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial. + rewrite G in EQ. + apply divide_add_cancel_r with (m*p*b). + now apply divide_mul_l. + rewrite (mul_comm _ b), mul_assoc. rewrite <- (mul_1_l p) at 2. + rewrite <- mul_add_distr_r, add_comm, <- EQ. + now apply divide_mul_l, divide_factor_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). le_elim 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, <- Hq, <- Hr; order. + symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order. +Qed. + +(** TODO : relation between gcd and division and modulo *) + +(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *) + +End NGcdProp. diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index d484a625..bcf746a7 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.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,9 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NIso.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import NBase. -Module Homomorphism (N1 N2 : NAxiomsSig). +Module Homomorphism (N1 N2 : NAxiomsRecSig). Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity). @@ -25,11 +23,8 @@ Definition natural_isomorphism : N1.t -> N2.t := Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism. Proof. unfold natural_isomorphism. -intros n m Eqxy. -apply N1.recursion_wd. -reflexivity. -intros _ _ _ y' y'' H. now apply N2.succ_wd. -assumption. +repeat red; intros. f_equiv; trivial. +repeat red; intros. now f_equiv. Qed. Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero. @@ -42,7 +37,7 @@ Theorem natural_isomorphism_succ : Proof. unfold natural_isomorphism. intro n. rewrite N1.recursion_succ; auto with *. -repeat red; intros. apply N2.succ_wd; auto. +repeat red; intros. now f_equiv. Qed. Theorem hom_nat_iso : homomorphism natural_isomorphism. @@ -53,9 +48,9 @@ Qed. End Homomorphism. -Module Inverse (N1 N2 : NAxiomsSig). +Module Inverse (N1 N2 : NAxiomsRecSig). -Module Import NBasePropMod1 := NBasePropFunct N1. +Module Import NBasePropMod1 := NBaseProp N1. (* This makes the tactic induct available. Since it is taken from (NBasePropFunct NAxiomsMod1), it refers to induction on N1. *) @@ -76,7 +71,7 @@ Qed. End Inverse. -Module Isomorphism (N1 N2 : NAxiomsSig). +Module Isomorphism (N1 N2 : NAxiomsRecSig). Module Hom12 := Homomorphism N1 N2. Module Hom21 := Homomorphism N2 N1. diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v new file mode 100644 index 00000000..1e8e678c --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -0,0 +1,290 @@ +(************************************************************************) +(* 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 NAxioms NSub NDiv NGcd. + +(** * 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 gcd. +*) + +Module Type NLcmProp + (Import A : NAxiomsSig') + (Import B : NSubProp A) + (Import C : NDivProp A B) + (Import D : NGcdProp A B). + +(** Divibility and modulo *) + +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 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. + +(** Gcd of divided elements, for exact divisions *) + +Lemma gcd_div_factor : forall a b c, c~=0 -> (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; try order. + f_equiv; symmetry; apply div_exact; try order; + apply mod_divide; trivial; try order. +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. + +(** 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 (gcd_comm _ b). + rewrite <- (gcd_add_mult_diag_r b (a mod b) (a/b)). + now rewrite add_comm, mul_comm, <- div_mod. +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 + + Nota: [lcm 0 0] should be 0, which isn't garantee with the third + equation above. +*) + +Definition lcm a b := 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_factor_l. +Qed. + +Lemma divide_lcm_r : forall a b, (b | lcm a b). +Proof. + unfold lcm. intros a b. 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. + 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_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; trivial. + 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. apply le_0_l. + 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 : forall n, lcm 1 n == n. +Proof. + intros. apply lcm_unique; trivial using divide_1_l, le_0_l, divide_refl. +Qed. + +Lemma lcm_1_r : forall n, lcm n 1 == n. +Proof. + intros. now rewrite lcm_comm, lcm_1_l. +Qed. + +Lemma lcm_diag : forall n, lcm n n == n. +Proof. + intros. apply lcm_unique; trivial using divide_refl, le_0_l. +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, (n|m) -> lcm n m == m. +Proof. + intros n m H. apply lcm_unique_alt; trivial using le_0_l. + intros q. split. split; trivial. now transitivity m. + now destruct 1. +Qed. + +Lemma divide_lcm_iff : forall n m, (n|m) <-> lcm n m == m. +Proof. + intros n m. split. now apply divide_lcm_eq_r. + intros EQ. rewrite <- EQ. apply divide_lcm_l. +Qed. + +Lemma lcm_mul_mono_l : + forall n m p, lcm (p * n) (p * m) == p * lcm n m. +Proof. + intros n m p. + destruct (eq_decidable p 0) as [Hp|Hp]. + rewrite Hp. nzsimpl. rewrite lcm_0_l. 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 mul_assoc. f_equiv. + now rewrite div_mul_cancel_l. +Qed. + +Lemma lcm_mul_mono_r : + forall n m p, lcm (n * p) (m * p) == lcm n m * p. +Proof. + intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm. +Qed. + +Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 -> + (gcd n m == 1 <-> lcm n m == n*m). +Proof. + intros n m Hn Hm. split; intros H. + unfold lcm. rewrite H. now rewrite div_1_r. + unfold lcm in *. + apply mul_cancel_l in H; trivial. + assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order). + assert (H' := gcd_divide_r n m). + apply mod_divide in H'; trivial. apply div_exact in H'; trivial. + rewrite H in H'. + rewrite <- (mul_1_l m) in H' at 1. + now apply mul_cancel_r in H'. +Qed. + +End NLcmProp. diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v new file mode 100644 index 00000000..74827c6e --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NLog.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(** Base-2 Logarithm Properties *) + +Require Import NAxioms NSub NPow NParity NZLog. + +Module Type NLog2Prop + (A : NAxiomsSig) + (B : NSubProp A) + (C : NParityProp A B) + (D : NPowProp A B C). + + (** For the moment we simply reuse NZ properties *) + + Include NZLog2Prop A A A B D.Private_NZPow. + Include NZLog2UpProp A A A B D.Private_NZPow. +End NLog2Prop. diff --git a/theories/Numbers/Natural/Abstract/NMaxMin.v b/theories/Numbers/Natural/Abstract/NMaxMin.v new file mode 100644 index 00000000..cdff6dbc --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMaxMin.v @@ -0,0 +1,135 @@ +(************************************************************************) +(* 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 NAxioms NSub GenericMinMax. + +(** * Properties of minimum and maximum specific to natural numbers *) + +Module Type NMaxMinProp (Import N : NAxiomsMiniSig'). +Include NSubProp N. + +(** Zero *) + +Lemma max_0_l : forall n, max 0 n == n. +Proof. + intros. apply max_r. apply le_0_l. +Qed. + +Lemma max_0_r : forall n, max n 0 == n. +Proof. + intros. apply max_l. apply le_0_l. +Qed. + +Lemma min_0_l : forall n, min 0 n == 0. +Proof. + intros. apply min_l. apply le_0_l. +Qed. + +Lemma min_0_r : forall n, min n 0 == 0. +Proof. + intros. apply min_r. apply le_0_l. +Qed. + +(** 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. + +(** 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. + +(** Mul *) + +Lemma mul_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]; try order; now apply mul_le_mono_l. +Qed. + +Lemma mul_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 mul_le_mono_r. +Qed. + +Lemma mul_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]; try order; now apply mul_le_mono_l. +Qed. + +Lemma mul_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 mul_le_mono_r. +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 apply sub_le_mono_l. + rewrite min_r by trivial. apply max_r. now apply 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 apply sub_le_mono_l. + rewrite max_l by trivial. apply min_l. now apply 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. + +End NMaxMinProp. diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index bdd4b674..1d6e8ba0 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.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: NMulOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NAddOrder. -Module NMulOrderPropFunct (Import N : NAxiomsSig'). -Include NAddOrderPropFunct N. +Module NMulOrderProp (Import N : NAxiomsMiniSig'). +Include NAddOrderProp N. (** Theorems that are either not valid on Z or have different proofs on N and Z *) @@ -55,7 +53,7 @@ Qed. Theorem lt_0_mul' : forall n m, n * m > 0 <-> n > 0 /\ m > 0. Proof. intros n m; split; [intro H | intros [H1 H2]]. -apply -> lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. +apply lt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. now apply mul_pos_pos. Qed. @@ -67,14 +65,18 @@ Proof. intros n m. split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]]. -apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ. +apply lt_1_r in H1. rewrite H1, mul_0_l in H. order'. rewrite H1, mul_1_l in H; now split. destruct (eq_0_gt_0_cases m) as [H2 | H2]. -rewrite H2, mul_0_r in H; false_hyp H neq_0_succ. -apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. +rewrite H2, mul_0_r in H. order'. +apply (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1. assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. -End NMulOrderPropFunct. +(** Alternative name : *) + +Definition mul_eq_1 := eq_mul_1. + +End NMulOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 17dd3466..8bba7d72 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.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,18 +8,16 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NAdd. -Module NOrderPropFunct (Import N : NAxiomsSig'). -Include NAddPropFunct N. +Module NOrderProp (Import N : NAxiomsMiniSig'). +Include NAddProp N. (* Theorems that are true for natural numbers but not for integers *) Theorem lt_wf_0 : well_founded lt. Proof. -setoid_replace lt with (fun n m => 0 <= n /\ n < m). +setoid_replace lt with (fun n m => 0 <= n < m). apply lt_wf. intros x y; split. intro H; split; [apply le_0_l | assumption]. now intros [_ H]. @@ -29,12 +27,12 @@ Defined. Theorem nlt_0_r : forall n, ~ n < 0. Proof. -intro n; apply -> le_ngt. apply le_0_l. +intro n; apply le_ngt. apply le_0_l. Qed. Theorem nle_succ_0 : forall n, ~ (S n <= 0). Proof. -intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r. +intros n H; apply le_succ_l in H; false_hyp H nlt_0_r. Qed. Theorem le_0_r : forall n, n <= 0 <-> n == 0. @@ -65,6 +63,7 @@ Qed. Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. +setoid_rewrite one_succ. induct n. now left. cases n. intros; right; now left. intros n IH. destruct IH as [H | [H | H]]. @@ -75,6 +74,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. +setoid_rewrite one_succ. cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. @@ -83,6 +83,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. +setoid_rewrite one_succ. cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. @@ -117,9 +118,9 @@ Proof. intros Base Step; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply eq_le_incl. -intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. +intros k H1 H2. apply le_succ_l in H1. apply lt_le_incl in H1. auto. Qed. Theorem lt_ind_rel : @@ -131,7 +132,7 @@ intros Base Step; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. intros n IH m H. elim H using lt_ind. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply lt_succ_diag_r. intros k H1 H2. apply lt_succ_l in H1. auto. Qed. @@ -175,7 +176,7 @@ Theorem lt_le_pred : forall n m, n < m -> n <= P m. Proof. intro n; cases m. intro H; false_hyp H nlt_0_r. -intros m IH. rewrite pred_succ; now apply -> lt_succ_r. +intros m IH. rewrite pred_succ; now apply lt_succ_r. Qed. Theorem lt_pred_le : forall n m, P n < m -> n <= m. @@ -183,7 +184,7 @@ Theorem lt_pred_le : forall n m, P n < m -> n <= m. Proof. intros n m; cases n. rewrite pred_0; intro H; now apply lt_le_incl. -intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l. +intros n IH. rewrite pred_succ in IH. now apply le_succ_l. Qed. Theorem lt_pred_lt : forall n m, n < P m -> n < m. @@ -200,7 +201,7 @@ Theorem pred_le_mono : forall n m, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) Proof. intros n m H; elim H using le_ind_rel. -solve_relation_wd. +solve_proper. intro; rewrite pred_0; apply le_0_l. intros p q H1 _; now do 2 rewrite pred_succ. Qed. @@ -208,12 +209,12 @@ Qed. Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m). Proof. intros n m H1; split; intro H2. -assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. +assert (m ~= 0). apply neq_0_lt_0. now apply lt_lt_0 with n. now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; -[apply <- succ_lt_mono | | |]. -assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). +[apply succ_lt_mono | | |]. +assert (m ~= 0). apply neq_0_lt_0. apply lt_lt_0 with (P n). apply lt_le_trans with (P m). assumption. apply le_pred_l. -apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. +apply succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. Qed. Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m. @@ -224,13 +225,13 @@ Qed. Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply lt_le_pred. now apply -> le_succ_l. +intros n m H. apply lt_le_pred. now apply le_succ_l. Qed. Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply <- lt_succ_r. now apply lt_pred_le. +intros n m H. apply lt_succ_r. now apply lt_pred_le. Qed. Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m. @@ -240,5 +241,5 @@ rewrite pred_0. split; intro H; apply le_0_l. intro n. rewrite pred_succ. apply succ_le_mono. Qed. -End NOrderPropFunct. +End NOrderProp. diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v new file mode 100644 index 00000000..6a1e20ce --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NParity.v @@ -0,0 +1,63 @@ +(************************************************************************) +(* 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 NSub NZParity. + +(** Some additionnal properties of [even], [odd]. *) + +Module Type NParityProp (Import N : NAxiomsSig')(Import NP : NSubProp N). + +Include NZParityProp N N NP. + +Lemma odd_pred : forall n, n~=0 -> odd (P n) = even n. +Proof. + intros. rewrite <- (succ_pred n) at 2 by trivial. + symmetry. apply even_succ. +Qed. + +Lemma even_pred : forall n, n~=0 -> even (P n) = odd n. +Proof. + intros. rewrite <- (succ_pred n) at 2 by trivial. + symmetry. apply odd_succ. +Qed. + +Lemma even_sub : forall n m, m<=n -> even (n-m) = Bool.eqb (even n) (even m). +Proof. + intros. + case_eq (even n); case_eq (even m); + rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; + intros (m',Hm) (n',Hn). + exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm. + exists (n'-m'-1). + rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r. + rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr. + symmetry. apply sub_add. + apply le_add_le_sub_l. + rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1. + rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'. + rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r. + destruct (le_gt_cases n' m') as [LE|GT]; trivial. + generalize (double_below _ _ LE). order. + exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm. + apply add_sub_swap. + apply mul_le_mono_pos_l; try order'. + destruct (le_gt_cases m' n') as [LE|GT]; trivial. + generalize (double_above _ _ GT). order. + exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l. + rewrite sub_add_distr. rewrite add_sub_swap. apply add_sub. + apply succ_le_mono. + rewrite add_1_r in Hm,Hn. order. +Qed. + +Lemma odd_sub : forall n m, m<=n -> odd (n-m) = xorb (odd n) (odd m). +Proof. + intros. rewrite <- !negb_even. rewrite even_sub by trivial. + now destruct (even n), (even m). +Qed. + +End NParityProp. diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v new file mode 100644 index 00000000..07aee9c6 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NPow.v @@ -0,0 +1,160 @@ +(************************************************************************) +(* 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 NAxioms NSub NParity NZPow. + +(** Derived properties of power, specialized on natural numbers *) + +Module Type NPowProp + (Import A : NAxiomsSig') + (Import B : NSubProp A) + (Import C : NParityProp A B). + + Module Import Private_NZPow := Nop <+ NZPowProp A A B. + +Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l. +Ltac wrap l := intros; apply l; auto'. + +Lemma pow_succ_r' : forall a b, a^(S b) == a * a^b. +Proof. wrap pow_succ_r. Qed. + +(** Power and basic constants *) + +Lemma pow_0_l : forall a, a~=0 -> 0^a == 0. +Proof. wrap pow_0_l. Qed. + +Definition pow_1_r : forall a, a^1 == a + := pow_1_r. + +Lemma pow_1_l : forall a, 1^a == 1. +Proof. wrap pow_1_l. Qed. + +Definition pow_2_r : forall a, a^2 == a*a + := pow_2_r. + +(** Power and addition, multiplication *) + +Lemma pow_add_r : forall a b c, a^(b+c) == a^b * a^c. +Proof. wrap pow_add_r. Qed. + +Lemma pow_mul_l : forall a b c, (a*b)^c == a^c * b^c. +Proof. wrap pow_mul_l. Qed. + +Lemma pow_mul_r : forall a b c, a^(b*c) == (a^b)^c. +Proof. wrap pow_mul_r. Qed. + +(** Power and nullity *) + +Lemma pow_eq_0 : forall a b, b~=0 -> a^b == 0 -> a == 0. +Proof. intros. apply (pow_eq_0 a b); trivial. auto'. Qed. + +Lemma pow_nonzero : forall a b, a~=0 -> a^b ~= 0. +Proof. wrap pow_nonzero. Qed. + +Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b~=0 /\ a==0. +Proof. + intros a b. split. + rewrite pow_eq_0_iff. intros [H |[H H']]. + generalize (le_0_l b); order. split; order. + intros (Hb,Ha). rewrite Ha. now apply pow_0_l'. +Qed. + +(** Monotonicity *) + +Lemma pow_lt_mono_l : forall a b c, c~=0 -> a<b -> a^c < b^c. +Proof. wrap pow_lt_mono_l. Qed. + +Lemma pow_le_mono_l : forall a b c, a<=b -> a^c <= b^c. +Proof. wrap pow_le_mono_l. Qed. + +Lemma pow_gt_1 : forall a b, 1<a -> b~=0 -> 1<a^b. +Proof. wrap pow_gt_1. Qed. + +Lemma pow_lt_mono_r : forall a b c, 1<a -> b<c -> a^b < a^c. +Proof. wrap pow_lt_mono_r. Qed. + +(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *) + +Lemma pow_le_mono_r : forall a b c, a~=0 -> b<=c -> a^b <= a^c. +Proof. wrap pow_le_mono_r. Qed. + +Lemma pow_le_mono : forall a b c d, a~=0 -> a<=c -> b<=d -> + a^b <= c^d. +Proof. wrap pow_le_mono. Qed. + +Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> + a^b < c^d + := pow_lt_mono. + +(** Injectivity *) + +Lemma pow_inj_l : forall a b c, c~=0 -> a^c == b^c -> a == b. +Proof. intros; eapply pow_inj_l; eauto; auto'. Qed. + +Lemma pow_inj_r : forall a b c, 1<a -> a^b == a^c -> b == c. +Proof. intros; eapply pow_inj_r; eauto; auto'. Qed. + +(** Monotonicity results, both ways *) + +Lemma pow_lt_mono_l_iff : forall a b c, c~=0 -> + (a<b <-> a^c < b^c). +Proof. wrap pow_lt_mono_l_iff. Qed. + +Lemma pow_le_mono_l_iff : forall a b c, c~=0 -> + (a<=b <-> a^c <= b^c). +Proof. wrap pow_le_mono_l_iff. Qed. + +Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> + (b<c <-> a^b < a^c). +Proof. wrap pow_lt_mono_r_iff. Qed. + +Lemma pow_le_mono_r_iff : forall a b c, 1<a -> + (b<=c <-> a^b <= a^c). +Proof. wrap pow_le_mono_r_iff. Qed. + +(** For any a>1, the a^x function is above the identity function *) + +Lemma pow_gt_lin_r : forall a b, 1<a -> b < a^b. +Proof. wrap pow_gt_lin_r. Qed. + +(** Someday, we should say something about the full Newton formula. + In the meantime, we can at least provide some inequalities about + (a+b)^c. +*) + +Lemma pow_add_lower : forall a b c, c~=0 -> + a^c + b^c <= (a+b)^c. +Proof. wrap pow_add_lower. Qed. + +(** This upper bound can also be seen as a convexity proof for x^c : + image of (a+b)/2 is below the middle of the images of a and b +*) + +Lemma pow_add_upper : forall a b c, c~=0 -> + (a+b)^c <= 2^(pred c) * (a^c + b^c). +Proof. wrap pow_add_upper. Qed. + +(** Power and parity *) + +Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a. +Proof. + intros a b Hb. rewrite neq_0_lt_0 in Hb. + apply lt_ind with (4:=Hb). solve_proper. + now nzsimpl. + clear b Hb. intros b Hb IH. + rewrite pow_succ_r', even_mul, IH. now destruct (even a). +Qed. + +Lemma odd_pow : forall a b, b~=0 -> odd (a^b) = odd a. +Proof. + intros. now rewrite <- !negb_even, even_pow. +Qed. + +End NPowProp. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index c9e05113..1edb6b51 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -1,22 +1,17 @@ (************************************************************************) (* 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: NProperties.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Export NAxioms. +Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits. -Require Export NAxioms NSub. +(** This functor summarizes all known facts about N. *) -(** This functor summarizes all known facts about N. - For the moment it is only an alias to [NSubPropFunct], which - subsumes all others. -*) - -Module Type NPropSig := NSubPropFunct. - -Module NPropFunct (N:NAxiomsSig) <: NPropSig N. - Include NPropSig N. -End NPropFunct. +Module Type NProp (N:NAxiomsSig) := + NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N + <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N + <+ NBitsProp N. diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v new file mode 100644 index 00000000..34b7d011 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSqrt.v @@ -0,0 +1,75 @@ +(************************************************************************) +(* 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 Square Root Function *) + +Require Import NAxioms NSub NZSqrt. + +Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A). + + Module Import Private_NZSqrt := Nop <+ NZSqrtProp A A B. + + Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l. + Ltac wrap l := intros; apply l; auto'. + + (** We redefine NZSqrt's results, without the non-negative hyps *) + +Lemma sqrt_spec' : forall a, √a*√a <= a < S (√a) * S (√a). +Proof. wrap sqrt_spec. Qed. + +Definition sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b + := sqrt_unique. + +Lemma sqrt_square : forall a, √(a*a) == a. +Proof. wrap sqrt_square. Qed. + +Definition sqrt_le_mono : forall a b, a<=b -> √a <= √b + := sqrt_le_mono. + +Definition sqrt_lt_cancel : forall a b, √a < √b -> a < b + := sqrt_lt_cancel. + +Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a. +Proof. wrap sqrt_le_square. Qed. + +Lemma sqrt_lt_square : forall a b, a<b*b <-> √a < b. +Proof. wrap sqrt_lt_square. Qed. + +Definition sqrt_0 := sqrt_0. +Definition sqrt_1 := sqrt_1. +Definition sqrt_2 := sqrt_2. + +Definition sqrt_lt_lin : forall a, 1<a -> √a<a + := sqrt_lt_lin. + +Lemma sqrt_le_lin : forall a, √a<=a. +Proof. wrap sqrt_le_lin. Qed. + +Definition sqrt_mul_below : forall a b, √a * √b <= √(a*b) + := sqrt_mul_below. + +Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b). +Proof. wrap sqrt_mul_above. Qed. + +Lemma sqrt_succ_le : forall a, √(S a) <= S (√a). +Proof. wrap sqrt_succ_le. Qed. + +Lemma sqrt_succ_or : forall a, √(S a) == S (√a) \/ √(S a) == √a. +Proof. wrap sqrt_succ_or. Qed. + +Definition sqrt_add_le : forall a b, √(a+b) <= √a + √b + := sqrt_add_le. + +Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)). +Proof. wrap add_sqrt_le. Qed. + +(** For the moment, we include stuff about [sqrt_up] with patching them. *) + +Include NZSqrtUpProp A A B Private_NZSqrt. + +End NSqrtProp. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index d9a2427d..607746d5 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.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,15 +8,15 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NStrongRec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) Require Export NSub. -Module NStrongRecPropFunct (Import N : NAxiomsSig'). -Include NSubPropFunct N. +Ltac f_equiv' := repeat progress (f_equiv; try intros ? ? ?; auto). + +Module NStrongRecProp (Import N : NAxiomsRecSig'). +Include NSubProp N. Section StrongRecursion. @@ -51,30 +51,18 @@ Proof. reflexivity. Qed. -(** We need a result similar to [f_equal], but for setoid equalities. *) -Lemma f_equiv : forall f g x y, - (N.eq==>Aeq)%signature f g -> N.eq x y -> Aeq (f x) (g y). -Proof. -auto. -Qed. - Instance strong_rec0_wd : Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq) strong_rec0. Proof. -unfold strong_rec0. -repeat red; intros. -apply f_equiv; auto. -apply recursion_wd; try red; auto. +unfold strong_rec0; f_equiv'. Qed. Instance strong_rec_wd : Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec. Proof. intros a a' Eaa' f f' Eff' n n' Enn'. -rewrite !strong_rec_alt. -apply strong_rec0_wd; auto. -now rewrite Enn'. +rewrite !strong_rec_alt; f_equiv'. Qed. Section FixPoint. @@ -92,18 +80,16 @@ Lemma strong_rec0_succ : forall a n m, Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m). Proof. intros. unfold strong_rec0. -apply f_equiv; auto with *. -rewrite recursion_succ; try (repeat red; auto with *; fail). -apply f_wd. -apply recursion_wd; try red; auto with *. +f_equiv. +rewrite recursion_succ; f_equiv'. +reflexivity. Qed. Lemma strong_rec_0 : forall a, Aeq (strong_rec a f 0) (f (fun _ => a) 0). Proof. -intros. rewrite strong_rec_alt, strong_rec0_succ. -apply f_wd; auto with *. -red; intros; rewrite strong_rec0_0; auto with *. +intros. rewrite strong_rec_alt, strong_rec0_succ; f_equiv'. +rewrite strong_rec0_0. reflexivity. Qed. (* We need an assumption saying that for every n, the step function (f h n) @@ -158,7 +144,7 @@ intros. transitivity (f (fun n => strong_rec0 a f (S n) n) n). rewrite strong_rec_alt. apply strong_rec0_fixpoint. -apply f_wd; auto with *. +f_equiv. intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *. Qed. @@ -204,7 +190,7 @@ Qed. End FixPoint. End StrongRecursion. -Implicit Arguments strong_rec [A]. +Arguments strong_rec [A] a f n. -End NStrongRecPropFunct. +End NStrongRecProp. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index c0be3114..d7143c67 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.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: NSub.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NMulOrder. -Module Type NSubPropFunct (Import N : NAxiomsSig'). -Include NMulOrderPropFunct N. +Module Type NSubProp (Import N : NAxiomsMiniSig'). +Include NMulOrderProp N. Theorem sub_0_l : forall n, 0 - n == 0. Proof. @@ -37,7 +35,7 @@ Qed. Theorem sub_gt : forall n m, n > m -> n - m ~= 0. Proof. intros n m H; elim H using lt_ind_rel; clear n m H. -solve_relation_wd. +solve_proper. intro; rewrite sub_0_r; apply neq_succ_0. intros; now rewrite sub_succ. Qed. @@ -47,8 +45,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite sub_0_r. intros p IH H. do 2 rewrite sub_succ_r. -rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). -rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +rewrite <- IH by (apply lt_le_incl; now apply le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply le_succ_l). reflexivity. Qed. @@ -205,6 +203,26 @@ Proof. intros n m p. rewrite add_comm; apply lt_add_lt_sub_r. Qed. +Theorem sub_lt : forall n m, m <= n -> 0 < m -> n - m < n. +Proof. +intros n m LE LT. +assert (LE' := le_sub_l n m). rewrite lt_eq_cases in LE'. +destruct LE' as [LT'|EQ]. assumption. +apply add_sub_eq_nz in EQ; [|order]. +rewrite (add_lt_mono_r _ _ n), add_0_l in LT. order. +Qed. + +Lemma sub_le_mono_r : forall n m p, n <= m -> n-p <= m-p. +Proof. + intros. rewrite le_sub_le_add_r. transitivity m. assumption. apply sub_add_le. +Qed. + +Lemma sub_le_mono_l : forall n m p, n <= m -> p-m <= p-n. +Proof. + intros. rewrite le_sub_le_add_r. + transitivity (p-n+n); [ apply sub_add_le | now apply add_le_mono_l]. +Qed. + (** Sub and mul *) Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. @@ -224,10 +242,10 @@ intros n IH. destruct (le_gt_cases m n) as [H | H]. rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. -now apply <- add_cancel_l. -assert (H1 : S n <= m); [now apply <- le_succ_l |]. -setoid_replace (S n - m) with 0 by now apply <- sub_0_le. -setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +now apply add_cancel_l. +assert (H1 : S n <= m); [now apply le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r). apply mul_0_l. Qed. @@ -298,5 +316,5 @@ Theorem add_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). Proof. exact le_alt_dichotomy. Qed. -End NSubPropFunct. +End NSubProp. |