diff options
Diffstat (limited to 'theories/Numbers')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 206 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 303 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsAxioms.v | 142 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder1.v | 423 |
4 files changed, 394 insertions, 680 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 0fd1be7a9..cb8ac3b5b 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -2,198 +2,174 @@ Require Import ZTimesOrder. Require Import ZArith. Open Local Scope Z_scope. -Module Export ZBinDomain <: ZDomainSignature. -Delimit Scope IntScope with Int. -(* Is this really necessary? Without it, applying ZDomainProperties -functor to this module produces an error since the functor opens the -scope. *) -Definition Z := Z. -Definition E := (@eq Z). -Definition e := Zeq_bool. +Module ZBinAxiomsMod <: ZAxiomsSig. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. -Theorem E_equiv_e : forall x y : Z, E x y <-> e x y. -Proof. -intros x y; unfold E, e, Zeq_bool; split; intro H. -rewrite H; now rewrite Zcompare_refl. -rewrite eq_true_unfold_pos in H. -assert (H1 : (x ?= y) = Eq). -case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H; -[reflexivity | discriminate H | discriminate H]. -now apply Zcompare_Eq_eq. -Qed. +Definition NZ := Z. +Definition NZE := (@eq Z). +Definition NZ0 := 0. +Definition NZsucc := Zsucc'. +Definition NZpred := Zpred'. +Definition NZplus := Zplus. +Definition NZminus := Zminus. +Definition NZtimes := Zmult. -Theorem E_equiv : equiv Z E. +Theorem NZE_equiv : equiv Z NZE. Proof. -apply eq_equiv with (A := Z). (* It does not work without "with (A := Z)" though it looks like it should *) +exact (@eq_equiv Z). 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 ZBinDomain. +Add Relation Z NZE + reflexivity proved by (proj1 NZE_equiv) + symmetry proved by (proj2 (proj2 NZE_equiv)) + transitivity proved by (proj1 (proj2 NZE_equiv)) +as NZE_rel. -Module Export ZBinInt <: IntSignature. -Module Export ZDomainModule := ZBinDomain. - -Definition O := 0. -Definition S := Zsucc'. -Definition P := Zpred'. - -Add Morphism S with signature E ==> E as S_wd. +Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. Proof. -intros; unfold E; congruence. -Qed. - -Add Morphism P with signature E ==> E as P_wd. -Proof. -intros; unfold E; congruence. +congruence. Qed. -Theorem S_inj : forall x y : Z, S x = S y -> x = y. +Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. Proof. -exact Zsucc'_inj. +congruence. Qed. -Theorem S_P : forall x : Z, S (P x) = x. +Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. Proof. -exact Zsucc'_pred'. +congruence. Qed. -Theorem induction : - forall Q : Z -> Prop, - pred_wd E Q -> Q 0 -> - (forall x, Q x -> Q (S x)) -> - (forall x, Q x -> Q (P x)) -> forall x, Q x. +Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. Proof. -intros; now apply Zind. +congruence. Qed. -End ZBinInt. - -Module Export ZBinPlus <: ZPlusSignature. -Module Export IntModule := ZBinInt. - -Definition plus := Zplus. -Definition minus := Zminus. -Definition uminus := Zopp. - -Add Morphism plus with signature E ==> E ==> E as plus_wd. +Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. Proof. -intros; congruence. +congruence. Qed. -Add Morphism minus with signature E ==> E ==> E as minus_wd. +Theorem NZpred_succ : forall n : Z, NZpred (NZsucc n) = n. Proof. -intros; congruence. +exact Zpred'_succ'. Qed. -Add Morphism uminus with signature E ==> E as uminus_wd. +Theorem NZinduction : + forall A : Z -> Prop, predicate_wd NZE A -> + A 0 -> (forall n : Z, A n <-> A (NZsucc n)) -> forall n : Z, A n. Proof. -intros; congruence. +intros A A_wd A0 AS n; apply Zind; clear n. +assumption. +intros; now apply -> AS. +intros n H. rewrite <- (Zsucc'_pred' n) in H. now apply <- AS. Qed. -Theorem plus_0 : forall n, 0 + n = n. +Theorem NZplus_0_l : forall n : Z, 0 + n = n. Proof. exact Zplus_0_l. Qed. -Theorem plus_S : forall n m, (S n) + m = S (n + m). +Theorem NZplus_succ_l : forall n m : Z, (NZsucc n) + m = NZsucc (n + m). Proof. intros; do 2 rewrite <- Zsucc_succ'; apply Zplus_succ_l. Qed. -Theorem minus_0 : forall n, n - 0 = n. +Theorem NZminus_0_r : forall n : Z, n - 0 = n. Proof. exact Zminus_0_r. Qed. -Theorem minus_S : forall n m, n - (S m) = P (n - m). +Theorem NZminus_succ_r : forall n m : Z, n - (NZsucc m) = NZpred (n - m). Proof. intros; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'; apply Zminus_succ_r. Qed. -Theorem uminus_0 : - 0 = 0. +Theorem NZtimes_0_r : forall n : Z, n * 0 = 0. Proof. -reflexivity. +exact Zmult_0_r. Qed. -Theorem uminus_S : forall n, - (S n) = P (- n). -Admitted. +Theorem NZtimes_succ_r : forall n m : Z, n * (NZsucc m) = n * m + n. +Proof. +intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r. +Qed. -End ZBinPlus. +End NZAxiomsMod. -Module Export ZBinTimes <: ZTimesSignature. -Module Export ZPlusModule := ZBinPlus. +Definition NZlt := Zlt. +Definition NZle := Zle. -Definition times := Zmult. +Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. +Proof. +unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. +Qed. -Add Morphism times with signature E ==> E ==> E as times_wd. +Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. Proof. -congruence. +unfold NZE. intros n1 n2 H1 m1 m2 H2; rewrite H1; now rewrite H2. Qed. -Theorem times_0 : forall n, n * 0 = 0. +Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n = m. Proof. -exact Zmult_0_r. +intros n m; split. apply Zle_lt_or_eq. +intro H; destruct H as [H | H]. now apply Zlt_le_weak. rewrite H; apply Zle_refl. Qed. -Theorem times_S : forall n m, n * (S m) = n * m + n. +Theorem NZlt_irrefl : forall n : Z, ~ n < n. Proof. -intros; rewrite <- Zsucc_succ'; apply Zmult_succ_r. +exact Zlt_irrefl. Qed. -End ZBinTimes. +Theorem NZlt_succ_le : forall n m : Z, n < (NZsucc m) <-> n <= m. +Proof. +intros; unfold NZsucc; rewrite <- Zsucc_succ'; split; +[apply Zlt_succ_le | apply Zle_lt_succ]. +Qed. -Module Export ZBinOrder <: ZOrderSignature. -Module Export IntModule := ZBinInt. +End NZOrdAxiomsMod. -Definition lt := Zlt_bool. -Definition le := Zle_bool. +Definition Zopp := Zopp. -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. +Add Morphism Zopp with signature NZE ==> NZE as Zopp_wd. Proof. congruence. Qed. -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Theorem Zsucc_pred : forall n : Z, NZsucc (NZpred n) = n. Proof. -congruence. +exact Zsucc'_pred'. Qed. -Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m. +Theorem Zopp_0 : - 0 = 0. Proof. -intros; unfold lt, le, Zlt_bool, Zle_bool. -case_eq (n ?= m); intro H. -apply Zcompare_Eq_eq in H; rewrite H; now split; intro; [right |]. -now split; intro; [left |]. -split; intro H1. now idtac. -destruct H1 as [H1 | H1]. -assumption. unfold E in H1; rewrite H1 in H. now rewrite Zcompare_refl in H. +reflexivity. Qed. -Theorem lt_irr : forall n, ~ (lt n n). +Theorem Zopp_succ : forall n : Z, - (NZsucc n) = NZpred (- n). Proof. -intro n; rewrite eq_true_unfold_pos; intro H. -assert (H1 : (Zlt n n)). -change (if true then (Zlt n n) else (Zge n n)). rewrite <- H. -unfold lt. apply Zlt_cases. -false_hyp H1 Zlt_irrefl. +intro; rewrite <- Zsucc_succ'; rewrite <- Zpred_pred'. apply Zopp_succ. Qed. -Theorem lt_S : forall n m, lt n (S m) <-> le n m. -Proof. -intros; unfold lt, le, S; do 2 rewrite eq_true_unfold_pos. -rewrite <- Zsucc_succ'; rewrite <- Zlt_is_lt_bool; rewrite <- Zle_is_le_bool. -split; intro; [now apply Zlt_succ_le | now apply Zle_lt_succ]. -Qed. +End ZBinAxiomsMod. + +Module Export ZBinTimesOrderPropMod := ZTimesOrderPropFunct ZBinAxiomsMod. -End ZBinOrder. -Module Export ZTimesOrderPropertiesModule := - ZTimesOrderProperties ZBinTimes ZBinOrder. + +(* +Theorem E_equiv_e : forall x y : Z, E x y <-> e x y. +Proof. +intros x y; unfold E, e, Zeq_bool; split; intro H. +rewrite H; now rewrite Zcompare_refl. +rewrite eq_true_unfold_pos in H. +assert (H1 : (x ?= y) = Eq). +case_eq (x ?= y); intro H1; rewrite H1 in H; simpl in H; +[reflexivity | discriminate H | discriminate H]. +now apply Zcompare_Eq_eq. +Qed. +*)
\ No newline at end of file diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v new file mode 100644 index 000000000..41fc7e75e --- /dev/null +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -0,0 +1,303 @@ +Require Import NMinus. (* The most complete file for natural numbers *) +Require Import ZTimesOrder. (* The most complete file for integers *) + +Module ZPairsAxiomsMod (Import NAxiomsMod : NAxiomsSig) <: ZAxiomsSig. +Module Import NPropMod := NMinusPropFunct NAxiomsMod. (* Get all properties of natural numbers *) +Notation Local N := NZ. (* To remember N without having to use a long qualifying name *) +Notation Local NE := NZE (only parsing). +Notation Local plus_wd := NZplus_wd (only parsing). +Open Local Scope NatIntScope. + +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ : Set := (NZ * NZ)%type. +Definition NZE (p1 p2 : NZ) := ((fst p1) + (snd p2) == (fst p2) + (snd p1)). +Notation Z := NZ (only parsing). +Notation E := NZE (only parsing). +Definition NZ0 := (0, 0). +Definition NZsucc (n : Z) := (S (fst n), snd n). +Definition NZpred (n : Z) := (fst n, S (snd n)). +(* 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. +In that case, we could get rid of setoids as well as arrive at integers as +signed natural numbers. *) +Definition NZplus (n m : Z) := ((fst n) + (fst m), (snd n) + (snd m)). +Definition NZminus (n m : Z) := ((fst n) + (snd m), (snd n) + (fst m)). +Definition NZuminus (n : Z) := (snd n, fst n). +(* Unfortunately, the elements of the pair keep increasing, even during +subtraction *) +Definition NZtimes (n m : Z) := + ((fst n) * (fst m) + (snd n) * (snd m), (fst n) * (snd m) + (snd n) * (fst m)). + +Theorem ZE_refl : reflexive Z E. +Proof. +unfold reflexive, E; reflexivity. +Qed. + +Theorem ZE_symm : symmetric Z E. +Proof. +unfold symmetric, E; now symmetry. +Qed. + +Theorem ZE_trans : transitive Z E. +Proof. +unfold transitive, E. 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 plus_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 -> plus_cancel_r in H3. +Qed. + +Theorem NZE_equiv : equiv Z E. +Proof. +unfold equiv; repeat split; [apply ZE_refl | apply ZE_trans | apply ZE_symm]. +Qed. + +Add Relation Z E + reflexivity proved by (proj1 NZE_equiv) + symmetry proved by (proj2 (proj2 NZE_equiv)) + transitivity proved by (proj1 (proj2 NZE_equiv)) +as NZE_rel. + +Add Morphism (@pair N N) with signature NE ==> NE ==> E as Zpair_wd. +Proof. +intros n1 n2 H1 m1 m2 H2; unfold E; simpl; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZsucc with signature E ==> E as NZsucc_wd. +Proof. +unfold NZsucc, E; intros n m H; simpl. +do 2 rewrite plus_succ_l; now rewrite H. +Qed. + +Add Morphism NZpred with signature E ==> E as NZpred_wd. +Proof. +unfold NZpred, E; intros n m H; simpl. +do 2 rewrite plus_succ_r; now rewrite H. +Qed. + +Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd. +Proof. +unfold E, NZplus; 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 plus_wd. +stepl (fst n1 + snd m1 + (fst n2 + snd m2)) by ring. +now stepr (fst m1 + snd n1 + (fst m2 + snd n2)) by ring. +Qed. + +Add Morphism NZminus with signature E ==> E ==> E as NZminus_wd. +Proof. +unfold E, NZminus; 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 plus_wd. +stepl (fst n1 + snd m1 + (fst m2 + snd n2)) by ring. +now stepr (fst m1 + snd n1 + (fst n2 + snd m2)) by ring. +Qed. + +Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd. +Proof. +unfold NZtimes, E; 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 plus_times_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 plus_times_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 plus_times_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 plus_times_repl_pair with (n := fst m1) (m := snd m1); [| now idtac]. +ring. +Qed. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with NZ. +Open Local Scope IntScope. +Notation "x == y" := (NZE x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ NZE x y) (at level 70) : IntScope. +Notation "0" := NZ0 : IntScope. +Notation "'S'" := NZsucc : IntScope. +Notation "'P'" := NZpred : IntScope. +Notation "1" := (S 0) : IntScope. +Notation "x + y" := (NZplus x y) : IntScope. +Notation "x - y" := (NZminus x y) : IntScope. +Notation "x * y" := (NZtimes x y) : IntScope. + +Theorem NZpred_succ : forall n : Z, P (S n) == n. +Proof. +unfold NZpred, NZsucc, E; intro n; simpl. +rewrite plus_succ_l; now rewrite plus_succ_r. +Qed. + +Section Induction. +Open Scope NatIntScope. (* automatically closes at the end of the section *) +Variable A : Z -> Prop. +Hypothesis A_wd : predicate_wd E A. + +Add Morphism A with signature E ==> iff as A_morph. +Proof. +exact A_wd. +Qed. + +Theorem NZinduction : + A 0 -> (forall n : Z, A n <-> A (S n)) -> forall n : Z, A n. (* 0 is interpreted as in Z due to "Bind" directive *) +Proof. +intros A0 AS n; unfold NZ0, NZsucc, predicate_wd, fun_wd, E in *. +destruct n as [n m]. +cut (forall p : N, A (p, 0)); [intro H1 |]. +cut (forall p : N, A (0, p)); [intro H2 |]. +destruct (plus_dichotomy n m) as [[p H] | [p H]]. +rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2. +rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1. +induct p. assumption. intros p IH. +apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_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. +Qed. + +End Induction. + +Theorem NZplus_0_l : forall n : Z, 0 + n == n. +Proof. +intro n; unfold NZplus, E; simpl. now do 2 rewrite plus_0_l. +Qed. + +Theorem NZplus_succ_l : forall n m : Z, (S n) + m == S (n + m). +Proof. +intros n m; unfold NZplus, E; simpl. now do 2 rewrite plus_succ_l. +Qed. + +Theorem NZminus_0_r : forall n : Z, n - 0 == n. +Proof. +intro n; unfold NZminus, E; simpl. now do 2 rewrite plus_0_r. +Qed. + +Theorem NZminus_succ_r : forall n m : Z, n - (S m) == P (n - m). +Proof. +intros n m; unfold NZminus, E; simpl. symmetry; now rewrite plus_succ_r. +Qed. + +Theorem NZtimes_0_r : forall n : Z, n * 0 == 0. +Proof. +intro n; unfold NZtimes, E; simpl. +repeat rewrite times_0_r. now rewrite plus_assoc. +Qed. + +Theorem NZtimes_succ_r : forall n m : Z, n * (S m) == n * m + n. +Proof. +intros n m; unfold NZtimes, NZsucc, E; simpl. +do 2 rewrite times_succ_r. ring. +Qed. + +End NZAxiomsMod. + +Definition NZlt (n m : Z) := (fst n) + (snd m) < (fst m) + (snd n). +Definition NZle (n m : Z) := (fst n) + (snd m) <= (fst m) + (snd n). + +Notation "x < y" := (NZlt x y) : IntScope. +Notation "x <= y" := (NZle x y) : IntScope. +Notation "x > y" := (NZlt y x) (only parsing) : IntScope. +Notation "x >= y" := (NZle y x) (only parsing) : IntScope. + +Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd. +Proof. +unfold NZlt, E; intros n1 m1 H1 n2 m2 H2; simpl. split; intro H. +stepr (snd m1 + fst m2) by apply plus_comm. +apply (plus_lt_repl_pair (fst n1) (snd n1)); [| assumption]. +stepl (snd m2 + fst n1) by apply plus_comm. +stepr (fst m2 + snd n1) by apply plus_comm. +apply (plus_lt_repl_pair (snd n2) (fst n2)). +now stepl (fst n1 + snd n2) by apply plus_comm. +stepl (fst m2 + snd n2) by apply plus_comm. now stepr (fst n2 + snd m2) by apply plus_comm. +stepr (snd n1 + fst n2) by apply plus_comm. +apply (plus_lt_repl_pair (fst m1) (snd m1)); [| now symmetry]. +stepl (snd n2 + fst m1) by apply plus_comm. +stepr (fst n2 + snd m1) by apply plus_comm. +apply (plus_lt_repl_pair (snd m2) (fst m2)). +now stepl (fst m1 + snd m2) by apply plus_comm. +stepl (fst n2 + snd m2) by apply plus_comm. now stepr (fst m2 + snd n2) by apply plus_comm. +Qed. + +Open Local Scope IntScope. + +Add Morphism NZle with signature E ==> E ==> iff as NZle_wd. +Proof. +unfold NZle, E; intros n1 m1 H1 n2 m2 H2; simpl. +do 2 rewrite le_lt_or_eq. rewrite (NZlt_wd n1 m1 H1 n2 m2 H2). fold (m1 < m2). +fold (n1 == n2) (m1 == m2); fold (n1 == m1) in H1; fold (n2 == m2) in H2. +now rewrite H1, H2. +Qed. + +Theorem NZle_lt_or_eq : forall n m : Z, n <= m <-> n < m \/ n == m. +Proof. +intros n m; unfold NZlt, NZle, E; simpl. apply le_lt_or_eq. +Qed. + +Theorem NZlt_irrefl : forall n : Z, ~ (n < n). +Proof. +intros n; unfold NZlt, E; simpl. apply lt_irrefl. +Qed. + +Theorem NZlt_succ_le : forall n m : Z, n < (S m) <-> n <= m. +Proof. +intros n m; unfold NZlt, NZle, E; simpl. rewrite plus_succ_l; apply lt_succ_le. +Qed. + +End NZOrdAxiomsMod. + +Definition Zopp (n : Z) := (snd n, fst n). + +Notation "- x" := (Zopp x) (at level 35, right associativity) : IntScope. + +Add Morphism Zopp with signature E ==> E as Zopp_wd. +Proof. +unfold E; intros n m H; simpl. symmetry. +stepl (fst n + snd m) by apply plus_comm. +now stepr (fst m + snd n) by apply plus_comm. +Qed. + +Open Local Scope IntScope. + +Theorem Zsucc_pred : forall n : Z, S (P n) == n. +Proof. +intro n; unfold NZsucc, NZpred, E; simpl. +rewrite plus_succ_l; now rewrite plus_succ_r. +Qed. + +Theorem Zopp_0 : - 0 == 0. +Proof. +unfold Zopp, E; simpl. now rewrite plus_0_l. +Qed. + +Theorem Zopp_succ : forall n, - (S n) == P (- n). +Proof. +reflexivity. +Qed. + +End ZPairsAxiomsMod. + +(* For example, let's build integers out of pairs of Peano natural numbers +and get their properties *) + +(* The following lines increase the compilation time at least twice *) +(* +Require Import NPeano. + +Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. +Module Export ZPairsTimesOrderPropMod := ZTimesOrderPropFunct ZPairsPeanoAxiomsMod. + +Open Local Scope IntScope. + +Eval compute in (3, 5) * (4, 6). +*) + diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v deleted file mode 100644 index 2a9b4f386..000000000 --- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v +++ /dev/null @@ -1,142 +0,0 @@ -Require Import NPlus. -Require Export ZAxioms. - -Module NatPairsDomain (Import NPlusMod : NPlusSig) <: ZDomainSignature. -(* with Definition Z := - (NPM.NBaseMod.DomainModule.N * NPM.NBaseMod.DomainModule.N)%type - with Definition E := - fun p1 p2 => - NPM.NBaseMod.DomainModule.E (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)) - with Definition e := - fun p1 p2 => - NPM.NBaseMod.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*) - -Module Export NPlusPropMod := NPlusPropFunct NBaseMod NPlusMod. -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 ZE_refl : reflexive Z E. -Proof. -unfold reflexive, E; reflexivity. -Qed. - -Theorem ZE_symm : symmetric Z E. -Proof. -unfold symmetric, E; now symmetry. -Qed. - -Theorem ZE_trans : transitive Z E. -Proof. -unfold transitive, E. 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. -Qed. - -Theorem E_equiv : equiv Z E. -Proof. -unfold equiv; split; [apply ZE_refl | split; [apply ZE_trans | apply ZE_symm]]. -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 NPlusMod : NPlusSig) <: ZBaseSig. -Module Export ZDomainModule := NatPairsDomain NPlusMod. -Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule. -Open Local Scope IntScope. - -Definition O : Z := (0, 0)%Nat. -Definition S (n : Z) := (NBaseMod.S (fst n), snd n). -Definition P (n : Z) := (fst n, NBaseMod.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 succ_wd. -Proof. -unfold S, E; intros n m H; simpl. -do 2 rewrite plus_succ_l; now rewrite H. -Qed. - -Add Morphism P with signature E ==> E as pred_wd. -Proof. -unfold P, E; intros n m H; simpl. -do 2 rewrite plus_succ_r; now rewrite H. -Qed. - -Theorem succ_inj : forall x y : Z, S x == S y -> x == y. -Proof. -unfold S, E; simpl; intros x y H. -do 2 rewrite plus_succ_l in H. now apply succ_inj in H. -Qed. - -Theorem succ_pred : forall x : Z, S (P x) == x. -Proof. -intro x; unfold S, P, E; simpl. -rewrite plus_succ_l; now rewrite plus_succ_r. -Qed. - -Section Induction. -Open Scope NatScope. (* automatically closes at the end of the section *) -Variable A : Z -> Prop. -Hypothesis Q_wd : predicate_wd E A. - -Add Morphism A with signature E ==> iff as Q_morph. -Proof. -exact Q_wd. -Qed. - -Theorem induction : - A 0 -> (forall x, A x -> A (S x)) -> (forall x, A x -> A (P x)) -> forall x, A x. -Proof. -intros Q0 QS QP x; unfold O, S, P, predicate_wd, E in *. -destruct x as [n m]. -cut (forall p : N, A (p, 0)); [intro H1 |]. -cut (forall p : N, A (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/NatInt/NZOrder1.v b/theories/Numbers/NatInt/NZOrder1.v deleted file mode 100644 index 6a15ddc6a..000000000 --- a/theories/Numbers/NatInt/NZOrder1.v +++ /dev/null @@ -1,423 +0,0 @@ -Require Export NZBase. - -Module Type NZOrderSig. -Declare Module Export NZBaseMod : NZBaseSig. - -Parameter Inline NZlt : NZ -> NZ -> Prop. -Parameter Inline NZle : NZ -> NZ -> Prop. - -Axiom NZlt_wd : rel_wd NZE NZE NZlt. -Axiom NZle_wd : rel_wd NZE NZE NZle. - -Notation "x < y" := (NZlt x y). -Notation "x <= y" := (NZle x y). - -Axiom NZle__lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. -Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). -Axiom NZlt_succ__le : forall n m : NZ, n < S m <-> n <= m. -End NZOrderSig. - -Module NZOrderPropFunct (Import NZOrderMod : NZOrderSig). -Module Export NZBasePropMod := NZBasePropFunct NZBaseMod. - -Ltac NZle_intro1 := rewrite NZle__lt_or_eq; left. -Ltac NZle_intro2 := rewrite NZle__lt_or_eq; right. -Ltac NZle_elim H := rewrite NZle__lt_or_eq in H; destruct H as [H | H]. - -Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_morph. -Proof. -exact NZlt_wd. -Qed. - -Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_morph. -Proof. -exact NZle_wd. -Qed. - -Lemma NZlt_stepl : forall x y z : NZ, x < y -> x == z -> z < y. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. - -Lemma NZlt_stepr : forall x y z : NZ, x < y -> y == z -> x < z. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. - -Lemma NZle_stepl : forall x y z : NZ, x <= y -> x == z -> z <= y. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. - -Lemma NZle_stepr : forall x y z : NZ, x <= y -> y == z -> x <= z. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. - -Declare Left Step NZlt_stepl. -Declare Right Step NZlt_stepr. -Declare Left Step NZle_stepl. -Declare Right Step NZle_stepr. - -Theorem NZlt_le_incl : forall n m : NZ, n < m -> n <= m. -Proof. -intros; now NZle_intro1. -Qed. - -Theorem NZlt_neq : forall n m : NZ, n < m -> n ~= m. -Proof. -intros n m H1 H2; rewrite H2 in H1; false_hyp H1 NZlt_irrefl. -Qed. - -Theorem NZle_refl : forall n : NZ, n <= n. -Proof. -intro; now NZle_intro2. -Qed. - -Theorem NZlt_succ_r : forall n : NZ, n < S n. -Proof. -intro n. rewrite NZlt_succ__le. now NZle_intro2. -Qed. - -Theorem NZle_succ_r : forall n : NZ, n <= S n. -Proof. -intro; NZle_intro1; apply NZlt_succ_r. -Qed. - -Theorem NZlt__lt_succ : forall n m : NZ, n < m -> n < S m. -Proof. -intros. rewrite NZlt_succ__le. now NZle_intro1. -Qed. - -Theorem NZle__le_succ : forall n m : NZ, n <= m -> n <= S m. -Proof. -intros n m H; rewrite <- NZlt_succ__le in H; now NZle_intro1. -Qed. - -Theorem NZle_succ__le_or_eq_succ : forall n m : NZ, n <= S m <-> n <= m \/ n == S m. -Proof. -intros n m; rewrite NZle__lt_or_eq. now rewrite NZlt_succ__le. -Qed. - -(** A corollary of having an order is that NZ is infinite *) - -(* This section about infinity of NZ relies on the type nat and can be -safely removed *) - -Definition succ_iter (n : nat) (m : NZ) := - nat_rec (fun _ => NZ) m (fun _ l => S l) n. - -Theorem NZlt_succ_iter_r : - forall (n : nat) (m : NZ), m < succ_iter (Datatypes.S n) m. -Proof. -intros n m; induction n as [| n IH]; simpl in *. -apply NZlt_succ_r. now apply NZlt__lt_succ. -Qed. - -Theorem NZneq_succ_iter_l : - forall (n : nat) (m : NZ), succ_iter (Datatypes.S n) m ~= m. -Proof. -intros n m H. pose proof (NZlt_succ_iter_r n m) as H1. rewrite H in H1. -false_hyp H1 NZlt_irrefl. -Qed. - -(* End of the section about the infinity of NZ *) - -(* The following theorem is a special case of NZneq_succ_iter_l, but we -prove it independently *) - -Theorem NZneq_succ_l : forall n : NZ, S n ~= n. -Proof. -intros n H. pose proof (NZlt_succ_r n) as H1. rewrite H in H1. -false_hyp H1 NZlt_irrefl. -Qed. - -Theorem NZnlt_succ_l : forall n : NZ, ~ S n < n. -Proof. -intros n H; apply NZlt__lt_succ in H. false_hyp H NZlt_irrefl. -Qed. - -Theorem NZnle_succ_l : forall n : NZ, ~ S n <= n. -Proof. -intros n H; NZle_elim H. -false_hyp H NZnlt_succ_l. false_hyp H NZneq_succ_l. -Qed. - -Theorem NZlt__le_succ : forall n m : NZ, n < m <-> S n <= m. -Proof. -intro n; NZinduct_center m n. -rewrite_false (n < n) NZlt_irrefl. now rewrite_false (S n <= n) NZnle_succ_l. -intro m. rewrite NZlt_succ__le. rewrite NZle_succ__le_or_eq_succ. -rewrite NZsucc_inj_wd. rewrite (NZle__lt_or_eq n m). -rewrite or_cancel_r. -apply NZlt_neq. -intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_l. -reflexivity. -Qed. - -Theorem NZlt_succ__lt : forall n m : NZ, S n < m -> n < m. -Proof. -intros n m H; apply <- NZlt__le_succ; now NZle_intro1. -Qed. - -Theorem NZle_succ__le : forall n m : NZ, S n <= m -> n <= m. -Proof. -intros n m H; NZle_intro1; now apply <- NZlt__le_succ. -Qed. - -Theorem NZsucc_lt_mono : forall n m : NZ, n < m <-> S n < S m. -Proof. -intros n m. rewrite NZlt__le_succ. symmetry. apply NZlt_succ__le. -Qed. - -Theorem NZsucc_le_mono : forall n m : NZ, n <= m <-> S n <= S m. -Proof. -intros n m. do 2 rewrite NZle__lt_or_eq. -rewrite <- NZsucc_lt_mono; now rewrite NZsucc_inj_wd. -Qed. - -Theorem NZlt_lt_false : forall n m, n < m -> m < n -> False. -Proof. -intros n m; NZinduct_center n m. -intros H _; false_hyp H NZlt_irrefl. -intro n; split; intros H H1 H2. -apply NZlt_succ__lt in H1. apply -> NZlt_succ__le in H2. NZle_elim H2. -now apply H. rewrite H2 in H1; false_hyp H1 NZlt_irrefl. -apply NZlt__lt_succ in H2. apply -> NZlt__le_succ in H1. NZle_elim H1. -now apply H. rewrite H1 in H2; false_hyp H2 NZlt_irrefl. -Qed. - -Theorem NZlt_asymm : forall n m, n < m -> ~ m < n. -Proof. -intros n m; unfold not; apply NZlt_lt_false. -Qed. - -Theorem NZlt_trans : forall n m p : NZ, n < m -> m < p -> n < p. -Proof. -intros n m p; NZinduct_center p m. -intros _ H; false_hyp H NZlt_irrefl. -intro p. do 2 rewrite NZlt_succ__le. -split; intros H H1 H2. -NZle_intro1; NZle_elim H2; [now apply H | now rewrite H2 in H1]. -assert (n <= p) as H3. apply H. assumption. now NZle_intro1. -NZle_elim H3. assumption. rewrite <- H3 in H2. elimtype False. -now apply (NZlt_lt_false n m). -Qed. - -Theorem NZle_trans : forall n m p : NZ, n <= m -> m <= p -> n <= p. -Proof. -intros n m p H1 H2; NZle_elim H1. -NZle_elim H2. NZle_intro1; now apply NZlt_trans with (m := m). -NZle_intro1; now rewrite <- H2. now rewrite H1. -Qed. - -Theorem NZle_lt_trans : forall n m p : NZ, n <= m -> m < p -> n < p. -Proof. -intros n m p H1 H2; NZle_elim H1. -now apply NZlt_trans with (m := m). now rewrite H1. -Qed. - -Theorem NZlt_le_trans : forall n m p : NZ, n < m -> m <= p -> n < p. -Proof. -intros n m p H1 H2; NZle_elim H2. -now apply NZlt_trans with (m := m). now rewrite <- H2. -Qed. - -Theorem NZle_antisym : forall n m : NZ, n <= m -> m <= n -> n == m. -Proof. -intros n m H1 H2; now (NZle_elim H1; NZle_elim H2); -[elimtype False; apply (NZlt_lt_false n m) | | |]. -Qed. - -(** Trichotomy, decidability, and double negation elimination *) - -Theorem NZlt_trichotomy : forall n m : NZ, n < m \/ n == m \/ m < n. -Proof. -intros n m; NZinduct_center n m. -right; now left. -intro n; rewrite NZlt_succ__le. stepr ((S n < m \/ S n == m) \/ m <= n) by tauto. -rewrite <- (NZle__lt_or_eq (S n) m). symmetry (n == m). -stepl (n < m \/ m < n \/ m == n) by tauto. rewrite <- NZle__lt_or_eq. -apply or_iff_compat_r. apply NZlt__le_succ. -Qed. - -Theorem NZle_lt_dec : forall n m : NZ, n <= m \/ m < n. -Proof. -intros n m; destruct (NZlt_trichotomy n m) as [H | [H | H]]. -left; now NZle_intro1. left; now NZle_intro2. now right. -Qed. - -Theorem NZle_nlt : forall n m : NZ, n <= m <-> ~ m < n. -Proof. -intros n m. split; intro H; [intro H1 |]. -eapply NZle_lt_trans in H; [| eassumption ..]. false_hyp H NZlt_irrefl. -destruct (NZle_lt_dec n m) as [H1 | H1]. -assumption. false_hyp H1 H. -Qed. - -Theorem NZlt_dec : forall n m : NZ, n < m \/ ~ n < m. -Proof. -intros n m; destruct (NZle_lt_dec m n); -[right; now apply -> NZle_nlt | now left]. -Qed. - -Theorem NZlt_dne : forall n m, ~ ~ n < m <-> n < m. -Proof. -intros n m; split; intro H; -[destruct (NZlt_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | -intro H1; false_hyp H H1]. -Qed. - -Theorem NZnle_lt : forall n m : NZ, ~ n <= m <-> m < n. -Proof. -intros n m. rewrite NZle_nlt. apply NZlt_dne. -Qed. - -Theorem NZle_dec : forall n m : NZ, n <= m \/ ~ n <= m. -Proof. -intros n m; destruct (NZle_lt_dec n m); -[now left | right; now apply <- NZnle_lt]. -Qed. - -Theorem NZle_dne : forall n m : NZ, ~ ~ n <= m <-> n <= m. -Proof. -intros n m; split; intro H; -[destruct (NZle_dec n m) as [H1 | H1]; [assumption | false_hyp H1 H] | -intro H1; false_hyp H H1]. -Qed. - -Theorem NZlt__nlt_succ : forall n m : NZ, n < m <-> ~ m < S n. -Proof. -intros n m; rewrite NZlt_succ__le; symmetry; apply NZnle_lt. -Qed. - -(** Stronger variant of induction with assumptions n >= 0 (n <= 0) -in the induction step *) - -Section Induction. - -Variable A : Z -> Prop. -Hypothesis Q_wd : predicate_wd NZE A. - -Add Morphism A with signature NZE ==> iff as Q_morph. -Proof Q_wd. - -Section Center. - -Variable z : Z. (* A z is the basis of induction *) - -Section RightInduction. - -Let Q' := fun n : Z => forall m : NZ, z <= m -> m < n -> A m. - -Add Morphism Q' with signature NZE ==> iff as Q'_pos_wd. -Proof. -intros x1 x2 H; unfold Q'; qmorphism x1 x2. -Qed. - -Theorem NZright_induction : - A z -> (forall n : NZ, z <= n -> A n -> A (S n)) -> forall n : NZ, z <= n -> A n. -Proof. -intros Qz QS k k_ge_z. -assert (H : forall n : NZ, Q' n). induct_n n z; unfold Q'. -intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. -intros n IH m H2 H3. -rewrite NZlt_succ in H3; Zle_elim H3. now apply IH. -Zle_elim H2. rewrite_succ_pred m. -apply QS. now apply -> lt_n_m_pred. apply IH. now apply -> lt_n_m_pred. -rewrite H3; apply NZlt_pred_l. now rewrite <- H2. -intros n IH m H2 H3. apply IH. assumption. now apply lt_n_predm. -pose proof (H (S k)) as H1; unfold Q' in H1. apply H1. -apply k_ge_z. apply NZlt_succ_r. -Qed. - -End RightInduction. - -Section LeftInduction. - -Let Q' := fun n : Z => forall m : NZ, m <= z -> n < m -> A m. - -Add Morphism Q' with signature NZE ==> iff as Q'_neg_wd. -Proof. -intros x1 x2 H; unfold Q'; qmorphism x1 x2. -Qed. - -Theorem NZleft_induction : - A z -> (forall n : NZ, n <= z -> A n -> A (P n)) -> forall n : NZ, n <= z -> A n. -Proof. -intros Qz QP k k_le_z. -assert (H : forall n : NZ, Q' n). induct_n n z; unfold Q'. -intros m H1 H2. apply -> le_gt in H1; false_hyp H2 H1. -intros n IH m H2 H3. apply IH. assumption. now apply lt_succ__lt. -intros n IH m H2 H3. -rewrite NZlt_pred in H3; Zle_elim H3. now apply IH. -Zle_elim H2. rewrite_pred_succ m. -apply QP. now apply -> lt_n_m_succ. apply IH. now apply -> lt_n_m_succ. -rewrite H3; apply NZlt_succ_r. now rewrite H2. -pose proof (H (P k)) as H1; unfold Q' in H1. apply H1. -apply k_le_z. apply NZlt_pred_l. -Qed. - -End LeftInduction. - -Theorem NZinduction_ord_n : - A z -> - (forall n : NZ, z <= n -> A n -> A (S n)) -> - (forall n : NZ, n <= z -> A n -> A (P n)) -> - forall n : NZ, A n. -Proof. -intros Qz QS QP n. -destruct (lt_total n z) as [H | [H | H]]. -now apply left_induction; [| | Zle_intro1]. -now rewrite H. -now apply right_induction; [| | Zle_intro1]. -Qed. - -End Center. - -Theorem NZinduction_ord : - A 0 -> - (forall n : NZ, 0 <= n -> A n -> A (S n)) -> - (forall n : NZ, n <= 0 -> A n -> A (P n)) -> - forall n : NZ, A n. -Proof (induction_ord_n 0). - -Theorem NZlt_ind : forall (n : Z), - A (S n) -> - (forall m : Z, n < m -> A m -> A (S m)) -> - forall m : Z, n < m -> A m. -Proof. -intros n H1 H2 m H3. -apply right_induction with (S n). assumption. -intros; apply H2; try assumption. now apply <- lt_n_m_succ. -now apply -> lt_n_m_succ. -Qed. - -Theorem NZle_ind : forall (n : Z), - A n -> - (forall m : Z, n <= m -> A m -> A (S m)) -> - forall m : Z, n <= m -> A m. -Proof. -intros n H1 H2 m H3. -now apply right_induction with n. -Qed. - -End Induction. - -Ltac induct_ord n := - try intros until n; - pattern n; apply induction_ord; clear n; - [unfold NumPrelude.predicate_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | | |]. - -End ZOrderProperties. - - - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) |