diff options
Diffstat (limited to 'theories/Numbers/Integer/NatPairs/ZNatPairs.v')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 506 |
1 files changed, 205 insertions, 301 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 9427b37b..8b5624cd 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -8,400 +8,306 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: ZNatPairs.v 11674 2008-12-12 19:48:40Z letouzey $ i*) +(*i $Id$ i*) -Require Import NSub. (* The most complete file for natural numbers *) -Require Export ZMulOrder. (* The most complete file for integers *) +Require Import NProperties. (* The most complete file for N *) +Require Export ZProperties. (* The most complete file for Z *) Require Export Ring. -Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. -Module Import NPropMod := NSubPropFunct NAxiomsMod. (* Get all properties of natural numbers *) - -(* We do not declare ring in Natural/Abstract for two reasons. First, some -of the properties proved in NAdd and NMul are used in the new BinNat, -and it is in turn used in Ring. Using ring in Natural/Abstract would be -circular. It is possible, however, not to make BinNat dependent on -Numbers/Natural and prove the properties necessary for ring from scratch -(this is, of course, how it used to be). In addition, if we define semiring -structures in the implementation subdirectories of Natural, we are able to -specify binary natural numbers as the type of coefficients. For these -reasons we define an abstract semiring here. *) - -Open Local Scope NatScope. - -Lemma Nsemi_ring : semi_ring_theory 0 1 add mul Neq. -Proof. -constructor. -exact add_0_l. -exact add_comm. -exact add_assoc. -exact mul_1_l. -exact mul_0_l. -exact mul_comm. -exact mul_assoc. -exact mul_add_distr_r. -Qed. - -Add Ring NSR : Nsemi_ring. - -(* The definitios of functions (NZadd, NZmul, etc.) will be unfolded by -the properties functor. Since we don't want Zadd_comm to refer to unfolded -definitions of equality: fun p1 p2 : NZ => (fst p1 + snd p2) = (fst p2 + snd p1), -we will provide an extra layer of definitions. *) - -Definition Z := (N * N)%type. -Definition Z0 : Z := (0, 0). -Definition Zeq (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). -Definition Zsucc (n : Z) : Z := (S (fst n), snd n). -Definition Zpred (n : Z) : Z := (fst n, S (snd n)). - -(* We do not have Zpred (Zsucc n) = n but only Zpred (Zsucc 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. In that case, we could get rid of setoids and arrive at -integers as signed natural numbers. *) - -Definition Zadd (n m : Z) : Z := ((fst n) + (fst m), (snd n) + (snd m)). -Definition Zsub (n m : Z) : Z := ((fst n) + (snd m), (snd n) + (fst m)). - -(* Unfortunately, the elements of the pair keep increasing, even during -subtraction *) - -Definition Zmul (n m : Z) : Z := - ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). -Definition Zlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). -Definition Zle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). -Definition Zmin (n m : Z) := (min ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)). -Definition Zmax (n m : Z) := (max ((fst n) + (snd m)) ((fst m) + (snd n)), (snd n) + (snd m)). - -Delimit Scope IntScope with Int. -Bind Scope IntScope with Z. -Notation "x == y" := (Zeq x y) (at level 70) : IntScope. -Notation "x ~= y" := (~ Zeq x y) (at level 70) : IntScope. -Notation "0" := Z0 : IntScope. -Notation "1" := (Zsucc Z0) : IntScope. -Notation "x + y" := (Zadd x y) : IntScope. -Notation "x - y" := (Zsub x y) : IntScope. -Notation "x * y" := (Zmul x y) : IntScope. -Notation "x < y" := (Zlt x y) : IntScope. -Notation "x <= y" := (Zle x y) : IntScope. -Notation "x > y" := (Zlt y x) (only parsing) : IntScope. -Notation "x >= y" := (Zle y x) (only parsing) : IntScope. - -Notation Local N := NZ. -(* To remember N without having to use a long qualifying name. since NZ will be redefined *) -Notation Local NE := NZeq (only parsing). -Notation Local add_wd := NZadd_wd (only parsing). - -Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. -Module Export NZAxiomsMod <: NZAxiomsSig. - -Definition NZ : Type := Z. -Definition NZeq := Zeq. -Definition NZ0 := Z0. -Definition NZsucc := Zsucc. -Definition NZpred := Zpred. -Definition NZadd := Zadd. -Definition NZsub := Zsub. -Definition NZmul := Zmul. - -Theorem ZE_refl : reflexive Z Zeq. -Proof. -unfold reflexive, Zeq. reflexivity. -Qed. - -Theorem ZE_sym : symmetric Z Zeq. -Proof. -unfold symmetric, Zeq; now symmetry. -Qed. - -Theorem ZE_trans : transitive Z Zeq. -Proof. -unfold transitive, Zeq. intros n m p H1 H2. -assert (H3 : (fst n + snd m) + (fst m + snd p) == (fst m + snd n) + (fst p + snd m)) -by now apply add_wd. -stepl ((fst n + snd p) + (fst m + snd m)) in H3 by ring. -stepr ((fst p + snd n) + (fst m + snd m)) in H3 by ring. -now apply -> add_cancel_r in H3. +Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. +Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. +Open Local Scope pair_scope. + +Module ZPairsAxiomsMod (Import N : NAxiomsSig) <: ZAxiomsSig. +Module Import NPropMod := NPropFunct N. (* Get all properties of N *) + +Delimit Scope NScope with N. +Bind Scope NScope with N.t. +Infix "==" := N.eq (at level 70) : NScope. +Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope. +Notation "0" := N.zero : NScope. +Notation "1" := (N.succ N.zero) : NScope. +Infix "+" := N.add : NScope. +Infix "-" := N.sub : NScope. +Infix "*" := N.mul : NScope. +Infix "<" := N.lt : NScope. +Infix "<=" := N.le : NScope. +Local Open Scope NScope. + +(** The definitions of functions ([add], [mul], etc.) will be unfolded + by the properties functor. Since we don't want [add_comm] to refer + to unfolded definitions of equality: [fun p1 p2 => (fst p1 + + snd p2) = (fst p2 + snd p1)], we will provide an extra layer of + definitions. *) + +Module Z. + +Definition t := (N.t * N.t)%type. +Definition zero : t := (0, 0). +Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2). +Definition succ (n : t) : t := (N.succ n#1, n#2). +Definition pred (n : t) : t := (n#1, N.succ n#2). +Definition opp (n : t) : t := (n#2, n#1). +Definition add (n m : t) : t := (n#1 + m#1, n#2 + m#2). +Definition sub (n m : t) : t := (n#1 + m#2, n#2 + m#1). +Definition mul (n m : t) : t := + (n#1 * m#1 + n#2 * m#2, n#1 * m#2 + n#2 * m#1). +Definition lt (n m : t) := n#1 + m#2 < m#1 + n#2. +Definition le (n m : t) := n#1 + m#2 <= m#1 + n#2. +Definition min (n m : t) : t := (min (n#1 + m#2) (m#1 + n#2), n#2 + m#2). +Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). + +(** NB : We do not have [Zpred (Zsucc n) = n] but only [Zpred (Zsucc 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. In that case, we + could get rid of setoids and arrive at integers as signed natural + numbers. *) + +(** NB : Unfortunately, the elements of the pair keep increasing during + many operations, even during subtraction. *) + +End Z. + +Delimit Scope ZScope with Z. +Bind Scope ZScope with Z.t. +Infix "==" := Z.eq (at level 70) : ZScope. +Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope. +Notation "0" := Z.zero : ZScope. +Notation "1" := (Z.succ Z.zero) : ZScope. +Infix "+" := Z.add : ZScope. +Infix "-" := Z.sub : ZScope. +Infix "*" := Z.mul : ZScope. +Notation "- x" := (Z.opp x) : ZScope. +Infix "<" := Z.lt : ZScope. +Infix "<=" := Z.le : ZScope. +Local Open Scope ZScope. + +Lemma sub_add_opp : forall n m, Z.sub n m = Z.add n (Z.opp m). +Proof. reflexivity. Qed. + +Instance eq_equiv : Equivalence Z.eq. +Proof. +split. +unfold Reflexive, Z.eq. reflexivity. +unfold Symmetric, Z.eq; now symmetry. +unfold Transitive, Z.eq. intros (n1,n2) (m1,m2) (p1,p2) H1 H2; simpl in *. +apply (add_cancel_r _ _ (m1+m2)%N). +rewrite add_shuffle2, H1, add_shuffle1, H2. +now rewrite add_shuffle1, (add_comm m1). +Qed. + +Instance pair_wd : Proper (N.eq==>N.eq==>Z.eq) (@pair N.t N.t). +Proof. +intros n1 n2 H1 m1 m2 H2; unfold Z.eq; simpl; now rewrite H1, H2. +Qed. + +Instance succ_wd : Proper (Z.eq ==> Z.eq) Z.succ. +Proof. +unfold Z.succ, Z.eq; intros n m H; simpl. +do 2 rewrite add_succ_l; now rewrite H. Qed. -Theorem NZeq_equiv : equiv Z Zeq. +Instance pred_wd : Proper (Z.eq ==> Z.eq) Z.pred. Proof. -unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_sym]. -Qed. - -Add Relation Z Zeq - reflexivity proved by (proj1 NZeq_equiv) - symmetry proved by (proj2 (proj2 NZeq_equiv)) - transitivity proved by (proj1 (proj2 NZeq_equiv)) -as NZeq_rel. - -Add Morphism (@pair N N) with signature NE ==> NE ==> Zeq as Zpair_wd. -Proof. -intros n1 n2 H1 m1 m2 H2; unfold Zeq; simpl; rewrite H1; now rewrite H2. +unfold Z.pred, Z.eq; intros n m H; simpl. +do 2 rewrite add_succ_r; now rewrite H. Qed. -Add Morphism NZsucc with signature Zeq ==> Zeq as NZsucc_wd. +Instance add_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.add. Proof. -unfold NZsucc, Zeq; intros n m H; simpl. -do 2 rewrite add_succ_l; now rewrite H. +unfold Z.eq, Z.add; intros n1 m1 H1 n2 m2 H2; simpl. +now rewrite add_shuffle1, H1, H2, add_shuffle1. Qed. -Add Morphism NZpred with signature Zeq ==> Zeq as NZpred_wd. +Instance opp_wd : Proper (Z.eq ==> Z.eq) Z.opp. Proof. -unfold NZpred, Zeq; intros n m H; simpl. -do 2 rewrite add_succ_r; now rewrite H. +unfold Z.eq, Z.opp; intros (n1,n2) (m1,m2) H; simpl in *. +now rewrite (add_comm n2), (add_comm m2). Qed. -Add Morphism NZadd with signature Zeq ==> Zeq ==> Zeq as NZadd_wd. +Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub. Proof. -unfold Zeq, NZadd; intros n1 m1 H1 n2 m2 H2; simpl. -assert (H3 : (fst n1 + snd m1) + (fst n2 + snd m2) == (fst m1 + snd n1) + (fst m2 + snd n2)) -by now apply add_wd. -stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. -now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. +intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp. +apply add_wd, opp_wd; auto. Qed. -Add Morphism NZsub with signature Zeq ==> Zeq ==> Zeq as NZsub_wd. +Lemma mul_comm : forall n m, n*m == m*n. Proof. -unfold Zeq, NZsub; intros n1 m1 H1 n2 m2 H2; simpl. -symmetry in H2. -assert (H3 : (fst n1 + snd m1) + (fst m2 + snd n2) == (fst m1 + snd n1) + (fst n2 + snd m2)) -by now apply add_wd. -stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. -now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. +intros (n1,n2) (m1,m2); compute. +rewrite (add_comm (m1*n2)%N). +apply N.add_wd; apply N.add_wd; apply mul_comm. Qed. -Add Morphism NZmul with signature Zeq ==> Zeq ==> Zeq as NZmul_wd. +Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul. Proof. -unfold NZmul, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. -stepl (fst n1 * fst n2 + (snd n1 * snd n2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. -stepr (fst n1 * snd n2 + (fst m1 * fst m2 + snd m1 * snd m2 + snd n1 * fst n2)) by ring. -apply add_mul_repl_pair with (n := fst m2) (m := snd m2); [| now idtac]. -stepl (snd n1 * snd n2 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. -stepr (snd n1 * fst n2 + (fst n1 * snd m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. -apply add_mul_repl_pair with (n := snd m2) (m := fst m2); -[| (stepl (fst n2 + snd m2) by ring); now stepr (fst m2 + snd n2) by ring]. -stepl (snd m2 * snd n1 + (fst n1 * fst m2 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. -stepr (snd m2 * fst n1 + (snd n1 * fst m2 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. -apply add_mul_repl_pair with (n := snd m1) (m := fst m1); -[ | (stepl (fst n1 + snd m1) by ring); now stepr (fst m1 + snd n1) by ring]. -stepl (fst m2 * fst n1 + (snd m2 * snd m1 + fst m1 * snd m2 + snd m1 * fst m2)) by ring. -stepr (fst m2 * snd n1 + (snd m2 * fst m1 + fst m1 * fst m2 + snd m1 * snd m2)) by ring. -apply add_mul_repl_pair with (n := fst m1) (m := snd m1); [| now idtac]. -ring. +assert (forall n, Proper (Z.eq ==> Z.eq) (Z.mul n)). + unfold Z.mul, Z.eq. intros (n1,n2) (p1,p2) (q1,q2) H; simpl in *. + rewrite add_shuffle1, (add_comm (n1*p1)%N). + symmetry. rewrite add_shuffle1. + rewrite <- ! mul_add_distr_l. + rewrite (add_comm p2), (add_comm q2), H. + reflexivity. +intros n n' Hn m m' Hm. +rewrite Hm, (mul_comm n), (mul_comm n'), Hn. +reflexivity. Qed. Section Induction. -Open Scope NatScope. (* automatically closes at the end of the section *) -Variable A : Z -> Prop. -Hypothesis A_wd : predicate_wd Zeq A. +Variable A : Z.t -> Prop. +Hypothesis A_wd : Proper (Z.eq==>iff) A. -Add Morphism A with signature Zeq ==> iff as A_morph. +Theorem bi_induction : + A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n. Proof. -exact A_wd. -Qed. - -Theorem NZinduction : - A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) -Proof. -intros A0 AS n; unfold NZ0, Zsucc, predicate_wd, fun_wd, Zeq in *. +intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *. destruct n as [n m]. -cut (forall p : N, A (p, 0)); [intro H1 |]. -cut (forall p : N, A (0, p)); [intro H2 |]. +cut (forall p, A (p, 0%N)); [intro H1 |]. +cut (forall p, A (0%N, p)); [intro H2 |]. destruct (add_dichotomy n m) as [[p H] | [p H]]. -rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm). +rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm). apply H2. -rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1. +rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1. induct p. assumption. intros p IH. -apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite add_0_l, add_1_l]. +apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l]. now apply <- AS. induct p. assumption. intros p IH. -replace 0 with (snd (p, 0)); [| reflexivity]. -replace (S p) with (S (fst (p, 0))); [| reflexivity]. now apply -> AS. +replace 0%N with (snd (p, 0%N)); [| reflexivity]. +replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS. Qed. End Induction. (* Time to prove theorems in the language of Z *) -Open Local Scope IntScope. - -Theorem NZpred_succ : forall n : Z, Zpred (Zsucc n) == n. +Theorem pred_succ : forall n, Z.pred (Z.succ n) == n. Proof. -unfold NZpred, NZsucc, Zeq; intro n; simpl. -rewrite add_succ_l; now rewrite add_succ_r. +unfold Z.pred, Z.succ, Z.eq; intro n; simpl; now nzsimpl. Qed. -Theorem NZadd_0_l : forall n : Z, 0 + n == n. +Theorem succ_pred : forall n, Z.succ (Z.pred n) == n. Proof. -intro n; unfold NZadd, Zeq; simpl. now do 2 rewrite add_0_l. +intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl. Qed. -Theorem NZadd_succ_l : forall n m : Z, (Zsucc n) + m == Zsucc (n + m). +Theorem opp_0 : - 0 == 0. Proof. -intros n m; unfold NZadd, Zeq; simpl. now do 2 rewrite add_succ_l. +unfold Z.opp, Z.eq; simpl. now nzsimpl. Qed. -Theorem NZsub_0_r : forall n : Z, n - 0 == n. +Theorem opp_succ : forall n, - (Z.succ n) == Z.pred (- n). Proof. -intro n; unfold NZsub, Zeq; simpl. now do 2 rewrite add_0_r. -Qed. - -Theorem NZsub_succ_r : forall n m : Z, n - (Zsucc m) == Zpred (n - m). -Proof. -intros n m; unfold NZsub, Zeq; simpl. symmetry; now rewrite add_succ_r. +reflexivity. Qed. -Theorem NZmul_0_l : forall n : Z, 0 * n == 0. +Theorem add_0_l : forall n, 0 + n == n. Proof. -intro n; unfold NZmul, Zeq; simpl. -repeat rewrite mul_0_l. now rewrite add_assoc. +intro n; unfold Z.add, Z.eq; simpl. now nzsimpl. Qed. -Theorem NZmul_succ_l : forall n m : Z, (Zsucc n) * m == n * m + m. +Theorem add_succ_l : forall n m, (Z.succ n) + m == Z.succ (n + m). Proof. -intros n m; unfold NZmul, NZsucc, Zeq; simpl. -do 2 rewrite mul_succ_l. ring. +intros n m; unfold Z.add, Z.eq; simpl. now nzsimpl. Qed. -End NZAxiomsMod. - -Definition NZlt := Zlt. -Definition NZle := Zle. -Definition NZmin := Zmin. -Definition NZmax := Zmax. - -Add Morphism NZlt with signature Zeq ==> Zeq ==> iff as NZlt_wd. +Theorem sub_0_r : forall n, n - 0 == n. Proof. -unfold NZlt, Zlt, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. -stepr (snd m1 + fst m2) by apply add_comm. -apply (add_lt_repl_pair (fst n1) (snd n1)); [| assumption]. -stepl (snd m2 + fst n1) by apply add_comm. -stepr (fst m2 + snd n1) by apply add_comm. -apply (add_lt_repl_pair (snd n2) (fst n2)). -now stepl (fst n1 + snd n2) by apply add_comm. -stepl (fst m2 + snd n2) by apply add_comm. now stepr (fst n2 + snd m2) by apply add_comm. -stepr (snd n1 + fst n2) by apply add_comm. -apply (add_lt_repl_pair (fst m1) (snd m1)); [| now symmetry]. -stepl (snd n2 + fst m1) by apply add_comm. -stepr (fst n2 + snd m1) by apply add_comm. -apply (add_lt_repl_pair (snd m2) (fst m2)). -now stepl (fst m1 + snd m2) by apply add_comm. -stepl (fst n2 + snd m2) by apply add_comm. now stepr (fst m2 + snd n2) by apply add_comm. +intro n; unfold Z.sub, Z.eq; simpl. now nzsimpl. Qed. -Add Morphism NZle with signature Zeq ==> Zeq ==> iff as NZle_wd. +Theorem sub_succ_r : forall n m, n - (Z.succ m) == Z.pred (n - m). Proof. -unfold NZle, Zle, Zeq; intros n1 m1 H1 n2 m2 H2; simpl. -do 2 rewrite lt_eq_cases. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2)%Int. -fold (n1 == n2)%Int (m1 == m2)%Int; fold (n1 == m1)%Int in H1; fold (n2 == m2)%Int in H2. -now rewrite H1, H2. +intros n m; unfold Z.sub, Z.eq; simpl. symmetry; now rewrite add_succ_r. Qed. -Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd. +Theorem mul_0_l : forall n, 0 * n == 0. Proof. -intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl. -destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. -rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. -rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by -now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). -stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. -unfold Zeq in H1. rewrite H1. ring. -rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. -rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by -now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). -stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. -unfold Zeq in H2. rewrite H2. ring. +intros (n1,n2); unfold Z.mul, Z.eq; simpl; now nzsimpl. Qed. -Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd. +Theorem mul_succ_l : forall n m, (Z.succ n) * m == n * m + m. Proof. -intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl. -destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H]. -rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. -rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by -now apply -> (NZle_wd n1 m1 H1 n2 m2 H2). -stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring. -unfold Zeq in H2. rewrite H2. ring. -rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption. -rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by -now apply -> (NZle_wd n2 m2 H2 n1 m1 H1). -stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring. -unfold Zeq in H1. rewrite H1. ring. +intros (n1,n2) (m1,m2); unfold Z.mul, Z.succ, Z.eq; simpl; nzsimpl. +rewrite <- (add_assoc _ m1), (add_comm m1), (add_assoc _ _ m1). +now rewrite <- (add_assoc _ m2), (add_comm m2), (add_assoc _ (n2*m1)%N m2). Qed. -Open Local Scope IntScope. +(** Order *) -Theorem NZlt_eq_cases : forall n m : Z, n <= m <-> n < m \/ n == m. +Lemma lt_eq_cases : forall n m, n<=m <-> n<m \/ n==m. Proof. -intros n m; unfold Zlt, Zle, Zeq; simpl. apply lt_eq_cases. +intros; apply N.lt_eq_cases. Qed. -Theorem NZlt_irrefl : forall n : Z, ~ (n < n). +Theorem lt_irrefl : forall n, ~ (n < n). Proof. -intros n; unfold Zlt, Zeq; simpl. apply lt_irrefl. +intros; apply N.lt_irrefl. Qed. -Theorem NZlt_succ_r : forall n m : Z, n < (Zsucc m) <-> n <= m. +Theorem lt_succ_r : forall n m, n < (Z.succ m) <-> n <= m. Proof. -intros n m; unfold Zlt, Zle, Zeq; simpl. rewrite add_succ_l; apply lt_succ_r. +intros n m; unfold Z.lt, Z.le, Z.eq; simpl; nzsimpl. apply lt_succ_r. Qed. -Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n. +Theorem min_l : forall n m, n <= m -> Z.min n m == n. Proof. -unfold Zmin, Zle, Zeq; simpl; intros n m H. -rewrite min_l by assumption. ring. +unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *. +rewrite min_l by assumption. +now rewrite <- add_assoc, (add_comm m2). Qed. -Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m. +Theorem min_r : forall n m, m <= n -> Z.min n m == m. Proof. -unfold Zmin, Zle, Zeq; simpl; intros n m H. -rewrite min_r by assumption. ring. +unfold Z.min, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *. +rewrite min_r by assumption. +now rewrite add_assoc. Qed. -Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n. +Theorem max_l : forall n m, m <= n -> Z.max n m == n. Proof. -unfold Zmax, Zle, Zeq; simpl; intros n m H. -rewrite max_l by assumption. ring. +unfold Z.max, Z.le, Z.eq; simpl; intros (n1,n2) (m1,m2) H; simpl in *. +rewrite max_l by assumption. +now rewrite <- add_assoc, (add_comm m2). Qed. -Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m. +Theorem max_r : forall n m, n <= m -> Z.max n m == m. Proof. -unfold Zmax, Zle, Zeq; simpl; intros n m H. -rewrite max_r by assumption. ring. +unfold Z.max, Z.le, Z.eq; simpl; intros n m H. +rewrite max_r by assumption. +now rewrite add_assoc. Qed. -End NZOrdAxiomsMod. - -Definition Zopp (n : Z) : Z := (snd n, fst n). - -Notation "- x" := (Zopp x) : IntScope. - -Add Morphism Zopp with signature Zeq ==> Zeq as Zopp_wd. -Proof. -unfold Zeq; intros n m H; simpl. symmetry. -stepl (fst n + snd m) by apply add_comm. -now stepr (fst m + snd n) by apply add_comm. -Qed. - -Open Local Scope IntScope. - -Theorem Zsucc_pred : forall n : Z, Zsucc (Zpred n) == n. +Theorem lt_nge : forall n m, n < m <-> ~(m<=n). Proof. -intro n; unfold Zsucc, Zpred, Zeq; simpl. -rewrite add_succ_l; now rewrite add_succ_r. +intros. apply lt_nge. Qed. -Theorem Zopp_0 : - 0 == 0. +Instance lt_wd : Proper (Z.eq ==> Z.eq ==> iff) Z.lt. Proof. -unfold Zopp, Zeq; simpl. now rewrite add_0_l. +assert (forall n, Proper (Z.eq==>iff) (Z.lt n)). + intros (n1,n2). apply proper_sym_impl_iff; auto with *. + unfold Z.lt, Z.eq; intros (r1,r2) (s1,s2) Eq H; simpl in *. + apply le_lt_add_lt with (r1+r2)%N (r1+r2)%N; [apply le_refl; auto with *|]. + rewrite add_shuffle2, (add_comm s2), Eq. + rewrite (add_comm s1 n2), (add_shuffle1 n2), (add_comm n2 r1). + now rewrite <- add_lt_mono_r. +intros n n' Hn m m' Hm. +rewrite Hm. rewrite 2 lt_nge, 2 lt_eq_cases, Hn; auto with *. Qed. -Theorem Zopp_succ : forall n, - (Zsucc n) == Zpred (- n). -Proof. -reflexivity. -Qed. +Definition t := Z.t. +Definition eq := Z.eq. +Definition zero := Z.zero. +Definition succ := Z.succ. +Definition pred := Z.pred. +Definition add := Z.add. +Definition sub := Z.sub. +Definition mul := Z.mul. +Definition opp := Z.opp. +Definition lt := Z.lt. +Definition le := Z.le. +Definition min := Z.min. +Definition max := Z.max. End ZPairsAxiomsMod. @@ -413,9 +319,7 @@ and get their properties *) Require Import NPeano. Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. -Module Export ZPairsMulOrderPropMod := ZMulOrderPropFunct ZPairsPeanoAxiomsMod. - -Open Local Scope IntScope. +Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod. Eval compute in (3, 5) * (4, 6). *) |