diff options
Diffstat (limited to 'theories/Numbers')
26 files changed, 743 insertions, 460 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v index 05b8ede94..6527bd11c 100644 --- a/theories/Numbers/Integer/Axioms/ZAxioms.v +++ b/theories/Numbers/Integer/Axioms/ZAxioms.v @@ -1,14 +1,14 @@ Require Export ZDomain. Module Type IntSignature. -Declare Module Export DomainModule : DomainSignature. -Open Local Scope ZScope. +Declare Module Export ZDomainModule : ZDomainSignature. +Open Local Scope IntScope. Parameter Inline O : Z. Parameter Inline S : Z -> Z. Parameter Inline P : Z -> Z. -Notation "0" := O : ZScope. +Notation "0" := O : IntScope. Add Morphism S with signature E ==> E as S_wd. Add Morphism P with signature E ==> E as P_wd. @@ -24,9 +24,9 @@ Axiom induction : End IntSignature. -Module IntProperties (Export IntModule : IntSignature). -Module Export DomainPropertiesModule := DomainProperties DomainModule. -Open Local Scope ZScope. +Module IntProperties (Import IntModule : IntSignature). +Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule. +Open Local Scope IntScope. Ltac induct n := try intros until n; diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v index 1a29eddf2..87c99066d 100644 --- a/theories/Numbers/Integer/Axioms/ZDomain.v +++ b/theories/Numbers/Integer/Axioms/ZDomain.v @@ -1,6 +1,6 @@ Require Export NumPrelude. -Module Type DomainSignature. +Module Type ZDomainSignature. Parameter Z : Set. Parameter E : relation Z. @@ -15,15 +15,15 @@ Add Relation Z E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. -Delimit Scope ZScope with Int. -Bind Scope ZScope with Z. -Notation "x == y" := (E x y) (at level 70) : ZScope. -Notation "x # y" := (~ E x y) (at level 70) : ZScope. +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. -End DomainSignature. +End ZDomainSignature. -Module DomainProperties (Export DomainModule : DomainSignature). -Open Local Scope ZScope. +Module ZDomainProperties (Import ZDomainModule : ZDomainSignature). +Open Local Scope IntScope. Add Morphism e with signature E ==> E ==> eq_bool as e_wd. Proof. @@ -42,4 +42,4 @@ Proof. intros n m H1 H2; symmetry in H2; false_hyp H2 H1. Qed. -End DomainProperties. +End ZDomainProperties. diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v index 803bfe43b..19a66aea3 100644 --- a/theories/Numbers/Integer/Axioms/ZOrder.v +++ b/theories/Numbers/Integer/Axioms/ZOrder.v @@ -1,45 +1,45 @@ Require Export ZAxioms. -Module Type OrderSignature. +Module Type ZOrderSignature. Declare Module Export IntModule : IntSignature. -Open Local Scope ZScope. +Open Local Scope IntScope. Parameter Inline lt : Z -> Z -> bool. Parameter Inline le : Z -> Z -> bool. Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Notation "n < m" := (lt n m) : ZScope. -Notation "n <= m" := (le n m) : ZScope. +Notation "n < m" := (lt n m) : IntScope. +Notation "n <= m" := (le n m) : IntScope. Axiom le_lt : forall n m, n <= m <-> n < m \/ n == m. Axiom lt_irr : forall n, ~ (n < n). Axiom lt_S : forall n m, n < (S m) <-> n <= m. -End OrderSignature. +End ZOrderSignature. -Module OrderProperties (Export OrderModule : OrderSignature). +Module ZOrderProperties (Import ZOrderModule : ZOrderSignature). Module Export IntPropertiesModule := IntProperties IntModule. -Open Local Scope ZScope. +Open Local Scope IntScope. -Ltac le_intro1 := rewrite le_lt; left. -Ltac le_intro2 := rewrite le_lt; right. -Ltac le_elim H := rewrite le_lt in H; destruct H as [H | H]. +Ltac Zle_intro1 := rewrite le_lt; left. +Ltac Zle_intro2 := rewrite le_lt; right. +Ltac Zle_elim H := rewrite le_lt in H; destruct H as [H | H]. Theorem le_refl : forall n, n <= n. Proof. -intro n; now le_intro2. +intro n; now Zle_intro2. Qed. Theorem lt_n_Sn : forall n, n < S n. Proof. -intro n. rewrite lt_S. now le_intro2. +intro n. rewrite lt_S. now Zle_intro2. Qed. Theorem le_n_Sn : forall n, n <= S n. Proof. -intro; le_intro1; apply lt_n_Sn. +intro; Zle_intro1; apply lt_n_Sn. Qed. Theorem lt_Pn_n : forall n, P n < n. @@ -49,17 +49,17 @@ Qed. Theorem le_Pn_n : forall n, P n <= n. Proof. -intro; le_intro1; apply lt_Pn_n. +intro; Zle_intro1; apply lt_Pn_n. Qed. Theorem lt_n_Sm : forall n m, n < m -> n < S m. Proof. -intros. rewrite lt_S. now le_intro1. +intros. rewrite lt_S. now Zle_intro1. Qed. Theorem le_n_Sm : forall n m, n <= m -> n <= S m. Proof. -intros n m H; rewrite <- lt_S in H; now le_intro1. +intros n m H; rewrite <- lt_S in H; now Zle_intro1. Qed. Theorem lt_n_m_P : forall n m, n < m <-> n <= P m. @@ -69,7 +69,7 @@ Qed. Theorem not_le_n_Pn : forall n, ~ n <= P n. Proof. -intros n H; le_elim H. +intros n H; Zle_elim H. apply lt_n_Sm in H; rewrite S_P in H; false_hyp H lt_irr. pose proof (lt_Pn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr. Qed. @@ -84,28 +84,28 @@ Proof. intro n; induct_n m (P n). split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn. intros m IH; split; intro H. -apply -> lt_S in H; le_elim H. +apply -> lt_S in H; Zle_elim H. apply -> IH in H; now apply le_n_Sm. -rewrite <- H; rewrite S_P; now le_intro2. +rewrite <- H; rewrite S_P; now Zle_intro2. apply -> le_S in H; destruct H as [H | H]. apply <- IH in H. now apply lt_n_Sm. rewrite H; rewrite P_S; apply lt_n_Sn. intros m IH; split; intro H. pose proof H as H1. apply lt_n_Sm in H; rewrite S_P in H. -apply -> IH in H; le_elim H. now apply -> lt_n_m_P. +apply -> IH in H; Zle_elim H. now apply -> lt_n_m_P. rewrite H in H1; false_hyp H1 lt_irr. pose proof H as H1. apply le_n_Sm in H. rewrite S_P in H. -apply <- IH in H. apply -> lt_n_m_P in H. le_elim H. +apply <- IH in H. apply -> lt_n_m_P in H. Zle_elim H. assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn. Qed. Theorem lt_Pn_m : forall n m, n < m -> P n < m. Proof. -intros; rewrite lt_P; now le_intro1. +intros; rewrite lt_P; now Zle_intro1. Qed. Theorem le_Pn_m : forall n m, n <= m -> P n <= m. Proof. -intros n m H; rewrite <- lt_P in H; now le_intro1. +intros n m H; rewrite <- lt_P in H; now Zle_intro1. Qed. Theorem lt_n_m_S : forall n m, n < m <-> S n <= m. @@ -120,7 +120,7 @@ Qed. Theorem le_Sn_m : forall n m, S n <= m -> n <= m. Proof. -intros n m H; rewrite <- lt_n_m_S in H; now le_intro1. +intros n m H; rewrite <- lt_n_m_S in H; now Zle_intro1. Qed. Theorem lt_n_Pm : forall n m, n < P m -> n < m. @@ -130,7 +130,7 @@ Qed. Theorem le_n_Pm : forall n m, n <= P m -> n <= m. Proof. -intros n m H; rewrite <- lt_n_m_P in H; now le_intro1. +intros n m H; rewrite <- lt_n_m_P in H; now Zle_intro1. Qed. Theorem lt_respects_S : forall n m, n < m <-> S n < S m. @@ -185,30 +185,30 @@ Proof. intros n m; induct_n n m. intros p H _; false_hyp H lt_irr. intros n IH p H1 H2. apply lt_Sn_m in H1. pose proof (IH p H1 H2) as H3. -rewrite lt_n_m_S in H3; le_elim H3. -assumption. rewrite <- H3 in H2. rewrite lt_S in H2; le_elim H2. +rewrite lt_n_m_S in H3; Zle_elim H3. +assumption. rewrite <- H3 in H2. rewrite lt_S in H2; Zle_elim H2. elimtype False; apply lt_irr with (n := n); now apply IH. rewrite H2 in H1; false_hyp H1 lt_irr. -intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; le_elim H1. +intros n IH p H1 H2. apply lt_Pn_m. rewrite lt_P in H1; Zle_elim H1. now apply IH. now rewrite H1. 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. +intros n m p H1 H2; Zle_elim H1. +Zle_elim H2. Zle_intro1; now apply lt_trans with (m := m). +Zle_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. +intros n m p H1 H2; Zle_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. +intros n m p H1 H2; Zle_elim H2. now apply lt_trans with (m := m). now rewrite <- H2. Qed. @@ -219,7 +219,7 @@ 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. +intros n m H1 H2; Zle_elim H1; Zle_elim H2. elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). now symmetry. assumption. assumption. Qed. @@ -231,7 +231,7 @@ Qed. Theorem not_le_Sn_n : forall n, ~ S n <= n. Proof. -intros n H; le_elim H. false_hyp H not_lt_Sn_n. +intros n H; Zle_elim H. false_hyp H not_lt_Sn_n. pose proof (lt_n_Sn n) as H1. rewrite H in H1; false_hyp H1 lt_irr. Qed. @@ -357,8 +357,8 @@ intros Qz QS k k_ge_z. assert (H : forall n, 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 lt_S in H3; le_elim H3. now apply IH. -le_elim H2. rewrite_S_P m. +rewrite lt_S in H3; Zle_elim H3. now apply IH. +Zle_elim H2. rewrite_S_P m. apply QS. now apply -> lt_n_m_P. apply IH. now apply -> lt_n_m_P. rewrite H3; apply lt_Pn_n. now rewrite <- H2. intros n IH m H2 H3. apply IH. assumption. now apply lt_n_Pm. @@ -385,8 +385,8 @@ assert (H : forall n, 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_Sn_m. intros n IH m H2 H3. -rewrite lt_P in H3; le_elim H3. now apply IH. -le_elim H2. rewrite_P_S m. +rewrite lt_P in H3; Zle_elim H3. now apply IH. +Zle_elim H2. rewrite_P_S m. apply QP. now apply -> lt_n_m_S. apply IH. now apply -> lt_n_m_S. rewrite H3; apply lt_n_Sn. now rewrite H2. pose proof (H (P k)) as H1; unfold Q' in H1. apply H1. @@ -403,9 +403,9 @@ Theorem induction_ord_n : Proof. intros Qz QS QP n. destruct (lt_total n z) as [H | [H | H]]. -now apply left_induction; [| | le_intro1]. +now apply left_induction; [| | Zle_intro1]. now rewrite H. -now apply right_induction; [| | le_intro1]. +now apply right_induction; [| | Zle_intro1]. Qed. End Center. @@ -447,5 +447,5 @@ Ltac induct_ord n := let m := fresh "m" in let H := fresh "H" in intros n m H; qmorphism n m | | |]. -End OrderProperties. +End ZOrderProperties. diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v index 484607094..6c1f49231 100644 --- a/theories/Numbers/Integer/Axioms/ZPlus.v +++ b/theories/Numbers/Integer/Axioms/ZPlus.v @@ -1,16 +1,16 @@ Require Export ZAxioms. -Module Type PlusSignature. +Module Type ZPlusSignature. Declare Module Export IntModule : IntSignature. -Open Local Scope ZScope. +Open Local Scope IntScope. Parameter Inline plus : Z -> Z -> Z. Parameter Inline minus : Z -> Z -> Z. Parameter Inline uminus : Z -> Z. -Notation "x + y" := (plus x y) : ZScope. -Notation "x - y" := (minus x y) : ZScope. -Notation "- x" := (uminus x) : ZScope. +Notation "x + y" := (plus x y) : IntScope. +Notation "x - y" := (minus x y) : IntScope. +Notation "- x" := (uminus x) : IntScope. Add Morphism plus with signature E ==> E ==> E as plus_wd. Add Morphism minus with signature E ==> E ==> E as minus_wd. @@ -25,11 +25,11 @@ Axiom minus_S : forall n m, n - (S m) == P (n - m). Axiom uminus_0 : - 0 == 0. Axiom uminus_S : forall n, - (S n) == P (- n). -End PlusSignature. +End ZPlusSignature. -Module PlusProperties (Export PlusModule : PlusSignature). +Module ZPlusProperties (Import ZPlusModule : ZPlusSignature). Module Export IntPropertiesModule := IntProperties IntModule. -Open Local Scope ZScope. +Open Local Scope IntScope. Theorem plus_P : forall n m, P n + m == P (n + m). Proof. @@ -218,4 +218,4 @@ Proof. intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0. Qed. -End PlusProperties. +End ZPlusProperties. diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v index dd311b49a..946bdf3cb 100644 --- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -1,14 +1,13 @@ Require Export ZOrder. Require Export ZPlus. -Module PlusOrderProperties (PlusModule : PlusSignature) - (OrderModule : OrderSignature with - Module IntModule := PlusModule.IntModule). -(* Warning: Notation _ == _ was already used in scope ZScope !!! *) -Module Export PlusPropertiesModule := PlusProperties PlusModule. -Module Export OrderPropertiesModule := OrderProperties OrderModule. +Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature) + (Import ZOrderModule : ZOrderSignature with + Module IntModule := ZPlusModule.IntModule). +Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. +Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule. (* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *) -Open Local Scope ZScope. +Open Local Scope IntScope. Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m. Proof. @@ -44,19 +43,19 @@ Qed. Theorem plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. Proof. -intros n m p q H1 H2. le_elim H2. now apply plus_lt_compat. +intros n m p q H1 H2. Zle_elim H2. now apply plus_lt_compat. rewrite H2. now apply -> plus_lt_compat_r. Qed. Theorem plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. Proof. -intros n m p q H1 H2. le_elim H1. now apply plus_lt_compat. +intros n m p q H1 H2. Zle_elim H1. now apply plus_lt_compat. rewrite H1. now apply -> plus_lt_compat_l. Qed. Theorem plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. Proof. -intros n m p q H1 H2. le_elim H1. le_intro1; now apply plus_lt_le_compat. +intros n m p q H1 H2. Zle_elim H1. Zle_intro1; now apply plus_lt_le_compat. rewrite H1. now apply -> plus_le_compat_l. Qed. @@ -71,7 +70,7 @@ induct n. induct_ord m. intro H; false_hyp H lt_irr. intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *. -le_elim H1. apply IH in H1. now apply lt_Pn_m. +Zle_elim H1. apply IH in H1. now apply lt_Pn_m. rewrite <- H1; rewrite uminus_0; apply lt_Pn_n. intros m H1 IH H2. apply lt_n_Pm in H2. apply -> le_gt in H1. false_hyp H2 H1. intros n IH m H. rewrite uminus_S. @@ -158,4 +157,4 @@ intros n m p. rewrite (minus_le_nondecr_l (n + p) m p). rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. Qed. -End PlusOrderProperties. +End ZPlusOrderProperties. diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v index 052dcf66f..7d4329a96 100644 --- a/theories/Numbers/Integer/Axioms/ZTimes.v +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -1,12 +1,12 @@ Require Export ZPlus. -Module Type TimesSignature. -Declare Module Export PlusModule : PlusSignature. -Open Local Scope ZScope. +Module Type ZTimesSignature. +Declare Module Export ZPlusModule : ZPlusSignature. +Open Local Scope IntScope. Parameter Inline times : Z -> Z -> Z. -Notation "x * y" := (times x y) : ZScope. +Notation "x * y" := (times x y) : IntScope. Add Morphism times with signature E ==> E ==> E as times_wd. @@ -26,11 +26,11 @@ 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 TimesSignature. +End ZTimesSignature. -Module TimesProperties (Export TimesModule : TimesSignature). -Module Export PlusPropertiesModule := PlusProperties PlusModule. -Open Local Scope ZScope. +Module ZTimesProperties (Import ZTimesModule : ZTimesSignature). +Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. +Open Local Scope IntScope. Theorem times_P : forall n m, n * (P m) == n * m - n. Proof. @@ -130,4 +130,4 @@ intros p IH. do 2 rewrite times_S. rewrite times_plus_distr_r. now rewrite IH. intros p IH. do 2 rewrite times_P. rewrite times_minus_distr_r. now rewrite IH. Qed. -End TimesProperties. +End ZTimesProperties. diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v index a72636a42..28c07a99d 100644 --- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v +++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v @@ -1,20 +1,20 @@ Require Export ZTimes. Require Export ZPlusOrder. -Module TimesOrderProperties (TimesModule : TimesSignature) - (OrderModule : OrderSignature with - Module IntModule := TimesModule.PlusModule.IntModule). -Module Export TimesPropertiesModule := TimesProperties TimesModule. -Module Export PlusOrderPropertiesModule := - PlusOrderProperties TimesModule.PlusModule OrderModule. -Open Local Scope ZScope. +Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature) + (Import ZOrderModule : ZOrderSignature with + Module IntModule := ZTimesModule.ZPlusModule.IntModule). +Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule. +Module Export ZPlusOrderPropertiesModule := + ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule. +Open Local Scope IntScope. Theorem mult_lt_compat_r : forall n m p, 0 < p -> n < m -> n * p < m * p. Proof. intros n m p; induct_ord p. intros H _; false_hyp H lt_irr. intros p H IH H1 H2. do 2 rewrite times_S. -apply -> lt_S in H1; le_elim H1. +apply -> lt_S in H1; Zle_elim H1. apply plus_lt_compat. now apply IH. assumption. rewrite <- H1. do 2 rewrite times_0; now do 2 rewrite plus_0. intros p H IH H1 H2. apply lt_n_Pm in H1. apply -> le_gt in H. @@ -29,9 +29,9 @@ Qed. Theorem mult_lt_le_compat_r : forall n m p, 0 < p -> n <= m -> n * p <= m * p. Proof. -intros n m p H1 H2; le_elim H2. -le_intro1; now apply mult_lt_compat_r. -rewrite H2. now le_intro2. +intros n m p H1 H2; Zle_elim H2. +Zle_intro1; now apply mult_lt_compat_r. +rewrite H2. now Zle_intro2. Qed. Theorem mult_lt_le_compat_l : forall n m p, 0 < p -> n <= m -> p * n <= p * m. @@ -86,4 +86,4 @@ false_hyp H4 H2. apply neq_symm. apply lt_neq. now apply mult_pos_pos. Qed. -End TimesOrderProperties. +End ZTimesOrderProperties. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 2ca4bc5d8..fb4b137d6 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -1,18 +1,28 @@ -Require Export NTimesLt. +Require Export NMinus. +Require Export NTimesOrder. Require Export ZTimesOrder. -Module NatPairsDomain (Export NPlusModule : NPlus.PlusSignature) : - ZDomain.DomainSignature - with Definition Z := (N * N)%type. - with Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat. - with Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat. +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 := NPlus.PlusProperties NPlusModule. +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)). -Definition E (p1 p2 : Z) := ((fst p1) + (snd p2) == (fst p2) + (snd p1))%Nat. -Definition e (p1 p2 : Z) := e ((fst p1) + (snd p2)) ((fst p2) + (snd p1))%Nat. +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. @@ -43,12 +53,12 @@ as E_rel. End NatPairsDomain. - -Module NatPairsInt (Export NPlusModule : NPlus.PlusSignature) <: IntSignature. - +Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature. Module Export ZDomainModule := NatPairsDomain NPlusModule. +Module Export ZDomainModuleProperties := ZDomainProperties ZDomainModule. +Open Local Scope IntScope. -Definition O := (0, 0). +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. @@ -57,6 +67,8 @@ 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. @@ -70,6 +82,25 @@ 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 *. + diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v index ad17e5255..da4c0af3d 100644 --- a/theories/Numbers/Natural/Axioms/NAxioms.v +++ b/theories/Numbers/Natural/Axioms/NAxioms.v @@ -5,21 +5,21 @@ Require Export NDomain. *********************************************************************) Module Type NatSignature. -Declare Module Export DomainModule : DomainSignature. +Declare Module Export NDomainModule : NDomainSignature. (* We use Export in the previous line to make sure that if we import a module of type NatSignature, then we also import (i.e., get access -without path qualifiers to) DomainModule. For example, the functor +without path qualifiers to) NDomainModule. For example, the functor NatProperties below, which accepts an implementation of NatSignature as an argument and imports it, will have access to N. Indeed, it does not make sense to get unqualified access to O and S but not to N. *) -Open Local Scope NScope. +Open Local Scope NatScope. Parameter Inline O : N. Parameter Inline S : N -> N. -Notation "0" := O : NScope. -Notation "1" := (S O) : NScope. +Notation "0" := O : NatScope. +Notation "1" := (S O) : NatScope. Add Morphism S with signature E ==> E as S_wd. @@ -174,9 +174,56 @@ Implicit Arguments recursion_S [A]. End NatSignature. -Module NatProperties (Export NatModule : NatSignature). -Module Export DomainPropertiesModule := DomainProperties DomainModule. -Open Local Scope NScope. +(* We would like to have a signature for the predecessor: first, to be +able to provide an efficient implementation, and second, to be able to +use this function in the signatures defining other functions, e.g., +subtraction. If we just define predecessor by recursion in +NatProperties functor, we would not be able to use it in other +signatures. We cannot put the functor NDefPred below in a different +file because the definition of the predecessor uses recursion and the +proof of injectivity of the successor uses the predecessor. *) + +Module Type NPredSignature. +Declare Module Export NatModule : NatSignature. +Open Local Scope NatScope. + +Parameter Inline P : N -> N. + +Add Morphism P with signature E ==> E as P_wd. + +Axiom P_0 : P 0 == 0. +Axiom P_S : forall n, P (S n) == n. + +End NPredSignature. + +Module NDefPred (Import NM : NatSignature) <: NPredSignature. +Module NatModule := NM. +Open Local Scope NatScope. + +Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n. + +Add Morphism P with signature E ==> E as P_wd. +Proof. +intros; unfold P. +now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. +Qed. + +Theorem P_0 : P 0 == 0. +Proof. +unfold P; now rewrite recursion_0. +Qed. + +Theorem P_S : forall n, P (S n) == n. +Proof. +intro n; unfold P; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |]. +Qed. + +End NDefPred. + +Module NatProperties (Import NatModule : NatSignature). +Module Export NDomainPropertiesModule := NDomainProperties NDomainModule. +Module Import NDefPredModule := NDefPred NatModule. (* Many warnings are printed here !!! *) +Open Local Scope NatScope. (* This tactic applies the induction axioms and solves the resulting goal "pred_wd E P" *) @@ -223,30 +270,12 @@ change (LE_Set bool (if_zero false true (S n)) (if_zero false true 0)). rewrite H. unfold LE_Set. reflexivity. Qed. -Definition pred (n : N) : N := recursion 0 (fun m _ => m) n. - -Add Morphism pred with signature E ==> E as pred_wd. -Proof. -intros; unfold pred. -now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. -Qed. - -Theorem pred_0 : pred 0 == 0. -Proof. -unfold pred; now rewrite recursion_0. -Qed. - -Theorem pred_S : forall n, pred (S n) == n. -Proof. -intro n; unfold pred; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |]. -Qed. - Theorem S_inj : forall m n, S m == S n -> m == n. Proof. intros m n H. -setoid_replace m with (pred (S m)) by (symmetry; apply pred_S). -setoid_replace n with (pred (S n)) by (symmetry; apply pred_S). -now apply pred_wd. +setoid_replace m with (P (S m)) by (symmetry; apply P_S). +setoid_replace n with (P (S n)) by (symmetry; apply P_S). +now apply P_wd. Qed. Theorem not_eq_S : forall n m, n # m -> S n # S m. diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v index 85ff0eb72..c525db3d2 100644 --- a/theories/Numbers/Natural/Axioms/NDepRec.v +++ b/theories/Numbers/Natural/Axioms/NDepRec.v @@ -5,13 +5,13 @@ equality. The reason is that, if the domain is A : nat -> Set, then (A n) must coincide with (A n') whenever n == n'. However, it is possible to try to use arbitrary domain and require that n == n' -> A n = A n'. *) -Module Type DepRecSignature. -Declare Module Export DomainModule : DomainEqSignature. +Module Type NDepRecSignature. +Declare Module Export NDomainModule : NDomainEqSignature. Declare Module Export NatModule : NatSignature with - Module DomainModule := DomainModule. + Module NDomainModule := NDomainModule. (* Instead of these two lines, I would like to say -Declare Module Export Nat : NatSignature with Module Domain : NatEqDomain. *) -Open Local Scope NScope. +Declare Module Export Nat : NatSignature with Module NDomain : NatEqDomain. *) +Open Local Scope NatScope. Parameter Inline dep_recursion : forall A : N -> Set, A 0 -> (forall n, A n -> A (S n)) -> forall n, A n. @@ -24,14 +24,14 @@ Axiom dep_recursion_S : forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)) (n : N), dep_recursion A a f (S n) = f n (dep_recursion A a f n). -End DepRecSignature. +End NDepRecSignature. -Module DepRecTimesProperties - (Export DepRecModule : DepRecSignature) - (TimesModule : TimesSignature - with Module PlusModule.NatModule := DepRecModule.NatModule). -Module Export TimesPropertiesModule := TimesProperties TimesModule. -Open Local Scope NScope. +Module NDepRecTimesProperties + (Import NDepRecModule : NDepRecSignature) + (Import NTimesModule : NTimesSignature + with Module NPlusModule.NatModule := NDepRecModule.NatModule). +Module Export NTimesPropertiesModule := NTimesProperties NTimesModule. +Open Local Scope NatScope. Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}. Proof. @@ -68,4 +68,4 @@ intros n _ m _ H. rewrite times_Sn_m in H; rewrite plus_Sn_m in H; now apply S_0 in H. Qed. -End DepRecTimesProperties. +End NDepRecTimesProperties. diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v index de2ddf116..5b3fde2c2 100644 --- a/theories/Numbers/Natural/Axioms/NDomain.v +++ b/theories/Numbers/Natural/Axioms/NDomain.v @@ -1,6 +1,6 @@ Require Export NumPrelude. -Module Type DomainSignature. +Module Type NDomainSignature. Parameter Inline N : Set. Parameter Inline E : relation N. @@ -28,17 +28,17 @@ Add Relation N E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. -Delimit Scope NScope with Nat. -Bind Scope NScope with N. -Notation "x == y" := (E x y) (at level 70) : NScope. -Notation "x # y" := (~ E x y) (at level 70) : NScope. +Delimit Scope NatScope with Nat. +Bind Scope NatScope with N. +Notation "x == y" := (E x y) (at level 70) : NatScope. +Notation "x # y" := (~ E x y) (at level 70) : NatScope. -End DomainSignature. +End NDomainSignature. -(* Now we give DomainSignature, but with E being Leibniz equality. If +(* Now we give NDomainSignature, but with E being Leibniz equality. If an implementation uses this signature, then more facts may be proved about it. *) -Module Type DomainEqSignature. +Module Type NDomainEqSignature. Parameter Inline N : Set. Definition E := (@eq N). @@ -53,17 +53,17 @@ Add Relation N E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. -Delimit Scope NScope with Nat. -Bind Scope NScope with N. -Notation "x == y" := (E x y) (at level 70) : NScope. -Notation "x # y" := ((E x y) -> False) (at level 70) : NScope. +Delimit Scope NatScope with Nat. +Bind Scope NatScope with N. +Notation "x == y" := (E x y) (at level 70) : NatScope. +Notation "x # y" := ((E x y) -> False) (at level 70) : NatScope. (* Why do we need a new notation for Leibniz equality? See DepRec.v *) -End DomainEqSignature. +End NDomainEqSignature. -Module DomainProperties (Export DomainModule : DomainSignature). +Module NDomainProperties (Import NDomainModule : NDomainSignature). (* It also accepts module of type NatDomainEq *) -Open Local Scope NScope. +Open Local Scope NatScope. (* The following easily follows from transitivity of e and E, but we need to deal with the coercion *) @@ -79,4 +79,4 @@ assert (x == y); [rewrite Exx'; now rewrite Eyy' | rewrite <- H2; assert (H3 : e x y); [now apply -> E_equiv_e | now inversion H3]]]. Qed. -End DomainProperties. +End NDomainProperties. diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v index 83bcf8ebe..ebd22e142 100644 --- a/theories/Numbers/Natural/Axioms/NIso.v +++ b/theories/Numbers/Natural/Axioms/NIso.v @@ -2,19 +2,15 @@ Require Export NAxioms. Module Homomorphism (Nat1 Nat2 : NatSignature). -(*Module Import DomainProperties1 := DomainProperties Nat1.DomainModule. -Module Import DomainProperties2 := DomainProperties Nat2.DomainModule.*) -(* This registers Nat1.Domain.E and Nat2.Domain.E as setoid relations *) - -Notation Local N1 := Nat1.DomainModule.N. -Notation Local N2 := Nat2.DomainModule.N. -Notation Local E1 := Nat1.DomainModule.E. -Notation Local E2 := Nat2.DomainModule.E. +Notation Local N1 := Nat1.NDomainModule.N. +Notation Local N2 := Nat2.NDomainModule.N. +Notation Local E1 := Nat1.NDomainModule.E. +Notation Local E2 := Nat2.NDomainModule.E. Notation Local O1 := Nat1.O. Notation Local O2 := Nat2.O. Notation Local S1 := Nat1.S. Notation Local S2 := Nat2.S. -Notation Local "x == y" := (Nat2.DomainModule.E x y) (at level 70). +Notation Local "x == y" := (Nat2.NDomainModule.E x y) (at level 70). Definition homomorphism (f : N1 -> N2) : Prop := f O1 == O2 /\ forall x : N1, f (S1 x) == S2 (f x). @@ -43,7 +39,7 @@ Theorem natural_isomorphism_S : forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x). Proof. unfold natural_isomorphism; -intro x; now rewrite (Nat1.recursion_S Nat2.DomainModule.E); +intro x; now rewrite (Nat1.recursion_S Nat2.NDomainModule.E); [| unfold fun2_wd; intros; apply Nat2.S_wd |]. Qed. @@ -64,12 +60,12 @@ NatProperties Nat1, it refers to Nat1.induction. *) Module Hom12 := Homomorphism Nat1 Nat2. Module Hom21 := Homomorphism Nat2 Nat1. -Notation Local N1 := Nat1.DomainModule.N. -Notation Local N2 := Nat2.DomainModule.N. +Notation Local N1 := Nat1.NDomainModule.N. +Notation Local N2 := Nat2.NDomainModule.N. Notation Local h12 := Hom12.natural_isomorphism. Notation Local h21 := Hom21.natural_isomorphism. -Notation Local "x == y" := (Nat1.DomainModule.E x y) (at level 70). +Notation Local "x == y" := (Nat1.NDomainModule.E x y) (at level 70). Lemma iso_inverse : forall x : N1, h21 (h12 x) == x. @@ -91,10 +87,10 @@ Module Hom21 := Homomorphism Nat2 Nat1. Module Inverse121 := Inverse Nat1 Nat2. Module Inverse212 := Inverse Nat2 Nat1. -Notation Local N1 := Nat1.DomainModule.N. -Notation Local N2 := Nat2.DomainModule.N. -Notation Local E1 := Nat1.DomainModule.E. -Notation Local E2 := Nat2.DomainModule.E. +Notation Local N1 := Nat1.NDomainModule.N. +Notation Local N2 := Nat2.NDomainModule.N. +Notation Local E1 := Nat1.NDomainModule.E. +Notation Local E2 := Nat2.NDomainModule.E. Notation Local h12 := Hom12.natural_isomorphism. Notation Local h21 := Hom21.natural_isomorphism. diff --git a/theories/Numbers/Natural/Axioms/NLt.v b/theories/Numbers/Natural/Axioms/NLt.v deleted file mode 100644 index 254db11d6..000000000 --- a/theories/Numbers/Natural/Axioms/NLt.v +++ /dev/null @@ -1,169 +0,0 @@ -Require Export NAxioms. - -Module Type LtSignature. -Declare Module Export NatModule : NatSignature. -Open Local Scope NScope. - -Parameter Inline lt : N -> N -> bool. - -Notation "x < y" := (lt x y) : NScope. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. - -Axiom lt_0 : forall x, ~ (x < 0). -Axiom lt_S : forall x y, x < S y <-> x < y \/ x == y. -End LtSignature. - -Module LtProperties (Export LtModule : LtSignature). -Module Export NatPropertiesModule := NatProperties NatModule. -Open Local Scope NScope. - -Theorem lt_n_Sn : forall n, n < S n. -Proof. -intro n. apply <- lt_S. now right. -Qed. - -Theorem lt_closed_S : forall n m, n < m -> n < S m. -Proof. -intros. apply <- lt_S. now left. -Qed. - -Theorem lt_S_lt : forall n m, S n < m -> n < m. -Proof. -intro n; induct m. -intro H; absurd_hyp H; [apply lt_0 | assumption]. -intros x IH H. -apply -> lt_S in H; elim H. -intro H1; apply IH in H1; now apply lt_closed_S. -intro H1; rewrite <- H1. -apply lt_closed_S; apply lt_n_Sn. -Qed. - -Theorem lt_0_Sn : forall n, 0 < S n. -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. -Proof. -intros n m p; induct m. -intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption]. -intros x IH H1 H2. -apply -> lt_S in H1; elim H1. -intro H; apply IH; [assumption | apply lt_S_lt; assumption]. -intro H; rewrite H; apply lt_S_lt; assumption. -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]. -Qed. - -Theorem S_respects_lt : forall n m, S n < S m <-> n < m. -Proof. -intros n m; split. -intro H; apply -> lt_S in H; elim H. -intros; apply lt_S_lt; assumption. -intro H1; rewrite <- H1; apply lt_n_Sn. -induct m. -intro H; absurd_hyp H; [ apply lt_0 | assumption]. -intros x IH H. -apply -> lt_S in H; elim H; intro H1. -apply lt_transitive with (m := S x). -apply IH; assumption. -apply lt_n_Sn. -rewrite H1; apply lt_n_Sn. -Qed. - -Theorem lt_n_m : forall n m, n < m <-> S n < m \/ S n == m. -Proof. -intros n m; nondep_induct m. -split; intro H; [false_hyp H lt_0 | -destruct H as [H | H]; [false_hyp H lt_0 | false_hyp H S_0]]. -intros m; split; intro H. -apply -> lt_S in H. destruct H; [left; now apply <- S_respects_lt | right; now apply S_wd]. -destruct H; [apply lt_transitive with (m := S n); [apply lt_n_Sn | assumption] | -apply S_inj in H; rewrite H; apply lt_n_Sn]. -Qed. - -Theorem lt_irreflexive : forall n, ~ (n < n). -Proof. -induct n. -apply lt_0. -intro x; unfold not; intros H1 H2; apply H1; now apply -> S_respects_lt. -Qed. - -Theorem neq_0_lt : forall n, 0 # n -> 0 < n. -Proof. -induct n. -intro H; now elim H. -intros; apply lt_0_Sn. -Qed. - -Theorem lt_0_neq : forall n, 0 < n -> 0 # n. -Proof. -induct n. -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). -Proof. -unfold not; intros n m [H1 H2]. -now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|]. -Qed. - -Theorem eq_0_or_lt_0: forall n, 0 == n \/ 0 < n. -Proof. -induct n; [now left | intros x; right; apply lt_0_Sn]. -Qed. - -Theorem lt_options : forall n m, n < m -> S n < m \/ S n == m. -Proof. -intros n m; induct m. -intro H; false_hyp H lt_0. -intros x IH H. -apply -> lt_S in H; elim H; intro H1. -apply IH in H1; elim H1; intro H2. -left; apply lt_transitive with (m := x); [assumption | apply lt_n_Sn]. -rewrite H2; left; apply lt_n_Sn. -right; rewrite H1; reflexivity. -Qed. - -Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. -Proof. -intros n m; induct n. -assert (H : 0 == m \/ 0 < m); [apply eq_0_or_lt_0 | tauto]. -intros n IH. destruct IH as [H | H]. -assert (S n < m \/ S n == m); [now apply lt_options | tauto]. -destruct H as [H1 | H1]. -right; right; rewrite H1; apply lt_n_Sn. -right; right; apply lt_transitive with (m := n); [assumption | apply lt_n_Sn]. -Qed. - -Theorem lt_dichotomy : 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. -Qed. - -Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. -Proof. -intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |]. -now destruct A as [A | A]; [elim H | right]. -Qed. - -Theorem lt_exists_pred : forall n, 0 < n -> exists m, n == S m. -Proof. -induct n. -intro H; false_hyp H lt_0. -intros n IH H; now exists n. -Qed. - -End LtProperties. diff --git a/theories/Numbers/Natural/Axioms/NMinus.v b/theories/Numbers/Natural/Axioms/NMinus.v new file mode 100644 index 000000000..1f112a7b4 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NMinus.v @@ -0,0 +1,81 @@ +Require Export NPlusOrder. + +Module Type NMinusSignature. +Declare Module Export NPredModule : NPredSignature. +Open Local Scope NatScope. + +Parameter Inline minus : N -> N -> N. + +Notation "x - y" := (minus x y) : NatScope. + +Add Morphism minus with signature E ==> E ==> E as minus_wd. + +Axiom minus_0_r : forall n, n - 0 == n. +Axiom minus_S_r : forall n m, n - (S m) == P (n - m). + +End NMinusSignature. + +Module NMinusProperties (Import NMinusModule : NMinusSignature) + (Import NPlusModule : NPlusSignature with + Module NatModule := NMinusModule.NPredModule.NatModule) + (Import NOrderModule : NOrderSignature with + Module NatModule := NMinusModule.NPredModule.NatModule). +Module Export NPlusOrderPropertiesModule := + NPlusOrderProperties NPlusModule NOrderModule. +Open Local Scope NatScope. + +Theorem minus_1_r : forall n, n - 1 == P n. +Proof. +intro n; rewrite minus_S_r; now rewrite minus_0_r. +Qed. + +Theorem minus_0_l : forall n, 0 - n == 0. +Proof. +induct n. +apply minus_0_r. +intros n IH; rewrite minus_S_r; rewrite IH. now apply P_0. +Qed. + +Theorem minus_comm_S : forall n m, S n - S m == n - m. +Proof. +intro n; induct m. +rewrite minus_S_r. do 2 rewrite minus_0_r. now rewrite P_S. +intros m IH. rewrite minus_S_r. rewrite IH. now rewrite minus_S_r. +Qed. + +Theorem minus_S_l : forall n m, n <= m -> S m - n == S (m - n). +Proof. +intros n m H; pattern n, m; apply le_ind_rel. +unfold rel_wd. intros x x' H1 y y' H2; rewrite H1; now rewrite H2. +intros; now do 2 rewrite minus_0_r. +clear n m H. intros n m H1 H2. +now do 2 rewrite minus_comm_S. assumption. +Qed. + +Theorem minus_le : forall n m, n <= m -> n - m == 0. +Proof. +intros n m H; pattern n, m; apply le_ind_rel. +unfold rel_wd; intros x x' H1 y y' H2; rewrite H1; now rewrite H2. +apply minus_0_l. +clear n m H; intros n m H1 H2. now rewrite minus_comm_S. +assumption. +Qed. + +Theorem minus_diag : forall n, n - n == 0. +Proof. +intro n; apply minus_le; apply le_refl. +Qed. + +Theorem minus_plus : forall n m, n <= m -> (m - n) + n == m. +Proof. +intros n m H; pattern n, m; apply le_ind_rel. +unfold rel_wd; intros x x' H1 y y' H2; rewrite H1; now rewrite H2. +intro; rewrite minus_0_r; now rewrite plus_0_r. +clear n m H. intros n m _ H2. rewrite minus_comm_S. rewrite plus_n_Sm. +now rewrite H2. +assumption. +Qed. + +End NMinusProperties. + + diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v index 38af96b1d..3b0c1c5eb 100644 --- a/theories/Numbers/Natural/Axioms/NMiscFunct.v +++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v @@ -1,11 +1,10 @@ -Require Export Bool. (* To get the negb function *) +Require Import Bool. (* To get the orb and negb function *) Require Export NStrongRec. -Require Export NTimesLt. +Require Export NTimesOrder. -Module MiscFunctFunctor (NatMod : NatSignature). -Module Export NatPropertiesModule := NatProperties NatMod. +Module MiscFunctFunctor (Import NatMod : NatSignature). Module Export StrongRecPropertiesModule := StrongRecProperties NatMod. -Open Local Scope NScope. +Open Local Scope NatScope. (*****************************************************) (** Addition *) @@ -84,6 +83,16 @@ Definition lt (m : N) : N -> bool := (fun _ f => fun n => recursion false (fun n' _ => f n') n) m. +(* It would be more efficient to make a three-way comparison, i.e., +return Eq, Lt, or Gt, but since these are no-use default functions, +we define <= as (< or =) *) +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. + 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. Qed. @@ -286,7 +295,7 @@ Qed. (** via recursion, we form the corresponding modules and *) (** apply the properties functors to these modules *) -Module DefaultPlusModule <: PlusSignature. +Module NDefaultPlusModule <: NPlusSignature. Module NatModule := NatMod. (* If we used the name NatModule instead of NatMod then this would @@ -310,10 +319,10 @@ Proof. exact plus_S. Qed. -End DefaultPlusModule. +End NDefaultPlusModule. -Module DefaultTimesModule <: TimesSignature. -Module PlusModule := DefaultPlusModule. +Module NDefaultTimesModule <: NTimesSignature. +Module NPlusModule := NDefaultPlusModule. Definition times := times. @@ -332,9 +341,9 @@ Proof. exact times_S. Qed. -End DefaultTimesModule. +End NDefaultTimesModule. -Module DefaultLtModule <: LtSignature. +Module NDefaultOrderModule <: NOrderSignature. Module NatModule := NatMod. Definition lt := lt. @@ -354,16 +363,9 @@ Proof. exact lt_S. Qed. -End DefaultLtModule. - -Module Export DefaultPlusProperties := PlusProperties DefaultPlusModule. -Module Export DefaultTimesProperties := TimesProperties DefaultTimesModule. -Module Export DefaultLtProperties := LtProperties DefaultLtModule. -Module Export DefaultPlusLtProperties := PlusLtProperties DefaultPlusModule DefaultLtModule. -Module Export DefaultTimesLtProperties := TimesLtProperties DefaultTimesModule DefaultLtModule. +End NDefaultOrderModule. -(*Opaque MiscFunctFunctor.plus. -Check plus_comm. (* This produces the following *) -Eval compute in (forall n m : PlusModule.NatModule.DomainModule.N, plus n m == plus m n).*) +Module Export DefaultTimesOrderProperties := + NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule. End MiscFunctFunctor. diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v new file mode 100644 index 000000000..c4e9a21a7 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NOrder.v @@ -0,0 +1,263 @@ +Require Export NAxioms. + +Module Type NOrderSignature. +Declare Module Export NatModule : NatSignature. +Open Local Scope NatScope. + +Parameter Inline lt : N -> N -> bool. +Parameter Inline le : N -> N -> bool. + +Notation "x < y" := (lt x y) : NatScope. +Notation "x <= y" := (le x y) : 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. + +Axiom le_lt : forall x y, x <= y <-> x < y \/ x == y. +Axiom lt_0 : forall x, ~ (x < 0). +Axiom lt_S : forall x y, x < S y <-> x <= y. +End NOrderSignature. + +Module NOrderProperties (Import NOrderModule : NOrderSignature). +Module Export NatPropertiesModule := NatProperties NatModule. +Open Local Scope NatScope. + +Ltac le_intro1 := rewrite le_lt; left. +Ltac le_intro2 := rewrite le_lt; right. +Ltac le_elim H := rewrite le_lt in H; destruct H as [H | H]. + +Theorem le_refl : forall n, n <= n. +Proof. +intro; now le_intro2. +Qed. + +Theorem le_0_r : forall n, n <= 0 -> n == 0. +Proof. +intros n H; le_elim H; [false_hyp H lt_0 | assumption]. +Qed. + +Theorem lt_n_Sn : forall n, n < S n. +Proof. +intro n. apply <- lt_S. now le_intro2. +Qed. + +Theorem lt_closed_S : forall n m, n < m -> n < S m. +Proof. +intros. apply <- lt_S. now le_intro1. +Qed. + +Theorem lt_S_lt : forall n m, S n < m -> n < m. +Proof. +intro n; induct m. +intro H; absurd_hyp H; [apply lt_0 | assumption]. +intros x IH H. +apply -> lt_S in H. le_elim H. +apply IH in H; now apply lt_closed_S. +rewrite <- H. +apply lt_closed_S; apply lt_n_Sn. +Qed. + +Theorem lt_0_Sn : forall n, 0 < S n. +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. +Proof. +intros n m p; induct m. +intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption]. +intros x IH H1 H2. +apply -> lt_S in H1. le_elim H1. +apply IH; [assumption | apply lt_S_lt; assumption]. +rewrite H1; apply lt_S_lt; assumption. +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]. +Qed. + +Theorem lt_resp_S : forall n m, S n < S m <-> n < m. +Proof. +intros n m; split. +intro H; apply -> lt_S in H; le_elim H. +intros; apply lt_S_lt; assumption. +rewrite <- H; apply lt_n_Sn. +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 IH; assumption. +apply lt_n_Sn. +rewrite H; apply lt_n_Sn. +Qed. + +Theorem le_resp_S : forall n m, S n <= S m <-> n <= m. +Proof. +intros n m; do 2 rewrite le_lt. +pose proof (S_wd n m); pose proof (S_inj n m); pose proof (lt_resp_S n m); tauto. +Qed. + +Theorem lt_le_S_l : forall n m, n < m <-> S n <= m. +Proof. +intros n m; nondep_induct m. +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] | +apply S_inj in H; rewrite H; apply lt_n_Sn]. +Qed. + +Theorem le_S_0 : forall n, ~ (S n <= 0). +Proof. +intros n H; apply <- lt_le_S_l in H; false_hyp H lt_0. +Qed. + +Theorem le_S_l_le : forall n m, S n <= m -> n <= m. +Proof. +intros; le_intro1; now apply <- lt_le_S_l. +Qed. + +Theorem lt_irreflexive : 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 neq_0_lt : forall n, 0 # n -> 0 < n. +Proof. +induct n. +intro H; now elim H. +intros; apply lt_0_Sn. +Qed. + +Theorem lt_0_neq : forall n, 0 < n -> 0 # n. +Proof. +induct n. +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). +Proof. +unfold not; intros n m [H1 H2]. +now apply (lt_transitive n m n) in H1; [false_hyp H1 lt_irreflexive|]. +Qed. + +Theorem le_0_l: forall n, 0 <= n. +Proof. +induct n; [now le_intro2 | intros; le_intro1; apply lt_0_Sn]. +Qed. + +Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. +Proof. +intros n m; induct n. +assert (H : 0 <= m); [apply le_0_l | apply -> le_lt in H; tauto]. +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]. +Qed. + +Theorem lt_dichotomy : 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. +Qed. + +Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. +Proof. +intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |]. +now destruct A as [A | A]; [elim H | right]. +Qed. + +Theorem lt_exists_pred : forall n, 0 < n -> exists m, n == S m. +Proof. +induct n. +intro H; false_hyp H lt_0. +intros n IH H; now exists n. +Qed. + +(** Elimination principles for < and <= *) + +Section Induction1. + +Variable Q : N -> Prop. +Hypothesis Q_wd : pred_wd E Q. +Variable n : N. + +Add Morphism Q with signature E ==> iff as Q_morph1. +Proof Q_wd. + +Theorem le_ind : + Q n -> + (forall m, n <= m -> Q m -> Q (S m)) -> + forall m, n <= m -> Q m. +Proof. +intros Base Step. induct m. +intro H. apply le_0_r in H. now rewrite <- H. +intros m IH H. le_elim H. +apply -> lt_S in H. now apply Step; [| apply IH]. +now rewrite <- H. +Qed. + +Theorem lt_ind : + Q (S n) -> + (forall m, n < m -> Q m -> Q (S m)) -> + forall m, n < m -> Q m. +Proof. +intros Base Step. induct m. +intro H; false_hyp H lt_0. +intros m IH H. apply -> lt_S in H. le_elim H. +now apply Step; [| apply IH]. now rewrite <- H. +Qed. + +End Induction1. + +Section Induction2. + +(* Variable Q : relation N. -- does not work !!! *) +Variable Q : N -> N -> Prop. +Hypothesis Q_wd : rel_wd E Q. + +Add Morphism Q with signature E ==> E ==> iff as Q_morph2. +Proof Q_wd. + +Theorem le_ind_rel : + (forall m, Q 0 m) -> + (forall n m, n <= m -> Q n m -> Q (S n) (S m)) -> + forall n m, n <= m -> Q n m. +Proof. +intros Base Step; induct n. +intros; apply Base. +intros n IH m; nondep_induct m. +intro H; false_hyp H le_S_0. +intros m H. apply -> le_resp_S in H. now apply Step; [| apply IH]. +Qed. + +Theorem lt_ind_rel : + (forall m, Q 0 (S m)) -> + (forall n m, n < m -> Q n m -> Q (S n) (S m)) -> + forall n m, n < m -> Q n m. +Proof. +intros Base Step; induct n. +intros m H. apply lt_exists_pred in H; destruct H as [m' H]. +rewrite H; apply Base. +intros n IH m; nondep_induct m. +intro H; false_hyp H lt_0. +intros m H. apply -> lt_resp_S in H. now apply Step; [| apply IH]. +Qed. + +End Induction2. + +End NOrderProperties. diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v index 6f51330f3..cf6738750 100644 --- a/theories/Numbers/Natural/Axioms/NOtherInd.v +++ b/theories/Numbers/Natural/Axioms/NOtherInd.v @@ -1,6 +1,6 @@ Require Export NDomain. -Declare Module Export DomainModule : DomainSignature. -Open Local Scope NScope. +Declare Module Export NDomainModule : NDomainSignature. +Open Local Scope NatScope. Parameter O : N. Parameter S : N -> N. diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v index 63cc8a40f..0ae12df97 100644 --- a/theories/Numbers/Natural/Axioms/NPlus.v +++ b/theories/Numbers/Natural/Axioms/NPlus.v @@ -1,25 +1,23 @@ Require Export NAxioms. -Module Type PlusSignature. +Module Type NPlusSignature. Declare Module Export NatModule : NatSignature. -(* We use Export here because if we have an access to plus, -then we need also an access to S and N *) -Open Local Scope NScope. +Open Local Scope NatScope. Parameter Inline plus : N -> N -> N. -Notation "x + y" := (plus x y) : NScope. +Notation "x + y" := (plus x y) : NatScope. Add Morphism plus with signature E ==> E ==> E as plus_wd. Axiom plus_0_n : forall n, 0 + n == n. Axiom plus_Sn_m : forall n m, (S n) + m == S (n + m). -End PlusSignature. +End NPlusSignature. -Module PlusProperties (Export PlusModule : PlusSignature). +Module NPlusProperties (Import NPlusModule : NPlusSignature). Module Export NatPropertiesModule := NatProperties NatModule. -Open Local Scope NScope. +Open Local Scope NatScope. Theorem plus_0_r : forall n, n + 0 == n. Proof. @@ -199,4 +197,4 @@ rewrite plus_Sn_m in H. apply S_inj in H. apply plus_eq_0 in H; split; [apply S_wd | ]; tauto. Qed. -End PlusProperties. +End NPlusProperties. diff --git a/theories/Numbers/Natural/Axioms/NPlusLt.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v index 3724f9ec5..fe43ff38d 100644 --- a/theories/Numbers/Natural/Axioms/NPlusLt.v +++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v @@ -1,12 +1,12 @@ Require Export NPlus. -Require Export NLt. +Require Export NOrder. -Module PlusLtProperties (PlusModule : PlusSignature) - (LtModule : LtSignature with - Module NatModule := PlusModule.NatModule). -Module Export PlusPropertiesModule := PlusProperties PlusModule. -Module Export LtPropertiesModule := LtProperties LtModule. -Open Local Scope NScope. +Module NPlusOrderProperties (Import NPlusModule : NPlusSignature) + (Import NOrderModule : NOrderSignature with + Module NatModule := NPlusModule.NatModule). +Module Export NPlusPropertiesModule := NPlusProperties NPlusModule. +Module Export NOrderPropertiesModule := NOrderProperties NOrderModule. +Open Local Scope NatScope. (* Print All locks up here !!! *) Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. @@ -21,7 +21,7 @@ Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. Proof. intros n m p H; induct p. do 2 rewrite plus_0_n; assumption. -intros x IH. do 2 rewrite plus_Sn_m. now apply <- S_respects_lt. +intros x IH. do 2 rewrite plus_Sn_m. now apply <- lt_resp_S. Qed. Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. @@ -44,7 +44,7 @@ intros n m p; induct p. now do 2 rewrite plus_0_n. intros x IH H. do 2 rewrite plus_Sn_m in H. -apply IH; now apply -> S_respects_lt. +apply IH; now apply -> lt_resp_S. Qed. -End PlusLtProperties. +End NPlusOrderProperties. diff --git a/theories/Numbers/Natural/Axioms/NPred.v b/theories/Numbers/Natural/Axioms/NPred.v new file mode 100644 index 000000000..d3da22660 --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NPred.v @@ -0,0 +1,45 @@ +Require Export NAxioms. + +(* We would like to have a signature for the predecessor: first, to be +able to provide an efficient implementation, and second, to be able to +use this function in the signatures defining other functions, e.g., +subtraction. If we just define predecessor by recursion in +NatProperties functor, we would not be able to use it in other +signatures. *) + +Module Type NPredSignature. +Declare Module Export NatModule : NatSignature. +Open Local Scope NatScope. + +Parameter Inline P : N -> N. + +Add Morphism P with signature E ==> E as P_wd. + +Axiom P_0 : P 0 == 0. +Axiom P_S : forall n, P (S n) == n. + +End NPredSignature. + +Module NDefPred (Import NM : NatSignature) <: NPredSignature. +Module NatModule := NM. +Open Local Scope NatScope. + +Definition P (n : N) : N := recursion 0 (fun m _ : N => m) n. + +Add Morphism P with signature E ==> E as P_wd. +Proof. +intros; unfold P. +now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. +Qed. + +Theorem P_0 : P 0 == 0. +Proof. +unfold P; now rewrite recursion_0. +Qed. + +Theorem P_S : forall n, P (S n) == n. +Proof. +intro n; unfold P; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |]. +Qed. + +End NDefPred. diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v index a2e73f99a..5c9a65781 100644 --- a/theories/Numbers/Natural/Axioms/NStrongRec.v +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -1,8 +1,8 @@ Require Export NAxioms. -Module StrongRecProperties (NatModule : NatSignature). +Module StrongRecProperties (Import NatModule : NatSignature). Module Export NatPropertiesModule := NatProperties NatModule. -Open Local Scope NScope. +Open Local Scope NatScope. Section StrongRecursion. diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v index 4d1d2b0ca..2dd052201 100644 --- a/theories/Numbers/Natural/Axioms/NTimes.v +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -1,23 +1,23 @@ Require Export NPlus. -Module Type TimesSignature. -Declare Module Export PlusModule : PlusSignature. -Open Local Scope NScope. +Module Type NTimesSignature. +Declare Module Export NPlusModule : NPlusSignature. +Open Local Scope NatScope. Parameter Inline times : N -> N -> N. -Notation "x * y" := (times x y) : NScope. +Notation "x * y" := (times x y) : NatScope. Add Morphism times with signature E ==> E ==> E as times_wd. Axiom times_0_n : forall n, 0 * n == 0. Axiom times_Sn_m : forall n m, (S n) * m == m + n * m. -End TimesSignature. +End NTimesSignature. -Module TimesProperties (Export TimesModule : TimesSignature). -Module Export PlusPropertiesModule := PlusProperties PlusModule. -Open Local Scope NScope. +Module NTimesProperties (Import NTimesModule : NTimesSignature). +Module Export NPlusPropertiesModule := NPlusProperties NPlusModule. +Open Local Scope NatScope. Theorem mult_0_r : forall n, n * 0 == 0. Proof. @@ -160,4 +160,4 @@ 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. -End TimesProperties. +End NTimesProperties. diff --git a/theories/Numbers/Natural/Axioms/NTimesLt.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v index 36989f1b3..f6afd5999 100644 --- a/theories/Numbers/Natural/Axioms/NTimesLt.v +++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v @@ -1,14 +1,13 @@ Require Export NTimes. -Require Export NPlusLt. +Require Export NPlusOrder. -Module TimesLtProperties (TimesModule : TimesSignature) - (LtModule : LtSignature with - Module NatModule := TimesModule.PlusModule.NatModule). -Module Export TimesPropertiesModule := - TimesProperties TimesModule. -Module Export PlusLtPropertiesModule := - PlusLtProperties TimesModule.PlusModule LtModule. -Open Local Scope NScope. +Module NTimesOrderProperties (Import NTimesModule : NTimesSignature) + (Import NOrderModule : NOrderSignature with + Module NatModule := NTimesModule.NPlusModule.NatModule). +Module Export NTimesPropertiesModule := NTimesProperties NTimesModule. +Module Export NPlusOrderPropertiesModule := + NPlusOrderProperties NTimesModule.NPlusModule NOrderModule. +Open Local Scope NatScope. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. Proof. @@ -61,4 +60,4 @@ now apply mult_S_lt_compat_l; assumption. now apply mult_lt_compat_r; [| apply lt_positive with (n := p)]. Qed. -End TimesLtProperties. +End NTimesOrderProperties. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 77fbdcaf7..f87baf687 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -2,12 +2,13 @@ Require Import NArith. Require Import Ndec. Require Export NDepRec. -Require Export NTimesLt. +Require Export NTimesOrder. +Require Export NMinus. Require Export NMiscFunct. Open Local Scope N_scope. -Module BinaryDomain : DomainEqSignature +Module NBinaryDomain : NDomainEqSignature with Definition N := N with Definition E := (@eq N) with Definition e := Neqb. @@ -31,11 +32,10 @@ Add Relation N E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. -End BinaryDomain. +End NBinaryDomain. Module BinaryNat <: NatSignature. - -Module Export DomainModule := BinaryDomain. +Module Export NDomainModule := NBinaryDomain. Definition O := N0. Definition S := Nsucc. @@ -92,8 +92,8 @@ Qed. End BinaryNat. -Module BinaryDepRec <: DepRecSignature. -Module Export DomainModule := BinaryDomain. +Module NBinaryDepRec <: NDepRecSignature. +Module Export NDomainModule := NBinaryDomain. Module Export NatModule := BinaryNat. Definition dep_recursion := Nrec. @@ -112,10 +112,9 @@ Proof. intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step. Qed. -End BinaryDepRec. - -Module BinaryPlus <: PlusSignature. +End NBinaryDepRec. +Module NBinaryPlus <: NPlusSignature. Module Export NatModule := BinaryNat. Definition plus := Nplus. @@ -135,10 +134,10 @@ Proof. exact Nplus_succ. Qed. -End BinaryPlus. +End NBinaryPlus. -Module BinaryTimes <: TimesSignature. -Module Export PlusModule := BinaryPlus. +Module NBinaryTimes <: NTimesSignature. +Module Export NPlusModule := NBinaryPlus. Definition times := Nmult. @@ -157,9 +156,9 @@ Proof. exact Nmult_Sn_m. Qed. -End BinaryTimes. +End NBinaryTimes. -Module BinaryLt <: LtSignature. +Module NBinaryLt <: NLtSignature. Module Export NatModule := BinaryNat. Definition lt (m n : N) := less_than (Ncompare m n). @@ -184,9 +183,9 @@ assert (H2 : lt x y <-> Ncompare x y = Lt); pose proof (Ncompare_n_Sm x y) as H. tauto. Qed. -End BinaryLt. +End NBinaryLt. -Module Export BinaryTimesLtProperties := TimesLtProperties BinaryTimes BinaryLt. +Module Export NBinaryTimesLtProperties := NTimesLtProperties NBinaryTimes NBinaryLt. (*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 00248a53c..9927bde0b 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,11 +1,14 @@ Require Export NDepRec. -Require Export NTimesLt. +Require Export NTimesOrder. +Require Export NMinus. Require Export NMiscFunct. -Module PeanoDomain : DomainEqSignature - with Definition N := nat +Module NPeanoDomain <: NDomainEqSignature. +(* with Definition N := nat with Definition E := (@eq nat) - with Definition e := eq_nat_bool. + with Definition e := eq_nat_bool.*) + +Delimit Scope NatScope with Nat. Definition N := nat. Definition E := (@eq nat). @@ -26,10 +29,10 @@ Add Relation N E transitivity proved by (proj1 (proj2 E_equiv)) as E_rel. -End PeanoDomain. +End NPeanoDomain. Module PeanoNat <: NatSignature. -Module Export DomainModule := PeanoDomain. +Module Export NDomainModule := NPeanoDomain. Definition O := 0. Definition S := S. @@ -80,9 +83,9 @@ Qed. End PeanoNat. -Module PeanoDepRec <: DepRecSignature. +Module NPeanoDepRec <: NDepRecSignature. -Module Export DomainModule := PeanoDomain. +Module Export NDomainModule := NPeanoDomain. Module Export NatModule <: NatSignature := PeanoNat. Definition dep_recursion := nat_rec. @@ -101,10 +104,9 @@ Proof. reflexivity. Qed. -End PeanoDepRec. - -Module PeanoPlus <: PlusSignature. +End NPeanoDepRec. +Module NPeanoPlus <: NPlusSignature. Module Export NatModule := PeanoNat. Definition plus := plus. @@ -124,10 +126,10 @@ Proof. reflexivity. Qed. -End PeanoPlus. +End NPeanoPlus. -Module PeanoTimes <: TimesSignature. -Module Export PlusModule := PeanoPlus. +Module NPeanoTimes <: NTimesSignature. +Module Export NPlusModule := NPeanoPlus. Definition times := mult. @@ -146,9 +148,9 @@ Proof. auto. Qed. -End PeanoTimes. +End NPeanoTimes. -Module PeanoLt <: LtSignature. +Module NPeanoLt <: NLtSignature. Module Export NatModule := PeanoNat. Definition lt := lt_bool. @@ -168,14 +170,15 @@ Proof. exact lt_bool_S. Qed. -End PeanoLt. +End NPeanoLt. -(* Obtaining properties for +, *, <, and their combinations *) +Module NPeanoPred <: NPredSignature. -Module Export PeanoTimesLtProperties := TimesLtProperties PeanoTimes PeanoLt. -Module Export PeanoDepRecTimesProperties := - DepRecTimesProperties PeanoDepRec PeanoTimes. +(* Obtaining properties for +, *, <, and their combinations *) -(*Module MiscFunctModule := MiscFunctFunctor PeanoNat.*) -(* The instruction above adds about 1M to the size of the .vo file !!! *) +Module Export NPeanoTimesLtProperties := NTimesLtProperties NPeanoTimes NPeanoLt. +Module Export NPeanoDepRecTimesProperties := + NDepRecTimesProperties NPeanoDepRec NPeanoTimes. +Module MiscFunctModule := MiscFunctFunctor PeanoNat. +(* The instruction above adds about 0.5M to the size of the .vo file !!! *) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 2fe547681..a23fb0bc0 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -18,7 +18,14 @@ Definition eq_bool := (@eq bool). Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. Coercion eq_true : bool >-> Sortclass. -Theorem neg_eq_true : forall x : bool, ~ x -> x = false. +Theorem eq_true_unfold : forall b : bool, b <-> b = true. +Proof. +intro b; split; intro H. +now inversion H. +now rewrite H. +Qed. + +Theorem eq_true_neg : forall x : bool, ~ x -> x = false. Proof. intros x H; destruct x; [elim (H is_eq_true) | reflexivity]. Qed. |