diff options
author | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-24 09:36:03 +0000 |
---|---|---|
committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-07-24 09:36:03 +0000 |
commit | 3fbfcfd052fd7e007d50c8ee19e44525f80577ac (patch) | |
tree | c9e98009b7629adcbbf7a8beecc3f860e5ba90cc /theories/Numbers | |
parent | 7c63540ea9ed995599aee1f835e4865c141a58b0 (diff) |
An update on axiomatization of numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsAxioms.v (renamed from theories/Numbers/Integer/NatPairs/ZNatPairs.v) | 44 | ||||
-rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsPlus.v | 82 | ||||
-rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsTimes.v | 37 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NMiscFunct.v | 44 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NOrder.v | 64 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NPlus.v | 77 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NPlusOrder.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NTimes.v | 39 | ||||
-rw-r--r-- | theories/Numbers/Natural/Axioms/NTimesOrder.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 71 | ||||
-rw-r--r-- | theories/Numbers/NumPrelude.v | 33 |
11 files changed, 462 insertions, 33 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v index fb4b137d6..5f592dbcb 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v @@ -1,4 +1,3 @@ -Require Export NMinus. Require Export NTimesOrder. Require Export ZTimesOrder. @@ -51,6 +50,13 @@ Add Relation Z E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. +Add Morphism (@pair N N) + with signature NDomainModule.E ==> NDomainModule.E ==> E + as pair_wd. +Proof. +intros x1 x2 H1 y1 y2 H2; unfold E; simpl; rewrite H1; now rewrite H2. +Qed. + End NatPairsDomain. Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature. @@ -93,16 +99,34 @@ intro x; unfold S, P, E; simpl. rewrite plus_Sn_m; now rewrite plus_n_Sm. Qed. -Theorem induction : - forall Q : Z -> Prop, - NumPrelude.pred_wd E Q -> Q 0 -> - (forall x, Q x -> Q (S x)) -> - (forall x, Q x -> Q (P x)) -> forall x, Q x. -Proof. -intros Q Q_wd Q0 QS QP x; unfold O, S, P in *. - +Section Induction. +Open Scope NatScope. (* automatically closes at the end of the section *) +Variable Q : Z -> Prop. +Hypothesis Q_wd : pred_wd E Q. +Add Morphism Q with signature E ==> iff as Q_morph. +Proof. +exact Q_wd. +Qed. +Theorem induction : + Q 0 -> (forall x, Q x -> Q (S x)) -> (forall x, Q x -> Q (P x)) -> forall x, Q x. +Proof. +intros Q0 QS QP x; unfold O, S, P, pred_wd, E in *. +destruct x as [n m]. +cut (forall p : N, Q (p, 0)); [intro H1 |]. +cut (forall p : N, Q (0, p)); [intro H2 |]. +destruct (plus_dichotomy n m) as [[p H] | [p H]]. +rewrite (Q_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2. +rewrite (Q_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1. +induct p. assumption. intros p IH. +replace 0 with (fst (0, p)); [| reflexivity]. +replace p with (snd (0, p)); [| reflexivity]. now apply QP. +induct p. assumption. intros p IH. +replace 0 with (snd (p, 0)); [| reflexivity]. +replace p with (fst (p, 0)); [| reflexivity]. now apply QS. +Qed. -Definition N_Z (n : nat) := nat_rec (fun _ : nat => Z) 0 (fun _ p => S p). +End Induction. +End NatPairsInt. diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v new file mode 100644 index 000000000..b69e4ce7d --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v @@ -0,0 +1,82 @@ +Require Export NTimesOrder. +Require Export ZTimesOrder. +Require Import ZPairsAxioms. + +Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature. +Module Export IntModule := NatPairsInt NPlusModule. +Open Local Scope NatScope. + +Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)). +Definition minus (x y : Z) := ((fst x) + (snd y), (snd x) + (fst y)). +Definition uminus (x : Z) := (snd x, fst x). +(* Unfortunately, the elements of pair keep increasing, even during subtraction *) + +Notation "x + y" := (plus x y) : IntScope. +Notation "x - y" := (minus x y) : IntScope. +Notation "- x" := (uminus x) : IntScope. + +(* Below, we need to rewrite subtems that have several occurrences. +Since with the currect setoid_rewrite we cannot point an accurrence +using pattern, we use symmetry tactic to make a particular occurrence +the leftmost, since that is what rewrite will use. *) +Add Morphism plus with signature E ==> E ==> E as plus_wd. +Proof. +unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl. +pose proof (plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 + (fst x2 + snd y2) (fst y2 + snd x2) H2) as H. +rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1. +Qed. + +Add Morphism minus with signature E ==> E ==> E as minus_wd. +Proof. +unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl. +rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2. +pose proof (NPlusModule.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 + (snd x2 + fst y2) (snd y2 + fst x2) H2) as H. +rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1. +Qed. + +Add Morphism uminus with signature E ==> E as uminus_wd. +Proof. +unfold E, plus; intros x y H; simpl. +rewrite plus_comm. symmetry. now rewrite plus_comm. +Qed. + +Open Local Scope IntScope. + +Theorem plus_0 : forall n, 0 + n == n. +Proof. +intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_n. +Qed. + +Theorem plus_S : forall n m, (S n) + m == S (n + m). +Proof. +intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_Sn_m. +Qed. + +Theorem minus_0 : forall n, n - 0 == n. +Proof. +intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r. +Qed. + +Theorem minus_S : forall n m, n - (S m) == P (n - m). +Proof. +intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_n_Sm. +Qed. + +Theorem uminus_0 : - 0 == 0. +Proof. +unfold uminus, E; simpl. now rewrite plus_0_n. +Qed. + +Theorem uminus_S : forall n, - (S n) == P (- n). +Proof. +reflexivity. +Qed. + +End NatPairsPlus. + +Module NatPairsPlusProperties (NPlusModule : NPlusSignature). +Module NatPairsPlusModule := NatPairsPlus NPlusModule. +Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule. +End NatPairsPlusProperties. diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v new file mode 100644 index 000000000..f5706276c --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v @@ -0,0 +1,37 @@ +Require Export ZPairsPlus. + +Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature. +Module Import ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *) +Open Local Scope NatScope. + +Definition times (n m : Z) := +(* let (n1, n2) := n in + let (m1, m2) := m in (n1 * m1 + n2 * m2, n1 * m2 + n2 * m1).*) + ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). + +Notation "x * y" := (times x y) : IntScope. + +Add Morphism times with signature E ==> E ==> E as times_wd. +Proof. +unfold times, E; intros x1 y1 H1 x2 y2 H2; simpl. +assert ((fst x1) + (fst y1) == (fst y1) + (fst x1)). +ring. + + +Axiom times_0 : forall n, n * 0 == 0. +Axiom times_S : forall n m, n * (S m) == n * m + n. + +(* Here recursion is done on the second argument to conform to the +usual definition of ordinal multiplication in set theory, which is not +commutative. It seems, however, that this definition in set theory is +unfortunate for two reasons. First, multiplication of two ordinals A +and B can be defined as (an order type of) the cartesian product B x A +(not A x B) ordered lexicographically. For example, omega * 2 = +2 x omega = {(0,0) < (0,1) < (0,2) < ... < (1,0) < (1,1) < (1,2) < ...}, +while 2 * omega = omega x 2 = {(0,0) < (0,1) < (1,0) < (1,1) < (2,0) < +(2,1) < ...} = omega. Secondly, the way the product 2 * 3 is said in +French (deux fois trois) and Russian (dvazhdy tri) implies 3 + 3, not +2 + 2 + 2. So it would possibly be more reasonable to define multiplication +(here as well as in set theory) by recursion on the first argument. *) + +End ZTimesSignature. diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v index 3b0c1c5eb..12cecca18 100644 --- a/theories/Numbers/Natural/Axioms/NMiscFunct.v +++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v @@ -91,7 +91,21 @@ Definition le (n m : N) := lt n m || e n m. Theorem le_lt : forall n m, le n m <-> lt n m \/ n == m. Proof. intros n m. rewrite E_equiv_e. unfold le. -do 4 rewrite eq_true_unfold. +do 3 rewrite eq_true_unfold. +assert (H : lt n m || e n m = true <-> lt n m = true \/ e n m = true). +split; [apply orb_prop | apply orb_true_intro]. +now rewrite H. +Qed. + +Theorem le_intro_left : forall n m, lt n m -> le n m. +Proof. +intros; rewrite le_lt; now left. +Qed. + +Theorem le_intro_right : forall n m, n == m -> le n m. +Proof. +intros; rewrite le_lt; now right. +Qed. Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true). unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_Set. @@ -129,6 +143,11 @@ Qed. as error "Impossible to unify", not just, e.g., "Cannot solve second-order unification problem". Something is probably wrong. *) +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Proof. +intros x1 x2 H1 x3 x4 H2; unfold le; rewrite H1; now rewrite H2. +Qed. + Theorem lt_base_eq : forall n, lt 0 n = if_zero false true n. Proof. intro n; unfold lt; now rewrite recursion_0. @@ -174,8 +193,9 @@ now unfold eq_bool. unfold fun2_wd; intros; now apply lt_wd. Qed. -Theorem lt_S : forall m n, lt m (S n) <-> lt m n \/ m == n. +Theorem lt_S : forall m n, lt m (S n) <-> le m n. Proof. +assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n). induct m. nondep_induct n; [split; intro; [now right | apply lt_0_1] | @@ -188,8 +208,8 @@ false_hyp H lt_0. false_hyp H S_0. intro m. pose proof (IH m) as H; clear IH. assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_Sn_Sm |]. assert (lt (S n) (S m) <-> lt n m); [apply lt_Sn_Sm |]. -assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|]. -tauto. +assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|]. tauto. +intros; rewrite le_lt; apply A. Qed. (*****************************************************) @@ -347,18 +367,32 @@ Module NDefaultOrderModule <: NOrderSignature. Module NatModule := NatMod. Definition lt := lt. +Definition le := le. Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. Proof. exact lt_wd. Qed. +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Proof. +exact le_wd. +Qed. + +(* This produces a warning about a morphism redeclaration. Why is not +there a warning after declaring lt? *) + +Theorem le_lt : forall x y, le x y <-> lt x y \/ x == y. +Proof. +exact le_lt. +Qed. + Theorem lt_0 : forall x, ~ (lt x 0). Proof. exact lt_0. Qed. -Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x == y. +Theorem lt_S : forall x y, lt x (S y) <-> le x y. Proof. exact lt_S. Qed. diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v index c4e9a21a7..08a6d44a8 100644 --- a/theories/Numbers/Natural/Axioms/NOrder.v +++ b/theories/Numbers/Natural/Axioms/NOrder.v @@ -9,6 +9,8 @@ Parameter Inline le : N -> N -> bool. Notation "x < y" := (lt x y) : NatScope. Notation "x <= y" := (le x y) : NatScope. +Notation "x > y" := (lt y x) (only parsing) : NatScope. +Notation "x >= y" := (le y x) (only parsing) : NatScope. Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. Add Morphism le with signature E ==> E ==> eq_bool as le_wd. @@ -62,7 +64,7 @@ Proof. induct n; [apply lt_n_Sn | intros x H; now apply lt_closed_S]. Qed. -Theorem lt_transitive : forall n m p, n < m -> m < p -> n < p. +Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. intros n m p; induct m. intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption]. @@ -72,12 +74,31 @@ apply IH; [assumption | apply lt_S_lt; assumption]. rewrite H1; apply lt_S_lt; assumption. Qed. +Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. +Proof. +intros n m p H1 H2; le_elim H1. +le_elim H2. le_intro1; now apply lt_trans with (m := m). +le_intro1; now rewrite <- H2. now rewrite H1. +Qed. + +Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. +Proof. +intros n m p H1 H2; le_elim H1. +now apply lt_trans with (m := m). now rewrite H1. +Qed. + +Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. +Proof. +intros n m p H1 H2; le_elim H2. +now apply lt_trans with (m := m). now rewrite <- H2. +Qed. + Theorem lt_positive : forall n m, n < m -> 0 < m. Proof. intros n m; induct n. trivial. intros x IH H. -apply lt_transitive with (m := S x); [apply lt_0_Sn | apply H]. +apply lt_trans with (m := S x); [apply lt_0_Sn | apply H]. Qed. Theorem lt_resp_S : forall n m, S n < S m <-> n < m. @@ -90,7 +111,7 @@ induct m. intro H; false_hyp H lt_0. intros x IH H. apply -> lt_S in H; le_elim H. -apply lt_transitive with (m := S x). +apply lt_trans with (m := S x). apply IH; assumption. apply lt_n_Sn. rewrite H; apply lt_n_Sn. @@ -109,7 +130,7 @@ split; intro H; [false_hyp H lt_0 | le_elim H; [false_hyp H lt_0 | false_hyp H S_0]]. intros m; split; intro H. apply -> lt_S in H. le_elim H; [le_intro1; now apply <- lt_resp_S | le_intro2; now apply S_wd]. -le_elim H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] | +le_elim H; [apply lt_trans with (m := S n); [apply lt_n_Sn | assumption] | apply S_inj in H; rewrite H; apply lt_n_Sn]. Qed. @@ -123,13 +144,20 @@ Proof. intros; le_intro1; now apply <- lt_le_S_l. Qed. -Theorem lt_irreflexive : forall n, ~ (n < n). +Theorem lt_irr : forall n, ~ (n < n). Proof. induct n. apply lt_0. intro x; unfold not; intros H1 H2; apply H1; now apply -> lt_resp_S. Qed. +Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m. +Proof. +intros n m H1 H2; le_elim H1; le_elim H2. +elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). +now symmetry. assumption. assumption. +Qed. + Theorem neq_0_lt : forall n, 0 # n -> 0 < n. Proof. induct n. @@ -144,10 +172,10 @@ intro H; absurd_hyp H; [apply lt_0 | assumption]. unfold not; intros; now apply S_0 with (n := n). Qed. -Theorem lt_asymmetric : forall n m, ~ (n < m /\ m < n). +Theorem lt_asymm : forall n m, ~ (n < m /\ m < n). Proof. unfold not; intros n m [H1 H2]. -now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|]. +now apply (lt_trans n m n) in H1; [false_hyp H1 lt_irr|]. Qed. Theorem le_0_l: forall n, 0 <= n. @@ -163,16 +191,30 @@ intros n IH. destruct IH as [H | H]. assert (H1 : S n <= m); [now apply -> lt_le_S_l | apply -> le_lt in H1; tauto]. destruct H as [H | H]. right; right; rewrite H; apply lt_n_Sn. -right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn]. +right; right; apply lt_trans with (m := n); [assumption | apply lt_n_Sn]. Qed. -Theorem lt_dichotomy : forall n m, n < m \/ ~ n < m. +(** The law of excluded middle for < *) +Theorem lt_em : forall n m, n < m \/ ~ n < m. Proof. intros n m; pose proof (lt_trichotomy n m) as H. destruct H as [H1 | H1]; [now left |]. destruct H1 as [H2 | H2]. -right; rewrite H2; apply lt_irreflexive. -right; intro; apply (lt_asymmetric n m); split; assumption. +right; rewrite H2; apply lt_irr. +right; intro; apply (lt_asymm n m); split; assumption. +Qed. + +Theorem not_lt : forall n m, ~ (n < m) <-> n >= m. +Proof. +intros n m; split; intro H. +destruct (lt_trichotomy n m) as [H1 | [H1 | H1]]. +false_hyp H1 H. rewrite H1; apply le_refl. now le_intro1. +intro; now apply (le_lt_trans m n m) in H; [false_hyp H lt_irr |]. +Qed. + +Theorem lt_or_ge : forall n m, n < m \/ n >= m. +Proof. +intros n m; rewrite <- not_lt; apply lt_em. Qed. Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v index 0ae12df97..d49794d28 100644 --- a/theories/Numbers/Natural/Axioms/NPlus.v +++ b/theories/Numbers/Natural/Axioms/NPlus.v @@ -112,6 +112,14 @@ intros n IH H. rewrite plus_Sn_m in H. absurd_hyp H; [|assumption]. unfold not; apply S_0. Qed. +Theorem plus_eq_S : + forall n m p, n + m == S p -> (exists n', n == S n') \/ (exists m', m == S m'). +Proof. +intros n m p; nondep_induct n. +intro H; rewrite plus_0_l in H; right; now exists p. +intros n _; left; now exists n. +Qed. + Theorem succ_plus_discr : forall n m, m # S (n + m). Proof. intro n; induct m. @@ -197,4 +205,73 @@ rewrite plus_Sn_m in H. apply S_inj in H. apply plus_eq_0 in H; split; [apply S_wd | ]; tauto. Qed. +(* One could define n <= m := exists p, p + n == m. Then we have +dichotomy: + +forall n m, n <= m \/ m <= n, + +i.e., + +forall n m, (exists p, p + n == m) \/ (exists p, 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 minus_plus from Minus.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 minus; it is enough to prove (1) +here. *) + +Theorem plus_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). +Proof. +intros n m; induct n. +left; exists m; apply plus_0_r. +intros n IH. +(* destruct IH as [p H | p H]. does not print a goal in ProofGeneral *) +destruct IH as [[p H] | [p H]]. +destruct (O_or_S p) as [H1 | [p' H1]]; rewrite H1 in H. +rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_Sn_m; now rewrite plus_0_l. +left; exists p'; rewrite plus_n_Sm; now rewrite plus_Sn_m in H. +right; exists (S p). rewrite plus_Sn_m; now rewrite H. +Qed. + +(* 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 * x + u == a * y + v -> x + y' == x' + y -> a * x' + u = a * y' + v (2) + +Here x + y' == x' + y represents equality of integers (x, y) and +(x', y'), since a pair of natural numbers represents their integer +difference. On integers, the (2) could be proved by moving +a * y to the left, factoring out a and replacing x - y by x' - y'. +However, the whole point is that we are only in the process of +constructing integers, so this has to be proved for natural numbers, +where we cannot move terms from one side of an equation to the other. +We first prove the special case of (2) where a == 1. *) + +Theorem plus_repl_pair : forall n m n' m' u v, + n + u == m + v -> n + m' == n' + m -> n' + u == m' + v. +Proof. +induct n. +intros m n' m' u v H1 H2. rewrite plus_0_l in H1. rewrite plus_0_l in H2. +rewrite H1; rewrite H2. now rewrite plus_assoc. +intros n IH m n' m' u v H1 H2. rewrite plus_Sn_m in H1. rewrite plus_Sn_m in H2. +assert (H : (exists m'', m == S m'') \/ ((exists v', v == S v') /\ (exists n'', n' == S n''))). +symmetry in H1; symmetry in H2; +destruct (plus_eq_S m v (n + u) H1); destruct (plus_eq_S n' m (n + m') H2). +now left. now left. right; now split. now left. +(* destruct H as [[m'' H] | [v' H3] [n'' H4]]. *) +(* The command above produces a warning and the PG does not show a goal !!! *) +destruct H as [[m'' H] | [[v' H3] [n'' H4]]]. +rewrite H in H1, H2. rewrite plus_Sn_m in H1; rewrite plus_n_Sm in H2. +apply S_inj in H1; apply S_inj in H2. now apply (IH m''). +rewrite H3; rewrite H4; rewrite plus_Sn_m; rewrite plus_n_Sm; apply S_wd. +rewrite H3 in H1; rewrite H4 in H2; rewrite plus_Sn_m in H2; rewrite plus_n_Sm in H1; +apply S_inj in H1; apply S_inj in H2. now apply (IH m). +Qed. + +(* The formula (2) will be proved in NTimes.v *) + End NPlusProperties. diff --git a/theories/Numbers/Natural/Axioms/NPlusOrder.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v index fe43ff38d..d152a0368 100644 --- a/theories/Numbers/Natural/Axioms/NPlusOrder.v +++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v @@ -34,7 +34,7 @@ Qed. Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. Proof. intros n m p q H1 H2. -apply lt_transitive with (m := m + p); +apply lt_trans with (m := m + p); [now apply plus_lt_compat_r | now apply plus_lt_compat_l]. Qed. diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v index 2dd052201..ed3498f1c 100644 --- a/theories/Numbers/Natural/Axioms/NTimes.v +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -1,3 +1,4 @@ +Require Import Ring. Require Export NPlus. Module Type NTimesSignature. @@ -160,4 +161,42 @@ apply plus_eq_0 in H; destruct H as [H1 H2]; apply plus_eq_0 in H2; destruct H2 as [H3 _]; rewrite H1; rewrite H3; now split. Qed. +(* See the notes on the theorem plus_repl_pair in NPlus.v *) + +Theorem plus_mult_repl_pair : forall a n m n' m' u v, + a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. +Proof. +induct a. +intros; repeat rewrite times_0_n in *; now repeat rewrite plus_0_n in *. +intros a IH n m n' m' u v H1 H2. +repeat rewrite times_Sn_m in *. +(*setoid_replace (n + a * n) with (a * n + n) in H1 by (apply plus_comm). +setoid_replace (m + a * m) with (a * m + m) in H1 by (apply plus_comm).*) +setoid_replace (n' + a * n') with (a * n' + n') by (apply plus_comm). +setoid_replace (m' + a * m') with (a * m' + m') by (apply plus_comm). +do 2 rewrite <- plus_assoc. apply IH with n m; [| assumption]. do 2 rewrite plus_assoc. +setoid_replace ((a * n) + n') with (n' + a * n) by (apply plus_comm). +setoid_replace (a * m + m') with (m' + a * m) by (apply plus_comm). +do 2 rewrite <- plus_assoc. apply plus_repl_pair with n m; [| assumption]. +now do 2 rewrite plus_assoc. +Qed. + +Theorem semi_ring : semi_ring_theory 0 (S 0) plus times E. +Proof. +constructor. +exact plus_0_l. +exact plus_comm. +exact plus_assoc. +exact mult_1_l. +exact mult_0_l. +exact mult_comm. +exact mult_assoc. +exact mult_plus_distr_r. +Qed. + +Add Ring SR : semi_ring. +Goal forall x y z : N, (x + y) * z == z * y + x * z. +intros. Set Printing All. ring. + + End NTimesProperties. diff --git a/theories/Numbers/Natural/Axioms/NTimesOrder.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v index f6afd5999..89ddcc7d4 100644 --- a/theories/Numbers/Natural/Axioms/NTimesOrder.v +++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v @@ -55,7 +55,7 @@ intros n m p q; induct n. intros; rewrite times_0_n; apply mult_positive; [assumption | apply lt_positive with (n := p); assumption]. intros x IH H1 H2. -apply lt_transitive with (m := ((S x) * q)). +apply lt_trans with (m := ((S x) * q)). now apply mult_S_lt_compat_l; assumption. now apply mult_lt_compat_r; [| apply lt_positive with (n := p)]. Qed. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 9927bde0b..0e07cd260 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,3 +1,5 @@ +Require Import Minus. + Require Export NDepRec. Require Export NTimesOrder. Require Export NMinus. @@ -150,35 +152,96 @@ Qed. End NPeanoTimes. -Module NPeanoLt <: NLtSignature. +Module NPeanoOrder <: NOrderSignature. Module Export NatModule := PeanoNat. Definition lt := lt_bool. +Definition le := le_bool. Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. Proof. unfold E, eq_bool; congruence. Qed. +Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Proof. +unfold E, eq_bool; congruence. +Qed. + +Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y. +Proof. +exact le_lt. +Qed. + Theorem lt_0 : forall x, ~ (lt x 0). Proof. exact lt_bool_0. Qed. -Theorem lt_S : forall x y, lt x (S y) <-> lt x y \/ x = y. +Theorem lt_S : forall x y, lt x (S y) <-> le x y. Proof. exact lt_bool_S. Qed. -End NPeanoLt. +End NPeanoOrder. Module NPeanoPred <: NPredSignature. +Module Export NatModule := PeanoNat. + +Definition P (n : nat) := +match n with +| 0 => 0 +| S n' => n' +end. + +Add Morphism P with signature E ==> E as P_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem P_0 : P 0 = 0. +Proof. +reflexivity. +Qed. + +Theorem P_S : forall n, P (S n) = n. +Proof. +now intro. +Qed. + +End NPeanoPred. + +Module NPeanoMinus <: NMinusSignature. +Module Export NPredModule := NPeanoPred. + +Definition minus := minus. + +Add Morphism minus with signature E ==> E ==> E as minus_wd. +Proof. +unfold E; congruence. +Qed. + +Theorem minus_0_r : forall n, n - 0 = n. +Proof. +now destruct n. +Qed. + +Theorem minus_S_r : forall n m, n - (S m) = P (n - m). +Proof. +induction n as [| n IH]; simpl. +now intro. +destruct m; simpl; [apply minus_0_r | apply IH]. +Qed. + +End NPeanoMinus. (* Obtaining properties for +, *, <, and their combinations *) -Module Export NPeanoTimesLtProperties := NTimesLtProperties NPeanoTimes NPeanoLt. +Module Export NPeanoTimesOrderProperties := NTimesOrderProperties NPeanoTimes NPeanoOrder. Module Export NPeanoDepRecTimesProperties := NDepRecTimesProperties NPeanoDepRec NPeanoTimes. +Module Export NPeanoMinusProperties := + NMinusProperties NPeanoMinus NPeanoPlus NPeanoOrder. Module MiscFunctModule := MiscFunctFunctor PeanoNat. (* The instruction above adds about 0.5M to the size of the .vo file !!! *) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index a23fb0bc0..b339fccf7 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -1,4 +1,5 @@ Require Export Setoid. +Require Import Bool. (* Contents: @@ -273,6 +274,13 @@ Proof. induction x; now simpl. Qed. +Theorem eq_nat_correct : forall x y, eq_nat_bool x y <-> x = y. +Proof. +intros; split. +now apply eq_nat_bool_implies_eq. +intro H; rewrite H; apply eq_nat_bool_refl. +Qed. + (* The boolean less function can be defined as fun n m => proj1_sig (nat_lt_ge_bool n m) using the standard library. @@ -292,15 +300,37 @@ match n, m with | _, 0 => false end. +Fixpoint le_bool (n m : nat) {struct n} : bool := +match n, m with +| 0, _ => true +| S n', S m' => le_bool n' m' +| S _, 0 => false +end. + (* The following properties are used both in Peano.v and in MPeano.v *) +Lemma le_lt_bool : forall x y, le_bool x y = (lt_bool x y) || (eq_nat_bool x y). +Proof. +induction x as [| x IH]; destruct y; simpl; (reflexivity || apply IH). +Qed. + +Theorem le_lt : forall x y, le_bool x y <-> lt_bool x y \/ x = y. +Proof. +intros x y. rewrite le_lt_bool. +setoid_replace (eq_true (lt_bool x y || eq_nat_bool x y)) with + (lt_bool x y = true \/ eq_nat_bool x y = true) using relation iff. +do 2 rewrite <- eq_true_unfold. now rewrite eq_nat_correct. +rewrite eq_true_unfold. split; [apply orb_prop | apply orb_true_intro]. +Qed. (* Can be simplified *) + Theorem lt_bool_0 : forall x, ~ (lt_bool x 0). Proof. destruct x as [|x]; simpl; now intro. Qed. -Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y. +Theorem lt_bool_S : forall x y, lt_bool x (S y) <-> le_bool x y. Proof. +assert (A : forall x y, lt_bool x (S y) <-> lt_bool x y \/ x = y). induction x as [| x IH]; destruct y as [| y]; simpl. split; [now right | now intro]. split; [now left | now intro]. @@ -308,6 +338,7 @@ split; [intro H; false_hyp H lt_bool_0 | intro H; destruct H as [H | H]; now auto]. assert (H : x = y <-> S x = S y); [split; auto|]. rewrite <- H; apply IH. +intros; rewrite le_lt; apply A. Qed. (** Miscellaneous *) |