diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAdd.v | 156 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAddOrder.v | 114 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 71 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 288 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NDefOps.v | 298 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 122 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMul.v | 87 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMulOrder.v | 131 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 539 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NStrongRec.v | 133 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NSub.v | 180 |
11 files changed, 2119 insertions, 0 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v new file mode 100644 index 00000000..f58b87d8 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAdd.v @@ -0,0 +1,156 @@ +(************************************************************************) +(* 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: NAdd.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NBase. + +Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NBasePropMod := NBasePropFunct NAxiomsMod. + +Open Local Scope NatScope. + +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. +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 + (apply -> neg_false; apply neq_succ_0). +setoid_replace (S n == 0) with False using relation iff 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'). +Proof. +intros n m; cases n. +split; intro H. +destruct H as [p H]. rewrite add_0_l in H; right; now exists p. +destruct H as [[n' H] | [m' H]]. +symmetry in H; false_hyp H neq_succ_0. +exists m'; now rewrite add_0_l. +intro n; split; intro H. +left; now exists n. +exists (n + m); now rewrite add_succ_l. +Qed. + +Theorem eq_add_1 : forall n m : N, + 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. +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. +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). +Proof. +intro n; induct m. +apply neq_symm. apply neq_succ_0. +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). +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). +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 new file mode 100644 index 00000000..7024fd00 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAddOrder.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* 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: NAddOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NOrder. + +Module NAddOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +Theorem add_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. +Proof NZadd_lt_mono_l. + +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. +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. +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. +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. +Proof. +intros; apply NZadd_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. +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). +Qed. + +End NAddOrderPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v new file mode 100644 index 00000000..750cc977 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -0,0 +1,71 @@ +(************************************************************************) +(* 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: NAxioms.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type NAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. + +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. + +Parameter Inline recursion : forall A : Type, A -> (N -> A -> A) -> N -> 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'). + +Axiom recursion_0 : + forall (A : Type) (a : A) (f : N -> 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)). + +(*Axiom dep_rec : + forall A : N -> Type, A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n.*) + +End NAxiomsSig. + diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v new file mode 100644 index 00000000..3e4032b5 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -0,0 +1,288 @@ +(************************************************************************) +(* 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: NBase.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export Decidable. +Require Export NAxioms. +Require Import NZMulOrder. (* The last property functor on NZ, which subsumes all others *) + +Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). + +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_symm : 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_symm : forall n m : N, n ~= m -> m ~= n. +Proof NZneq_symm. + +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 +function (by recursion) that maps 0 to false and the successor to true *) + +Definition if_zero (A : Set) (a b : A) (n : N) : A := + recursion a (fun _ _ => b) n. + +Add Parametric Morphism (A : Set) : (if_zero A) with signature (@eq _ ==> @eq _ ==> Neq ==> @eq _) as if_zero_wd. +Proof. +intros; unfold if_zero. apply recursion_wd with (Aeq := (@eq A)). +reflexivity. unfold fun2_eq; now intros. assumption. +Qed. + +Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A 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. +Proof. +intros; unfold if_zero. +now rewrite (@recursion_succ A (@eq A)); [| | unfold fun2_wd; now intros]. +Qed. + +Implicit Arguments if_zero [A]. + +Theorem neq_succ_0 : forall n : 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. +Qed. + +Theorem neq_0_succ : forall n : N, 0 ~= S n. +Proof. +intro n; apply neq_symm; apply neq_succ_0. +Qed. + +(* 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. +Proof. +NZinduct n. +now apply NZeq_le_incl. +intro n; split. +apply NZle_le_succ_r. +intro H; apply -> NZle_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. +Proof. +intros A A_wd A0 AS n; apply NZright_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 +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" +commands again, since the data for stepl and stepr tactics is inherited +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. +Proof. +intros; apply induction; auto. +Qed. + +Ltac cases n := induction_maker n ltac:(apply case_analysis). + +Theorem neq_0 : ~ forall n, n == 0. +Proof. +intro H; apply (neq_succ_0 0). apply H. +Qed. + +Theorem neq_0_r : forall n, n ~= 0 <-> exists m, n == S m. +Proof. +cases n. split; intro H; +[now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. +intro n; split; intro H; [now exists n | apply neq_succ_0]. +Qed. + +Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m. +Proof. +cases n. +now left. +intro n; right; now exists n. +Qed. + +Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1. +Proof. +cases n. +rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. +split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. +intro n. rewrite pred_succ. +setoid_replace (S n == 0) with False using relation iff by + (apply -> neg_false; apply neq_succ_0). +rewrite succ_inj_wd. tauto. +Qed. + +Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n. +Proof. +cases n. +intro H; elimtype False; 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. +Proof. +intros n m; cases n. +intros H; elimtype False; now apply H. +intros n _; cases m. +intros H; elimtype False; 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., +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. + +Theorem pair_induction : + A 0 -> A 1 -> + (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. +Proof. +intros until 3. +assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. +induct n; [ | intros n [IH1 IH2]]; auto. +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 *) +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. + +Theorem two_dim_induction : + R 0 0 -> + (forall n m, R n m -> R n (S m)) -> + (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. +Proof. +intros H1 H2 H3. induct n. +induct m. +exact H1. exact (H2 0). +intros n IH. induct m. +now apply H3. exact (H2 (S n)). +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. + +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. +Proof. +intros H1 H2 H3; induct n; auto. +intros n H; cases m; auto. +Qed. + +End DoubleInduction. + +Ltac double_induct n m := + try intros until n; + try intros until m; + pattern n, m; apply double_induction; clear n m; + [solve_relation_wd | | | ]. + +End NBasePropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v new file mode 100644 index 00000000..e15e4672 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -0,0 +1,298 @@ +(************************************************************************) +(* 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: NDefOps.v 11039 2008-06-02 23:26:13Z letouzey $ i*) + +Require Import Bool. (* To get the orb and negb function *) +Require Export NStrongRec. + +Module NdefOpsPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NStrongRecPropMod := NStrongRecPropFunct NAxiomsMod. +Open Local Scope NatScope. + +(*****************************************************) +(** Addition *) + +Definition def_add (x y : N) := recursion y (fun _ p => S p) x. + +Infix Local "++" := def_add (at level 50, left associativity). + +Add Morphism def_add with signature Neq ==> Neq ==> Neq as def_add_wd. +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. +Qed. + +Theorem def_add_0_l : forall y : N, 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). +Proof. +intros x y; unfold def_add. +rewrite (@recursion_succ N Neq); try reflexivity. +unfold fun2_wd. intros _ _ _ m1 m2 H2. now rewrite H2. +Qed. + +Theorem def_add_add : forall n m : N, n ++ m == n + m. +Proof. +intros n m; induct n. +now rewrite def_add_0_l, add_0_l. +intros n H. now rewrite def_add_succ_l, add_succ_l, H. +Qed. + +(*****************************************************) +(** Multiplication *) + +Definition def_mul (x y : N) := recursion 0 (fun _ p => p ++ x) y. + +Infix Local "**" := 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). +Proof. +unfold fun2_wd. 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. +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. +Qed. + +Theorem def_mul_0_r : forall x : N, 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. +Proof. +intros x y; unfold def_mul. +now rewrite (@recursion_succ N Neq); [| apply def_mul_step_wd |]. +Qed. + +Theorem def_mul_mul : forall n m : N, n ** m == n * m. +Proof. +intros n m; induct m. +now rewrite def_mul_0_r, mul_0_r. +intros m IH; now rewrite def_mul_succ_r, mul_succ_r, def_add_add, IH. +Qed. + +(*****************************************************) +(** Order *) + +Definition def_ltb (m : N) : N -> bool := +recursion + (if_zero false true) + (fun _ f => fun 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. + +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). +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. +Qed. + +Lemma lt_curry_wd : + forall m m' : N, m == m' -> fun_eq Neq (@eq bool) (def_ltb m) (def_ltb m'). +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. +Qed. + +Add Morphism def_ltb with signature Neq ==> Neq ==> (@eq bool) as def_ltb_wd. +Proof. +intros; now apply lt_curry_wd. +Qed. + +Theorem def_ltb_base : forall n : N, 0 << n = if_zero false true n. +Proof. +intro n; unfold def_ltb; now rewrite recursion_0. +Qed. + +Theorem def_ltb_step : + forall m n : 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. +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. +Proof. +cases n. +rewrite def_ltb_base; now rewrite if_zero_0. +intro n; rewrite def_ltb_step. now rewrite recursion_0. +Qed. + +Theorem def_ltb_0_succ : forall n : N, 0 << S n = true. +Proof. +intro n; rewrite def_ltb_base; now rewrite if_zero_succ. +Qed. + +Theorem succ_def_ltb_mono : forall n m : N, (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. +Qed. + +Theorem def_ltb_lt : forall n m : N, 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. +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. + +Add Morphism even with signature Neq ==> (@eq bool) as even_wd. +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. +Qed. + +Theorem even_0 : even 0 = true. +Proof. +unfold even. +now rewrite recursion_0. +Qed. + +Theorem even_succ : forall x : N, 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. +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. + +Definition half (x : N) := snd (half_aux x). + +Definition E2 := prod_rel Neq Neq. + +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_symm 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. + +Lemma half_step_wd: fun2_wd Neq E2 E2 (fun _ p => let (x1, x2) := p in ((S x2, x1))). +Proof. +unfold fun2_wd, E2, prod_rel. +intros _ _ _ p1 p2 [H1 H2]. +destruct p1; destruct p2; simpl in *. +now split; [rewrite H2 |]. +Qed. + +Add Morphism half with signature Neq ==> Neq as half_wd. +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). +Qed. + +(*****************************************************) +(** Logarithm for the base 2 *) + +Definition log (x : N) : N := +strong_rec 0 + (fun x g => + if (e x 0) then 0 + else if (e x 1) then 0 + else S (g (half x))) + x. + +Add Morphism log with signature Neq ==> Neq as log_wd. +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). +Qed. +*) +End NdefOpsPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v new file mode 100644 index 00000000..f6ccf3db --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -0,0 +1,122 @@ +(************************************************************************) +(* 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: NIso.v 10934 2008-05-15 21:58:20Z letouzey $ i*) + +Require Import NBase. + +Module Homomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module NBasePropMod2 := NBasePropFunct NAxiomsMod2. + +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 -> N2) : Prop := + f O1 == O2 /\ forall n : N1, f (S1 n) == S2 (f n). + +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. +Proof. +unfold natural_isomorphism. +intros n m Eqxy. +apply NAxiomsMod1.recursion_wd with (Aeq := Eq2). +reflexivity. +unfold fun2_eq. intros _ _ _ y' y'' H. now apply NBasePropMod2.succ_wd. +assumption. +Qed. + +Theorem natural_isomorphism_0 : natural_isomorphism O1 == O2. +Proof. +unfold natural_isomorphism; now rewrite NAxiomsMod1.recursion_0. +Qed. + +Theorem natural_isomorphism_succ : + forall n : N1, natural_isomorphism (S1 n) == S2 (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]. +Qed. + +Theorem hom_nat_iso : homomorphism natural_isomorphism. +Proof. +unfold homomorphism, natural_isomorphism; split; +[exact natural_isomorphism_0 | exact natural_isomorphism_succ]. +Qed. + +End Homomorphism. + +Module Inverse (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module Import NBasePropMod1 := NBasePropFunct NAxiomsMod1. +(* 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. + +Notation Local "n == m" := (NAxiomsMod1.Neq n m) (at level 70, no associativity). + +Lemma inverse_nat_iso : forall n : N1, h21 (h12 n) == n. +Proof. +induct n. +now rewrite Hom12.natural_isomorphism_0, Hom21.natural_isomorphism_0. +intros n IH. +now rewrite Hom12.natural_isomorphism_succ, Hom21.natural_isomorphism_succ, IH. +Qed. + +End Inverse. + +Module Isomorphism (NAxiomsMod1 NAxiomsMod2 : NAxiomsSig). + +Module Hom12 := Homomorphism NAxiomsMod1 NAxiomsMod2. +Module Hom21 := Homomorphism NAxiomsMod2 NAxiomsMod1. + +Module Inverse12 := Inverse NAxiomsMod1 NAxiomsMod2. +Module Inverse21 := Inverse NAxiomsMod2 NAxiomsMod1. + +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. + +Definition isomorphism (f1 : N1 -> N2) (f2 : N2 -> N1) : Prop := + Hom12.homomorphism f1 /\ Hom21.homomorphism f2 /\ + forall n : N1, Eq1 (f2 (f1 n)) n /\ + forall n : N2, Eq2 (f1 (f2 n)) n. + +Theorem iso_nat_iso : isomorphism h12 h21. +Proof. +unfold isomorphism. +split. apply Hom12.hom_nat_iso. +split. apply Hom21.hom_nat_iso. +split. apply Inverse12.inverse_nat_iso. +apply Inverse21.inverse_nat_iso. +Qed. + +End Isomorphism. + diff --git a/theories/Numbers/Natural/Abstract/NMul.v b/theories/Numbers/Natural/Abstract/NMul.v new file mode 100644 index 00000000..0b00f689 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMul.v @@ -0,0 +1,87 @@ +(************************************************************************) +(* 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 new file mode 100644 index 00000000..aa21fb50 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NMulOrder.v @@ -0,0 +1,131 @@ +(************************************************************************) +(* 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: NMulOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NAddOrder. + +Module NMulOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NAddOrderPropMod := NAddOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +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. + +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. +Proof. +intros n m; split; intro; +[apply NZsquare_lt_mono_nonneg | apply NZsquare_lt_simpl_nonneg]; +try assumption; apply le_0_l. +Qed. + +Theorem square_le_mono : forall n m : N, n <= m <-> n * n <= m * m. +Proof. +intros n m; split; intro; +[apply NZsquare_le_mono_nonneg | apply NZsquare_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. +Proof. +intros; apply NZmul_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. +Proof. +intros; apply NZmul_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. +Proof. +intros; apply NZmul_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. +Proof. +intros; apply NZmul_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. +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. +Qed. + +Notation mul_pos := lt_0_mul (only parsing). + +Theorem eq_mul_1 : forall n m : N, 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]]. +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). +rewrite H in H3; false_hyp H3 lt_irrefl. +Qed. + +End NMulOrderPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v new file mode 100644 index 00000000..826ffa2c --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -0,0 +1,539 @@ +(************************************************************************) +(* 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: NOrder.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NMul. + +Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NMulPropMod := NMulPropFunct NAxiomsMod. +Open Local Scope NatScope. + +(* 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. + +Theorem lt_wf_0 : well_founded lt. +Proof. +assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)). +intros x y; split. +intro H; split; [apply le_0_l | assumption]. now intros [_ H]. +rewrite H; apply lt_wf. +(* does not work: +setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*) +Qed. + +(* 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. +Proof. +intro n; apply -> le_ngt. apply le_0_l. +Qed. + +Theorem nle_succ_0 : forall n : 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. +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. +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. +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. +Proof. +cases n. +now left. +intro; right; apply lt_0_succ. +Qed. + +Theorem zero_one : forall n : N, n == 0 \/ n == 1 \/ 1 < n. +Proof. +induct n. now left. +cases n. intros; right; now left. +intros n IH. destruct IH as [H | [H | H]]. +false_hyp H neq_succ_0. +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. +Proof. +cases n. +split; intro; [reflexivity | apply lt_succ_diag_r]. +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. +Proof. +cases n. +split; intro; [now left | apply le_succ_diag_r]. +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. +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. +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. +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. + +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. +Proof. +intros Base Step; induct n. +intros; apply Base. +intros n IH m H. elim H using le_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply eq_le_incl. +intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. +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. +Proof. +intros Base Step; induct n. +intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. +rewrite H; apply Base. +intros n IH m H. elim H using lt_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply lt_succ_diag_r. +intros k H1 H2. apply lt_succ_l in H1. auto. +Qed. + +End RelElim. + +(** Predecessor and order *) + +Theorem succ_pred_pos : forall n : 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. +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. +Proof. +cases n. +intro H; elimtype False; 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. +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. +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 *) +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 *) +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. +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. +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 *) +Proof. +intros n m H; elim H using le_ind_rel. +solve_relation_wd. +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). +Proof. +intros n m H1; split; intro H2. +assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. +now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; +[apply <- succ_lt_mono | | |]. +assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). +apply 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. +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 *) +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 *) +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. +Proof. +intros n m; cases n. +rewrite pred_0. split; intro H; apply le_0_l. +intro n. rewrite pred_succ. apply succ_le_mono. +Qed. + +End NOrderPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v new file mode 100644 index 00000000..031dbdea --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NStrongRec.v @@ -0,0 +1,133 @@ +(************************************************************************) +(* 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: NStrongRec.v 11040 2008-06-03 00:04:16Z letouzey $ 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. + +Section StrongRecursion. + +Variable A : Set. +Variable Aeq : relation A. + +Notation Local "x ==A y" := (Aeq x y) (at level 70, no associativity). + +Hypothesis Aeq_equiv : equiv A Aeq. + +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_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. + +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'. +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. +now rewrite Enn'. +unfold strong_rec. +now apply H. +Qed. + +(*Section FixPoint. + +Variable a : A. +Variable f : N -> (N -> A) -> A. + +Hypothesis f_wd : fun2_wd Neq (fun_eq Neq Aeq) Aeq f. + +Let g (n : N) : A := strong_rec a f n. + +Add Morphism g with signature Neq ==> Aeq as g_wd. +Proof. +intros n1 n2 H. unfold g. now apply strong_rec_wd. +Qed. + +Theorem NtoA_eq_symm : symmetric (N -> A) (fun_eq Neq Aeq). +Proof. +apply fun_eq_symm. +exact (proj2 (proj2 NZeq_equiv)). +exact (proj2 (proj2 Aeq_equiv)). +Qed. + +Theorem NtoA_eq_trans : transitive (N -> A) (fun_eq Neq Aeq). +Proof. +apply fun_eq_trans. +exact (proj1 NZeq_equiv). +exact (proj1 (proj2 NZeq_equiv)). +exact (proj1 (proj2 Aeq_equiv)). +Qed. + +Add Relation (N -> A) (fun_eq Neq Aeq) + symmetry proved by NtoA_eq_symm + transitivity proved by NtoA_eq_trans +as NtoA_eq_rel. + +Add Morphism f with signature Neq ==> (fun_eq Neq Aeq) ==> Aeq as f_morph. +Proof. +apply f_wd. +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) *) + +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). + +(* Todo: +Theorem strong_rec_fixpoint : forall n : N, Aeq (g n) (f n g). +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. +*) + +End FixPoint.*) +End StrongRecursion. + +Implicit Arguments strong_rec [A]. + +End NStrongRecPropFunct. + diff --git a/theories/Numbers/Natural/Abstract/NSub.v b/theories/Numbers/Natural/Abstract/NSub.v new file mode 100644 index 00000000..f67689dd --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NSub.v @@ -0,0 +1,180 @@ +(************************************************************************) +(* 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: NSub.v 11040 2008-06-03 00:04:16Z letouzey $ i*) + +Require Export NMulOrder. + +Module NSubPropFunct (Import NAxiomsMod : NAxiomsSig). +Module Export NMulOrderPropMod := NMulOrderPropFunct NAxiomsMod. +Open Local Scope NatScope. + +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. +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. +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. +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. +Proof. +intros n m H; elim H using lt_ind_rel; clear n m H. +solve_relation_wd. +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. +Proof. +intros n m p; induct p. +intro; now do 2 rewrite sub_0_r. +intros p IH H. do 2 rewrite sub_succ_r. +rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). +rewrite add_pred_r by (apply sub_gt; now apply -> le_succ_l). +reflexivity. +Qed. + +Theorem sub_succ_l : forall n m : N, 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. +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. +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. +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. +Proof. +intros n m p H; rewrite add_comm in H; now apply add_sub_eq_l. +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. +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. +intro n; rewrite sub_0_r; now rewrite add_0_l. +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. +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. +Proof. +intros n m p H. +rewrite (add_comm n m). +rewrite <- add_sub_assoc by assumption. +now rewrite (add_comm m (n - p)). +Qed. + +(** Sub and order *) + +Theorem le_sub_l : forall n m : N, n - m <= n. +Proof. +intro n; induct m. +rewrite sub_0_r; now apply eq_le_incl. +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. +Proof. +double_induct n m. +intro m; split; intro; [apply le_0_l | apply sub_0_l]. +intro m; rewrite sub_0_r; split; intro H; +[false_hyp H neq_succ_0 | false_hyp H nle_succ_0]. +intros n m H. rewrite <- succ_le_mono. now rewrite sub_succ. +Qed. + +(** Sub and mul *) + +Theorem mul_pred_r : forall n m : N, n * (P m) == n * m - n. +Proof. +intros n m; cases m. +now rewrite pred_0, mul_0_r, sub_0_l. +intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc. +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. +Proof. +intros n m p; induct n. +now rewrite sub_0_l, mul_0_l, sub_0_l. +intros n IH. destruct (le_gt_cases m n) as [H | H]. +rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. +rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). +rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. +now apply <- add_cancel_l. +assert (H1 : S n <= m); [now apply <- le_succ_l |]. +setoid_replace (S n - m) with 0 by now apply <- sub_0_le. +setoid_replace ((S n * p) - m * p) with 0 by (apply <- sub_0_le; now apply mul_le_mono_r). +apply mul_0_l. +Qed. + +Theorem mul_sub_distr_l : forall n m p : N, 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. + +End NSubPropFunct. + |