diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 109 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAddOrder.v | 88 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 58 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 180 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 477 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDiv.v | 239 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 84 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMul.v | 87 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 101 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 390 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NProperties.v | 22 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 231 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 196 |
13 files changed, 1101 insertions, 1161 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v index 91ae5b70..9f0b54a6 100644 --- a/theories/Numbers/Natural/Abstract/NAdd.v +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -8,74 +8,30 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NAdd.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) Require Export NBase. -Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NBasePropMod := NBasePropFunct NAxiomsMod. +Module NAddPropFunct (Import N : NAxiomsSig'). +Include NBasePropFunct N. -Open Local Scope NatScope. +(** 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 *) -Theorem add_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2. -Proof NZadd_wd. - -Theorem add_0_l : forall n : N, 0 + n == n. -Proof NZadd_0_l. - -Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m). -Proof NZadd_succ_l. - -(** Theorems that are valid for both natural numbers and integers *) - -Theorem add_0_r : forall n : N, n + 0 == n. -Proof NZadd_0_r. - -Theorem add_succ_r : forall n m : N, n + S m == S (n + m). -Proof NZadd_succ_r. - -Theorem add_comm : forall n m : N, n + m == m + n. -Proof NZadd_comm. - -Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p. -Proof NZadd_assoc. - -Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q). -Proof NZadd_shuffle1. - -Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p). -Proof NZadd_shuffle2. - -Theorem add_1_l : forall n : N, 1 + n == S n. -Proof NZadd_1_l. - -Theorem add_1_r : forall n : N, n + 1 == S n. -Proof NZadd_1_r. - -Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m. -Proof NZadd_cancel_l. - -Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m. -Proof NZadd_cancel_r. - -(* Theorems that are valid for natural numbers but cannot be proved for Z *) - -Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. +Theorem eq_add_0 : forall n m, n + m == 0 <-> n == 0 /\ m == 0. Proof. intros n m; induct n. -(* The next command does not work with the axiom add_0_l from NAddSig *) -rewrite add_0_l. intuition reflexivity. -intros n IH. rewrite add_succ_l. -setoid_replace (S (n + m) == 0) with False using relation iff by +nzsimpl; intuition. +intros n IH. nzsimpl. +setoid_replace (S (n + m) == 0) with False by (apply -> neg_false; apply neq_succ_0). -setoid_replace (S n == 0) with False using relation iff by +setoid_replace (S n == 0) with False by (apply -> neg_false; apply neq_succ_0). tauto. Qed. Theorem eq_add_succ : - forall n m : N, (exists p : N, n + m == S p) <-> - (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). + forall n m, (exists p, n + m == S p) <-> + (exists n', n == S n') \/ (exists m', m == S m'). Proof. intros n m; cases n. split; intro H. @@ -88,11 +44,11 @@ left; now exists n. exists (n + m); now rewrite add_succ_l. Qed. -Theorem eq_add_1 : forall n m : N, +Theorem eq_add_1 : forall n m, n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. intros n m H. -assert (H1 : exists p : N, n + m == S p) by now exists 0. +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]]. 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. @@ -100,7 +56,7 @@ 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. Qed. -Theorem succ_add_discr : forall n m : N, m ~= S (n + m). +Theorem succ_add_discr : forall n m, m ~= S (n + m). Proof. intro n; induct m. apply neq_sym. apply neq_succ_0. @@ -108,49 +64,18 @@ intros m IH H. apply succ_inj in H. rewrite add_succ_r in H. unfold not in IH; now apply IH. Qed. -Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m). +Theorem add_pred_l : forall n m, n ~= 0 -> P n + m == P (n + m). Proof. intros n m; cases n. intro H; now elim H. intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ. Qed. -Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m). +Theorem add_pred_r : forall n m, m ~= 0 -> n + P m == P (n + m). Proof. intros n m H; rewrite (add_comm n (P m)); rewrite (add_comm n m); now apply add_pred_l. Qed. -(* One could define n <= m as exists p : N, p + n == m. Then we have -dichotomy: - -forall n m : N, n <= m \/ m <= n, - -i.e., - -forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) - -We will need (1) in the proof of induction principle for integers -constructed as pairs of natural numbers. The formula (1) can be proved -using properties of order and truncated subtraction. Thus, p would be -m - n or n - m and (1) would hold by theorem sub_add from Sub.v -depending on whether n <= m or m <= n. However, in proving induction -for integers constructed from natural numbers we do not need to -require implementations of order and sub; it is enough to prove (1) -here. *) - -Theorem add_dichotomy : - forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n). -Proof. -intros n m; induct n. -left; exists m; apply add_0_r. -intros n IH. -destruct IH as [[p H] | [p H]]. -destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. -rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l. -left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. -right; exists (S p). rewrite add_succ_l; now rewrite H. -Qed. - End NAddPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAddOrder.v b/theories/Numbers/Natural/Abstract/NAddOrder.v index 7024fd00..0ce04e54 100644 --- a/theories/Numbers/Natural/Abstract/NAddOrder.v +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -8,107 +8,41 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) Require Export NOrder. -Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module NAddOrderPropFunct (Import N : NAxiomsSig'). +Include NOrderPropFunct N. -Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. -Proof NZadd_lt_mono_l. +(** Theorems true for natural numbers, not for integers *) -Theorem add_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. -Proof NZadd_lt_mono_r. - -Theorem add_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. -Proof NZadd_lt_mono. - -Theorem add_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. -Proof NZadd_le_mono_l. - -Theorem add_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. -Proof NZadd_le_mono_r. - -Theorem add_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. -Proof NZadd_le_mono. - -Theorem add_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. -Proof NZadd_lt_le_mono. - -Theorem add_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. -Proof NZadd_le_lt_mono. - -Theorem add_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. -Proof NZadd_pos_pos. - -Theorem lt_add_pos_l : forall n m : N, 0 < n -> m < n + m. -Proof NZlt_add_pos_l. - -Theorem lt_add_pos_r : forall n m : N, 0 < n -> m < m + n. -Proof NZlt_add_pos_r. - -Theorem le_lt_add_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. -Proof NZle_lt_add_lt. - -Theorem lt_le_add_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. -Proof NZlt_le_add_lt. - -Theorem le_le_add_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. -Proof NZle_le_add_le. - -Theorem add_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. -Proof NZadd_lt_cases. - -Theorem add_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. -Proof NZadd_le_cases. - -Theorem add_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. -Proof NZadd_pos_cases. - -(* Theorems true for natural numbers *) - -Theorem le_add_r : forall n m : N, n <= n + m. +Theorem le_add_r : forall n m, n <= n + m. Proof. intro n; induct m. rewrite add_0_r; now apply eq_le_incl. intros m IH. rewrite add_succ_r; now apply le_le_succ_r. Qed. -Theorem lt_lt_add_r : forall n m p : N, n < m -> n < m + p. +Theorem lt_lt_add_r : forall n m p, n < m -> n < m + p. Proof. intros n m p H; rewrite <- (add_0_r n). apply add_lt_le_mono; [assumption | apply le_0_l]. Qed. -Theorem lt_lt_add_l : forall n m p : N, n < m -> n < p + m. +Theorem lt_lt_add_l : forall n m p, n < m -> n < p + m. Proof. intros n m p; rewrite add_comm; apply lt_lt_add_r. Qed. -Theorem add_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Theorem add_pos_l : forall n m, 0 < n -> 0 < n + m. Proof. -intros; apply NZadd_pos_nonneg. assumption. apply le_0_l. +intros; apply add_pos_nonneg. assumption. apply le_0_l. Qed. -Theorem add_pos_r : forall n m : N, 0 < m -> 0 < n + m. -Proof. -intros; apply NZadd_nonneg_pos. apply le_0_l. assumption. -Qed. - -(* The following property is used to prove the correctness of the -definition of order on integers constructed from pairs of natural numbers *) - -Theorem add_lt_repl_pair : forall n m n' m' u v : N, - n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. +Theorem add_pos_r : forall n m, 0 < m -> 0 < n + m. Proof. -intros n m n' m' u v H1 H2. -symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl. -pose proof (add_lt_le_mono _ _ _ _ H1 H3) as H4. -rewrite (add_shuffle2 n u), (add_shuffle1 m v), (add_comm m n) in H4. -do 2 rewrite <- add_assoc in H4. do 2 apply <- add_lt_mono_l in H4. -now rewrite (add_comm n' u), (add_comm m' v). +intros; apply add_nonneg_pos. apply le_0_l. assumption. Qed. End NAddOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index 750cc977..42016ab1 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,64 +8,32 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) Require Export NZAxioms. Set Implicit Arguments. -Module Type NAxiomsSig. -Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. +Module Type NAxioms (Import NZ : NZDomainSig'). -Delimit Scope NatScope with Nat. -Notation N := NZ. -Notation Neq := NZeq. -Notation N0 := NZ0. -Notation N1 := (NZsucc NZ0). -Notation S := NZsucc. -Notation P := NZpred. -Notation add := NZadd. -Notation mul := NZmul. -Notation sub := NZsub. -Notation lt := NZlt. -Notation le := NZle. -Notation min := NZmin. -Notation max := NZmax. -Notation "x == y" := (Neq x y) (at level 70) : NatScope. -Notation "x ~= y" := (~ Neq x y) (at level 70) : NatScope. -Notation "0" := NZ0 : NatScope. -Notation "1" := (NZsucc NZ0) : NatScope. -Notation "x + y" := (NZadd x y) : NatScope. -Notation "x - y" := (NZsub x y) : NatScope. -Notation "x * y" := (NZmul x y) : NatScope. -Notation "x < y" := (NZlt x y) : NatScope. -Notation "x <= y" := (NZle x y) : NatScope. -Notation "x > y" := (NZlt y x) (only parsing) : NatScope. -Notation "x >= y" := (NZle y x) (only parsing) : NatScope. - -Open Local Scope NatScope. +Axiom pred_0 : P 0 == 0. -Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> A. +Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A. Implicit Arguments recursion [A]. -Axiom pred_0 : P 0 == 0. - -Axiom recursion_wd : forall (A : Type) (Aeq : relation A), - forall a a' : A, Aeq a a' -> - forall f f' : N -> A -> A, fun2_eq Neq Aeq Aeq f f' -> - forall x x' : N, x == x' -> - Aeq (recursion a f x) (recursion a' f' x'). +Declare Instance recursion_wd (A : Type) (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). Axiom recursion_0 : - forall (A : Type) (a : A) (f : N -> A -> A), recursion a f 0 = a. + forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a. Axiom recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : N -> A -> A), - Aeq a a -> fun2_wd Neq Aeq Aeq f -> - forall n : N, Aeq (recursion a f (S n)) (f n (recursion a f n)). + forall (A : Type) (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)). -(*Axiom dep_rec : - forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*) +End NAxioms. -End NAxiomsSig. +Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms. +Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms. diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index 85e2c2ab..842f4bcf 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -8,135 +8,78 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NBase.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) Require Export Decidable. Require Export NAxioms. -Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *) +Require Import NZProperties. -Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). +Module NBasePropFunct (Import N : NAxiomsSig'). +(** First, we import all known facts about both natural numbers and integers. *) +Include NZPropFunct N. -Open Local Scope NatScope. - -(* We call the last property functor on NZ, which includes all the previous -ones, to get all properties of NZ at once. This way we will include them -only one time. *) - -Module Export NZMulOrderMod := NZMulOrderPropFunct NZOrdAxiomsMod. - -(* Here we probably need to re-prove all axioms declared in NAxioms.v to -make sure that the definitions like N, S and add are unfolded in them, -since unfolding is done only inside a functor. In fact, we'll do it in the -files that prove the corresponding properties. In those files, we will also -rename properties proved in NZ files by removing NZ from their names. In -this way, one only has to consult, for example, NAdd.v to see all -available properties for add, i.e., one does not have to go to NAxioms.v -for axioms and NZAdd.v for theorems. *) - -Theorem succ_wd : forall n1 n2 : N, n1 == n2 -> S n1 == S n2. -Proof NZsucc_wd. - -Theorem pred_wd : forall n1 n2 : N, n1 == n2 -> P n1 == P n2. -Proof NZpred_wd. - -Theorem pred_succ : forall n : N, P (S n) == n. -Proof NZpred_succ. - -Theorem pred_0 : P 0 == 0. -Proof pred_0. - -Theorem Neq_refl : forall n : N, n == n. -Proof (proj1 NZeq_equiv). - -Theorem Neq_sym : forall n m : N, n == m -> m == n. -Proof (proj2 (proj2 NZeq_equiv)). - -Theorem Neq_trans : forall n m p : N, n == m -> m == p -> n == p. -Proof (proj1 (proj2 NZeq_equiv)). - -Theorem neq_sym : forall n m : N, n ~= m -> m ~= n. -Proof NZneq_sym. - -Theorem succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2. -Proof NZsucc_inj. - -Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2. -Proof NZsucc_inj_wd. - -Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m. -Proof NZsucc_inj_wd_neg. - -(* Decidability and stability of equality was proved only in NZOrder, but -since it does not mention order, we'll put it here *) - -Theorem eq_dec : forall n m : N, decidable (n == m). -Proof NZeq_dec. - -Theorem eq_dne : forall n m : N, ~ ~ n == m <-> n == m. -Proof NZeq_dne. - -(* Now we prove that the successor of a number is not zero by defining a +(** 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 : Set) (a b : A) (n : N) : A := +Definition if_zero (A : Type) (a b : A) (n : N.t) : A := recursion a (fun _ _ => b) n. -Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd. +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. apply recursion_wd with (Aeq := (@eq A)). -reflexivity. unfold fun2_eq; now intros. assumption. +intros; unfold if_zero. +repeat red; intros. apply recursion_wd; auto. repeat red; auto. Qed. -Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. +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 : Set) (a b : A) (n : N), if_zero A a b (S n) = b. +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 A (@eq A)); [| | unfold fun2_wd; now intros]. +now rewrite recursion_succ. Qed. -Implicit Arguments if_zero [A]. - -Theorem neq_succ_0 : forall n : N, S n ~= 0. +Theorem neq_succ_0 : forall n, S n ~= 0. Proof. intros n H. -assert (true = false); [| discriminate]. -replace true with (if_zero false true (S n)) by apply if_zero_succ. -pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0. -now rewrite H. +generalize (Logic.eq_refl (if_zero false true 0)). +rewrite <- H at 1. rewrite if_zero_0, if_zero_succ; discriminate. Qed. -Theorem neq_0_succ : forall n : N, 0 ~= S n. +Theorem neq_0_succ : forall n, 0 ~= S n. Proof. intro n; apply neq_sym; apply neq_succ_0. Qed. -(* Next, we show that all numbers are nonnegative and recover regular induction -from the bidirectional induction on NZ *) +(** Next, we show that all numbers are nonnegative and recover regular + induction from the bidirectional induction on NZ *) -Theorem le_0_l : forall n : N, 0 <= n. +Theorem le_0_l : forall n, 0 <= n. Proof. -NZinduct n. -now apply NZeq_le_incl. +nzinduct n. +now apply eq_le_incl. intro n; split. -apply NZle_le_succ_r. -intro H; apply -> NZle_succ_r in H; destruct H as [H | H]. +apply le_le_succ_r. +intro H; apply -> le_succ_r in H; destruct H as [H | H]. assumption. symmetry in H; false_hyp H neq_succ_0. Qed. Theorem induction : - forall A : N -> Prop, predicate_wd Neq A -> - A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n. + forall A : N.t -> Prop, Proper (N.eq==>iff) A -> + A 0 -> (forall n, A n -> A (S n)) -> forall n, A n. Proof. -intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption. +intros A A_wd A0 AS n; apply right_induction with 0; try assumption. intros; auto; apply le_0_l. apply le_0_l. Qed. -(* The theorems NZinduction, NZcentral_induction and the tactic NZinduct +(** The theorems [bi_induction], [central_induction] and the tactic [nzinduct] refer to bidirectional induction, which is not useful on natural numbers. Therefore, we define a new induction tactic for natural numbers. We do not have to call "Declare Left Step" and "Declare Right Step" @@ -146,8 +89,8 @@ from NZ. *) Ltac induct n := induction_maker n ltac:(apply induction). Theorem case_analysis : - forall A : N -> Prop, predicate_wd Neq A -> - A 0 -> (forall n : N, A (S n)) -> forall n : N, A n. + forall A : N.t -> Prop, Proper (N.eq==>iff) A -> + A 0 -> (forall n, A (S n)) -> forall n, A n. Proof. intros; apply induction; auto. Qed. @@ -173,7 +116,7 @@ now left. intro n; right; now exists n. Qed. -Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1. +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. @@ -184,34 +127,29 @@ setoid_replace (S n == 0) with False using relation iff by rewrite succ_inj_wd. tauto. Qed. -Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n. +Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n. Proof. cases n. -intro H; elimtype False; now apply H. +intro H; exfalso; now apply H. intros; now rewrite pred_succ. Qed. -Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. +Theorem pred_inj : forall n m, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. Proof. intros n m; cases n. -intros H; elimtype False; now apply H. +intros H; exfalso; now apply H. intros n _; cases m. -intros H; elimtype False; now apply H. +intros H; exfalso; now apply H. intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3. Qed. -(* The following induction principle is useful for reasoning about, e.g., +(** The following induction principle is useful for reasoning about, e.g., Fibonacci numbers *) Section PairInduction. -Variable A : N -> Prop. -Hypothesis A_wd : predicate_wd Neq A. - -Add Morphism A with signature Neq ==> iff as A_morph. -Proof. -exact A_wd. -Qed. +Variable A : N.t -> Prop. +Hypothesis A_wd : Proper (N.eq==>iff) A. Theorem pair_induction : A 0 -> A 1 -> @@ -224,18 +162,12 @@ Qed. End PairInduction. -(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*) +(** The following is useful for reasoning about, e.g., Ackermann function *) -(* The following is useful for reasoning about, e.g., Ackermann function *) Section TwoDimensionalInduction. -Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph. -Proof. -exact R_wd. -Qed. +Variable R : N.t -> N.t -> Prop. +Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R. Theorem two_dim_induction : R 0 0 -> @@ -251,26 +183,16 @@ Qed. End TwoDimensionalInduction. -(*Ltac two_dim_induct n m := - try intros until n; - try intros until m; - pattern n, m; apply two_dim_induction; clear n m; - [solve_relation_wd | | | ].*) Section DoubleInduction. -Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph1. -Proof. -exact R_wd. -Qed. +Variable R : N.t -> N.t -> Prop. +Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R. Theorem double_induction : - (forall m : N, R 0 m) -> - (forall n : N, R (S n) 0) -> - (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m. + (forall m, R 0 m) -> + (forall n, R (S n) 0) -> + (forall n m, R n m -> R (S n) (S m)) -> forall n m, R n m. Proof. intros H1 H2 H3; induct n; auto. intros n H; cases m; auto. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 0a8f5f1e..22eb2cb3 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -8,45 +8,47 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NDefOps.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) Require Import Bool. (* To get the orb and negb function *) +Require Import RelationPairs. Require Export NStrongRec. -Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module NdefOpsPropFunct (Import N : NAxiomsSig'). +Include NStrongRecPropFunct N. (*****************************************************) (** Addition *) -Definition def_add (x y : N) := recursion y (fun _ p => S p) x. +Definition def_add (x y : N.t) := recursion y (fun _ => S) x. -Infix Local "++" := def_add (at level 50, left associativity). +Local Infix "+++" := def_add (at level 50, left associativity). -Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd. +Instance def_add_prewd : Proper (N.eq==>N.eq==>N.eq) (fun _ => S). Proof. -unfold def_add. -intros x x' Exx' y y' Eyy'. -apply recursion_wd with (Aeq := Neq). -assumption. -unfold fun2_eq; intros _ _ _ p p' Epp'; now rewrite Epp'. -assumption. +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. Qed. -Theorem def_add_0_l : forall y : N, 0 ++ y == y. +Theorem def_add_0_l : forall y, 0 +++ y == y. Proof. intro y. unfold def_add. now rewrite recursion_0. Qed. -Theorem def_add_succ_l : forall x y : N, S x ++ y == S (x ++ y). +Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y). Proof. intros x y; unfold def_add. -rewrite (@recursion_succ N Neq); try reflexivity. -unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2. +rewrite recursion_succ; auto with *. Qed. -Theorem def_add_add : forall n m : N, n ++ m == n + m. +Theorem def_add_add : forall n m, n +++ m == n + m. Proof. intros n m; induct n. now rewrite def_add_0_l, add_0_l. @@ -56,42 +58,37 @@ Qed. (*****************************************************) (** Multiplication *) -Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y. +Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y. -Infix Local "**" := def_mul (at level 40, left associativity). +Local Infix "**" := def_mul (at level 40, left associativity). -Lemma def_mul_step_wd : forall x : N, fun2_wd Neq Neq Neq (fun _ p => def_add p x). +Instance def_mul_prewd : + Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun x _ p => p +++ x). Proof. -unfold fun2_wd. intros. now apply def_add_wd. +repeat red; intros; now apply def_add_wd. Qed. -Lemma def_mul_step_equal : - forall x x' : N, x == x' -> - fun2_eq Neq Neq Neq (fun _ p => def_add p x) (fun x p => def_add p x'). -Proof. -unfold fun2_eq; intros; apply def_add_wd; assumption. -Qed. - -Add Morphism def_mul with signature Neq ==> Neq ==> Neq as def_mul_wd. +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 with (Aeq := Neq). -reflexivity. apply def_mul_step_equal. assumption. assumption. +apply recursion_wd; auto with *. +now apply def_mul_prewd. Qed. -Theorem def_mul_0_r : forall x : N, x ** 0 == 0. +Theorem def_mul_0_r : forall x, x ** 0 == 0. Proof. intro. unfold def_mul. now rewrite recursion_0. Qed. -Theorem def_mul_succ_r : forall x y : N, x ** S y == x ** y ++ x. +Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x. Proof. intros x y; unfold def_mul. -now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |]. +rewrite recursion_succ; auto with *. +now apply def_mul_prewd. Qed. -Theorem def_mul_mul : forall n m : N, n ** m == n * m. +Theorem def_mul_mul : forall n m, n ** m == n * m. Proof. intros n m; induct m. now rewrite def_mul_0_r, mul_0_r. @@ -101,120 +98,99 @@ Qed. (*****************************************************) (** Order *) -Definition def_ltb (m : N) : N -> bool := +Definition ltb (m : N.t) : N.t -> bool := recursion (if_zero false true) - (fun _ f => fun n => recursion false (fun n' _ => f n') n) + (fun _ f n => recursion false (fun n' _ => f n') n) m. -Infix Local "<<" := def_ltb (at level 70, no associativity). - -Lemma lt_base_wd : fun_wd Neq (@eq bool) (if_zero false true). -unfold fun_wd; intros; now apply if_zero_wd. -Qed. +Local Infix "<<" := ltb (at level 70, no associativity). -Lemma lt_step_wd : -fun2_wd Neq (fun_eq Neq (@eq bool)) (fun_eq Neq (@eq bool)) - (fun _ f => fun n => recursion false (fun n' _ => f n') n). +Instance ltb_prewd1 : Proper (N.eq==>Logic.eq) (if_zero false true). Proof. -unfold fun2_wd, fun_eq. -intros x x' Exx' f f' Eff' y y' Eyy'. -apply recursion_wd with (Aeq := @eq bool). -reflexivity. -unfold fun2_eq; intros; now apply Eff'. -assumption. +red; intros; apply if_zero_wd; auto. Qed. -Lemma lt_curry_wd : - forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m'). +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. -unfold def_ltb. -intros m m' Emm'. -apply recursion_wd with (Aeq := fun_eq Neq (@eq bool)). -apply lt_base_wd. -apply lt_step_wd. -assumption. +repeat red; intros; simpl. +apply recursion_wd; auto with *. +repeat red; auto. Qed. -Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd. +Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb. Proof. -intros; now apply lt_curry_wd. +unfold ltb. +intros n n' Hn m m' Hm. +apply f_equiv; auto with *. +apply recursion_wd; auto; [ apply ltb_prewd1 | apply ltb_prewd2 ]. Qed. -Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n. +Theorem ltb_base : forall n, 0 << n = if_zero false true n. Proof. -intro n; unfold def_ltb; now rewrite recursion_0. +intro n; unfold ltb; now rewrite recursion_0. Qed. -Theorem def_ltb_step : - forall m n : N, S m << n = recursion false (fun n' _ => m << n') n. +Theorem ltb_step : + forall m n, S m << n = recursion false (fun n' _ => m << n') n. Proof. -intros m n; unfold def_ltb. -pose proof - (@recursion_succ - (N -> bool) - (fun_eq Neq (@eq bool)) - (if_zero false true) - (fun _ f => fun n => recursion false (fun n' _ => f n') n) - lt_base_wd - lt_step_wd - m n n) as H. -now rewrite H. +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. Qed. (* Above, we rewrite applications of function. Is it possible to rewrite functions themselves, i.e., rewrite (recursion lt_base lt_step (S n)) to lt_step n (recursion lt_base lt_step n)? *) -Theorem def_ltb_0 : forall n : N, n << 0 = false. +Theorem ltb_0 : forall n, n << 0 = false. Proof. cases n. -rewrite def_ltb_base; now rewrite if_zero_0. -intro n; rewrite def_ltb_step. now rewrite recursion_0. +rewrite ltb_base; now rewrite if_zero_0. +intro n; rewrite ltb_step. now rewrite recursion_0. Qed. -Theorem def_ltb_0_succ : forall n : N, 0 << S n = true. +Theorem ltb_0_succ : forall n, 0 << S n = true. Proof. -intro n; rewrite def_ltb_base; now rewrite if_zero_succ. +intro n; rewrite ltb_base; now rewrite if_zero_succ. Qed. -Theorem succ_def_ltb_mono : forall n m : N, (S n << S m) = (n << m). +Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m). Proof. intros n m. -rewrite def_ltb_step. rewrite (@recursion_succ bool (@eq bool)); try reflexivity. -unfold fun2_wd; intros; now apply def_ltb_wd. +rewrite ltb_step. rewrite recursion_succ; try reflexivity. +repeat red; intros; now apply ltb_wd. Qed. -Theorem def_ltb_lt : forall n m : N, n << m = true <-> n < m. +Theorem ltb_lt : forall n m, n << m = true <-> n < m. Proof. double_induct n m. cases m. -rewrite def_ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r]. -intro n. rewrite def_ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity]. -intro n. rewrite def_ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r]. -intros n m. rewrite succ_def_ltb_mono. now rewrite <- succ_lt_mono. +rewrite ltb_0. split; intro H; [discriminate H | false_hyp H nlt_0_r]. +intro n. rewrite ltb_0_succ. split; intro; [apply lt_0_succ | reflexivity]. +intro n. rewrite ltb_0. split; intro H; [discriminate | false_hyp H nlt_0_r]. +intros n m. rewrite succ_ltb_mono. now rewrite <- succ_lt_mono. +Qed. + +Theorem ltb_ge : forall n m, n << m = false <-> n >= m. +Proof. +intros. rewrite <- not_true_iff_false, ltb_lt. apply nlt_ge. Qed. -(* (*****************************************************) (** Even *) -Definition even (x : N) := recursion true (fun _ p => negb p) x. - -Lemma even_step_wd : fun2_wd Neq (@eq bool) (@eq bool) (fun x p => if p then false else true). -Proof. -unfold fun2_wd. -intros x x' Exx' b b' Ebb'. -unfold eq_bool; destruct b; destruct b'; now simpl. -Qed. +Definition even (x : N.t) := recursion true (fun _ p => negb p) x. -Add Morphism even with signature Neq ==> (@eq bool) as even_wd. +Instance even_wd : Proper (N.eq==>Logic.eq) even. Proof. -unfold even; intros. -apply recursion_wd with (A := bool) (Aeq := (@eq bool)). -now unfold eq_bool. -unfold fun2_eq. intros _ _ _ b b' Ebb'. unfold eq_bool; destruct b; destruct b'; now simpl. -assumption. +intros n n' Hn. unfold even. +apply recursion_wd; auto. +congruence. Qed. Theorem even_0 : even 0 = true. @@ -223,76 +199,281 @@ unfold even. now rewrite recursion_0. Qed. -Theorem even_succ : forall x : N, even (S x) = negb (even x). +Theorem even_succ : forall x, even (S x) = negb (even x). Proof. unfold even. -intro x; rewrite (recursion_succ (@eq bool)); try reflexivity. -unfold fun2_wd. -intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl. +intro x; rewrite recursion_succ; try reflexivity. +congruence. Qed. (*****************************************************) (** Division by 2 *) -Definition half_aux (x : N) : N * N := - recursion (0, 0) (fun _ p => let (x1, x2) := p in ((S x2, x1))) x. +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 (x : N) := snd (half_aux x). +Definition half_aux (x : N.t) : N.t * N.t := + recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x. -Definition E2 := prod_rel Neq Neq. +Definition half (x : N.t) := snd (half_aux x). -Add Relation (prod N N) E2 -reflexivity proved by (prod_rel_refl N N Neq Neq E_equiv E_equiv) -symmetry proved by (prod_rel_sym N N Neq Neq E_equiv E_equiv) -transitivity proved by (prod_rel_trans N N Neq Neq E_equiv E_equiv) -as E2_rel. +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 *. +intros y y' Hy (u,v) (u',v') (Hu,Hv). compute in *. +rewrite Hu, Hv; auto with *. +Qed. -Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))). +Instance half_wd : Proper (N.eq==>N.eq) half. Proof. -unfold fun2_wd, E2, prod_rel. -intros _ _ _ p1 p2 [H1 H2]. -destruct p1; destruct p2; simpl in *. -now split; [rewrite H2 |]. +intros x x' Hx. unfold half. rewrite Hx; auto with *. Qed. -Add Morphism half with signature Neq ==> Neq as half_wd. +Lemma half_aux_0 : half_aux 0 = (0,0). Proof. -unfold half. -assert (H: forall x y, x == y -> E2 (half_aux x) (half_aux y)). -intros x y Exy; unfold half_aux; apply recursion_wd with (Aeq := E2); unfold E2. -unfold E2. -unfold prod_rel; simpl; now split. -unfold fun2_eq, prod_rel; simpl. -intros _ _ _ p1 p2; destruct p1; destruct p2; simpl. -intros [H1 H2]; split; [rewrite H2 | assumption]. reflexivity. assumption. -unfold E2, prod_rel in H. intros x y Exy; apply H in Exy. -exact (proj2 Exy). +unfold half_aux. rewrite recursion_0; auto. Qed. +Lemma half_aux_succ : forall x, + half_aux (S x) = (S (snd (half_aux x)), fst (half_aux x)). +Proof. +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. +Qed. + +Theorem half_aux_spec : forall n, + n == fst (half_aux n) + snd (half_aux n). +Proof. +apply induction. +intros x x' Hx. setoid_rewrite Hx; auto with *. +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. +Qed. + +Theorem half_aux_spec2 : forall n, + fst (half_aux n) == snd (half_aux n) \/ + fst (half_aux n) == S (snd (half_aux n)). +Proof. +apply induction. +intros x x' Hx. setoid_rewrite Hx; auto with *. +rewrite half_aux_0; simpl. auto with *. +intros. +rewrite half_aux_succ; simpl. +destruct H; auto with *. +right; apply succ_wd; auto with *. +Qed. + +Theorem half_0 : half 0 == 0. +Proof. +unfold half. rewrite half_aux_0; simpl; auto with *. +Qed. + +Theorem half_1 : half 1 == 0. +Proof. +unfold half. rewrite 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. +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. +Qed. + +Theorem half_upper_bound : forall n, 2 * half n <= n. +Proof. +intros. +destruct (half_double n) as [E|E]; rewrite E at 2. +apply le_refl. +nzsimpl. +apply le_le_succ_r, le_refl. +Qed. + +Theorem half_lower_bound : forall n, n <= 1 + 2 * half n. +Proof. +intros. +destruct (half_double n) as [E|E]; rewrite E at 1. +nzsimpl. +apply le_le_succ_r, le_refl. +apply le_refl. +Qed. + +Theorem half_nz : forall n, 1 < n -> 0 < half n. +Proof. +intros n LT. +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). +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. +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_0_l at 1. +rewrite <- add_lt_mono_r. +rewrite add_succ_l. apply lt_0_succ. +Qed. + + +(*****************************************************) +(** Power *) + +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. +Qed. + +Lemma pow_0 : forall n, n^^0 == 1. +Proof. +intros. unfold pow. rewrite recursion_0. auto with *. +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. +Qed. + + (*****************************************************) (** Logarithm for the base 2 *) -Definition log (x : N) : N := +Definition log (x : N.t) : N.t := strong_rec 0 - (fun x g => - if (e x 0) then 0 - else if (e x 1) then 0 + (fun g x => + if x << 2 then 0 else S (g (half x))) x. -Add Morphism log with signature Neq ==> Neq as log_wd. +Instance log_prewd : + Proper ((N.eq==>N.eq)==>N.eq==>N.eq) + (fun g x => if x<<2 then 0 else S (g (half x))). +Proof. +intros g g' Hg n n' Hn. +rewrite Hn. +destruct (n' << 2); auto with *. +apply succ_wd. +apply Hg. rewrite Hn; auto with *. +Qed. + +Instance log_wd : Proper (N.eq==>N.eq) log. Proof. intros x x' Exx'. unfold log. -apply strong_rec_wd with (Aeq := Neq); try (reflexivity || assumption). -unfold fun2_eq. intros y y' Eyy' g g' Egg'. -assert (H : e y 0 = e y' 0); [now apply e_wd|]. -rewrite <- H; clear H. -assert (H : e y 1 = e y' 1); [now apply e_wd|]. -rewrite <- H; clear H. -assert (H : S (g (half y)) == S (g' (half y'))); -[apply succ_wd; apply Egg'; now apply half_wd|]. -now destruct (e y 0); destruct (e y 1). +apply strong_rec_wd; auto with *. +apply log_prewd. Qed. + +Lemma log_good_step : forall n h1 h2, + (forall m, m < n -> h1 m == h2 m) -> + (if n << 2 then 0 else S (h1 (half n))) == + (if n << 2 then 0 else S (h2 (half n))). +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. +Qed. +Hint Resolve log_good_step. + +Theorem log_init : forall n, n < 2 -> log n == 0. +Proof. +intros n Hn. unfold log. rewrite strong_rec_fixpoint; auto with *. +replace (n << 2) with true; auto with *. +symmetry. now rewrite ltb_lt. +Qed. + +Theorem log_step : forall n, 2 <= n -> log n == S (log (half n)). +Proof. +intros n Hn. unfold log. rewrite strong_rec_fixpoint; auto with *. +replace (n << 2) with false; auto with *. +symmetry. rewrite <- not_true_iff_false, ltb_lt, nlt_ge; auto. +Qed. + +Theorem pow2_log : forall n, 0 < n -> half n < 2^^(log n) <= n. +Proof. +intro n; generalize (le_refl n). set (k:=n) at -2. clearbody k. +revert k. pattern n. apply induction; clear n. +intros n n' Hn; setoid_rewrite Hn; auto with *. +intros k Hk1 Hk2. + le_elim Hk1. destruct (nlt_0_r _ Hk1). + rewrite Hk1 in Hk2. destruct (nlt_0_r _ Hk2). + +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. +le_elim Hk2. +rewrite <- 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. +destruct (IH (half k)) as (IH1,IH2). + rewrite <- lt_succ_r. apply lt_le_trans with k; auto. + now apply half_decrease. + apply half_nz; auto. +set (K:=2^^log (half k)) in *; clearbody K. +split. +rewrite <- le_succ_l in IH1. +apply mul_le_mono_l with (p:=2) in IH1. +eapply lt_le_trans; eauto. +nzsimpl. +rewrite lt_succ_r. +eapply le_trans; [ eapply half_lower_bound | ]. +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. diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v new file mode 100644 index 00000000..0cb5665a --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NDiv.v @@ -0,0 +1,239 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Euclidean Division *) + +Require Import NAxioms NProperties NZDiv. + +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 NDivSig := NAxiomsSig <+ DivMod <+ NZDivCommon <+ NDivSpecific. +Module Type NDivSig' := NAxiomsSig' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. + +Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N). + +(** We benefit from what already exists for NZ *) + + 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. + + Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l. + +(** Let's now state again theorems, but without useless hypothesis. *) + +(** Uniqueness theorems *) + +Theorem div_mod_unique : + forall b q1 q2 r1 r2, r1<b -> r2<b -> + b*q1+r1 == b*q2+r2 -> q1 == q2 /\ r1 == r2. +Proof. intros. apply div_mod_unique with b; auto'. Qed. + +Theorem div_unique: + forall a b q r, r<b -> a == b*q + r -> q == a/b. +Proof. intros; apply div_unique with r; auto'. Qed. + +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. + +(** A division by itself returns 1 *) + +Lemma div_same : forall a, a~=0 -> a/a == 1. +Proof. intros. apply div_same; auto'. Qed. + +Lemma mod_same : forall a, a~=0 -> a mod a == 0. +Proof. intros. apply mod_same; auto'. Qed. + +(** A division of a small number by a bigger one yields zero. *) + +Theorem div_small: forall a b, a<b -> a/b == 0. +Proof. intros. apply div_small; auto'. Qed. + +(** Same situation, in term of modulo: *) + +Theorem mod_small: forall a b, a<b -> a mod b == a. +Proof. intros. apply mod_small; auto'. Qed. + +(** * Basic values of divisions and modulo. *) + +Lemma div_0_l: forall a, a~=0 -> 0/a == 0. +Proof. intros. apply div_0_l; auto'. Qed. + +Lemma mod_0_l: forall a, a~=0 -> 0 mod a == 0. +Proof. intros. apply mod_0_l; auto'. Qed. + +Lemma div_1_r: forall a, a/1 == a. +Proof. intros. apply div_1_r; auto'. Qed. + +Lemma mod_1_r: forall a, a mod 1 == 0. +Proof. intros. apply mod_1_r; auto'. Qed. + +Lemma div_1_l: forall a, 1<a -> 1/a == 0. +Proof. exact div_1_l. Qed. + +Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1. +Proof. exact mod_1_l. Qed. + +Lemma div_mul : forall a b, b~=0 -> (a*b)/b == a. +Proof. intros. apply div_mul; auto'. Qed. + +Lemma mod_mul : forall a b, b~=0 -> (a*b) mod b == 0. +Proof. intros. apply mod_mul; auto'. Qed. + + +(** * Order results about mod and div *) + +(** A modulo cannot grow beyond its starting point. *) + +Theorem mod_le: forall a b, b~=0 -> a mod b <= a. +Proof. intros. apply mod_le; auto'. Qed. + +Lemma div_str_pos : forall a b, 0<b<=a -> 0 < a/b. +Proof. exact div_str_pos. Qed. + +Lemma div_small_iff : forall a b, b~=0 -> (a/b==0 <-> a<b). +Proof. intros. apply div_small_iff; auto'. Qed. + +Lemma mod_small_iff : forall a b, b~=0 -> (a mod b == a <-> a<b). +Proof. intros. apply mod_small_iff; auto'. Qed. + +Lemma div_str_pos_iff : forall a b, b~=0 -> (0<a/b <-> b<=a). +Proof. intros. apply div_str_pos_iff; auto'. Qed. + + +(** As soon as the divisor is strictly greater than 1, + the division is strictly decreasing. *) + +Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. +Proof. exact div_lt. Qed. + +(** [le] is compatible with a positive division. *) + +Lemma div_le_mono : forall a b c, c~=0 -> a<=b -> a/c <= b/c. +Proof. intros. apply div_le_mono; auto'. Qed. + +Lemma mul_div_le : forall a b, b~=0 -> b*(a/b) <= a. +Proof. intros. apply mul_div_le; auto'. Qed. + +Lemma mul_succ_div_gt: forall a b, b~=0 -> a < b*(S (a/b)). +Proof. intros; apply mul_succ_div_gt; auto'. Qed. + +(** The previous inequality is exact iff the modulo is zero. *) + +Lemma div_exact : forall a b, b~=0 -> (a == b*(a/b) <-> a mod b == 0). +Proof. intros. apply div_exact; auto'. Qed. + +(** Some additionnal inequalities about div. *) + +Theorem div_lt_upper_bound: + forall a b q, b~=0 -> a < b*q -> a/b < q. +Proof. intros. apply div_lt_upper_bound; auto'. Qed. + +Theorem div_le_upper_bound: + forall a b q, b~=0 -> a <= b*q -> a/b <= q. +Proof. intros; apply div_le_upper_bound; auto'. Qed. + +Theorem div_le_lower_bound: + forall a b q, b~=0 -> b*q <= a -> q <= a/b. +Proof. intros; apply div_le_lower_bound; auto'. Qed. + +(** A division respects opposite monotonicity for the divisor *) + +Lemma div_le_compat_l: forall p q r, 0<q<=r -> p/r <= p/q. +Proof. intros. apply div_le_compat_l. auto'. auto. Qed. + +(** * Relations between usual operations and mod and div *) + +Lemma mod_add : forall a b c, c~=0 -> + (a + b * c) mod c == a mod c. +Proof. intros. apply mod_add; auto'. Qed. + +Lemma div_add : forall a b c, c~=0 -> + (a + b * c) / c == a / c + b. +Proof. intros. apply div_add; auto'. Qed. + +Lemma div_add_l: forall a b c, b~=0 -> + (a * b + c) / b == a + c / b. +Proof. intros. apply div_add_l; auto'. Qed. + +(** Cancellations. *) + +Lemma div_mul_cancel_r : forall a b c, b~=0 -> c~=0 -> + (a*c)/(b*c) == a/b. +Proof. intros. apply div_mul_cancel_r; auto'. Qed. + +Lemma div_mul_cancel_l : forall a b c, b~=0 -> c~=0 -> + (c*a)/(c*b) == a/b. +Proof. intros. apply div_mul_cancel_l; auto'. Qed. + +Lemma mul_mod_distr_r: forall a b c, b~=0 -> c~=0 -> + (a*c) mod (b*c) == (a mod b) * c. +Proof. intros. apply mul_mod_distr_r; auto'. Qed. + +Lemma mul_mod_distr_l: forall a b c, b~=0 -> c~=0 -> + (c*a) mod (c*b) == c * (a mod b). +Proof. intros. apply mul_mod_distr_l; auto'. Qed. + +(** Operations modulo. *) + +Theorem mod_mod: forall a n, n~=0 -> + (a mod n) mod n == a mod n. +Proof. intros. apply mod_mod; auto'. Qed. + +Lemma mul_mod_idemp_l : forall a b n, n~=0 -> + ((a mod n)*b) mod n == (a*b) mod n. +Proof. intros. apply mul_mod_idemp_l; auto'. Qed. + +Lemma mul_mod_idemp_r : forall a b n, n~=0 -> + (a*(b mod n)) mod n == (a*b) mod n. +Proof. intros. apply mul_mod_idemp_r; auto'. Qed. + +Theorem mul_mod: forall a b n, n~=0 -> + (a * b) mod n == ((a mod n) * (b mod n)) mod n. +Proof. intros. apply mul_mod; auto'. Qed. + +Lemma add_mod_idemp_l : forall a b n, n~=0 -> + ((a mod n)+b) mod n == (a+b) mod n. +Proof. intros. apply add_mod_idemp_l; auto'. Qed. + +Lemma add_mod_idemp_r : forall a b n, n~=0 -> + (a+(b mod n)) mod n == (a+b) mod n. +Proof. intros. apply add_mod_idemp_r; auto'. Qed. + +Theorem add_mod: forall a b n, n~=0 -> + (a+b) mod n == (a mod n + b mod n) mod n. +Proof. intros. apply add_mod; auto'. Qed. + +Lemma div_div : forall a b c, b~=0 -> c~=0 -> + (a/b)/c == a/(b*c). +Proof. intros. apply div_div; auto'. Qed. + +(** A last inequality: *) + +Theorem div_mul_le: + forall a b c, b~=0 -> c*(a/b) <= (c*a)/b. +Proof. intros. apply div_mul_le; auto'. Qed. + +(** mod is related to divisibility *) + +Lemma mod_divides : forall a b, b~=0 -> + (a mod b == 0 <-> exists c, a == b*c). +Proof. intros. apply mod_divides; auto'. Qed. + +End NDivPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index f6ccf3db..47bf38cb 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -8,51 +8,41 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NIso.v 10934 2008-05-15 21:58:20Z letouzey $ i*) +(*i $Id$ i*) Require Import NBase. -Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). +Module Homomorphism (N1 N2 : NAxiomsSig). -Module NBasePropMod2 := NBasePropFunct NAxiomsMod2. +Local Notation "n == m" := (N2.eq n m) (at level 70, no associativity). -Notation Local N1 := NAxiomsMod1.N. -Notation Local N2 := NAxiomsMod2.N. -Notation Local Eq1 := NAxiomsMod1.Neq. -Notation Local Eq2 := NAxiomsMod2.Neq. -Notation Local O1 := NAxiomsMod1.N0. -Notation Local O2 := NAxiomsMod2.N0. -Notation Local S1 := NAxiomsMod1.S. -Notation Local S2 := NAxiomsMod2.S. -Notation Local "n == m" := (Eq2 n m) (at level 70, no associativity). +Definition homomorphism (f : N1.t -> N2.t) : Prop := + f N1.zero == N2.zero /\ forall n, f (N1.succ n) == N2.succ (f n). -Definition homomorphism (f : N1 -> N2) : Prop := - f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n). +Definition natural_isomorphism : N1.t -> N2.t := + N1.recursion N2.zero (fun (n : N1.t) (p : N2.t) => N2.succ p). -Definition natural_isomorphism : N1 -> N2 := - NAxiomsMod1.recursion O2 (fun (n : N1) (p : N2) => S2 p). - -Add Morphism natural_isomorphism with signature Eq1 ==> Eq2 as natural_isomorphism_wd. +Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism. Proof. unfold natural_isomorphism. intros n m Eqxy. -apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). +apply N1.recursion_wd. reflexivity. -unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. +intros _ _ _ y' y'' H. now apply N2.succ_wd. assumption. Qed. -Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2. +Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero. Proof. -unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0. +unfold natural_isomorphism; now rewrite N1.recursion_0. Qed. Theorem natural_isomorphism_succ : - forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). + forall n : N1.t, natural_isomorphism (N1.succ n) == N2.succ (natural_isomorphism n). Proof. unfold natural_isomorphism. -intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ; -[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd]. +intro n. rewrite N1.recursion_succ; auto with *. +repeat red; intros. apply N2.succ_wd; auto. Qed. Theorem hom_nat_iso : homomorphism natural_isomorphism. @@ -63,23 +53,20 @@ Qed. End Homomorphism. -Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). +Module Inverse (N1 N2 : NAxiomsSig). -Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1. +Module Import NBasePropMod1 := NBasePropFunct N1. (* This makes the tactic induct available. Since it is taken from (NBasePropFunct NAxiomsMod1), it refers to induction on N1. *) -Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. -Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. - -Notation Local N1 := NAxiomsMod1.N. -Notation Local N2 := NAxiomsMod2.N. -Notation Local h12 := Hom12.natural_isomorphism. -Notation Local h21 := Hom21.natural_isomorphism. +Module Hom12 := Homomorphism N1 N2. +Module Hom21 := Homomorphism N2 N1. -Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity). +Local Notation h12 := Hom12.natural_isomorphism. +Local Notation h21 := Hom21.natural_isomorphism. +Local Notation "n == m" := (N1.eq n m) (at level 70, no associativity). -Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n. +Lemma inverse_nat_iso : forall n : N1.t, h21 (h12 n) == n. Proof. induct n. now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0. @@ -89,25 +76,20 @@ Qed. End Inverse. -Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). - -Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. -Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. +Module Isomorphism (N1 N2 : NAxiomsSig). -Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2. -Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1. +Module Hom12 := Homomorphism N1 N2. +Module Hom21 := Homomorphism N2 N1. +Module Inverse12 := Inverse N1 N2. +Module Inverse21 := Inverse N2 N1. -Notation Local N1 := NAxiomsMod1.N. -Notation Local N2 := NAxiomsMod2.N. -Notation Local Eq1 := NAxiomsMod1.Neq. -Notation Local Eq2 := NAxiomsMod2.Neq. -Notation Local h12 := Hom12.natural_isomorphism. -Notation Local h21 := Hom21.natural_isomorphism. +Local Notation h12 := Hom12.natural_isomorphism. +Local Notation h21 := Hom21.natural_isomorphism. -Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop := +Definition isomorphism (f1 : N1.t -> N2.t) (f2 : N2.t -> N1.t) : Prop := Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\ - forall n : N1, Eq1 (f2 (f1 n)) n /\ - forall n : N2, Eq2 (f1 (f2 n)) n. + forall n, N1.eq (f2 (f1 n)) n /\ + forall n, N2.eq (f1 (f2 n)) n. Theorem iso_nat_iso : isomorphism h12 h21. Proof. diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v deleted file mode 100644 index 0b00f689..00000000 --- a/theories/Numbers/Natural/Abstract/NMul.v +++ /dev/null @@ -1,87 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) -(* Evgeny Makarov, INRIA, 2007 *) -(************************************************************************) - -(*i $Id: NMul.v 11040 2008-06-03 00:04:16Z letouzey $ i*) - -Require Export NAdd. - -Module NMulPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NAddPropMod := NAddPropFunct NAxiomsMod. -Open Local Scope NatScope. - -Theorem mul_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 * m1 == n2 * m2. -Proof NZmul_wd. - -Theorem mul_0_l : forall n : N, 0 * n == 0. -Proof NZmul_0_l. - -Theorem mul_succ_l : forall n m : N, (S n) * m == n * m + m. -Proof NZmul_succ_l. - -(** Theorems that are valid for both natural numbers and integers *) - -Theorem mul_0_r : forall n, n * 0 == 0. -Proof NZmul_0_r. - -Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. -Proof NZmul_succ_r. - -Theorem mul_comm : forall n m : N, n * m == m * n. -Proof NZmul_comm. - -Theorem mul_add_distr_r : forall n m p : N, (n + m) * p == n * p + m * p. -Proof NZmul_add_distr_r. - -Theorem mul_add_distr_l : forall n m p : N, n * (m + p) == n * m + n * p. -Proof NZmul_add_distr_l. - -Theorem mul_assoc : forall n m p : N, n * (m * p) == (n * m) * p. -Proof NZmul_assoc. - -Theorem mul_1_l : forall n : N, 1 * n == n. -Proof NZmul_1_l. - -Theorem mul_1_r : forall n : N, n * 1 == n. -Proof NZmul_1_r. - -(* Theorems that cannot be proved in NZMul *) - -(* In proving the correctness of the definition of multiplication on -integers constructed from pairs of natural numbers, we'll need the -following fact about natural numbers: - -a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u = a * m' + v - -Here n + m' == n' + m expresses equality of integers (n, m) and (n', m'), -since a pair (a, b) of natural numbers represents the integer a - b. On -integers, the formula above could be proved by moving a * m to the left, -factoring out a and replacing n - m by n' - m'. However, the formula is -required in the process of constructing integers, so it has to be proved -for natural numbers, where terms cannot be moved from one side of an -equation to the other. The proof uses the cancellation laws add_cancel_l -and add_cancel_r. *) - -Theorem add_mul_repl_pair : forall a n m n' m' u v : N, - a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. -Proof. -intros a n m n' m' u v H1 H2. -apply (@NZmul_wd a a) in H2; [| reflexivity]. -do 2 rewrite mul_add_distr_l in H2. symmetry in H2. -pose proof (NZadd_wd _ _ H1 _ _ H2) as H3. -rewrite (add_shuffle1 (a * m)), (add_comm (a * m) (a * n)) in H3. -do 2 rewrite <- add_assoc in H3. apply -> add_cancel_l in H3. -rewrite (add_assoc u), (add_comm (a * m)) in H3. -apply -> add_cancel_r in H3. -now rewrite (add_comm (a * n') u), (add_comm (a * m') v). -Qed. - -End NMulPropFunct. - diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v index aa21fb50..a2162b13 100644 --- a/theories/Numbers/Natural/Abstract/NMulOrder.v +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -8,122 +8,71 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) Require Export NAddOrder. -Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module NMulOrderPropFunct (Import N : NAxiomsSig'). +Include NAddOrderPropFunct N. -Theorem mul_lt_pred : - forall p q n m : N, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). -Proof NZmul_lt_pred. +(** Theorems that are either not valid on Z or have different proofs + on N and Z *) -Theorem mul_lt_mono_pos_l : forall p n m : N, 0 < p -> (n < m <-> p * n < p * m). -Proof NZmul_lt_mono_pos_l. - -Theorem mul_lt_mono_pos_r : forall p n m : N, 0 < p -> (n < m <-> n * p < m * p). -Proof NZmul_lt_mono_pos_r. - -Theorem mul_cancel_l : forall n m p : N, p ~= 0 -> (p * n == p * m <-> n == m). -Proof NZmul_cancel_l. - -Theorem mul_cancel_r : forall n m p : N, p ~= 0 -> (n * p == m * p <-> n == m). -Proof NZmul_cancel_r. - -Theorem mul_id_l : forall n m : N, m ~= 0 -> (n * m == m <-> n == 1). -Proof NZmul_id_l. - -Theorem mul_id_r : forall n m : N, n ~= 0 -> (n * m == n <-> m == 1). -Proof NZmul_id_r. - -Theorem mul_le_mono_pos_l : forall n m p : N, 0 < p -> (n <= m <-> p * n <= p * m). -Proof NZmul_le_mono_pos_l. - -Theorem mul_le_mono_pos_r : forall n m p : N, 0 < p -> (n <= m <-> n * p <= m * p). -Proof NZmul_le_mono_pos_r. - -Theorem mul_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m. -Proof NZmul_pos_pos. - -Theorem lt_1_mul_pos : forall n m : N, 1 < n -> 0 < m -> 1 < n * m. -Proof NZlt_1_mul_pos. - -Theorem eq_mul_0 : forall n m : N, n * m == 0 <-> n == 0 \/ m == 0. -Proof NZeq_mul_0. - -Theorem neq_mul_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. -Proof NZneq_mul_0. - -Theorem eq_square_0 : forall n : N, n * n == 0 <-> n == 0. -Proof NZeq_square_0. - -Theorem eq_mul_0_l : forall n m : N, n * m == 0 -> m ~= 0 -> n == 0. -Proof NZeq_mul_0_l. - -Theorem eq_mul_0_r : forall n m : N, n * m == 0 -> n ~= 0 -> m == 0. -Proof NZeq_mul_0_r. - -Theorem square_lt_mono : forall n m : N, n < m <-> n * n < m * m. +Theorem square_lt_mono : forall n m, n < m <-> n * n < m * m. Proof. intros n m; split; intro; -[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; +[apply square_lt_mono_nonneg | apply square_lt_simpl_nonneg]; try assumption; apply le_0_l. Qed. -Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. +Theorem square_le_mono : forall n m, n <= m <-> n * n <= m * m. Proof. intros n m; split; intro; -[apply NZsquare_le_mono_nonneg | apply NZsquare_le_simpl_nonneg]; +[apply square_le_mono_nonneg | apply square_le_simpl_nonneg]; try assumption; apply le_0_l. Qed. -Theorem mul_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. -Proof NZmul_2_mono_l. - -(* Theorems that are either not valid on Z or have different proofs on N and Z *) - -Theorem mul_le_mono_l : forall n m p : N, n <= m -> p * n <= p * m. +Theorem mul_le_mono_l : forall n m p, n <= m -> p * n <= p * m. Proof. -intros; apply NZmul_le_mono_nonneg_l. apply le_0_l. assumption. +intros; apply mul_le_mono_nonneg_l. apply le_0_l. assumption. Qed. -Theorem mul_le_mono_r : forall n m p : N, n <= m -> n * p <= m * p. +Theorem mul_le_mono_r : forall n m p, n <= m -> n * p <= m * p. Proof. -intros; apply NZmul_le_mono_nonneg_r. apply le_0_l. assumption. +intros; apply mul_le_mono_nonneg_r. apply le_0_l. assumption. Qed. -Theorem mul_lt_mono : forall n m p q : N, n < m -> p < q -> n * p < m * q. +Theorem mul_lt_mono : forall n m p q, n < m -> p < q -> n * p < m * q. Proof. -intros; apply NZmul_lt_mono_nonneg; try assumption; apply le_0_l. +intros; apply mul_lt_mono_nonneg; try assumption; apply le_0_l. Qed. -Theorem mul_le_mono : forall n m p q : N, n <= m -> p <= q -> n * p <= m * q. +Theorem mul_le_mono : forall n m p q, n <= m -> p <= q -> n * p <= m * q. Proof. -intros; apply NZmul_le_mono_nonneg; try assumption; apply le_0_l. +intros; apply mul_le_mono_nonneg; try assumption; apply le_0_l. Qed. -Theorem lt_0_mul : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0. +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 -> NZlt_0_mul in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r. -now apply NZmul_pos_pos. +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. -Notation mul_pos := lt_0_mul (only parsing). +Notation mul_pos := lt_0_mul' (only parsing). -Theorem eq_mul_1 : forall n m : N, n * m == 1 <-> n == 1 /\ m == 1. +Theorem eq_mul_1 : forall n m, n * m == 1 <-> n == 1 /\ m == 1. Proof. intros n m. split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l]. -intro H; destruct (NZlt_trichotomy n 1) as [H1 | [H1 | H1]]. +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. 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. -assert (H3 : 1 < n * m) by now apply (lt_1_l 0 m). +assert (H3 : 1 < n * m) by now apply (lt_1_l m). rewrite H in H3; false_hyp H3 lt_irrefl. Qed. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 15aed7ab..090c02ec 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -8,355 +8,62 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NOrder.v 11282 2008-07-28 11:51:53Z msozeau $ i*) +(*i $Id$ i*) -Require Export NMul. +Require Export NAdd. -Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NMulPropMod := NMulPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module NOrderPropFunct (Import N : NAxiomsSig'). +Include NAddPropFunct N. -(* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *) - -(* Axioms *) - -Theorem lt_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 < m1 <-> n2 < m2). -Proof NZlt_wd. - -Theorem le_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> (n1 <= m1 <-> n2 <= m2). -Proof NZle_wd. - -Theorem min_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> min n1 m1 == min n2 m2. -Proof NZmin_wd. - -Theorem max_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> max n1 m1 == max n2 m2. -Proof NZmax_wd. - -Theorem lt_eq_cases : forall n m : N, n <= m <-> n < m \/ n == m. -Proof NZlt_eq_cases. - -Theorem lt_irrefl : forall n : N, ~ n < n. -Proof NZlt_irrefl. - -Theorem lt_succ_r : forall n m : N, n < S m <-> n <= m. -Proof NZlt_succ_r. - -Theorem min_l : forall n m : N, n <= m -> min n m == n. -Proof NZmin_l. - -Theorem min_r : forall n m : N, m <= n -> min n m == m. -Proof NZmin_r. - -Theorem max_l : forall n m : N, m <= n -> max n m == n. -Proof NZmax_l. - -Theorem max_r : forall n m : N, n <= m -> max n m == m. -Proof NZmax_r. - -(* Renaming theorems from NZOrder.v *) - -Theorem lt_le_incl : forall n m : N, n < m -> n <= m. -Proof NZlt_le_incl. - -Theorem eq_le_incl : forall n m : N, n == m -> n <= m. -Proof NZeq_le_incl. - -Theorem lt_neq : forall n m : N, n < m -> n ~= m. -Proof NZlt_neq. - -Theorem le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m. -Proof NZle_neq. - -Theorem le_refl : forall n : N, n <= n. -Proof NZle_refl. - -Theorem lt_succ_diag_r : forall n : N, n < S n. -Proof NZlt_succ_diag_r. - -Theorem le_succ_diag_r : forall n : N, n <= S n. -Proof NZle_succ_diag_r. - -Theorem lt_0_1 : 0 < 1. -Proof NZlt_0_1. - -Theorem le_0_1 : 0 <= 1. -Proof NZle_0_1. - -Theorem lt_lt_succ_r : forall n m : N, n < m -> n < S m. -Proof NZlt_lt_succ_r. - -Theorem le_le_succ_r : forall n m : N, n <= m -> n <= S m. -Proof NZle_le_succ_r. - -Theorem le_succ_r : forall n m : N, n <= S m <-> n <= m \/ n == S m. -Proof NZle_succ_r. - -Theorem neq_succ_diag_l : forall n : N, S n ~= n. -Proof NZneq_succ_diag_l. - -Theorem neq_succ_diag_r : forall n : N, n ~= S n. -Proof NZneq_succ_diag_r. - -Theorem nlt_succ_diag_l : forall n : N, ~ S n < n. -Proof NZnlt_succ_diag_l. - -Theorem nle_succ_diag_l : forall n : N, ~ S n <= n. -Proof NZnle_succ_diag_l. - -Theorem le_succ_l : forall n m : N, S n <= m <-> n < m. -Proof NZle_succ_l. - -Theorem lt_succ_l : forall n m : N, S n < m -> n < m. -Proof NZlt_succ_l. - -Theorem succ_lt_mono : forall n m : N, n < m <-> S n < S m. -Proof NZsucc_lt_mono. - -Theorem succ_le_mono : forall n m : N, n <= m <-> S n <= S m. -Proof NZsucc_le_mono. - -Theorem lt_asymm : forall n m : N, n < m -> ~ m < n. -Proof NZlt_asymm. - -Notation lt_ngt := lt_asymm (only parsing). - -Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p. -Proof NZlt_trans. - -Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p. -Proof NZle_trans. - -Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p. -Proof NZle_lt_trans. - -Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p. -Proof NZlt_le_trans. - -Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m. -Proof NZle_antisymm. - -(** Trichotomy, decidability, and double negation elimination *) - -Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. -Proof NZlt_trichotomy. - -Notation lt_eq_gt_cases := lt_trichotomy (only parsing). - -Theorem lt_gt_cases : forall n m : N, n ~= m <-> n < m \/ n > m. -Proof NZlt_gt_cases. - -Theorem le_gt_cases : forall n m : N, n <= m \/ n > m. -Proof NZle_gt_cases. - -Theorem lt_ge_cases : forall n m : N, n < m \/ n >= m. -Proof NZlt_ge_cases. - -Theorem le_ge_cases : forall n m : N, n <= m \/ n >= m. -Proof NZle_ge_cases. - -Theorem le_ngt : forall n m : N, n <= m <-> ~ n > m. -Proof NZle_ngt. - -Theorem nlt_ge : forall n m : N, ~ n < m <-> n >= m. -Proof NZnlt_ge. - -Theorem lt_dec : forall n m : N, decidable (n < m). -Proof NZlt_dec. - -Theorem lt_dne : forall n m : N, ~ ~ n < m <-> n < m. -Proof NZlt_dne. - -Theorem nle_gt : forall n m : N, ~ n <= m <-> n > m. -Proof NZnle_gt. - -Theorem lt_nge : forall n m : N, n < m <-> ~ n >= m. -Proof NZlt_nge. - -Theorem le_dec : forall n m : N, decidable (n <= m). -Proof NZle_dec. - -Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. -Proof NZle_dne. - -Theorem nlt_succ_r : forall n m : N, ~ m < S n <-> n < m. -Proof NZnlt_succ_r. - -Theorem lt_exists_pred : - forall z n : N, z < n -> exists k : N, n == S k /\ z <= k. -Proof NZlt_exists_pred. - -Theorem lt_succ_iter_r : - forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m. -Proof NZlt_succ_iter_r. - -Theorem neq_succ_iter_l : - forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m. -Proof NZneq_succ_iter_l. - -(** Stronger variant of induction with assumptions n >= 0 (n < 0) -in the induction step *) - -Theorem right_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, A z -> - (forall n : N, z <= n -> A n -> A (S n)) -> - forall n : N, z <= n -> A n. -Proof NZright_induction. - -Theorem left_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, A z -> - (forall n : N, n < z -> A (S n) -> A n) -> - forall n : N, n <= z -> A n. -Proof NZleft_induction. - -Theorem right_induction' : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, n <= z -> A n) -> - (forall n : N, z <= n -> A n -> A (S n)) -> - forall n : N, A n. -Proof NZright_induction'. - -Theorem left_induction' : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, z <= n -> A n) -> - (forall n : N, n < z -> A (S n) -> A n) -> - forall n : N, A n. -Proof NZleft_induction'. - -Theorem strong_right_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> - forall n : N, z <= n -> A n. -Proof NZstrong_right_induction. - -Theorem strong_left_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> - forall n : N, n <= z -> A n. -Proof NZstrong_left_induction. - -Theorem strong_right_induction' : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, n <= z -> A n) -> - (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> - forall n : N, A n. -Proof NZstrong_right_induction'. - -Theorem strong_left_induction' : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, - (forall n : N, z <= n -> A n) -> - (forall n : N, n <= z -> (forall m : N, m <= z -> S n <= m -> A m) -> A n) -> - forall n : N, A n. -Proof NZstrong_left_induction'. - -Theorem order_induction : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, A z -> - (forall n : N, z <= n -> A n -> A (S n)) -> - (forall n : N, n < z -> A (S n) -> A n) -> - forall n : N, A n. -Proof NZorder_induction. - -Theorem order_induction' : - forall A : N -> Prop, predicate_wd Neq A -> - forall z : N, A z -> - (forall n : N, z <= n -> A n -> A (S n)) -> - (forall n : N, n <= z -> A n -> A (P n)) -> - forall n : N, A n. -Proof NZorder_induction'. - -(* We don't need order_induction_0 and order_induction'_0 (see NZOrder and -ZOrder) since they boil down to regular induction *) - -(** Elimintation principle for < *) - -Theorem lt_ind : - forall A : N -> Prop, predicate_wd Neq A -> - forall n : N, - A (S n) -> - (forall m : N, n < m -> A m -> A (S m)) -> - forall m : N, n < m -> A m. -Proof NZlt_ind. - -(** Elimintation principle for <= *) - -Theorem le_ind : - forall A : N -> Prop, predicate_wd Neq A -> - forall n : N, - A n -> - (forall m : N, n <= m -> A m -> A (S m)) -> - forall m : N, n <= m -> A m. -Proof NZle_ind. - -(** Well-founded relations *) - -Theorem lt_wf : forall z : N, well_founded (fun n m : N => z <= n /\ n < m). -Proof NZlt_wf. - -Theorem gt_wf : forall z : N, well_founded (fun n m : N => m < n /\ n <= z). -Proof NZgt_wf. +(* 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 : N => 0 <= n /\ n < m) - using relation (@relations_eq N N). +setoid_replace lt with (fun n m => 0 <= n /\ n < m). apply lt_wf. intros x y; split. intro H; split; [apply le_0_l | assumption]. now intros [_ H]. Defined. -(* Theorems that are true for natural numbers but not for integers *) - (* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *) -Theorem nlt_0_r : forall n : N, ~ n < 0. +Theorem nlt_0_r : forall n, ~ n < 0. Proof. intro n; apply -> le_ngt. apply le_0_l. Qed. -Theorem nle_succ_0 : forall n : N, ~ (S n <= 0). +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. Qed. -Theorem le_0_r : forall n : N, n <= 0 <-> n == 0. +Theorem le_0_r : forall n, n <= 0 <-> n == 0. Proof. intros n; split; intro H. le_elim H; [false_hyp H nlt_0_r | assumption]. now apply eq_le_incl. Qed. -Theorem lt_0_succ : forall n : N, 0 < S n. +Theorem lt_0_succ : forall n, 0 < S n. Proof. induct n; [apply lt_succ_diag_r | intros n H; now apply lt_lt_succ_r]. Qed. -Theorem neq_0_lt_0 : forall n : N, n ~= 0 <-> 0 < n. +Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n. Proof. cases n. split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed. -Theorem eq_0_gt_0_cases : forall n : N, n == 0 \/ 0 < n. +Theorem eq_0_gt_0_cases : forall n, n == 0 \/ 0 < n. Proof. cases n. now left. intro; right; apply lt_0_succ. Qed. -Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n. +Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. induct n. now left. cases n. intros; right; now left. @@ -366,7 +73,7 @@ right; right. rewrite H. apply lt_succ_diag_r. right; right. now apply lt_lt_succ_r. Qed. -Theorem lt_1_r : forall n : N, n < 1 <-> n == 0. +Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. @@ -374,7 +81,7 @@ intros n. rewrite <- succ_lt_mono. split; intro H; [false_hyp H nlt_0_r | false_hyp H neq_succ_0]. Qed. -Theorem le_1_r : forall n : N, n <= 1 <-> n == 0 \/ n == 1. +Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. cases n. split; intro; [now left | apply le_succ_diag_r]. @@ -382,36 +89,30 @@ intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. split; [intro; now right | intros [H | H]; [false_hyp H neq_succ_0 | assumption]]. Qed. -Theorem lt_lt_0 : forall n m : N, n < m -> 0 < m. +Theorem lt_lt_0 : forall n m, n < m -> 0 < m. Proof. intros n m; induct n. trivial. intros n IH H. apply IH; now apply lt_succ_l. Qed. -Theorem lt_1_l : forall n m p : N, n < m -> m < p -> 1 < p. +Theorem lt_1_l' : forall n m p, n < m -> m < p -> 1 < p. Proof. -intros n m p H1 H2. -apply le_lt_trans with m. apply <- le_succ_l. apply le_lt_trans with n. -apply le_0_l. assumption. assumption. +intros. apply lt_1_l with m; auto. +apply le_lt_trans with n; auto. now apply le_0_l. Qed. (** Elimination principlies for < and <= for relations *) Section RelElim. -(* FIXME: Variable R : relation N. -- does not work *) - -Variable R : N -> N -> Prop. -Hypothesis R_wd : relation_wd Neq Neq R. - -Add Morphism R with signature Neq ==> Neq ==> iff as R_morph2. -Proof. apply R_wd. Qed. +Variable R : relation N.t. +Hypothesis R_wd : Proper (N.eq==>N.eq==>iff) R. Theorem le_ind_rel : - (forall m : N, R 0 m) -> - (forall n m : N, n <= m -> R n m -> R (S n) (S m)) -> - forall n m : N, n <= m -> R n m. + (forall m, R 0 m) -> + (forall n m, n <= m -> R n m -> R (S n) (S m)) -> + forall n m, n <= m -> R n m. Proof. intros Base Step; induct n. intros; apply Base. @@ -422,9 +123,9 @@ intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. Qed. Theorem lt_ind_rel : - (forall m : N, R 0 (S m)) -> - (forall n m : N, n < m -> R n m -> R (S n) (S m)) -> - forall n m : N, n < m -> R n m. + (forall m, R 0 (S m)) -> + (forall n m, n < m -> R n m -> R (S n) (S m)) -> + forall n m, n < m -> R n m. Proof. intros Base Step; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. @@ -439,61 +140,64 @@ End RelElim. (** Predecessor and order *) -Theorem succ_pred_pos : forall n : N, 0 < n -> S (P n) == n. +Theorem succ_pred_pos : forall n, 0 < n -> S (P n) == n. Proof. intros n H; apply succ_pred; intro H1; rewrite H1 in H. false_hyp H lt_irrefl. Qed. -Theorem le_pred_l : forall n : N, P n <= n. +Theorem le_pred_l : forall n, P n <= n. Proof. cases n. rewrite pred_0; now apply eq_le_incl. intros; rewrite pred_succ; apply le_succ_diag_r. Qed. -Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n. +Theorem lt_pred_l : forall n, n ~= 0 -> P n < n. Proof. cases n. -intro H; elimtype False; now apply H. +intro H; exfalso; now apply H. intros; rewrite pred_succ; apply lt_succ_diag_r. Qed. -Theorem le_le_pred : forall n m : N, n <= m -> P n <= m. +Theorem le_le_pred : forall n m, n <= m -> P n <= m. Proof. intros n m H; apply le_trans with n. apply le_pred_l. assumption. Qed. -Theorem lt_lt_pred : forall n m : N, n < m -> P n < m. +Theorem lt_lt_pred : forall n m, n < m -> P n < m. Proof. intros n m H; apply le_lt_trans with n. apply le_pred_l. assumption. Qed. -Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *) +Theorem lt_le_pred : forall n m, n < m -> n <= P m. + (* Converse is false for n == m == 0 *) Proof. intro n; cases m. intro H; false_hyp H nlt_0_r. intros m IH. rewrite pred_succ; now apply -> lt_succ_r. Qed. -Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *) +Theorem lt_pred_le : forall n m, P n < m -> n <= m. + (* Converse is false for n == m == 0 *) 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. Qed. -Theorem lt_pred_lt : forall n m : N, n < P m -> n < m. +Theorem lt_pred_lt : forall n m, n < P m -> n < m. Proof. intros n m H; apply lt_le_trans with (P m); [assumption | apply le_pred_l]. Qed. -Theorem le_pred_le : forall n m : N, n <= P m -> n <= m. +Theorem le_pred_le : forall n m, n <= P m -> n <= m. Proof. intros n m H; apply le_trans with (P m); [assumption | apply le_pred_l]. Qed. -Theorem pred_le_mono : forall n m : N, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) +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. @@ -501,7 +205,7 @@ intro; rewrite pred_0; apply le_0_l. intros p q H1 _; now do 2 rewrite pred_succ. Qed. -Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m). +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. @@ -512,22 +216,24 @@ 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. Qed. -Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m. +Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m. Proof. intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ. Qed. -Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) +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. Qed. -Theorem lt_pred_lt_succ : forall n m : N, P n < m -> n < S m. (* Converse is false for n == m == 0 *) +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. Qed. -Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m. +Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m. Proof. intros n m; cases n. rewrite pred_0. split; intro H; apply le_0_l. diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v new file mode 100644 index 00000000..30262bd9 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Export NAxioms NSub. + +(** 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. diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v index c6a6da48..cbbcdbff 100644 --- a/theories/Numbers/Natural/Abstract/NStrongRec.v +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -8,123 +8,200 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NStrongRec.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) (** This file defined the strong (course-of-value, well-founded) recursion and proves its properties *) Require Export NSub. -Module NStrongRecPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NSubPropMod := NSubPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module NStrongRecPropFunct (Import N : NAxiomsSig'). +Include NSubPropFunct N. Section StrongRecursion. -Variable A : Set. +Variable A : Type. Variable Aeq : relation A. +Variable Aeq_equiv : Equivalence Aeq. + +(** [strong_rec] allows to define a recursive function [phi] given by + an equation [phi(n) = F(phi)(n)] where recursive calls to [phi] + in [F] are made on strictly lower numbers than [n]. + + For [strong_rec a F n]: + - Parameter [a:A] is a default value used internally, it has no + effect on the final result. + - Parameter [F:(N->A)->N->A] is the step function: + [F f n] should return [phi(n)] when [f] is a function + that coincide with [phi] for numbers strictly less than [n]. +*) -Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity). +Definition strong_rec (a : A) (f : (N.t -> A) -> N.t -> A) (n : N.t) : A := + recursion (fun _ => a) (fun _ => f) (S n) n. -Hypothesis Aeq_equiv : equiv A Aeq. +(** For convenience, we use in proofs an intermediate definition + between [recursion] and [strong_rec]. *) -Add Relation A Aeq - reflexivity proved by (proj1 Aeq_equiv) - symmetry proved by (proj2 (proj2 Aeq_equiv)) - transitivity proved by (proj1 (proj2 Aeq_equiv)) -as Aeq_rel. +Definition strong_rec0 (a : A) (f : (N.t -> A) -> N.t -> A) : N.t -> N.t -> A := + recursion (fun _ => a) (fun _ => f). -Definition strong_rec (a : A) (f : N -> (N -> A) -> A) (n : N) : A := -recursion - (fun _ : N => a) - (fun (m : N) (p : N -> A) (k : N) => f k p) - (S n) - n. +Lemma strong_rec_alt : forall a f n, + strong_rec a f n = strong_rec0 a f (S n) n. +Proof. +reflexivity. +Qed. -Theorem strong_rec_wd : -forall a a' : A, a ==A a' -> - forall f f', fun2_eq Neq (fun_eq Neq Aeq) Aeq f f' -> - forall n n', n == n' -> - strong_rec a f n ==A strong_rec a' f' n'. +(** 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. +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'. -(* First we prove that recursion (which is on type N -> A) returns -extensionally equal functions, and then we use the fact that n == n' *) -assert (H : fun_eq Neq Aeq - (recursion - (fun _ : N => a) - (fun (m : N) (p : N -> A) (k : N) => f k p) - (S n)) - (recursion - (fun _ : N => a') - (fun (m : N) (p : N -> A) (k : N) => f' k p) - (S n'))). -apply recursion_wd with (Aeq := fun_eq Neq Aeq). -unfold fun_eq; now intros. -unfold fun2_eq. intros y y' Eyy' p p' Epp'. unfold fun_eq. auto. +rewrite !strong_rec_alt. +apply strong_rec0_wd; auto. now rewrite Enn'. -unfold strong_rec. -now apply H. Qed. -(*Section FixPoint. - -Variable a : A. -Variable f : N -> (N -> A) -> A. +Section FixPoint. -Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f. +Variable f : (N.t -> A) -> N.t -> A. +Variable f_wd : Proper ((N.eq==>Aeq)==>N.eq==>Aeq) f. -Let g (n : N) : A := strong_rec a f n. +Lemma strong_rec0_0 : forall a m, + (strong_rec0 a f 0 m) = a. +Proof. +intros. unfold strong_rec0. rewrite recursion_0; auto. +Qed. -Add Morphism g with signature Neq ==> Aeq as g_wd. +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 n1 n2 H. unfold g. now apply strong_rec_wd. +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 *. Qed. -Theorem NtoA_eq_sym : symmetric (N -> A) (fun_eq Neq Aeq). +Lemma strong_rec_0 : forall a, + Aeq (strong_rec a f 0) (f (fun _ => a) 0). Proof. -apply fun_eq_sym. -exact (proj2 (proj2 NZeq_equiv)). -exact (proj2 (proj2 Aeq_equiv)). +intros. rewrite strong_rec_alt, strong_rec0_succ. +apply f_wd; auto with *. +red; intros; rewrite strong_rec0_0; auto with *. Qed. -Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq). +(* We need an assumption saying that for every n, the step function (f h n) +calls h only on the segment [0 ... n - 1]. This means that if h1 and h2 +coincide on values < n, then (f h1 n) coincides with (f h2 n) *) + +Hypothesis step_good : + forall (n : N.t) (h1 h2 : N.t -> A), + (forall m : N.t, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f h1 n) (f h2 n). + +Lemma strong_rec0_more_steps : forall a k n m, m < n -> + Aeq (strong_rec0 a f n m) (strong_rec0 a f (n+k) m). Proof. -apply fun_eq_trans. -exact (proj1 NZeq_equiv). -exact (proj1 (proj2 NZeq_equiv)). -exact (proj1 (proj2 Aeq_equiv)). + intros a k n. pattern n. + apply induction; clear n. + + intros n n' Hn; setoid_rewrite Hn; auto with *. + + intros m Hm. destruct (nlt_0_r _ Hm). + + intros n IH m Hm. + rewrite lt_succ_r in Hm. + rewrite add_succ_l. + rewrite 2 strong_rec0_succ. + apply step_good. + intros m' Hm'. + apply IH. + apply lt_le_trans with m; auto. Qed. -Add Relation (N -> A) (fun_eq Neq Aeq) - symmetry proved by NtoA_eq_sym - transitivity proved by NtoA_eq_trans -as NtoA_eq_rel. +Lemma strong_rec0_fixpoint : forall (a : A) (n : N.t), + Aeq (strong_rec0 a f (S n) n) (f (fun n => strong_rec0 a f (S n) n) n). +Proof. +intros. +rewrite strong_rec0_succ. +apply step_good. +intros m Hm. +symmetry. +setoid_replace n with (S m + (n - S m)). +apply strong_rec0_more_steps. +apply lt_succ_diag_r. +rewrite add_comm. +symmetry. +apply sub_add. +rewrite le_succ_l; auto. +Qed. -Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph. +Theorem strong_rec_fixpoint : forall (a : A) (n : N.t), + Aeq (strong_rec a f n) (f (strong_rec a f) n). Proof. -apply f_wd. +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 *. +intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *. Qed. -(* We need an assumption saying that for every n, the step function (f n h) -calls h only on the segment [0 ... n - 1]. This means that if h1 and h2 -coincide on values < n, then (f n h1) coincides with (f n h2) *) +(** NB: without the [step_good] hypothesis, we have proved that + [strong_rec a f 0] is [f (fun _ => a) 0]. Now we can prove + that the first argument of [f] is arbitrary in this case... +*) -Hypothesis step_good : - forall (n : N) (h1 h2 : N -> A), - (forall m : N, m < n -> Aeq (h1 m) (h2 m)) -> Aeq (f n h1) (f n h2). +Theorem strong_rec_0_any : forall (a : A)(any : N.t->A), + Aeq (strong_rec a f 0) (f any 0). +Proof. +intros. +rewrite strong_rec_fixpoint. +apply step_good. +intros m Hm. destruct (nlt_0_r _ Hm). +Qed. -(* Todo: -Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g). +(** ... and that first argument of [strong_rec] is always arbitrary. *) + +Lemma strong_rec_any_fst_arg : forall a a' n, + Aeq (strong_rec a f n) (strong_rec a' f n). Proof. -apply induction. -unfold predicate_wd, fun_wd. -intros x y H. rewrite H. unfold fun_eq; apply g_wd. -reflexivity. -unfold g, strong_rec. -*) +intros a a' n. +generalize (le_refl n). +set (k:=n) at -2. clearbody k. revert k. pattern n. +apply induction; clear n. +(* compat *) +intros n n' Hn. setoid_rewrite Hn; auto with *. +(* 0 *) +intros k Hk. rewrite le_0_r in Hk. +rewrite Hk, strong_rec_0. symmetry. apply strong_rec_0_any. +(* S *) +intros n IH k Hk. +rewrite 2 strong_rec_fixpoint. +apply step_good. +intros m Hm. +apply IH. +rewrite succ_le_mono. +apply le_trans with k; auto. +rewrite le_succ_l; auto. +Qed. -End FixPoint.*) +End FixPoint. End StrongRecursion. Implicit Arguments strong_rec [A]. diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v index f67689dd..35d3b8aa 100644 --- a/theories/Numbers/Natural/Abstract/NSub.v +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -8,49 +8,33 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NSub.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id$ i*) Require Export NMulOrder. -Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig). -Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. +Module Type NSubPropFunct (Import N : NAxiomsSig'). +Include NMulOrderPropFunct N. -Theorem sub_wd : - forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 - m1 == n2 - m2. -Proof NZsub_wd. - -Theorem sub_0_r : forall n : N, n - 0 == n. -Proof NZsub_0_r. - -Theorem sub_succ_r : forall n m : N, n - (S m) == P (n - m). -Proof NZsub_succ_r. - -Theorem sub_1_r : forall n : N, n - 1 == P n. -Proof. -intro n; rewrite sub_succ_r; now rewrite sub_0_r. -Qed. - -Theorem sub_0_l : forall n : N, 0 - n == 0. +Theorem sub_0_l : forall n, 0 - n == 0. Proof. induct n. apply sub_0_r. intros n IH; rewrite sub_succ_r; rewrite IH. now apply pred_0. Qed. -Theorem sub_succ : forall n m : N, S n - S m == n - m. +Theorem sub_succ : forall n m, S n - S m == n - m. Proof. intro n; induct m. rewrite sub_succ_r. do 2 rewrite sub_0_r. now rewrite pred_succ. intros m IH. rewrite sub_succ_r. rewrite IH. now rewrite sub_succ_r. Qed. -Theorem sub_diag : forall n : N, n - n == 0. +Theorem sub_diag : forall n, n - n == 0. Proof. induct n. apply sub_0_r. intros n IH; rewrite sub_succ; now rewrite IH. Qed. -Theorem sub_gt : forall n m : N, n > m -> n - m ~= 0. +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. @@ -58,7 +42,7 @@ intro; rewrite sub_0_r; apply neq_succ_0. intros; now rewrite sub_succ. Qed. -Theorem add_sub_assoc : forall n m p : N, p <= m -> n + (m - p) == (n + m) - p. +Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p. Proof. intros n m p; induct p. intro; now do 2 rewrite sub_0_r. @@ -68,32 +52,32 @@ rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). reflexivity. Qed. -Theorem sub_succ_l : forall n m : N, n <= m -> S m - n == S (m - n). +Theorem sub_succ_l : forall n m, n <= m -> S m - n == S (m - n). Proof. intros n m H. rewrite <- (add_1_l m). rewrite <- (add_1_l (m - n)). symmetry; now apply add_sub_assoc. Qed. -Theorem add_sub : forall n m : N, (n + m) - m == n. +Theorem add_sub : forall n m, (n + m) - m == n. Proof. intros n m. rewrite <- add_sub_assoc by (apply le_refl). rewrite sub_diag; now rewrite add_0_r. Qed. -Theorem sub_add : forall n m : N, n <= m -> (m - n) + n == m. +Theorem sub_add : forall n m, n <= m -> (m - n) + n == m. Proof. intros n m H. rewrite add_comm. rewrite add_sub_assoc by assumption. rewrite add_comm. apply add_sub. Qed. -Theorem add_sub_eq_l : forall n m p : N, m + p == n -> n - m == p. +Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p. Proof. intros n m p H. symmetry. assert (H1 : m + p - m == n - m) by now rewrite H. rewrite add_comm in H1. now rewrite add_sub in H1. Qed. -Theorem add_sub_eq_r : forall n m p : N, m + p == n -> n - p == m. +Theorem add_sub_eq_r : forall n m p, m + p == n -> n - p == m. Proof. intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. Qed. @@ -101,7 +85,7 @@ Qed. (* This could be proved by adding m to both sides. Then the proof would use add_sub_assoc and sub_0_le, which is proven below. *) -Theorem add_sub_eq_nz : forall n m p : N, p ~= 0 -> n - m == p -> m + p == n. +Theorem add_sub_eq_nz : forall n m p, p ~= 0 -> n - m == p -> m + p == n. Proof. intros n m p H; double_induct n m. intros m H1; rewrite sub_0_l in H1. symmetry in H1; false_hyp H1 H. @@ -110,14 +94,14 @@ intros n m IH H1. rewrite sub_succ in H1. apply IH in H1. rewrite add_succ_l; now rewrite H1. Qed. -Theorem sub_add_distr : forall n m p : N, n - (m + p) == (n - m) - p. +Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p. Proof. intros n m; induct p. rewrite add_0_r; now rewrite sub_0_r. intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. Qed. -Theorem add_sub_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. +Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m. Proof. intros n m p H. rewrite (add_comm n m). @@ -127,7 +111,7 @@ Qed. (** Sub and order *) -Theorem le_sub_l : forall n m : N, n - m <= n. +Theorem le_sub_l : forall n m, n - m <= n. Proof. intro n; induct m. rewrite sub_0_r; now apply eq_le_incl. @@ -135,7 +119,7 @@ intros m IH. rewrite sub_succ_r. apply le_trans with (n - m); [apply le_pred_l | assumption]. Qed. -Theorem sub_0_le : forall n m : N, n - m == 0 <-> n <= m. +Theorem sub_0_le : forall n m, n - m == 0 <-> n <= m. Proof. double_induct n m. intro m; split; intro; [apply le_0_l | apply sub_0_l]. @@ -144,9 +128,86 @@ intro m; rewrite sub_0_r; split; intro H; intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. Qed. +Theorem sub_add_le : forall n m, n <= n - m + m. +Proof. +intros. +destruct (le_ge_cases n m) as [LE|GE]. +rewrite <- sub_0_le in LE. rewrite LE; nzsimpl. +now rewrite <- sub_0_le. +rewrite sub_add by assumption. apply le_refl. +Qed. + +Theorem le_sub_le_add_r : forall n m p, + n - p <= m <-> n <= m + p. +Proof. +intros n m p. +split; intros LE. +rewrite (add_le_mono_r _ _ p) in LE. +apply le_trans with (n-p+p); auto using sub_add_le. +destruct (le_ge_cases n p) as [LE'|GE]. +rewrite <- sub_0_le in LE'. rewrite LE'. apply le_0_l. +rewrite (add_le_mono_r _ _ p). now rewrite sub_add. +Qed. + +Theorem le_sub_le_add_l : forall n m p, n - m <= p <-> n <= m + p. +Proof. +intros n m p. rewrite add_comm; apply le_sub_le_add_r. +Qed. + +Theorem lt_sub_lt_add_r : forall n m p, + n - p < m -> n < m + p. +Proof. +intros n m p LT. +rewrite (add_lt_mono_r _ _ p) in LT. +apply le_lt_trans with (n-p+p); auto using sub_add_le. +Qed. + +(** Unfortunately, we do not have [n < m + p -> n - p < m]. + For instance [1<0+2] but not [1-2<0]. *) + +Theorem lt_sub_lt_add_l : forall n m p, n - m < p -> n < m + p. +Proof. +intros n m p. rewrite add_comm; apply lt_sub_lt_add_r. +Qed. + +Theorem le_add_le_sub_r : forall n m p, n + p <= m -> n <= m - p. +Proof. +intros n m p LE. +apply (add_le_mono_r _ _ p). +rewrite sub_add. assumption. +apply le_trans with (n+p); trivial. +rewrite <- (add_0_l p) at 1. rewrite <- add_le_mono_r. apply le_0_l. +Qed. + +(** Unfortunately, we do not have [n <= m - p -> n + p <= m]. + For instance [0<=1-2] but not [2+0<=1]. *) + +Theorem le_add_le_sub_l : forall n m p, n + p <= m -> p <= m - n. +Proof. +intros n m p. rewrite add_comm; apply le_add_le_sub_r. +Qed. + +Theorem lt_add_lt_sub_r : forall n m p, n + p < m <-> n < m - p. +Proof. +intros n m p. +destruct (le_ge_cases p m) as [LE|GE]. +rewrite <- (sub_add p m) at 1 by assumption. +now rewrite <- add_lt_mono_r. +assert (GE' := GE). rewrite <- sub_0_le in GE'; rewrite GE'. +split; intros LT. +elim (lt_irrefl m). apply le_lt_trans with (n+p); trivial. + rewrite <- (add_0_l m). apply add_le_mono. apply le_0_l. assumption. +now elim (nlt_0_r n). +Qed. + +Theorem lt_add_lt_sub_l : forall n m p, n + p < m <-> p < m - n. +Proof. +intros n m p. rewrite add_comm; apply lt_add_lt_sub_r. +Qed. + (** Sub and mul *) -Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. +Theorem mul_pred_r : forall n m, n * (P m) == n * m - n. Proof. intros n m; cases m. now rewrite pred_0, mul_0_r, sub_0_l. @@ -155,7 +216,7 @@ now rewrite sub_diag, add_0_r. now apply eq_le_incl. Qed. -Theorem mul_sub_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. +Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p. Proof. intros n m p; induct n. now rewrite sub_0_l, mul_0_l, sub_0_l. @@ -170,11 +231,72 @@ setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_l apply mul_0_l. Qed. -Theorem mul_sub_distr_l : forall n m p : N, p * (n - m) == p * n - p * m. +Theorem mul_sub_distr_l : forall n m p, p * (n - m) == p * n - p * m. Proof. intros n m p; rewrite (mul_comm p (n - m)), (mul_comm p n), (mul_comm p m). apply mul_sub_distr_r. Qed. +(** Alternative definitions of [<=] and [<] based on [+] *) + +Definition le_alt n m := exists p, p + n == m. +Definition lt_alt n m := exists p, S p + n == m. + +Lemma le_equiv : forall n m, le_alt n m <-> n <= m. +Proof. +split. +intros (p,H). rewrite <- H, add_comm. apply le_add_r. +intro H. exists (m-n). now apply sub_add. +Qed. + +Lemma lt_equiv : forall n m, lt_alt n m <-> n < m. +Proof. +split. +intros (p,H). rewrite <- H, add_succ_l, lt_succ_r, add_comm. apply le_add_r. +intro H. exists (m-S n). rewrite add_succ_l, <- add_succ_r. +apply sub_add. now rewrite le_succ_l. +Qed. + +Instance le_alt_wd : Proper (eq==>eq==>iff) le_alt. +Proof. + intros x x' Hx y y' Hy; unfold le_alt. + setoid_rewrite Hx. setoid_rewrite Hy. auto with *. +Qed. + +Instance lt_alt_wd : Proper (eq==>eq==>iff) lt_alt. +Proof. + intros x x' Hx y y' Hy; unfold lt_alt. + setoid_rewrite Hx. setoid_rewrite Hy. auto with *. +Qed. + +(** With these alternative definition, the dichotomy: + +[forall n m, n <= m \/ m <= n] + +becomes: + +[forall n m, (exists p, p + n == m) \/ (exists p, p + m == n)] + +We will need this in the proof of induction principle for integers +constructed as pairs of natural numbers. This formula can be proved +from know properties of [<=]. However, it can also be done directly. *) + +Theorem le_alt_dichotomy : forall n m, le_alt n m \/ le_alt m n. +Proof. +intros n m; induct n. +left; exists m; apply add_0_r. +intros n IH. +destruct IH as [[p H] | [p H]]. +destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. +rewrite add_0_l in H. right; exists (S 0); rewrite H, add_succ_l; + now rewrite add_0_l. +left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H. +right; exists (S p). rewrite add_succ_l; now rewrite H. +Qed. + +Theorem add_dichotomy : + forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). +Proof. exact le_alt_dichotomy. Qed. + End NSubPropFunct. |