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/Integer/NatPairs/ZNatPairs.v | 108 ------------------- theories/Numbers/Integer/NatPairs/ZPairsAxioms.v | 132 +++++++++++++++++++++++ theories/Numbers/Integer/NatPairs/ZPairsPlus.v | 82 ++++++++++++++ theories/Numbers/Integer/NatPairs/ZPairsTimes.v | 37 +++++++ 4 files changed, 251 insertions(+), 108 deletions(-) delete mode 100644 theories/Numbers/Integer/NatPairs/ZNatPairs.v create mode 100644 theories/Numbers/Integer/NatPairs/ZPairsAxioms.v create mode 100644 theories/Numbers/Integer/NatPairs/ZPairsPlus.v create mode 100644 theories/Numbers/Integer/NatPairs/ZPairsTimes.v (limited to 'theories/Numbers/Integer') diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v deleted file mode 100644 index fb4b137d63..0000000000 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ /dev/null @@ -1,108 +0,0 @@ -Require Export NMinus. -Require Export NTimesOrder. -Require Export ZTimesOrder. - -Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature. -(* with Definition Z := - (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type - with Definition E := - fun p1 p2 => - NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)) - with Definition e := - fun p1 p2 => - NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*) - -Module Export NPlusPropertiesModule := NPlusProperties NPlusModule. -Open Local Scope NatScope. - -Definition Z : Set := (N * N)%type. -Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). -Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)). - -Delimit Scope IntScope with Int. -Bind Scope IntScope with Z. -Notation "x == y" := (E x y) (at level 70) : IntScope. -Notation "x # y" := (~ E x y) (at level 70) : IntScope. - -Theorem E_equiv_e : forall x y : Z, E x y <-> e x y. -Proof. -intros x y; unfold E, e; apply E_equiv_e. -Qed. - -Theorem E_equiv : equiv Z E. -Proof. -split; [| split]; unfold reflexive, symmetric, transitive, E. -(* reflexivity *) -now intro. -(* transitivity *) -intros x y z H1 H2. -apply plus_cancel_l with (p := fst y + snd y). -rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)). -rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)). -rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)). -rewrite (plus_comm (snd y) (fst z)). now apply plus_wd. -(* symmetry *) -now intros. -Qed. - -Add Relation Z E - reflexivity proved by (proj1 E_equiv) - symmetry proved by (proj2 (proj2 E_equiv)) - transitivity proved by (proj1 (proj2 E_equiv)) -as E_rel. - -End NatPairsDomain. - -Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature. -Module Export ZDomainModule := NatPairsDomain NPlusModule. -Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule. -Open Local Scope IntScope. - -Definition O : Z := (0, 0)%Nat. -Definition S (n : Z) := (NatModule.S (fst n), snd n). -Definition P (n : Z) := (fst n, NatModule.S (snd n)). -(* Unfortunately, we do not have P (S n) = n but only P (S n) == n. -It could be possible to consider as "canonical" only pairs where one of -the elements is 0, and make all operations convert canonical values into -other canonical values. We do not do this because this is more complex -and because we do not have the predecessor function on N at this point. *) - -Notation "0" := O : IntScope. - -Add Morphism S with signature E ==> E as S_wd. -Proof. -unfold S, E; intros n m H; simpl. -do 2 rewrite plus_Sn_m; now rewrite H. -Qed. - -Add Morphism P with signature E ==> E as P_wd. -Proof. -unfold P, E; intros n m H; simpl. -do 2 rewrite plus_n_Sm; now rewrite H. -Qed. - -Theorem S_inj : forall x y : Z, S x == S y -> x == y. -Proof. -unfold S, E; simpl; intros x y H. -do 2 rewrite plus_Sn_m in H. now apply S_inj in H. -Qed. - -Theorem S_P : forall x : Z, S (P x) == x. -Proof. -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 *. - - - - -Definition N_Z (n : nat) := nat_rec (fun _ : nat => Z) 0 (fun _ p => S p). - diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v new file mode 100644 index 0000000000..5f592dbcb9 --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v @@ -0,0 +1,132 @@ +Require Export NTimesOrder. +Require Export ZTimesOrder. + +Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature. +(* with Definition Z := + (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type + with Definition E := + fun p1 p2 => + NPM.NatModule.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)) + with Definition e := + fun p1 p2 => + NPM.NatModule.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*) + +Module Export NPlusPropertiesModule := NPlusProperties NPlusModule. +Open Local Scope NatScope. + +Definition Z : Set := (N * N)%type. +Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). +Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1)). + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Notation "x == y" := (E x y) (at level 70) : IntScope. +Notation "x # y" := (~ E x y) (at level 70) : IntScope. + +Theorem E_equiv_e : forall x y : Z, E x y <-> e x y. +Proof. +intros x y; unfold E, e; apply E_equiv_e. +Qed. + +Theorem E_equiv : equiv Z E. +Proof. +split; [| split]; unfold reflexive, symmetric, transitive, E. +(* reflexivity *) +now intro. +(* transitivity *) +intros x y z H1 H2. +apply plus_cancel_l with (p := fst y + snd y). +rewrite (plus_shuffle2 (fst y) (snd y) (fst x) (snd z)). +rewrite (plus_shuffle2 (fst y) (snd y) (fst z) (snd x)). +rewrite plus_comm. rewrite (plus_comm (snd y) (fst x)). +rewrite (plus_comm (snd y) (fst z)). now apply plus_wd. +(* symmetry *) +now intros. +Qed. + +Add Relation Z E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + 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. +Module Export ZDomainModule := NatPairsDomain NPlusModule. +Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule. +Open Local Scope IntScope. + +Definition O : Z := (0, 0)%Nat. +Definition S (n : Z) := (NatModule.S (fst n), snd n). +Definition P (n : Z) := (fst n, NatModule.S (snd n)). +(* Unfortunately, we do not have P (S n) = n but only P (S n) == n. +It could be possible to consider as "canonical" only pairs where one of +the elements is 0, and make all operations convert canonical values into +other canonical values. We do not do this because this is more complex +and because we do not have the predecessor function on N at this point. *) + +Notation "0" := O : IntScope. + +Add Morphism S with signature E ==> E as S_wd. +Proof. +unfold S, E; intros n m H; simpl. +do 2 rewrite plus_Sn_m; now rewrite H. +Qed. + +Add Morphism P with signature E ==> E as P_wd. +Proof. +unfold P, E; intros n m H; simpl. +do 2 rewrite plus_n_Sm; now rewrite H. +Qed. + +Theorem S_inj : forall x y : Z, S x == S y -> x == y. +Proof. +unfold S, E; simpl; intros x y H. +do 2 rewrite plus_Sn_m in H. now apply S_inj in H. +Qed. + +Theorem S_P : forall x : Z, S (P x) == x. +Proof. +intro x; unfold S, P, E; simpl. +rewrite plus_Sn_m; now rewrite plus_n_Sm. +Qed. + +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. + +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 0000000000..b69e4ce7d2 --- /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 0000000000..f5706276c9 --- /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. -- cgit v1.2.3