From 3fbfcfd052fd7e007d50c8ee19e44525f80577ac Mon Sep 17 00:00:00 2001 From: emakarov Date: Tue, 24 Jul 2007 09:36:03 +0000 Subject: An update on axiomatization of numbers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10041 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Axioms/NMiscFunct.v | 44 +++++++++++++-- theories/Numbers/Natural/Axioms/NOrder.v | 64 ++++++++++++++++++---- theories/Numbers/Natural/Axioms/NPlus.v | 77 +++++++++++++++++++++++++++ theories/Numbers/Natural/Axioms/NPlusOrder.v | 2 +- theories/Numbers/Natural/Axioms/NTimes.v | 39 ++++++++++++++ theories/Numbers/Natural/Axioms/NTimesOrder.v | 2 +- theories/Numbers/Natural/Peano/NPeano.v | 71 ++++++++++++++++++++++-- 7 files changed, 277 insertions(+), 22 deletions(-) (limited to 'theories/Numbers/Natural') 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 !!! *) -- cgit v1.2.3