diff options
| author |  emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-13 11:19:53 +0000 |
|---|---|---|
| committer | emakarov <emakarov@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-09-13 11:19:53 +0000 |
| commit | 46667827cc7884d28fc048ff74b19a6517f19d59 (patch) | |
| tree | ce1b60528ac6eb86c6b6a25b0e577fc33ceeb4a2 | |
| parent | c9f6bc800e589551a9e812b570269934b237a053 (diff) | |
Update before joining all signatures into one.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10119 85f007b7-540e-0410-9357-904b9bb8a0f7
35 files changed, 1994 insertions, 1704 deletions
diff --git a/theories/Numbers/Integer/Axioms/ZAxioms.v b/theories/Numbers/Integer/Axioms/ZAxioms.v deleted file mode 100644 index 6527bd11c..000000000 --- a/theories/Numbers/Integer/Axioms/ZAxioms.v +++ /dev/null @@ -1,119 +0,0 @@ -Require Export ZDomain. - -Module Type IntSignature. -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 : IntScope. - -Add Morphism S with signature E ==> E as S_wd. -Add Morphism P with signature E ==> E as P_wd. - -Axiom S_inj : forall x y : Z, S x == S y -> x == y. -Axiom S_P : forall x : Z, S (P x) == x. - -Axiom 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. - -End IntSignature. - -Module IntProperties (Import IntModule : IntSignature). -Module Export ZDomainPropertiesModule := ZDomainProperties ZDomainModule. -Open Local Scope IntScope. - -Ltac induct n := - try intros until n; - pattern n; apply induction; clear n; - [unfold NumPrelude.pred_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | | |]. - -Theorem P_inj : forall x y, P x == P y -> x == y. -Proof. -intros x y H. -setoid_replace x with (S (P x)); [| symmetry; apply S_P]. -setoid_replace y with (S (P y)); [| symmetry; apply S_P]. -now rewrite H. -Qed. - -Theorem P_S : forall x, P (S x) == x. -Proof. -intro x. -apply S_inj. -now rewrite S_P. -Qed. - -(* The following tactics are intended for replacing a certain -occurrence of a term t in the goal by (S (P t)) or by (P (S t)). -Unfortunately, this cannot be done by setoid_replace tactic for two -reasons. First, it seems impossible to do rewriting when one side of -the equation in question (S_P or P_S) is a variable, due to bug 1604. -This does not work even when the predicate is an identifier (e.g., -when one tries to rewrite (Q x) into (Q (S (P x)))). Second, the -setoid_rewrite tactic, like the ordinary rewrite tactic, does not -allow specifying the exact occurrence of the term to be rewritten. Now -while not in the setoid context, this occurrence can be specified -using the pattern tactic, it does not work with setoids, since pattern -creates a lambda abstractuion, and setoid_rewrite does not work with -them. *) - -Ltac rewrite_SP t set_tac repl thm := -let x := fresh "x" in -set_tac x t; -setoid_replace x with (repl x); [| symmetry; apply thm]; -unfold x; clear x. - -Tactic Notation "rewrite_S_P" constr(t) := -rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) S_P. - -Tactic Notation "rewrite_S_P" constr(t) "at" integer(k) := -rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) S_P. - -Tactic Notation "rewrite_P_S" constr(t) := -rewrite_SP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) P_S. - -Tactic Notation "rewrite_P_S" constr(t) "at" integer(k) := -rewrite_SP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) P_S. - -(* One can add tactic notations for replacements in assumptions rather -than in the goal. For the reason of many possible variants, the core -of the tactic is factored out. *) - -Section Induction. - -Variable Q : Z -> Prop. -Hypothesis Q_wd : pred_wd E Q. - -Add Morphism Q with signature E ==> iff as Q_morph. -Proof Q_wd. - -Theorem induction_n : - forall n, Q n -> - (forall m, Q m -> Q (S m)) -> - (forall m, Q m -> Q (P m)) -> forall m, Q m. -Proof. -induct n. -intros; now apply induction. -intros n IH H1 H2 H3; apply IH; try assumption. apply H3 in H1; now rewrite P_S in H1. -intros n IH H1 H2 H3; apply IH; try assumption. apply H2 in H1; now rewrite S_P in H1. -Qed. - -End Induction. - -Ltac induct_n k n := - try intros until k; - pattern k; apply induction_n with (n := n); clear k; - [unfold NumPrelude.pred_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | | |]. - -End IntProperties. diff --git a/theories/Numbers/Integer/Axioms/ZBase.v b/theories/Numbers/Integer/Axioms/ZBase.v new file mode 100644 index 000000000..e0b753d4e --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZBase.v @@ -0,0 +1,103 @@ +Require Export NumPrelude. +Require Import NZBase. + +Module Type ZBaseSig. + +Parameter Z : Set. +Parameter ZE : Z -> Z -> Prop. + +Delimit Scope IntScope with Int. +Bind Scope IntScope with Z. +Open Local Scope IntScope. + +Notation "x == y" := (ZE x y) (at level 70) : IntScope. +Notation "x ~= y" := (~ ZE x y) (at level 70) : IntScope. + +Axiom ZE_equiv : equiv Z ZE. + +Add Relation Z ZE + reflexivity proved by (proj1 ZE_equiv) + symmetry proved by (proj2 (proj2 ZE_equiv)) + transitivity proved by (proj1 (proj2 ZE_equiv)) +as ZE_rel. + +Parameter Z0 : Z. +Parameter Zsucc : Z -> Z. + +Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd. + +Notation "0" := Z0 : IntScope. +Notation "'S'" := Zsucc : IntScope. +Notation "1" := (S 0) : IntScope. +(* Note: if we put the line declaring 1 before the line declaring 'S' and +change (S 0) to (Zsucc 0), then 1 will be parsed but not printed ((S 0) +will be printed instead of 1) *) + +Axiom Zsucc_inj : forall x y : Z, S x == S y -> x == y. + +Axiom Zinduction : + forall A : predicate Z, predicate_wd ZE A -> + A 0 -> (forall x, A x <-> A (S x)) -> forall x, A x. + +End ZBaseSig. + +Module ZBasePropFunct (Import ZBaseMod : ZBaseSig). +Open Local Scope IntScope. + +Module NZBaseMod <: NZBaseSig. + +Definition NZ := Z. +Definition NZE := ZE. +Definition NZ0 := Z0. +Definition NZsucc := Zsucc. + +(* Axioms *) +Definition NZE_equiv := ZE_equiv. + +Add Relation NZ NZE + 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 NZsucc with signature NZE ==> NZE as NZsucc_wd. +Proof Zsucc_wd. + +Definition NZsucc_inj := Zsucc_inj. +Definition NZinduction := Zinduction. + +End NZBaseMod. + +Module Export NZBasePropMod := NZBasePropFunct NZBaseMod. + +Theorem Zneq_symm : forall n m : Z, n ~= m -> m ~= n. +Proof NZneq_symm. + +Theorem Zcentral_induction : + forall A : Z -> Prop, predicate_wd ZE A -> + forall z : Z, A z -> + (forall n : Z, A n <-> A (S n)) -> + forall n : Z, A n. +Proof NZcentral_induction. + +Theorem Zsucc_inj_wd : forall n m, S n == S m <-> n == m. +Proof NZsucc_inj_wd. + +Theorem Zsucc_inj_neg : forall n m, S n ~= S m <-> n ~= m. +Proof NZsucc_inj_wd_neg. + +Tactic Notation "Zinduct" ident(n) := + induction_maker n ltac:(apply Zinduction). +(* FIXME: Zinduction probably has to be redeclared in the functor because +the parameters like Zsucc are not unfolded for Zinduction in the signature *) + +Tactic Notation "Zinduct" ident(n) constr(z) := + induction_maker n ltac:(apply Zcentral_induction with z). + +End ZBasePropFunct. + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZDec.v b/theories/Numbers/Integer/Axioms/ZDec.v new file mode 100644 index 000000000..9a7aaa099 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZDec.v @@ -0,0 +1,8 @@ +Axiom E_equiv_e : forall x y : Z, E x y <-> e x y. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZDomain.v b/theories/Numbers/Integer/Axioms/ZDomain.v index 579f8face..028128cf7 100644 --- a/theories/Numbers/Integer/Axioms/ZDomain.v +++ b/theories/Numbers/Integer/Axioms/ZDomain.v @@ -53,3 +53,10 @@ Declare Left Step ZE_stepl. Declare Right Step (proj1 (proj2 E_equiv)). End ZDomainProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZOrder.v b/theories/Numbers/Integer/Axioms/ZOrder.v index 19a66aea3..cc834b442 100644 --- a/theories/Numbers/Integer/Axioms/ZOrder.v +++ b/theories/Numbers/Integer/Axioms/ZOrder.v @@ -1,7 +1,7 @@ Require Export ZAxioms. Module Type ZOrderSignature. -Declare Module Export IntModule : IntSignature. +Declare Module Export ZBaseMod : ZBaseSig. Open Local Scope IntScope. Parameter Inline lt : Z -> Z -> bool. @@ -14,13 +14,13 @@ 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. +Axiom lt_succ : forall n m, n < (S m) <-> n <= m. End ZOrderSignature. Module ZOrderProperties (Import ZOrderModule : ZOrderSignature). -Module Export IntPropertiesModule := IntProperties IntModule. +Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod. Open Local Scope IntScope. Ltac Zle_intro1 := rewrite le_lt; left. @@ -32,147 +32,147 @@ Proof. intro n; now Zle_intro2. Qed. -Theorem lt_n_Sn : forall n, n < S n. +Theorem lt_n_succn : forall n, n < S n. Proof. -intro n. rewrite lt_S. now Zle_intro2. +intro n. rewrite lt_succ. now Zle_intro2. Qed. -Theorem le_n_Sn : forall n, n <= S n. +Theorem le_n_succn : forall n, n <= S n. Proof. -intro; Zle_intro1; apply lt_n_Sn. +intro; Zle_intro1; apply lt_n_succn. Qed. -Theorem lt_Pn_n : forall n, P n < n. +Theorem lt_predn_n : forall n, P n < n. Proof. -intro n; rewrite_S_P n at 2; apply lt_n_Sn. +intro n; rewrite_succ_pred n at 2; apply lt_n_succn. Qed. -Theorem le_Pn_n : forall n, P n <= n. +Theorem le_predn_n : forall n, P n <= n. Proof. -intro; Zle_intro1; apply lt_Pn_n. +intro; Zle_intro1; apply lt_predn_n. Qed. -Theorem lt_n_Sm : forall n m, n < m -> n < S m. +Theorem lt_n_succm : forall n m, n < m -> n < S m. Proof. -intros. rewrite lt_S. now Zle_intro1. +intros. rewrite lt_succ. now Zle_intro1. Qed. -Theorem le_n_Sm : forall n m, n <= m -> n <= S m. +Theorem le_n_succm : forall n m, n <= m -> n <= S m. Proof. -intros n m H; rewrite <- lt_S in H; now Zle_intro1. +intros n m H; rewrite <- lt_succ in H; now Zle_intro1. Qed. -Theorem lt_n_m_P : forall n m, n < m <-> n <= P m. +Theorem lt_n_m_pred : forall n m, n < m <-> n <= P m. Proof. -intros n m; rewrite_S_P m; rewrite P_S; apply lt_S. +intros n m; rewrite_succ_pred m; rewrite pred_succ; apply lt_succ. Qed. -Theorem not_le_n_Pn : forall n, ~ n <= P n. +Theorem not_le_n_predn : forall n, ~ n <= P n. Proof. 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. +apply lt_n_succm in H; rewrite succ_pred in H; false_hyp H lt_irr. +pose proof (lt_predn_n n) as H1; rewrite <- H in H1; false_hyp H1 lt_irr. Qed. -Theorem le_S : forall n m, n <= S m <-> n <= m \/ n == S m. +Theorem le_succ : forall n m, n <= S m <-> n <= m \/ n == S m. Proof. -intros n m; rewrite le_lt. now rewrite lt_S. +intros n m; rewrite le_lt. now rewrite lt_succ. Qed. -Theorem lt_P : forall n m, (P n) < m <-> n <= m. +Theorem lt_pred : forall n m, (P n) < m <-> n <= m. Proof. intro n; induct_n m (P n). -split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_Pn. +split; intro H. false_hyp H lt_irr. false_hyp H not_le_n_predn. intros m IH; split; intro H. -apply -> lt_S in H; Zle_elim H. -apply -> IH in H; now apply le_n_Sm. -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. +apply -> lt_succ in H; Zle_elim H. +apply -> IH in H; now apply le_n_succm. +rewrite <- H; rewrite succ_pred; now Zle_intro2. +apply -> le_succ in H; destruct H as [H | H]. +apply <- IH in H. now apply lt_n_succm. rewrite H; rewrite pred_succ; apply lt_n_succn. 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; Zle_elim H. now apply -> lt_n_m_P. +pose proof H as H1. apply lt_n_succm in H; rewrite succ_pred in H. +apply -> IH in H; Zle_elim H. now apply -> lt_n_m_pred. 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. Zle_elim H. -assumption. apply P_inj in H; rewrite H in H1; false_hyp H1 not_le_n_Pn. +pose proof H as H1. apply le_n_succm in H. rewrite succ_pred in H. +apply <- IH in H. apply -> lt_n_m_pred in H. Zle_elim H. +assumption. apply pred_inj in H; rewrite H in H1; false_hyp H1 not_le_n_predn. Qed. -Theorem lt_Pn_m : forall n m, n < m -> P n < m. +Theorem lt_predn_m : forall n m, n < m -> P n < m. Proof. -intros; rewrite lt_P; now Zle_intro1. +intros; rewrite lt_pred; now Zle_intro1. Qed. -Theorem le_Pn_m : forall n m, n <= m -> P n <= m. +Theorem le_predn_m : forall n m, n <= m -> P n <= m. Proof. -intros n m H; rewrite <- lt_P in H; now Zle_intro1. +intros n m H; rewrite <- lt_pred in H; now Zle_intro1. Qed. -Theorem lt_n_m_S : forall n m, n < m <-> S n <= m. +Theorem lt_n_m_succ : forall n m, n < m <-> S n <= m. Proof. -intros n m; rewrite_P_S n; rewrite S_P; apply lt_P. +intros n m; rewrite_pred_succ n; rewrite succ_pred; apply lt_pred. Qed. -Theorem lt_Sn_m : forall n m, S n < m -> n < m. +Theorem lt_succn_m : forall n m, S n < m -> n < m. Proof. -intros n m H; rewrite_P_S n; now apply lt_Pn_m. +intros n m H; rewrite_pred_succ n; now apply lt_predn_m. Qed. -Theorem le_Sn_m : forall n m, S n <= m -> n <= m. +Theorem le_succn_m : forall n m, S n <= m -> n <= m. Proof. -intros n m H; rewrite <- lt_n_m_S in H; now Zle_intro1. +intros n m H; rewrite <- lt_n_m_succ in H; now Zle_intro1. Qed. -Theorem lt_n_Pm : forall n m, n < P m -> n < m. +Theorem lt_n_predm : forall n m, n < P m -> n < m. Proof. -intros n m H; rewrite_S_P m; now apply lt_n_Sm. +intros n m H; rewrite_succ_pred m; now apply lt_n_succm. Qed. -Theorem le_n_Pm : forall n m, n <= P m -> n <= m. +Theorem le_n_predm : forall n m, n <= P m -> n <= m. Proof. -intros n m H; rewrite <- lt_n_m_P in H; now Zle_intro1. +intros n m H; rewrite <- lt_n_m_pred in H; now Zle_intro1. Qed. -Theorem lt_respects_S : forall n m, n < m <-> S n < S m. +Theorem lt_respects_succ : forall n m, n < m <-> S n < S m. Proof. -intros n m. rewrite lt_n_m_S. symmetry. apply lt_S. +intros n m. rewrite lt_n_m_succ. symmetry. apply lt_succ. Qed. -Theorem le_respects_S : forall n m, n <= m <-> S n <= S m. +Theorem le_respects_succ : forall n m, n <= m <-> S n <= S m. Proof. intros n m. do 2 rewrite le_lt. -firstorder using lt_respects_S S_wd S_inj. +firstorder using lt_respects_succ succ_wd succ_inj. Qed. -Theorem lt_respects_P : forall n m, n < m <-> P n < P m. +Theorem lt_respects_pred : forall n m, n < m <-> P n < P m. Proof. -intros n m. rewrite lt_n_m_P. symmetry; apply lt_P. +intros n m. rewrite lt_n_m_pred. symmetry; apply lt_pred. Qed. -Theorem le_respects_P : forall n m, n <= m <-> P n <= P m. +Theorem le_respects_pred : forall n m, n <= m <-> P n <= P m. Proof. intros n m. do 2 rewrite le_lt. -firstorder using lt_respects_P P_wd P_inj. +firstorder using lt_respects_pred pred_wd pred_inj. Qed. -Theorem lt_S_P : forall n m, S n < m <-> n < P m. +Theorem lt_succ_pred : forall n m, S n < m <-> n < P m. Proof. -intros n m; rewrite_P_S n at 2; apply lt_respects_P. +intros n m; rewrite_pred_succ n at 2; apply lt_respects_pred. Qed. -Theorem le_S_P : forall n m, S n <= m <-> n <= P m. +Theorem le_succ_pred : forall n m, S n <= m <-> n <= P m. Proof. -intros n m; rewrite_P_S n at 2; apply le_respects_P. +intros n m; rewrite_pred_succ n at 2; apply le_respects_pred. Qed. -Theorem lt_P_S : forall n m, P n < m <-> n < S m. +Theorem lt_pred_succ : forall n m, P n < m <-> n < S m. Proof. -intros n m; rewrite_S_P n at 2; apply lt_respects_S. +intros n m; rewrite_succ_pred n at 2; apply lt_respects_succ. Qed. -Theorem le_P_S : forall n m, P n <= m <-> n <= S m. +Theorem le_pred_succ : forall n m, P n <= m <-> n <= S m. Proof. -intros n m; rewrite_S_P n at 2; apply le_respects_S. +intros n m; rewrite_succ_pred n at 2; apply le_respects_succ. Qed. Theorem lt_neq : forall n m, n < m -> n # m. @@ -184,12 +184,12 @@ Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. 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; Zle_elim H3. -assumption. rewrite <- H3 in H2. rewrite lt_S in H2; Zle_elim H2. +intros n IH p H1 H2. apply lt_succn_m in H1. pose proof (IH p H1 H2) as H3. +rewrite lt_n_m_succ in H3; Zle_elim H3. +assumption. rewrite <- H3 in H2. rewrite lt_succ 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; Zle_elim H1. +intros n IH p H1 H2. apply lt_predn_m. rewrite lt_pred in H1; Zle_elim H1. now apply IH. now rewrite H1. Qed. @@ -224,15 +224,15 @@ elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). now symmetry. assumption. assumption. Qed. -Theorem not_lt_Sn_n : forall n, ~ S n < n. +Theorem not_lt_succn_n : forall n, ~ S n < n. Proof. -intros n H; apply (lt_asymm n (S n)). apply lt_n_Sn. assumption. +intros n H; apply (lt_asymm n (S n)). apply lt_n_succn. assumption. Qed. -Theorem not_le_Sn_n : forall n, ~ S n <= n. +Theorem not_le_succn_n : forall n, ~ S n <= n. Proof. -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. +intros n H; Zle_elim H. false_hyp H not_lt_succn_n. +pose proof (lt_n_succn n) as H1. rewrite H in H1; false_hyp H1 lt_irr. Qed. Theorem lt_gt : forall n m, n < m -> m < n -> False. @@ -245,13 +245,13 @@ Proof. intros n m; induct_n n m. right; now left. intros n IH; destruct IH as [H | [H | H]]. -rewrite lt_n_m_S in H. rewrite le_lt in H; tauto. -right; right; rewrite H; apply lt_n_Sn. -right; right; now apply lt_n_Sm. +rewrite lt_n_m_succ in H. rewrite le_lt in H; tauto. +right; right; rewrite H; apply lt_n_succn. +right; right; now apply lt_n_succm. intros n IH; destruct IH as [H | [H | H]]. -left; now apply lt_Pn_m. -left; rewrite H; apply lt_Pn_n. -rewrite lt_n_m_P in H. rewrite le_lt in H. +left; now apply lt_predn_m. +left; rewrite H; apply lt_predn_n. +rewrite lt_n_m_pred in H. rewrite le_lt in H. setoid_replace (m == P n) with (P n == m) in H using relation iff. tauto. split; intro; now symmetry. Qed. @@ -274,7 +274,7 @@ Qed. Theorem lt_discrete : forall n m, n < m -> m < S n -> False. Proof. -intros n m H1 H2; apply -> lt_S in H2; apply -> lt_ge in H1; false_hyp H2 H1. +intros n m H1 H2; apply -> lt_succ in H2; apply -> lt_ge in H1; false_hyp H2 H1. Qed. (* Decidability of order can be proved either from totality or from the fact @@ -283,46 +283,46 @@ that < and <= are boolean functions *) (** A corollary of having an order is that Z is infinite in both directions *) -Theorem neq_Sn_n : forall n, S n # n. +Theorem neq_succn_n : forall n, S n # n. Proof. -intros n H. pose proof (lt_n_Sn n) as H1. rewrite H in H1. false_hyp H1 lt_irr. +intros n H. pose proof (lt_n_succn n) as H1. rewrite H in H1. false_hyp H1 lt_irr. Qed. -Theorem neq_Pn_n : forall n, P n # n. +Theorem neq_predn_n : forall n, P n # n. Proof. -intros n H. apply S_wd in H. rewrite S_P in H. now apply neq_Sn_n with (n := n). +intros n H. apply succ_wd in H. rewrite succ_pred in H. now apply neq_succn_n with (n := n). Qed. -Definition nth_S (n : nat) (m : Z) := +Definition nth_succ (n : nat) (m : Z) := nat_rec (fun _ => Z) m (fun _ l => S l) n. -Definition nth_P (n : nat) (m : Z) := +Definition nth_pred (n : nat) (m : Z) := nat_rec (fun _ => Z) m (fun _ l => P l) n. -Lemma lt_m_Skm : - forall (n : nat) (m : Z), m < nth_S (Datatypes.S n) m. +Lemma lt_m_succkm : + forall (n : nat) (m : Z), m < nth_succ (Datatypes.S n) m. Proof. intros n m; induction n as [| n IH]; simpl in *. -apply lt_n_Sn. now apply lt_n_Sm. +apply lt_n_succn. now apply lt_n_succm. Qed. -Lemma lt_Pkm_m : - forall (n : nat) (m : Z), nth_P (Datatypes.S n) m < m. +Lemma lt_predkm_m : + forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m < m. Proof. intros n m; induction n as [| n IH]; simpl in *. -apply lt_Pn_n. now apply lt_Pn_m. +apply lt_predn_n. now apply lt_predn_m. Qed. -Theorem neq_m_Skm : - forall (n : nat) (m : Z), nth_S (Datatypes.S n) m # m. +Theorem neq_m_succkm : + forall (n : nat) (m : Z), nth_succ (Datatypes.S n) m # m. Proof. -intros n m H. pose proof (lt_m_Skm n m) as H1. rewrite H in H1. +intros n m H. pose proof (lt_m_succkm n m) as H1. rewrite H in H1. false_hyp H1 lt_irr. Qed. -Theorem neq_Pkm_m : - forall (n : nat) (m : Z), nth_P (Datatypes.S n) m # m. +Theorem neq_predkm_m : + forall (n : nat) (m : Z), nth_pred (Datatypes.S n) m # m. Proof. -intros n m H. pose proof (lt_Pkm_m n m) as H1. rewrite H in H1. +intros n m H. pose proof (lt_predkm_m n m) as H1. rewrite H in H1. false_hyp H1 lt_irr. Qed. @@ -331,19 +331,19 @@ in the induction step *) Section Induction. -Variable Q : Z -> Prop. -Hypothesis Q_wd : pred_wd E Q. +Variable A : Z -> Prop. +Hypothesis Q_wd : predicate_wd E A. -Add Morphism Q with signature E ==> iff as Q_morph. +Add Morphism A with signature E ==> iff as Q_morph. Proof Q_wd. Section Center. -Variable z : Z. (* Q z is the basis of induction *) +Variable z : Z. (* A z is the basis of induction *) Section RightInduction. -Let Q' := fun n : Z => forall m, z <= m -> m < n -> Q m. +Let Q' := fun n : Z => forall m, z <= m -> m < n -> A m. Add Morphism Q' with signature E ==> iff as Q'_pos_wd. Proof. @@ -351,26 +351,26 @@ intros x1 x2 H; unfold Q'; qmorphism x1 x2. Qed. Theorem right_induction : - Q z -> (forall n, z <= n -> Q n -> Q (S n)) -> forall n, z <= n -> Q n. + A z -> (forall n, z <= n -> A n -> A (S n)) -> forall n, z <= n -> A n. Proof. 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; 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. +rewrite lt_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 lt_predn_n. 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 lt_n_Sn. +apply k_ge_z. apply lt_n_succn. Qed. End RightInduction. Section LeftInduction. -Let Q' := fun n : Z => forall m, m <= z -> n < m -> Q m. +Let Q' := fun n : Z => forall m, m <= z -> n < m -> A m. Add Morphism Q' with signature E ==> iff as Q'_neg_wd. Proof. @@ -378,28 +378,28 @@ intros x1 x2 H; unfold Q'; qmorphism x1 x2. Qed. Theorem left_induction : - Q z -> (forall n, n <= z -> Q n -> Q (P n)) -> forall n, n <= z -> Q n. + A z -> (forall n, n <= z -> A n -> A (P n)) -> forall n, n <= z -> A n. Proof. intros Qz QP k k_le_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. apply IH. assumption. now apply lt_Sn_m. +intros n IH m H2 H3. apply IH. assumption. now apply lt_succn_m. intros n IH m H2 H3. -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. +rewrite lt_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 lt_n_succn. now rewrite H2. pose proof (H (P k)) as H1; unfold Q' in H1. apply H1. -apply k_le_z. apply lt_Pn_n. +apply k_le_z. apply lt_predn_n. Qed. End LeftInduction. Theorem induction_ord_n : - Q z -> - (forall n, z <= n -> Q n -> Q (S n)) -> - (forall n, n <= z -> Q n -> Q (P n)) -> - forall n, Q n. + A z -> + (forall n, z <= n -> A n -> A (S n)) -> + (forall n, n <= z -> A n -> A (P n)) -> + forall n, A n. Proof. intros Qz QS QP n. destruct (lt_total n z) as [H | [H | H]]. @@ -411,27 +411,27 @@ Qed. End Center. Theorem induction_ord : - Q 0 -> - (forall n, 0 <= n -> Q n -> Q (S n)) -> - (forall n, n <= 0 -> Q n -> Q (P n)) -> - forall n, Q n. + A 0 -> + (forall n, 0 <= n -> A n -> A (S n)) -> + (forall n, n <= 0 -> A n -> A (P n)) -> + forall n, A n. Proof (induction_ord_n 0). Theorem lt_ind : forall (n : Z), - Q (S n) -> - (forall m : Z, n < m -> Q m -> Q (S m)) -> - forall m : Z, n < m -> Q m. + 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_S. -now apply -> lt_n_m_S. +intros; apply H2; try assumption. now apply <- lt_n_m_succ. +now apply -> lt_n_m_succ. Qed. Theorem le_ind : forall (n : Z), - Q n -> - (forall m : Z, n <= m -> Q m -> Q (S m)) -> - forall m : Z, n <= m -> Q m. + 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. @@ -442,10 +442,17 @@ End Induction. Ltac induct_ord n := try intros until n; pattern n; apply induction_ord; clear n; - [unfold NumPrelude.pred_wd; + [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: +*) diff --git a/theories/Numbers/Integer/Axioms/ZPlus.v b/theories/Numbers/Integer/Axioms/ZPlus.v index 6c1f49231..624f85f04 100644 --- a/theories/Numbers/Integer/Axioms/ZPlus.v +++ b/theories/Numbers/Integer/Axioms/ZPlus.v @@ -1,7 +1,7 @@ Require Export ZAxioms. Module Type ZPlusSignature. -Declare Module Export IntModule : IntSignature. +Declare Module Export ZBaseMod : ZBaseSig. Open Local Scope IntScope. Parameter Inline plus : Z -> Z -> Z. @@ -17,62 +17,62 @@ Add Morphism minus with signature E ==> E ==> E as minus_wd. Add Morphism uminus with signature E ==> E as uminus_wd. Axiom plus_0 : forall n, 0 + n == n. -Axiom plus_S : forall n m, (S n) + m == S (n + m). +Axiom plus_succ : forall n m, (S n) + m == S (n + m). Axiom minus_0 : forall n, n - 0 == n. -Axiom minus_S : forall n m, n - (S m) == P (n - m). +Axiom minus_succ : forall n m, n - (S m) == P (n - m). Axiom uminus_0 : - 0 == 0. -Axiom uminus_S : forall n, - (S n) == P (- n). +Axiom uminus_succ : forall n, - (S n) == P (- n). End ZPlusSignature. Module ZPlusProperties (Import ZPlusModule : ZPlusSignature). -Module Export IntPropertiesModule := IntProperties IntModule. +Module Export ZBasePropFunctModule := ZBasePropFunct ZBaseMod. Open Local Scope IntScope. -Theorem plus_P : forall n m, P n + m == P (n + m). +Theorem plus_pred : forall n m, P n + m == P (n + m). Proof. -intros n m. rewrite_S_P n at 2. rewrite plus_S. now rewrite P_S. +intros n m. rewrite_succ_pred n at 2. rewrite plus_succ. now rewrite pred_succ. Qed. -Theorem minus_P : forall n m, n - (P m) == S (n - m). +Theorem minus_pred : forall n m, n - (P m) == S (n - m). Proof. -intros n m. rewrite_S_P m at 2. rewrite minus_S. now rewrite S_P. +intros n m. rewrite_succ_pred m at 2. rewrite minus_succ. now rewrite succ_pred. Qed. -Theorem uminus_P : forall n, - (P n) == S (- n). +Theorem uminus_pred : forall n, - (P n) == S (- n). Proof. -intro n. rewrite_S_P n at 2. rewrite uminus_S. now rewrite S_P. +intro n. rewrite_succ_pred n at 2. rewrite uminus_succ. now rewrite succ_pred. Qed. Theorem plus_n_0 : forall n, n + 0 == n. Proof. induct n. now rewrite plus_0. -intros n IH. rewrite plus_S. now rewrite IH. -intros n IH. rewrite plus_P. now rewrite IH. +intros n IH. rewrite plus_succ. now rewrite IH. +intros n IH. rewrite plus_pred. now rewrite IH. Qed. -Theorem plus_n_Sm : forall n m, n + S m == S (n + m). +Theorem plus_n_succm : forall n m, n + S m == S (n + m). Proof. intros n m; induct n. now do 2 rewrite plus_0. -intros n IH. do 2 rewrite plus_S. now rewrite IH. -intros n IH. do 2 rewrite plus_P. rewrite IH. rewrite P_S; now rewrite S_P. +intros n IH. do 2 rewrite plus_succ. now rewrite IH. +intros n IH. do 2 rewrite plus_pred. rewrite IH. rewrite pred_succ; now rewrite succ_pred. Qed. -Theorem plus_n_Pm : forall n m, n + P m == P (n + m). +Theorem plus_n_predm : forall n m, n + P m == P (n + m). Proof. -intros n m; rewrite_S_P m at 2. rewrite plus_n_Sm; now rewrite P_S. +intros n m; rewrite_succ_pred m at 2. rewrite plus_n_succm; now rewrite pred_succ. Qed. Theorem plus_opp_minus : forall n m, n + (- m) == n - m. Proof. induct m. rewrite uminus_0; rewrite minus_0; now rewrite plus_n_0. -intros m IH. rewrite uminus_S; rewrite minus_S. rewrite plus_n_Pm; now rewrite IH. -intros m IH. rewrite uminus_P; rewrite minus_P. rewrite plus_n_Sm; now rewrite IH. +intros m IH. rewrite uminus_succ; rewrite minus_succ. rewrite plus_n_predm; now rewrite IH. +intros m IH. rewrite uminus_pred; rewrite minus_pred. rewrite plus_n_succm; now rewrite IH. Qed. Theorem minus_0_n : forall n, 0 - n == - n. @@ -80,38 +80,38 @@ Proof. intro n; rewrite <- plus_opp_minus; now rewrite plus_0. Qed. -Theorem minus_Sn_m : forall n m, S n - m == S (n - m). +Theorem minus_succn_m : forall n m, S n - m == S (n - m). Proof. -intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_S. +intros n m; do 2 rewrite <- plus_opp_minus; now rewrite plus_succ. Qed. -Theorem minus_Pn_m : forall n m, P n - m == P (n - m). +Theorem minus_predn_m : forall n m, P n - m == P (n - m). Proof. -intros n m. rewrite_S_P n at 2; rewrite minus_Sn_m; now rewrite P_S. +intros n m. rewrite_succ_pred n at 2; rewrite minus_succn_m; now rewrite pred_succ. Qed. Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p. Proof. intros n m p; induct n. now do 2 rewrite plus_0. -intros n IH. do 3 rewrite plus_S. now rewrite IH. -intros n IH. do 3 rewrite plus_P. now rewrite IH. +intros n IH. do 3 rewrite plus_succ. now rewrite IH. +intros n IH. do 3 rewrite plus_pred. now rewrite IH. Qed. Theorem plus_comm : forall n m, n + m == m + n. Proof. intros n m; induct n. rewrite plus_0; now rewrite plus_n_0. -intros n IH; rewrite plus_S; rewrite plus_n_Sm; now rewrite IH. -intros n IH; rewrite plus_P; rewrite plus_n_Pm; now rewrite IH. +intros n IH; rewrite plus_succ; rewrite plus_n_succm; now rewrite IH. +intros n IH; rewrite plus_pred; rewrite plus_n_predm; now rewrite IH. Qed. Theorem minus_diag : forall n, n - n == 0. Proof. induct n. now rewrite minus_0. -intros n IH. rewrite minus_S; rewrite minus_Sn_m; rewrite P_S; now rewrite IH. -intros n IH. rewrite minus_P; rewrite minus_Pn_m; rewrite S_P; now rewrite IH. +intros n IH. rewrite minus_succ; rewrite minus_succn_m; rewrite pred_succ; now rewrite IH. +intros n IH. rewrite minus_pred; rewrite minus_predn_m; rewrite succ_pred; now rewrite IH. Qed. Theorem plus_opp_r : forall n, n + (- n) == 0. @@ -144,16 +144,16 @@ Theorem double_opp : forall n, - (- n) == n. Proof. induct n. now do 2 rewrite uminus_0. -intros n IH. rewrite uminus_S; rewrite uminus_P; now rewrite IH. -intros n IH. rewrite uminus_P; rewrite uminus_S; now rewrite IH. +intros n IH. rewrite uminus_succ; rewrite uminus_pred; now rewrite IH. +intros n IH. rewrite uminus_pred; rewrite uminus_succ; now rewrite IH. Qed. Theorem opp_plus_distr : forall n m, - (n + m) == - n + (- m). Proof. intros n m; induct n. rewrite uminus_0; now do 2 rewrite plus_0. -intros n IH. rewrite plus_S; do 2 rewrite uminus_S. rewrite IH. now rewrite plus_P. -intros n IH. rewrite plus_P; do 2 rewrite uminus_P. rewrite IH. now rewrite plus_S. +intros n IH. rewrite plus_succ; do 2 rewrite uminus_succ. rewrite IH. now rewrite plus_pred. +intros n IH. rewrite plus_pred; do 2 rewrite uminus_pred. rewrite IH. now rewrite plus_succ. Qed. Theorem opp_minus_distr : forall n m, - (n - m) == - n + m. @@ -219,3 +219,10 @@ intros n m H. rewrite <- (plus_minus_inverse m n). rewrite H. apply plus_n_0. Qed. End ZPlusProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZPlusOrder.v b/theories/Numbers/Integer/Axioms/ZPlusOrder.v index 946bdf3cb..95f0fa8c6 100644 --- a/theories/Numbers/Integer/Axioms/ZPlusOrder.v +++ b/theories/Numbers/Integer/Axioms/ZPlusOrder.v @@ -3,7 +3,7 @@ Require Export ZPlus. Module ZPlusOrderProperties (Import ZPlusModule : ZPlusSignature) (Import ZOrderModule : ZOrderSignature with - Module IntModule := ZPlusModule.IntModule). + Module ZBaseMod := ZPlusModule.ZBaseMod). Module Export ZPlusPropertiesModule := ZPlusProperties ZPlusModule. Module Export ZOrderPropertiesModule := ZOrderProperties ZOrderModule. (* <W> Grammar extension: in [tactic:simple_tactic], some rule has been masked !!! *) @@ -13,8 +13,8 @@ Theorem plus_lt_compat_l : forall n m p, n < m <-> p + n < p + m. Proof. intros n m p; induct p. now do 2 rewrite plus_0. -intros p IH. do 2 rewrite plus_S. now rewrite <- lt_respects_S. -intros p IH. do 2 rewrite plus_P. now rewrite <- lt_respects_P. +intros p IH. do 2 rewrite plus_succ. now rewrite <- lt_respects_succ. +intros p IH. do 2 rewrite plus_pred. now rewrite <- lt_respects_pred. Qed. Theorem plus_lt_compat_r : forall n m p, n < m <-> n + p < m + p. @@ -25,7 +25,7 @@ Qed. Theorem plus_le_compat_l : forall n m p, n <= m <-> p + n <= p + m. Proof. -intros n m p; do 2 rewrite <- lt_S. rewrite <- plus_n_Sm; +intros n m p; do 2 rewrite <- lt_succ. rewrite <- plus_n_succm; apply plus_lt_compat_l. Qed. @@ -69,14 +69,14 @@ Proof. induct n. induct_ord m. intro H; false_hyp H lt_irr. -intros m H1 IH H2. rewrite uminus_S. rewrite uminus_0 in *. -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. -apply -> lt_S_P in H. apply IH in H. rewrite uminus_P in H. now apply -> lt_S_P. -intros n IH m H. rewrite uminus_P. -apply -> lt_P_S in H. apply IH in H. rewrite uminus_S in H. now apply -> lt_P_S. +intros m H1 IH H2. rewrite uminus_succ. rewrite uminus_0 in *. +Zle_elim H1. apply IH in H1. now apply lt_predn_m. +rewrite <- H1; rewrite uminus_0; apply lt_predn_n. +intros m H1 IH H2. apply lt_n_predm in H2. apply -> le_gt in H1. false_hyp H2 H1. +intros n IH m H. rewrite uminus_succ. +apply -> lt_succ_pred in H. apply IH in H. rewrite uminus_pred in H. now apply -> lt_succ_pred. +intros n IH m H. rewrite uminus_pred. +apply -> lt_pred_succ in H. apply IH in H. rewrite uminus_succ in H. now apply -> lt_pred_succ. Qed. Theorem lt_opp : forall n m, n < m <-> - m < - n. @@ -158,3 +158,10 @@ rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. Qed. End ZPlusOrderProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZPred.v b/theories/Numbers/Integer/Axioms/ZPred.v new file mode 100644 index 000000000..ffcb2dea8 --- /dev/null +++ b/theories/Numbers/Integer/Axioms/ZPred.v @@ -0,0 +1,60 @@ +Axiom succ_pred : forall x : Z, S (P x) == x. +Add Morphism P with signature E ==> E as pred_wd. + +Theorem pred_inj : forall x y, P x == P y -> x == y. +Proof. +intros x y H. +setoid_replace x with (S (P x)); [| symmetry; apply succ_pred]. +setoid_replace y with (S (P y)); [| symmetry; apply succ_pred]. +now rewrite H. +Qed. + +Theorem pred_succ : forall x, P (S x) == x. +Proof. +intro x. +apply succ_inj. +now rewrite succ_pred. +Qed. + +(* The following tactics are intended for replacing a certain +occurrence of a term t in the goal by (S (P t)) or by (P (S t)). +Unfortunately, this cannot be done by setoid_replace tactic for two +reasons. First, it seems impossible to do rewriting when one side of +the equation in question (succ_pred or pred_succ) is a variable, due to bug 1604. +This does not work even when the predicate is an identifier (e.g., +when one tries to rewrite (A x) into (A (S (P x)))). Second, the +setoid_rewrite tactic, like the ordinary rewrite tactic, does not +allow specifying the exact occurrence of the term to be rewritten. Now +while not in the setoid context, this occurrence can be specified +using the pattern tactic, it does not work with setoids, since pattern +creates a lambda abstractuion, and setoid_rewrite does not work with +them. *) + +Ltac rewrite_succP t set_tac repl thm := +let x := fresh "x" in +set_tac x t; +setoid_replace x with (repl x); [| symmetry; apply thm]; +unfold x; clear x. + +Tactic Notation "rewrite_succ_pred" constr(t) := +rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (S (P x))) succ_pred. + +Tactic Notation "rewrite_succ_pred" constr(t) "at" integer(k) := +rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (S (P x))) succ_pred. + +Tactic Notation "rewrite_pred_succ" constr(t) := +rewrite_succP t ltac:(fun x t => (set (x := t))) (fun x => (P (S x))) pred_succ. + +Tactic Notation "rewrite_pred_succ" constr(t) "at" integer(k) := +rewrite_succP t ltac:(fun x t => (set (x := t) in |-* at k)) (fun x => (P (S x))) pred_succ. + +(* One can add tactic notations for replacements in assumptions rather +than in the goal. For the reason of many possible variants, the core +of the tactic is factored out. *) + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZTimes.v b/theories/Numbers/Integer/Axioms/ZTimes.v index 5dc0b7505..38311aa2b 100644 --- a/theories/Numbers/Integer/Axioms/ZTimes.v +++ b/theories/Numbers/Integer/Axioms/ZTimes.v @@ -11,7 +11,7 @@ Notation "x * y" := (times x y) : IntScope. Add Morphism times with signature E ==> E ==> E as times_wd. Axiom times_0 : forall n, n * 0 == 0. -Axiom times_S : forall n m, n * (S m) == n * m + n. +Axiom times_succ : forall n m, n * (S m) == n * m + n. End ZTimesSignature. @@ -19,9 +19,9 @@ 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. +Theorem times_pred : forall n m, n * (P m) == n * m - n. Proof. -intros n m. rewrite_S_P m at 2. rewrite times_S. rewrite <- plus_minus_distr. +intros n m. rewrite_succ_pred m at 2. rewrite times_succ. rewrite <- plus_minus_distr. rewrite minus_diag. now rewrite plus_n_0. Qed. @@ -29,26 +29,26 @@ Theorem times_0_n : forall n, 0 * n == 0. Proof. induct n. now rewrite times_0. -intros n IH. rewrite times_S. rewrite IH; now rewrite plus_0. -intros n IH. rewrite times_P. rewrite IH; now rewrite minus_0. +intros n IH. rewrite times_succ. rewrite IH; now rewrite plus_0. +intros n IH. rewrite times_pred. rewrite IH; now rewrite minus_0. Qed. -Theorem times_Sn_m : forall n m, (S n) * m == n * m + m. +Theorem times_succn_m : forall n m, (S n) * m == n * m + m. Proof. induct m. do 2 rewrite times_0. now rewrite plus_0. -intros m IH. do 2 rewrite times_S. rewrite IH. +intros m IH. do 2 rewrite times_succ. rewrite IH. do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. -do 2 rewrite plus_n_Sm; now rewrite plus_comm. -intros m IH. do 2 rewrite times_P. rewrite IH. +do 2 rewrite plus_n_succm; now rewrite plus_comm. +intros m IH. do 2 rewrite times_pred. rewrite IH. rewrite <- plus_minus_swap. do 2 rewrite <- plus_minus_distr. apply plus_wd. reflexivity. -rewrite minus_S. now rewrite minus_Pn_m. +rewrite minus_succ. now rewrite minus_predn_m. Qed. -Theorem times_Pn_m : forall n m, (P n) * m == n * m - m. +Theorem times_predn_m : forall n m, (P n) * m == n * m - m. Proof. -intros n m. rewrite_S_P n at 2. rewrite times_Sn_m. +intros n m. rewrite_succ_pred n at 2. rewrite times_succn_m. rewrite <- plus_minus_distr. rewrite minus_diag; now rewrite plus_n_0. Qed. @@ -56,17 +56,17 @@ Theorem times_comm : forall n m, n * m == m * n. Proof. intros n m; induct n. rewrite times_0_n; now rewrite times_0. -intros n IH. rewrite times_Sn_m; rewrite times_S; now rewrite IH. -intros n IH. rewrite times_Pn_m; rewrite times_P; now rewrite IH. +intros n IH. rewrite times_succn_m; rewrite times_succ; now rewrite IH. +intros n IH. rewrite times_predn_m; rewrite times_pred; now rewrite IH. Qed. Theorem times_opp_r : forall n m, n * (- m) == - (n * m). Proof. intros n m; induct m. rewrite uminus_0; rewrite times_0; now rewrite uminus_0. -intros m IH. rewrite uminus_S. rewrite times_P; rewrite times_S. rewrite IH. +intros m IH. rewrite uminus_succ. rewrite times_pred; rewrite times_succ. rewrite IH. rewrite <- plus_opp_minus; now rewrite opp_plus_distr. -intros m IH. rewrite uminus_P. rewrite times_P; rewrite times_S. rewrite IH. +intros m IH. rewrite uminus_pred. rewrite times_pred; rewrite times_succ. rewrite IH. now rewrite opp_minus_distr. Qed. @@ -85,9 +85,9 @@ Theorem times_plus_distr_r : forall n m p, n * (m + p) == n * m + n * p. Proof. intros n m p; induct m. rewrite times_0; now do 2 rewrite plus_0. -intros m IH. rewrite plus_S. do 2 rewrite times_S. rewrite IH. +intros m IH. rewrite plus_succ. do 2 rewrite times_succ. rewrite IH. do 2 rewrite <- plus_assoc; apply plus_wd; [reflexivity | apply plus_comm]. -intros m IH. rewrite plus_P. do 2 rewrite times_P. rewrite IH. +intros m IH. rewrite plus_pred. do 2 rewrite times_pred. rewrite IH. apply plus_minus_swap. Qed. @@ -113,8 +113,15 @@ Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p. Proof. intros n m p; induct p. now do 3 rewrite times_0. -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. +intros p IH. do 2 rewrite times_succ. rewrite times_plus_distr_r. now rewrite IH. +intros p IH. do 2 rewrite times_pred. rewrite times_minus_distr_r. now rewrite IH. Qed. End ZTimesProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/Axioms/ZTimesOrder.v b/theories/Numbers/Integer/Axioms/ZTimesOrder.v index 28c07a99d..055342bcc 100644 --- a/theories/Numbers/Integer/Axioms/ZTimesOrder.v +++ b/theories/Numbers/Integer/Axioms/ZTimesOrder.v @@ -3,7 +3,7 @@ Require Export ZPlusOrder. Module ZTimesOrderProperties (Import ZTimesModule : ZTimesSignature) (Import ZOrderModule : ZOrderSignature with - Module IntModule := ZTimesModule.ZPlusModule.IntModule). + Module ZBaseMod := ZTimesModule.ZPlusModule.ZBaseMod). Module Export ZTimesPropertiesModule := ZTimesProperties ZTimesModule. Module Export ZPlusOrderPropertiesModule := ZPlusOrderProperties ZTimesModule.ZPlusModule ZOrderModule. @@ -13,11 +13,11 @@ 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; Zle_elim H1. +intros p H IH H1 H2. do 2 rewrite times_succ. +apply -> lt_succ 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. +intros p H IH H1 H2. apply lt_n_predm in H1. apply -> le_gt in H. false_hyp H1 H. Qed. @@ -87,3 +87,10 @@ apply neq_symm. apply lt_neq. now apply mult_pos_pos. Qed. End ZTimesOrderProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v index 683b86ec6..73b0bee7e 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsAxioms.v @@ -1,17 +1,17 @@ Require Import NPlus. Require Export ZAxioms. -Module NatPairsDomain (Import NPlusModule : NPlusSignature) <: ZDomainSignature. +Module NatPairsDomain (Import NPlusMod : NPlusSig) <: ZDomainSignature. (* with Definition Z := - (NPM.NatModule.DomainModule.N * NPM.NatModule.DomainModule.N)%type + (NPM.NBaseMod.DomainModule.N * NPM.NBaseMod.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)) + NPM.NBaseMod.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)).*) + NPM.NBaseMod.DomainModule.e (NPM.plus (fst p1) (snd p2)) (NPM.plus (fst p2) (snd p1)).*) -Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule. +Module Export NPlusPropMod := NPlusPropFunct NBaseMod NPlusMod. Open Local Scope NatScope. Definition Z : Set := (N * N)%type. @@ -68,14 +68,14 @@ Qed. End NatPairsDomain. -Module NatPairsInt (Import NPlusModule : NPlusSignature) <: IntSignature. -Module Export ZDomainModule := NatPairsDomain NPlusModule. +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) := (NatModule.S (fst n), snd n). -Definition P (n : Z) := (fst n, NatModule.S (snd n)). +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 @@ -84,47 +84,47 @@ 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. +Add Morphism S with signature E ==> E as succ_wd. Proof. unfold S, E; intros n m H; simpl. -do 2 rewrite plus_S_l; now rewrite H. +do 2 rewrite plus_succ_l; now rewrite H. Qed. -Add Morphism P with signature E ==> E as P_wd. +Add Morphism P with signature E ==> E as pred_wd. Proof. unfold P, E; intros n m H; simpl. -do 2 rewrite plus_S_r; now rewrite H. +do 2 rewrite plus_succ_r; now rewrite H. Qed. -Theorem S_inj : forall x y : Z, S x == S y -> x == y. +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_S_l in H. now apply S_inj in H. +do 2 rewrite plus_succ_l in H. now apply succ_inj in H. Qed. -Theorem S_P : forall x : Z, S (P x) == x. +Theorem succ_pred : forall x : Z, S (P x) == x. Proof. intro x; unfold S, P, E; simpl. -rewrite plus_S_l; now rewrite plus_S_r. +rewrite plus_succ_l; now rewrite plus_succ_r. Qed. Section Induction. Open Scope NatScope. (* automatically closes at the end of the section *) -Variable Q : Z -> Prop. -Hypothesis Q_wd : pred_wd E Q. +Variable A : Z -> Prop. +Hypothesis Q_wd : predicate_wd E A. -Add Morphism Q with signature E ==> iff as Q_morph. +Add Morphism A with signature E ==> iff as Q_morph. Proof. exact Q_wd. Qed. Theorem induction : - Q 0 -> (forall x, Q x -> Q (S x)) -> (forall x, Q x -> Q (P x)) -> forall x, Q x. + 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, pred_wd, E in *. +intros Q0 QS QP x; unfold O, S, P, predicate_wd, E in *. destruct x as [n m]. -cut (forall p : N, Q (p, 0)); [intro H1 |]. -cut (forall p : N, Q (0, p)); [intro H2 |]. +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. @@ -139,3 +139,10 @@ Qed. End Induction. End NatPairsInt. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v index 29181e0c6..8943afde9 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsOrder.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsOrder.v @@ -2,12 +2,12 @@ Require Import NPlusOrder. Require Export ZPlusOrder. Require Export ZPairsPlus. -Module NatPairsOrder (Import NPlusModule : NPlusSignature) - (Import NOrderModule : NOrderSignature - with Module NatModule := NPlusModule.NatModule) <: ZOrderSignature. +Module NatPairsOrder (Import NPlusMod : NPlusSig) + (Import NOrderModule : NOrderSig + with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature. Module Import NPlusOrderPropertiesModule := - NPlusOrderProperties NPlusModule NOrderModule. -Module Export IntModule := NatPairsInt NPlusModule. + NPlusOrderProperties NPlusMod NOrderModule. +Module Export ZBaseMod := NatPairsInt NPlusMod. Open Local Scope NatScope. Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1). @@ -58,17 +58,17 @@ unfold le, E; intros x1 y1 H1 x2 y2 H2; simpl. rewrite eq_true_iff. do 2 rewrite le_lt. pose proof (lt_wd x1 y1 H1 x2 y2 H2) as H; unfold lt in H; rewrite H; clear H. (* This is a remark about an extra level of definitions created by -"with Module NatModule := NPlusModule.NatModule" constraint in the beginning +"with Module NBaseMod := NPlusMod.NBaseMod" constraint in the beginning of this functor. We cannot just say "fold (x1 == x2)%Int" because it turns out -that it expand to (NPlusModule.NatModule.NDomainModule.E ... ...), since -NPlusModule was imported first. On the other hand, the goal uses -NOrderModule.NatModule.NDomainModule.E, or just NDomainModule.E, since le_lt +that it expand to (NPlusMod.NBaseMod.NDomainModule.E ... ...), since +NPlusMod was imported first. On the other hand, the goal uses +NOrderModule.NBaseMod.NDomainModule.E, or just NDomainModule.E, since le_lt theorem was proved in NOrderDomain module. (E without qualifiers refers to ZDomainModule.E.) Therefore, we issue the "replace" command. It would be nicer, -though, if the constraint "with Module NatModule := NPlusModule.NatModule" in the +though, if the constraint "with Module NBaseMod := NPlusMod.NBaseMod" in the declaration of this functor would not create an extra level of definitions and there would be only one NDomainModule.E. *) -replace NDomainModule.E with NPlusModule.NatModule.NDomainModule.E by reflexivity. +replace NDomainModule.E with NPlusMod.NBaseMod.NDomainModule.E by reflexivity. fold (x1 == x2)%Int. fold (y1 == y2)%Int. assert (H1' : (x1 == y1)%Int); [exact H1 |]. (* We do this instead of "fold (x1 == y1)%Int in H1" *) @@ -86,26 +86,33 @@ Qed. Theorem lt_irr : forall n : Z, ~ (n < n). Proof. intros n; unfold lt, E; simpl. apply lt_irr. -(* refers to NPlusOrderPropertiesModule.NOrderPropertiesModule.lt_irr *) +(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *) Qed. -Theorem lt_S : forall n m, n < (S m) <-> n <= m. +Theorem lt_succ : forall n m, n < (S m) <-> n <= m. Proof. -intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S. +intros n m; unfold lt, le, E; simpl. rewrite plus_succ_l; apply lt_succ. Qed. End NatPairsOrder. (* Since to define the order on integers we need both plus and order on natural numbers, we can export the properties of plus and order together *) -(*Module NatPairsPlusOrderProperties (NPlusModule : NPlusSignature) - (NOrderModule : NOrderSignature - with Module NatModule := NPlusModule.NatModule). -Module Export NatPairsPlusModule := NatPairsPlus NPlusModule. -Module Export NatPairsOrderModule := NatPairsOrder NPlusModule NOrderModule. +(*Module NatPairsPlusOrderProperties (NPlusMod : NPlusSig) + (NOrderModule : NOrderSig + with Module NBaseMod := NPlusMod.NBaseMod). +Module Export NatPairsPlusModule := NatPairsPlus NPlusMod. +Module Export NatPairsOrderModule := NatPairsOrder NPlusMod NOrderModule. Module Export NatPairsPlusOrderPropertiesModule := ZPlusOrderProperties NatPairsPlusModule NatPairsOrderModule. End NatPairsPlusOrderProperties.*) -(* We cannot prove to Coq that NatPairsPlusModule.IntModule and -NatPairsOrderModule.IntModule are the same *) +(* We cannot prove to Coq that NatPairsPlusModule.ZBaseMod and +NatPairsOrderModule.ZBaseMod are the same *) + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v index d18076265..d1ae7679b 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsPlus.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsPlus.v @@ -2,8 +2,8 @@ Require Import NPlus. Require Export ZPlus. Require Export ZPairsAxioms. -Module NatPairsPlus (Import NPlusModule : NPlusSignature) <: ZPlusSignature. -Module Export IntModule := NatPairsInt NPlusModule. +Module NatPairsPlus (Import NPlusMod : NPlusSig) <: ZPlusSignature. +Module Export ZBaseMod := NatPairsInt NPlusMod. Open Local Scope NatScope. Definition plus (x y : Z) := ((fst x) + (fst y), (snd x) + (snd y)). @@ -31,7 +31,7 @@ Add Morphism minus with signature E ==> E ==> E as minus_wd. Proof. unfold E, plus; intros x1 y1 H1 x2 y2 H2; simpl. rewrite plus_comm in H2. symmetry in H2; rewrite plus_comm in H2. -pose proof (NPlusModule.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 +pose proof (NPlusMod.plus_wd (fst x1 + snd y1) (fst y1 + snd x1) H1 (snd x2 + fst y2) (snd y2 + fst x2) H2) as H. rewrite plus_shuffle1. symmetry. now rewrite plus_shuffle1. Qed. @@ -46,12 +46,12 @@ Open Local Scope IntScope. Theorem plus_0 : forall n, 0 + n == n. Proof. -intro n; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_0_l. +intro n; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_0_l. Qed. -Theorem plus_S : forall n m, (S n) + m == S (n + m). +Theorem plus_succ : forall n m, (S n) + m == S (n + m). Proof. -intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusModule.plus_S_l. +intros n m; unfold plus, E; simpl. now do 2 rewrite NPlusMod.plus_succ_l. Qed. Theorem minus_0 : forall n, n - 0 == n. @@ -59,9 +59,9 @@ Proof. intro n; unfold minus, E; simpl. now do 2 rewrite plus_0_r. Qed. -Theorem minus_S : forall n m, n - (S m) == P (n - m). +Theorem minus_succ : forall n m, n - (S m) == P (n - m). Proof. -intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_S_r. +intros n m; unfold minus, E; simpl. symmetry; now rewrite plus_succ_r. Qed. Theorem uminus_0 : - 0 == 0. @@ -69,14 +69,21 @@ Proof. unfold uminus, E; simpl. now rewrite plus_0_l. Qed. -Theorem uminus_S : forall n, - (S n) == P (- n). +Theorem uminus_succ : forall n, - (S n) == P (- n). Proof. reflexivity. Qed. End NatPairsPlus. -Module NatPairsPlusProperties (NPlusModule : NPlusSignature). -Module Export NatPairsPlusModule := NatPairsPlus NPlusModule. +Module NatPairsPlusProperties (NPlusMod : NPlusSig). +Module Export NatPairsPlusModule := NatPairsPlus NPlusMod. Module Export NatPairsPlusPropertiesModule := ZPlusProperties NatPairsPlusModule. End NatPairsPlusProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v index b72847c08..47bf8cd08 100644 --- a/theories/Numbers/Integer/NatPairs/ZPairsTimes.v +++ b/theories/Numbers/Integer/NatPairs/ZPairsTimes.v @@ -3,9 +3,9 @@ Require Import NTimes. Require Export ZTimes. Require Export ZPairsPlus. -Module NatPairsTimes (Import NTimesModule : NTimesSignature) <: ZTimesSignature. -Module Export ZPlusModule := NatPairsPlus NTimesModule.NPlusModule. (* "NTimesModule." is optional *) -Module Import NTimesPropertiesModule := NTimesProperties NTimesModule. +Module NatPairsTimes (Import NTimesMod : NTimesSig) <: ZTimesSignature. +Module Export ZPlusModule := NatPairsPlus NTimesMod.NPlusMod. (* "NTimesMod." is optional *) +Module Import NTimesPropertiesModule := NTimesPropFunct NTimesMod. Open Local Scope NatScope. Definition times (n m : Z) := @@ -41,15 +41,22 @@ intro n; unfold times, E; simpl. repeat rewrite times_0_r. now rewrite plus_assoc. Qed. -Theorem times_S : forall n m, n * (S m) == n * m + n. +Theorem times_succ : forall n m, n * (S m) == n * m + n. Proof. intros n m; unfold times, S, E; simpl. -do 2 rewrite times_S_r. ring. +do 2 rewrite times_succ_r. ring. Qed. End NatPairsTimes. -Module NatPairsTimesProperties (NTimesModule : NTimesSignature). -Module Export NatPairsTimesModule := NatPairsTimes NTimesModule. +Module NatPairsTimesProperties (NTimesMod : NTimesSig). +Module Export NatPairsTimesModule := NatPairsTimes NTimesMod. Module Export NatPairsTimesPropertiesModule := ZTimesProperties NatPairsTimesModule. End NatPairsTimesProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NAxioms.v b/theories/Numbers/Natural/Axioms/NAxioms.v deleted file mode 100644 index ceccf840a..000000000 --- a/theories/Numbers/Natural/Axioms/NAxioms.v +++ /dev/null @@ -1,413 +0,0 @@ -Require Export NDomain. - -(********************************************************************* -* Peano Axioms * -*********************************************************************) - -Module Type NatSignature. -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) 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 NatScope. - -Parameter Inline O : N. -Parameter (*Inline*) S : N -> N. - -Notation "0" := O : NatScope. -Notation "1" := (S O) : NatScope. - -Add Morphism S with signature E ==> E as S_wd. - -(* It is natural to formulate induction for well-defined predicates -only because standard induction -forall P, P 0 -> (forall n, P n -> P (S n)) -> forall n, P n -does not hold in the setoid context (for example, there is no reason -for (P x) hold when x == 0 but x <> 0). However, it is possible to -formulate induction without mentioning well-defidedness (see OtherInd.v); -this formulation is equivalent. *) -Axiom induction : - forall P : N -> Prop, pred_wd E P -> - P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n. - -(* Why do we separate induction and recursion? - -(1) When induction and recursion are the same, they are dependent -(nondependent induction does not make sense). However, one must impose -conditions on the predicate, or codomain, that it respects the setoid -equality. For induction this means considering predicates P for which -forall n n', n == n' -> (P n <-> P n') holds. For recursion, where P : -nat -> Set, we cannot say (P n <-> P n'). It may make sense to require -forall n n', n == n' -> (P n = P n'). - -(2) Unlike induction, recursion requires that two equalities hold: -[recursion a f 0 == a] and [recursion a f (S n) == f n (recursion a f n)] -(or something like this). It may be difficult to state, let alone prove, -these equalities because the left- and the right-hand sides may have -different types (P t1) and (P t2) where t1 == t2 is provable but t1 and t2 -are not convertible into each other. Nevertheless, these equalities may -be proved using dependent equality (EqdepFacts) or JM equality (JMeq). -However, requiring this for any implementation of natural numbers seems -a little complex. It may make sense to devote a separate module to dependent -recursion (see DepRec.v). *) - -Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A. - -Implicit Arguments recursion [A]. - -(* Suppose the codomain A has a setoid equality relation EA. If A is a -function space C -> D, it makes sense to consider extensional -functional equality as EA. Indeed, suppose, for example, that we say -[Definition g (x : N) : C -> D := (recursion ... x ...)]. We would -like to show that the function g of two arguments is well-defined. -This requirement is the same as the requirement that the functions of -one argument (g x) and (g x') are extensionally equal whenever x == -x', i.e., - -forall x x' : N, x == x' -> eq_fun (g x) (g x'), - -which is the same as - -forall x x' : N, x == x' -> forall y y' : C, EC y y' -> ED (g x y) (g x' y') - -where EC and ED are setoid equalities on C and D, respectively. - -Now, if we consider EA to be extensional equality on the function -space, we cannot require that EA is reflexive. Indeed, reflexivity of -EA: - -forall f : C -> D, eq_fun f f - -or - -forall f : C -> D, forall x x', EC x x' -> ED (f x) (f x') - -means that every function f ; C -> D is well-defined, which is in -general false. We can expect that EA is symmetric and transitive, -i.e., that EA is a partial equivalence relation (PER). However, there -seems to be no need to require this in the following axioms. - -When we defined a function by recursion, the arguments of this -function may occur in the recursion's base case a, the counter x, or -the step function f. For example, in the following definition: - -Definition plus (x y : N) := recursion y (fun _ p => S p) x. - -one argument becomes the base case and the other becomes the counter. - -In the definitions of times: - -Definition times (x y : N) := recursion 0 (fun x p => plus y p) x. - -the argument y occurs in the step function. Thus it makes sense to -formulate an axiom saying that (recursion a f x) is equal to -(recursion a' f' x') whenever (EA a a'), x == x', and eq_fun2 f f'. We -need to vary all three arguments; for example, claiming that -(recursion a f x) equals (recursion a' f x') with the same f whenever -(EA a a') and x == x' is not enough to prove well-defidedness of -multiplication defined above. - -This leads to the axioms given below. There is a question if it is -possible to formulate simpler axioms that would imply this statement -for any implementation. Indeed, the proof seems to have to proceed by -straighforward induction on x. The difficulty is that we cannot prove -(EA (recursion a f x) (recursion a' f' x')) using the induction axioms -above because recursion is not declared to be a setoid morphism: -that's what we are proving! Therefore, this has to be proved by -induction inside each particular implementation. *) - -Axiom recursion_wd : forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> - forall x x' : N, x == x' -> - EA (recursion a f x) (recursion a' f' x'). - -(* Can we instead declare recursion as a morphism? It does not seem -so. For this, we need to register the relation EA, and for this we -need to declare it as a variable in a section. But information about -morhisms is lost when sections are closed. *) - -(* When the function recursion is polymorphic on the codomain A, there -seems no other option than to return the given base case a when the -counter is 0. Therefore, we can formulate the following axioms with -Leibniz equality. *) - -Axiom recursion_0 : - forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. - -Axiom recursion_S : - forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). - -(* It may be possible to formulate recursion_0 and recursion_S as follows: -Axiom recursion_0 : - forall (a : A) (f : N -> A -> A), - EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. - -Axiom recursion_S : - forall (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). - -Then it is possible to prove recursion_wd (see IotherInd.v). This -raises some questions: - -(1) Can the axioms recursion_wd, recursion_0 and recursion_S (both -variants) proved for all reasonable implementations? - -(2) Can these axioms be proved without assuming that EA is symmetric -and transitive? In OtherInd.v, recursion_wd can be proved from -recursion_0 and recursion_S by assuming symmetry and transitivity. - -(2) Which variant requires proving less for each implementation? Can -it be that proving all three axioms about recursion has some common -parts which have to be repeated? *) - -Implicit Arguments recursion_wd [A]. -Implicit Arguments recursion_0 [A]. -Implicit Arguments recursion_S [A]. - -End NatSignature. - -(* We use the predecessor function to prove the injectivity of S. There -are two ways to get this function: define it by primitive recursion, or -declare a signature and allow the user to provide an implementation, -similar to how this is done to plus, times, etc. We would like to use -the first option: first, to allow the user to provide an efficient -implementation, and second, to be able to use predecessor in signatures -defining other functions, e.g., subtraction. If we just define -predecessor by recursion in the NatProperties functor, we would not be -able to use it in other signatures, since those signatures do not invoke -the NatProperties functor. After giving a signature for the predecessor, -we define the functor NDefPred, which defines an implementation of a -predecessor by primitive recursion. We cannot put NDefPred in a -different file because the definition of the predecessor uses recursion, -which is introduced in this file, and the proof of injectivity of the -successor (also in this file) 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" *) -Ltac induct n := - try intros until n; - pattern n; apply induction; clear n; - [unfold NumPrelude.pred_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | |]. - -Theorem nondep_induction : - forall P : N -> Prop, NumPrelude.pred_wd E P -> - P 0 -> (forall n, P (S n)) -> forall n, P n. -Proof. -intros; apply induction; auto. -Qed. - -Ltac nondep_induct n := - try intros until n; - pattern n; apply nondep_induction; clear n; - [unfold NumPrelude.pred_wd; - let n := fresh "n" in - let m := fresh "m" in - let H := fresh "H" in intros n m H; qmorphism n m | |]. - -Definition if_zero (A : Set) (a b : A) (n : N) : A := - recursion a (fun _ _ => b) n. - -Add Morphism if_zero with signature LE_Set ==> LE_Set ==> E ==> LE_Set as if_zero_wd. -Proof. -unfold LE_Set. -intros; unfold if_zero; now apply recursion_wd with (EA := (@eq A)); -[| unfold eq_fun2; now intros |]. -Qed. - -Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. -Proof. -unfold if_zero; intros; now rewrite recursion_0. -Qed. - -Theorem if_zero_S : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b. -Proof. -intros; unfold if_zero. -now rewrite (recursion_S (@eq A)); [| | unfold fun2_wd; now intros]. -Qed. - -Implicit Arguments if_zero [A]. - -(* To prove this statement, we need to provably different terms, -e.g., true and false *) -Theorem S_0 : forall n, ~ S n == 0. -Proof. -intros n H. -assert (true = false); [| discriminate]. -replace true with (if_zero false true (S n)) by apply if_zero_S. -pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0. -change (LE_Set bool (if_zero false true (S n)) (if_zero false true 0)). -rewrite H. unfold LE_Set. reflexivity. -Qed. - -Theorem S_inj : forall m n, S m == S n -> m == n. -Proof. -intros m n H. -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 S_inj_contrap : forall n m, n # m -> S n # S m. -Proof. -intros n m H1 H2. apply S_inj in H2. now apply H1. -Qed. - -Definition iter_S (k : nat) (n : N) := - nat_rec (fun _ => N) n (fun _ p => S p) k. - -Add Morphism iter_S with signature (@eq nat) ==> E ==> E as iter_S_wd. -Proof. -intros k n m; induction k as [| k IH]; simpl in *. -trivial. -intro; apply S_wd; now apply IH. -Qed. - -Theorem iter_S_S : forall (k : nat) (n : N), iter_S k (S n) == S (iter_S k n). -Proof. -now (intros k n; induction k; simpl); [| apply S_wd]. -Qed. - -Theorem iter_S_neq_0 : forall k : nat, iter_S (Datatypes.S k) 0 # 0. -Proof. -destruct k; simpl; apply S_0. -Qed. - -Theorem iter_S_neq : forall (k : nat) (n : N), iter_S (Datatypes.S k) n # n. -Proof. -intro k; induct n; simpl. -apply S_0. -intros n IH H. apply S_inj in H. apply IH. now rewrite <- iter_S_S. -Qed. - -Theorem S_neq : forall n, S n # n. -Proof. -intro n; apply (iter_S_neq 0 n). -(* "apply iter_S_neq with (k := 0) (n := n)" does not work here !!! *) -Qed. - -Theorem SS_neq : forall n, S (S n) # n. -Proof. -intro n; apply (iter_S_neq 1 n). -Qed. - -Theorem SSS_neq : forall n, S (S (S n)) # n. -Proof. -intro n; apply (iter_S_neq 2 n). -Qed. - -Theorem not_all_eq_0 : ~ forall n, n == 0. -Proof. -intro H; apply (S_0 0). apply H. -Qed. - -Theorem not_0_implies_S : forall n, n # 0 <-> exists m, n == S m. -Proof. -intro n; split. -induct n; [intro H; now elim H | intros n _ _; now exists n]. -intro H; destruct H as [m H]; rewrite H; apply S_0. -Qed. - -Theorem O_or_S : forall n, n == 0 \/ exists m, n == S m. -Proof. -nondep_induct n; [now left | intros n; right; now exists n]. -Qed. - -(* The following is useful for reasoning about, e.g., Fibonacci numbers *) -Section DoubleInduction. -Variable P : N -> Prop. -Hypothesis P_correct : NumPrelude.pred_wd E P. - -Add Morphism P with signature E ==> iff as P_morphism. -Proof. -exact P_correct. -Qed. - -Theorem double_induction : - P 0 -> P 1 -> - (forall n, P n -> P (S n) -> P (S (S n))) -> forall n, P n. -Proof. -intros until 3. -assert (D : forall n, P n /\ P (S n)); [ |intro n; exact (proj1 (D n))]. -induct n; [ | intros n [IH1 IH2]]; auto. -Qed. - -End DoubleInduction. - -(* The following is useful for reasoning about, e.g., Ackermann function *) -Section TwoDimensionalInduction. -Variable R : N -> N -> Prop. -Hypothesis R_correct : rel_wd E R. - -Add Morphism R with signature E ==> E ==> iff as R_morphism. -Proof. -exact R_correct. -Qed. - -Theorem two_dim_induction : - R 0 0 -> - (forall n m, R n m -> R n (S m)) -> - (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. -Proof. -intros H1 H2 H3. induct n. -induct m. -exact H1. exact (H2 0). -intros n IH. induct m. -now apply H3. exact (H2 (S n)). -Qed. - -End TwoDimensionalInduction. - -End NatProperties. diff --git a/theories/Numbers/Natural/Axioms/NBase.v b/theories/Numbers/Natural/Axioms/NBase.v new file mode 100644 index 000000000..fd483265d --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NBase.v @@ -0,0 +1,196 @@ +Require Export NumPrelude. +Require Import NZBase. + +Module Type NBaseSig. + +Parameter Inline N : Set. +Parameter Inline E : N -> N -> Prop. +Parameter Inline O : N. +Parameter Inline S : N -> N. + +Delimit Scope NatScope with Nat. +Open Local Scope NatScope. + +Notation "x == y" := (E x y) (at level 70) : NatScope. +Notation "x ~= y" := (~ E x y) (at level 70) : NatScope. +Notation "0" := O : NatScope. +Notation "1" := (S O) : NatScope. + +Axiom E_equiv : equiv N E. +Add Relation N 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 S with signature E ==> E as S_wd. + +Axiom succ_inj : forall n1 n2 : N, S n1 == S n2 -> n1 == n2. +Axiom succ_neq_0 : forall n : N, S n ~= 0. + +Axiom induction : + forall A : N -> Prop, predicate_wd E A -> + A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n. + +End NBaseSig. + +Module NBasePropFunct (Import NBaseMod : NBaseSig). +Open Local Scope NatScope. + +(*Theorem E_equiv : equiv N E. +Proof E_equiv. + +Theorem succ_inj_wd : forall n1 n2 : N, S n1 == S n2 <-> n1 == n2. +Proof succ_inj_wd. + +Theorem succ_neq_0 : forall n : N, S n ~= 0. +Proof succ_neq_0. + +Theorem induction : + forall A : N -> Prop, predicate_wd E A -> + A 0 -> (forall n : N, A n -> A (S n)) -> forall n : N, A n. +Proof induction.*) + +Module NZBaseMod <: NZBaseSig. +Definition NZ := N. +Definition NZE := E. +Definition NZ0 := 0. +Definition NZsucc := S. + +(* Axioms *) +Definition NZE_equiv := E_equiv. +Definition NZsucc_inj := succ_inj. + +Add Relation NZ NZE + 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 NZsucc with signature NZE ==> NZE as NZsucc_wd. +Proof S_wd. + +Theorem NZinduction : + forall A : N -> Prop, predicate_wd E A -> + A 0 -> (forall n : N, A n <-> A (S n)) -> forall n : N, A n. +Proof. +intros A A_wd Base Step. +apply induction; try assumption. +intros; now apply -> Step. +Qed. + +End NZBaseMod. + +Module Export NZBasePropMod := NZBasePropFunct NZBaseMod. + +Theorem neq_symm : forall n m : N, n ~= m -> m ~= n. +Proof NZneq_symm. + +Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m. +Proof NZsucc_inj_wd_neg. + +Ltac induct n := induction_maker n ltac:(apply induction). + +Theorem nondep_induction : + forall A : N -> Prop, predicate_wd E A -> + A 0 -> (forall n : N, A (S n)) -> forall n : N, A n. +Proof. +intros; apply induction; auto. +Qed. + +Ltac nondep_induct n := induction_maker n ltac:(apply nondep_induction). + +Theorem neq_0 : ~ forall n, n == 0. +Proof. +intro H; apply (succ_neq_0 0). apply H. +Qed. + +Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m. +Proof. +nondep_induct n. split; intro H; +[now elim H | destruct H as [m H]; symmetry in H; false_hyp H succ_neq_0]. +intro n; split; intro H; [now exists n | apply succ_neq_0]. +Qed. + +Theorem zero_or_succ : forall n, n == 0 \/ exists m, n == S m. +Proof. +nondep_induct n; [now left | intros n; right; now exists n]. +Qed. + +(* The following is useful for reasoning about, e.g., Fibonacci numbers *) +Section DoubleInduction. + +Variable A : N -> Prop. +Hypothesis A_wd : predicate_wd E A. + +Add Morphism A with signature E ==> iff as A_morph. +Proof. +exact A_wd. +Qed. + +Theorem double_induction : + A 0 -> A 1 -> + (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n. +Proof. +intros until 3. +assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))]. +induct n; [ | intros n [IH1 IH2]]; auto. +Qed. + +End DoubleInduction. + +Ltac double_induct n := induction_maker n ltac:(apply double_induction). + +(* The following is useful for reasoning about, e.g., Ackermann function *) +Section TwoDimensionalInduction. + +Variable R : N -> N -> Prop. +Hypothesis R_wd : rel_wd E E R. + +Add Morphism R with signature E ==> E ==> iff as R_morph. +Proof. +exact R_wd. +Qed. + +Theorem two_dim_induction : + R 0 0 -> + (forall n m, R n m -> R n (S m)) -> + (forall n, (forall m, R n m) -> R (S n) 0) -> forall n m, R n m. +Proof. +intros H1 H2 H3. induct n. +induct m. +exact H1. exact (H2 0). +intros n IH. induct m. +now apply H3. exact (H2 (S n)). +Qed. + +End TwoDimensionalInduction. + +Ltac two_dim_induct n m := + try intros until n; + try intros until m; + pattern n, m; apply two_dim_induction; clear n m; + [unfold rel_wd; unfold fun2_wd; + let x1 := fresh "x" in + let y1 := fresh "y" in + let H1 := fresh "H" in + let x2 := fresh "x" in + let y2 := fresh "y" in + let H2 := fresh "H" in + intros x1 y1 H1 x2 y2 H2; + qsetoid_rewrite H1; + qiff x2 y2 H2 | | | ]. +(* This is not a very efficient approach because qsetoid_rewrite uses +qiff to take the formula apart in order to make it quantifier-free, +and then qiff is called again and takes the formula apart for the +second time. It is better to analyze the formula once and generalize +qiff to take a list of equalities that it has to rewrite. *) + +End NBasePropFunct. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NDepRec.v b/theories/Numbers/Natural/Axioms/NDepRec.v index de261bfbe..9ad0b4650 100644 --- a/theories/Numbers/Natural/Axioms/NDepRec.v +++ b/theories/Numbers/Natural/Axioms/NDepRec.v @@ -7,10 +7,10 @@ to try to use arbitrary domain and require that n == n' -> A n = A n'. *) Module Type NDepRecSignature. Declare Module Export NDomainModule : NDomainEqSignature. -Declare Module Export NatModule : NatSignature with +Declare Module Export NBaseMod : NBaseSig with Module NDomainModule := NDomainModule. (* Instead of these two lines, I would like to say -Declare Module Export Nat : NatSignature with Module NDomain : NatEqDomain. *) +Declare Module Export Nat : NBaseSig with Module NDomain : NatEqDomain. *) Open Local Scope NatScope. Parameter Inline dep_recursion : @@ -20,7 +20,7 @@ Axiom dep_recursion_0 : forall (A : N -> Set) (a : A 0) (f : forall n, A n -> A (S n)), dep_recursion A a f 0 = a. -Axiom dep_recursion_S : +Axiom dep_recursion_succ : 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). @@ -28,12 +28,12 @@ End NDepRecSignature. Module NDepRecTimesProperties (Import NDepRecModule : NDepRecSignature) - (Import NTimesModule : NTimesSignature - with Module NPlusModule.NatModule := NDepRecModule.NatModule). -Module Export NTimesPropertiesModule := NTimesProperties NTimesModule. + (Import NTimesMod : NTimesSig + with Module NPlusMod.NBaseMod := NDepRecModule.NBaseMod). +Module Export NTimesPropertiesModule := NTimesPropFunct NTimesMod. Open Local Scope NatScope. -Theorem not_0_implies_S_dep : forall n, n # O -> {m : N | n == S m}. +Theorem not_0_implies_succ_dep : forall n, n # O -> {m : N | n == S m}. Proof. intro n; pattern n; apply dep_recursion; clear n; [intro H; now elim H | intros n _ _; now exists n]. @@ -51,7 +51,7 @@ Proof. intros m n; pattern m; apply dep_recursion; clear m. intro H. rewrite plus_0_l in H. left; now split. -intros m IH H. rewrite plus_S_l in H. apply S_inj in H. +intros m IH H. rewrite plus_succ_l in H. apply succ_inj in H. apply plus_eq_0 in H. destruct H as [H1 H2]. right; now split; [rewrite H1 |]. Qed. @@ -65,7 +65,14 @@ intros; left; reflexivity. intros; left; reflexivity. intros; right; reflexivity. intros n _ m _ H. -rewrite times_S_l in H. rewrite plus_S_r in H; now apply S_0 in H. +rewrite times_succ_l in H. rewrite plus_succ_r in H; now apply succ_0 in H. Qed. End NDepRecTimesProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NDomain.v b/theories/Numbers/Natural/Axioms/NDomain.v index 52148cd38..a95c94ca0 100644 --- a/theories/Numbers/Natural/Axioms/NDomain.v +++ b/theories/Numbers/Natural/Axioms/NDomain.v @@ -99,3 +99,10 @@ Ltac stepl_ring t := stepl t; [| ring]. Ltac stepr_ring t := stepr t; [| ring]. End NDomainProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NIso.v b/theories/Numbers/Natural/Axioms/NIso.v index ebd22e142..9ee79022e 100644 --- a/theories/Numbers/Natural/Axioms/NIso.v +++ b/theories/Numbers/Natural/Axioms/NIso.v @@ -1,6 +1,6 @@ Require Export NAxioms. -Module Homomorphism (Nat1 Nat2 : NatSignature). +Module Homomorphism (Nat1 Nat2 : NBaseSig). Notation Local N1 := Nat1.NDomainModule.N. Notation Local N2 := Nat2.NDomainModule.N. @@ -26,7 +26,7 @@ unfold natural_isomorphism. intros x y Exy. apply Nat1.recursion_wd with (EA := E2). reflexivity. -unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.S_wd. +unfold eq_fun2. intros _ _ _ y' y'' H. now apply Nat2.succ_wd. assumption. Qed. @@ -35,27 +35,27 @@ Proof. unfold natural_isomorphism; now rewrite Nat1.recursion_0. Qed. -Theorem natural_isomorphism_S : +Theorem natural_isomorphism_succ : forall x : N1, natural_isomorphism (S1 x) == S2 (natural_isomorphism x). Proof. unfold natural_isomorphism; -intro x; now rewrite (Nat1.recursion_S Nat2.NDomainModule.E); -[| unfold fun2_wd; intros; apply Nat2.S_wd |]. +intro x; now rewrite (Nat1.recursion_succ Nat2.NDomainModule.E); +[| unfold fun2_wd; intros; apply Nat2.succ_wd |]. Qed. Theorem iso_hom : homomorphism natural_isomorphism. Proof. unfold homomorphism, natural_isomorphism; split; -[exact natural_isomorphism_0 | exact natural_isomorphism_S]. +[exact natural_isomorphism_0 | exact natural_isomorphism_succ]. Qed. End Homomorphism. -Module Inverse (Nat1 Nat2 : NatSignature). +Module Inverse (Nat1 Nat2 : NBaseSig). -Module Import NatProperties1 := NatProperties Nat1. +Module Import NBasePropMod1 := NBasePropFunct Nat1. (* This makes the tactic induct available. Since it is taken from -NatProperties Nat1, it refers to Nat1.induction. *) +NBasePropFunct Nat1, it refers to Nat1.induction. *) Module Hom12 := Homomorphism Nat1 Nat2. Module Hom21 := Homomorphism Nat2 Nat1. @@ -73,13 +73,13 @@ Proof. induct x. now rewrite Hom12.natural_isomorphism_0; rewrite Hom21.natural_isomorphism_0. intros x IH. -rewrite Hom12.natural_isomorphism_S; rewrite Hom21.natural_isomorphism_S; +rewrite Hom12.natural_isomorphism_succ; rewrite Hom21.natural_isomorphism_succ; now rewrite IH. Qed. End Inverse. -Module Isomorphism (Nat1 Nat2 : NatSignature). +Module Isomorphism (Nat1 Nat2 : NBaseSig). Module Hom12 := Homomorphism Nat1 Nat2. Module Hom21 := Homomorphism Nat2 Nat1. @@ -109,3 +109,10 @@ apply Inverse212.iso_inverse. Qed. End Isomorphism. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NLeibniz.v b/theories/Numbers/Natural/Axioms/NLeibniz.v new file mode 100644 index 000000000..d9c4718aa --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NLeibniz.v @@ -0,0 +1,4 @@ +(* This file proves or redefines properties that are true for Leibniz +equality. For example, it removes the premise predicate_wd from +induction theorems. *) + diff --git a/theories/Numbers/Natural/Axioms/NMinus.v b/theories/Numbers/Natural/Axioms/NMinus.v index 70fd8c719..2bac3c5c3 100644 --- a/theories/Numbers/Natural/Axioms/NMinus.v +++ b/theories/Numbers/Natural/Axioms/NMinus.v @@ -11,45 +11,45 @@ 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). +Axiom minus_succ_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). + (Import NPlusMod : NPlusSig with + Module NBaseMod := NMinusModule.NPredModule.NBaseMod) + (Import NOrderModule : NOrderSig with + Module NBaseMod := NMinusModule.NPredModule.NBaseMod). Module Export NPlusOrderPropertiesModule := - NPlusOrderProperties NPlusModule NOrderModule. + NPlusOrderProperties NPlusMod 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. +intro n; rewrite minus_succ_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. +intros n IH; rewrite minus_succ_r; rewrite IH. now apply pred_0. Qed. -Theorem minus_comm_S : forall n m, S n - S m == n - m. +Theorem minus_comm_succ : 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. +rewrite minus_succ_r. do 2 rewrite minus_0_r. now rewrite pred_succ. +intros m IH. rewrite minus_succ_r. rewrite IH. now rewrite minus_succ_r. Qed. -Theorem minus_S_l : forall n m, n <= m -> S m - n == S (m - n). +Theorem minus_succ_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. +now do 2 rewrite minus_comm_succ. assumption. Qed. Theorem minus_le : forall n m, n <= m -> n - m == 0. @@ -57,7 +57,7 @@ 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. +clear n m H; intros n m H1 H2. now rewrite minus_comm_succ. assumption. Qed. @@ -71,7 +71,7 @@ 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_S_r. +clear n m H. intros n m _ H2. rewrite minus_comm_succ. rewrite plus_succ_r. now rewrite H2. assumption. Qed. @@ -79,3 +79,10 @@ Qed. End NMinusProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NMiscFunct.v b/theories/Numbers/Natural/Axioms/NMiscFunct.v index 8743f5961..82a922453 100644 --- a/theories/Numbers/Natural/Axioms/NMiscFunct.v +++ b/theories/Numbers/Natural/Axioms/NMiscFunct.v @@ -2,7 +2,7 @@ Require Import Bool. (* To get the orb and negb function *) Require Export NStrongRec. Require Export NTimesOrder. -Module MiscFunctFunctor (Import NatMod : NatSignature). +Module MiscFunctFunctor (Import NatMod : NBaseSig). Module Export StrongRecPropertiesModule := StrongRecProperties NatMod. Open Local Scope NatScope. @@ -33,10 +33,10 @@ intro y. unfold plus. rewrite recursion_0. apply (proj1 E_equiv). Qed. -Theorem plus_S : forall x y, plus (S x) y == S (plus x y). +Theorem plus_succ : forall x y, plus (S x) y == S (plus x y). Proof. intros x y; unfold plus. -now rewrite (recursion_S E); [|apply plus_step_wd|]. +now rewrite (recursion_succ E); [|apply plus_step_wd|]. Qed. (*****************************************************) @@ -68,10 +68,10 @@ Proof. intro. unfold times. now rewrite recursion_0. Qed. -Theorem times_S_r : forall x y, times x (S y) == plus (times x y) x. +Theorem times_succ_r : forall x y, times x (S y) == plus (times x y) x. Proof. intros x y; unfold times. -now rewrite (recursion_S E); [| apply times_step_wd |]. +now rewrite (recursion_succ E); [| apply times_step_wd |]. Qed. (*****************************************************) @@ -107,7 +107,7 @@ intros; rewrite le_lt; now right. Qed. Lemma lt_base_wd : eq_fun E eq_bool (if_zero false true) (if_zero false true). -unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_Set. +unfold eq_fun, eq_bool; intros; apply if_zero_wd; now unfold LE_succet. Qed. Lemma lt_step_wd : @@ -155,7 +155,7 @@ Qed. Theorem lt_step_eq : forall m n, lt (S m) n = recursion false (fun n' _ => lt m n') n. Proof. intros m n; unfold lt. -pose proof (recursion_S (eq_fun E eq_bool) (if_zero false true) +pose proof (recursion_succ (eq_fun E eq_bool) (if_zero false true) (fun _ f => fun n => recursion false (fun n' _ => f n') n) lt_base_wd lt_step_wd m n n) as H. unfold eq_bool in H. @@ -175,39 +175,39 @@ lt_step n (recursion lt_base lt_step n)? *) Lemma lt_0_1 : lt 0 1. Proof. -rewrite lt_base_eq; now rewrite if_zero_S. +rewrite lt_base_eq; now rewrite if_zero_succ. Qed. -Lemma lt_0_Sn : forall n, lt 0 (S n). +Lemma lt_0_succn : forall n, lt 0 (S n). Proof. -intro n; rewrite lt_base_eq; now rewrite if_zero_S. +intro n; rewrite lt_base_eq; now rewrite if_zero_succ. Qed. -Lemma lt_Sn_Sm : forall n m, lt (S n) (S m) <-> lt n m. +Lemma lt_succn_succm : forall n m, lt (S n) (S m) <-> lt n m. Proof. intros n m. -rewrite lt_step_eq. rewrite (recursion_S eq_bool). +rewrite lt_step_eq. rewrite (recursion_succ eq_bool). reflexivity. now unfold eq_bool. unfold fun2_wd; intros; now apply lt_wd. Qed. -Theorem lt_S : forall m n, lt m (S n) <-> le m n. +Theorem lt_succ : forall m n, lt m (S n) <-> le m n. Proof. assert (A : forall m n, lt m (S n) <-> lt m n \/ m == n). induct m. nondep_induct n; [split; intro; [now right | apply lt_0_1] | -intro n; split; intro; [left |]; apply lt_0_Sn]. +intro n; split; intro; [left |]; apply lt_0_succn]. intros n IH. nondep_induct n0. split. -intro. assert (H1 : lt n 0); [now apply -> lt_Sn_Sm | false_hyp H1 lt_0]. +intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0]. intro H; destruct H as [H | H]. -false_hyp H lt_0. false_hyp H S_0. +false_hyp H lt_0. false_hyp H succ_0. intro m. pose proof (IH m) as H; clear IH. -assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_Sn_Sm |]. -assert (lt (S n) (S m) <-> lt n m); [apply lt_Sn_Sm |]. -assert (S n == S m <-> n == m); [split; [ apply S_inj | apply S_wd]|]. tauto. +assert (lt (S n) (S (S m)) <-> lt n (S m)); [apply lt_succn_succm |]. +assert (lt (S n) (S m) <-> lt n m); [apply lt_succn_succm |]. +assert (S n == S m <-> n == m); [split; [ apply succ_inj | apply succ_wd]|]. tauto. intros; rewrite le_lt; apply A. Qed. @@ -238,10 +238,10 @@ unfold even. now rewrite recursion_0. Qed. -Theorem even_S : forall x : N, even (S x) = negb (even x). +Theorem even_succ : forall x : N, even (S x) = negb (even x). Proof. unfold even. -intro x; rewrite (recursion_S (@eq bool)); try reflexivity. +intro x; rewrite (recursion_succ (@eq bool)); try reflexivity. unfold fun2_wd. intros _ _ _ b b' Ebb'. destruct b; destruct b'; now simpl. Qed. @@ -305,7 +305,7 @@ rewrite <- H; clear H. assert (H : e y 1 = e y' 1); [now apply e_wd|]. rewrite <- H; clear H. assert (H : S (g (half y)) == S (g' (half y'))); -[apply S_wd; apply Egg'; now apply half_wd|]. +[apply succ_wd; apply Egg'; now apply half_wd|]. now destruct (e y 0); destruct (e y 1). Qed. @@ -314,12 +314,12 @@ Qed. (** via recursion, we form the corresponding modules and *) (** apply the properties functors to these modules *) -Module NDefaultPlusModule <: NPlusSignature. +Module NDefaultPlusModule <: NPlusSig. -Module NatModule := NatMod. -(* If we used the name NatModule instead of NatMod then this would +Module NBaseMod := NatMod. +(* If we used the name NBaseMod instead of NatMod then this would produce many warnings like "Trying to mask the absolute name -NatModule", "Trying to mask the absolute name Nat.O" etc. *) +NBaseMod", "Trying to mask the absolute name Nat.O" etc. *) Definition plus := plus. @@ -333,15 +333,15 @@ Proof. exact plus_0. Qed. -Theorem plus_S_l : forall n m, plus (S n) m == S (plus n m). +Theorem plus_succ_l : forall n m, plus (S n) m == S (plus n m). Proof. -exact plus_S. +exact plus_succ. Qed. End NDefaultPlusModule. -Module NDefaultTimesModule <: NTimesSignature. -Module NPlusModule := NDefaultPlusModule. +Module NDefaultTimesModule <: NTimesSig. +Module NPlusMod := NDefaultPlusModule. Definition times := times. @@ -351,12 +351,12 @@ exact times_wd. Qed. Definition times_0_r := times_0_r. -Definition times_S_r := times_S_r. +Definition times_succ_r := times_succ_r. End NDefaultTimesModule. -Module NDefaultOrderModule <: NOrderSignature. -Module NatModule := NatMod. +Module NDefaultOrderModule <: NOrderSig. +Module NBaseMod := NatMod. Definition lt := lt. Definition le := le. @@ -384,9 +384,9 @@ Proof. exact lt_0. Qed. -Theorem lt_S : forall x y, lt x (S y) <-> le x y. +Theorem lt_succ : forall x y, lt x (S y) <-> le x y. Proof. -exact lt_S. +exact lt_succ. Qed. End NDefaultOrderModule. @@ -395,3 +395,10 @@ Module Export DefaultTimesOrderProperties := NTimesOrderProperties NDefaultTimesModule NDefaultOrderModule. End MiscFunctFunctor. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NOrder.v b/theories/Numbers/Natural/Axioms/NOrder.v index 1b631ce64..b4f363901 100644 --- a/theories/Numbers/Natural/Axioms/NOrder.v +++ b/theories/Numbers/Natural/Axioms/NOrder.v @@ -1,330 +1,339 @@ -Require Export NAxioms. +Require Export NBase. +Require Import NZOrder. -Module Type NOrderSignature. -Declare Module Export NatModule : NatSignature. +Module Type NOrderSig. +Declare Module Export NBaseMod : NBaseSig. Open Local Scope NatScope. -Parameter Inline lt : N -> N -> bool. -Parameter Inline le : N -> N -> bool. +Parameter Inline lt : N -> N -> Prop. +Parameter Inline le : N -> N -> Prop. Notation "x < y" := (lt x y) : NatScope. Notation "x <= y" := (le x y) : NatScope. Notation "x > y" := (lt y x) (only parsing) : NatScope. Notation "x >= y" := (le y x) (only parsing) : NatScope. -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. +Add Morphism lt with signature E ==> E ==> iff as lt_wd. +Add Morphism le with signature E ==> E ==> iff 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. +Axiom le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y. +Axiom nlt_0_r : forall x, ~ (x < 0). +Axiom lt_succ_le : forall x y, x < S y <-> x <= y. -Module NOrderProperties (Import NOrderModule : NOrderSignature). -Module Export NatPropertiesModule := NatProperties NatModule. +End NOrderSig. + +Module NOrderPropFunct (Import NOrderModule : NOrderSig). +Module Export NBasePropMod := NBasePropFunct NBaseMod. 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]. +Ltac le_intro1 := rewrite le_lt_or_eq; left. +Ltac le_intro2 := rewrite le_lt_or_eq; right. +Ltac le_elim H := rewrite le_lt_or_eq in H; destruct H as [H | H]. -Lemma lt_stepl : forall x y z, x < y -> x == z -> z < y. +Theorem lt_succ_lt : forall n m : N, S n < m -> n < m. Proof. -intros x y z H1 H2; now rewrite <- H2. +intro n; induct m. +intro H; false_hyp H nlt_0_r. +intros m IH H. apply <- lt_succ_le. apply -> lt_succ_le in H. le_elim H. +le_intro1; now apply IH. +rewrite <- H; le_intro1. apply <- lt_succ_le; now le_intro2. Qed. -Lemma lt_stepr : forall x y z, x < y -> y == z -> x < z. +Theorem lt_irrefl : forall n : N, ~ (n < n). Proof. -intros x y z H1 H2; now rewrite <- H2. +induct n. +apply nlt_0_r. +intros n IH H. apply -> lt_succ_le in H; le_elim H. +apply lt_succ_lt in H; now apply IH. +assert (n < S n) by (apply <- lt_succ_le; now le_intro2). +rewrite H in *; now apply IH. Qed. -Lemma le_stepl : forall x y z, x <= y -> x == z -> z <= y. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. +Module NZOrderMod <: NZOrderSig. +Module NZBaseMod := NZBaseMod. -Lemma le_stepr : forall x y z, x <= y -> y == z -> x <= z. -Proof. -intros x y z H1 H2; now rewrite <- H2. -Qed. +Definition NZlt := lt. +Definition NZle := le. -Declare Left Step lt_stepl. -Declare Right Step lt_stepr. -Declare Left Step le_stepl. -Declare Right Step le_stepr. +Add Morphism NZlt with signature E ==> E ==> iff as NZlt_wd. +Proof lt_wd. -Theorem le_refl : forall n, n <= n. -Proof. -intro; now le_intro2. -Qed. +Add Morphism NZle with signature E ==> E ==> iff as NZle_wd. +Proof le_wd. -Theorem le_0_r : forall n, n <= 0 -> n == 0. -Proof. -intros n H; le_elim H; [false_hyp H lt_0 | assumption]. -Qed. +Definition NZle_lt_or_eq := le_lt_or_eq. +Definition NZlt_succ_le := lt_succ_le. +Definition NZlt_succ_lt := lt_succ_lt. +Definition NZlt_irrefl := lt_irrefl. -Theorem lt_n_Sn : forall n, n < S n. -Proof. -intro n. apply <- lt_S. now le_intro2. -Qed. +End NZOrderMod. -Theorem lt_closed_S : forall n m, n < m -> n < S m. -Proof. -intros. apply <- lt_S. now le_intro1. -Qed. +Module Export NZOrderPropMod := NZOrderPropFunct NZOrderMod. -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. +(* Renaming theorems from NZOrder.v *) -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_le_incl : forall n m : N, n < m -> n <= m. +Proof NZlt_le_incl. -Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. -Proof. -intros n m p; induct m. -intros H1 H2; absurd_hyp H1; [ apply lt_0 | assumption]. -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_neq : forall n m : N, n < m -> n ~= m. +Proof NZlt_neq. -Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. -Proof. -intros n m p H1 H2; le_elim H1. -le_elim H2. le_intro1; now apply lt_trans with (m := m). -le_intro1; now rewrite <- H2. now rewrite H1. -Qed. +Theorem le_refl : forall n : N, n <= n. +Proof NZle_refl. -Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. -Proof. -intros n m p H1 H2; le_elim H1. -now apply lt_trans with (m := m). now rewrite H1. -Qed. +Theorem lt_succ_r : forall n : N, n < S n. +Proof NZlt_succ_r. -Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. -Proof. -intros n m p H1 H2; le_elim H2. -now apply lt_trans with (m := m). now rewrite <- H2. -Qed. +Theorem le_succ_r : forall n : N, n <= S n. +Proof NZle_succ_r. -Theorem lt_positive : forall n m, n < m -> 0 < m. -Proof. -intros n m; induct n. -trivial. -intros x IH H. -apply lt_trans with (m := S x); [apply lt_0_Sn | apply H]. -Qed. +Theorem lt_lt_succ : forall n m : N, n < m -> n < S m. +Proof NZlt_lt_succ. -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_trans with (m := S x). -apply IH; assumption. -apply lt_n_Sn. -rewrite H; apply lt_n_Sn. -Qed. +Theorem le_le_succ : forall n m : N, n <= m -> n <= S m. +Proof NZle_le_succ. -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 le_succ_le_or_eq_succ : forall n m : N, n <= S m <-> n <= m \/ n == S m. +Proof NZle_succ_le_or_eq_succ. -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_trans with (m := S n); [apply lt_n_Sn | assumption] | -apply S_inj in H; rewrite H; apply lt_n_Sn]. -Qed. +Theorem neq_succ_l : forall n : N, S n ~= n. +Proof NZneq_succ_l. -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 nlt_succ_l : forall n : N, ~ S n < n. +Proof NZnlt_succ_l. -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 nle_succ_l : forall n : N, ~ S n <= n. +Proof NZnle_succ_l. -Theorem lt_irr : forall n, ~ (n < n). -Proof. -induct n. -apply lt_0. -intro x; unfold not; intros H1 H2; apply H1; now apply -> lt_resp_S. -Qed. +Theorem lt_le_succ : forall n m : N, n < m <-> S n <= m. +Proof NZlt_le_succ. -Theorem le_antisym : forall n m, n <= m -> m <= n -> n == m. -Proof. -intros n m H1 H2; le_elim H1; le_elim H2. -elimtype False; apply lt_irr with (n := n); now apply lt_trans with (m := m). -now symmetry. assumption. assumption. -Qed. +Theorem le_succ_le : forall n m : N, S n <= m -> n <= m. +Proof NZle_succ_le. -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 succ_lt_mono : forall n m : N, n < m <-> S n < S m. +Proof NZsucc_lt_mono. -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 succ_le_mono : forall n m : N, n <= m <-> S n <= S m. +Proof NZsucc_le_mono. -Theorem lt_asymm : forall n m, ~ (n < m /\ m < n). -Proof. -unfold not; intros n m [H1 H2]. -now apply (lt_trans n m n) in H1; [false_hyp H1 lt_irr|]. -Qed. +Theorem lt_lt_false : forall n m, n < m -> m < n -> False. +Proof NZlt_lt_false. -Theorem le_0_l: forall n, 0 <= n. -Proof. -induct n; [now le_intro2 | intros; le_intro1; apply lt_0_Sn]. -Qed. +Theorem lt_asymm : forall n m, n < m -> ~ m < n. +Proof NZlt_asymm. + +Theorem lt_trans : forall n m p : N, n < m -> m < p -> n < p. +Proof NZlt_trans. + +Theorem le_trans : forall n m p : N, n <= m -> m <= p -> n <= p. +Proof NZle_trans. + +Theorem le_lt_trans : forall n m p : N, n <= m -> m < p -> n < p. +Proof NZle_lt_trans. + +Theorem lt_le_trans : forall n m p : N, n < m -> m <= p -> n < p. +Proof NZlt_le_trans. + +Theorem le_antisymm : forall n m : N, n <= m -> m <= n -> n == m. +Proof NZle_antisymm. + +(** Trichotomy, decidability, and double negation elimination *) + +Theorem lt_trichotomy : forall n m : N, n < m \/ n == m \/ m < n. +Proof NZlt_trichotomy. + +Theorem le_lt_dec : forall n m : N, n <= m \/ m < n. +Proof NZle_lt_dec. + +Theorem le_nlt : forall n m : N, n <= m <-> ~ m < n. +Proof NZle_nlt. + +Theorem lt_dec : forall n m : N, n < m \/ ~ n < m. +Proof NZlt_dec. + +Theorem lt_dne : forall n m, ~ ~ n < m <-> n < m. +Proof NZlt_dne. + +Theorem nle_lt : forall n m : N, ~ n <= m <-> m < n. +Proof NZnle_lt. + +Theorem le_dec : forall n m : N, n <= m \/ ~ n <= m. +Proof NZle_dec. + +Theorem le_dne : forall n m : N, ~ ~ n <= m <-> n <= m. +Proof NZle_dne. + +Theorem lt_nlt_succ : forall n m : N, n < m <-> ~ m < S n. +Proof NZlt_nlt_succ. + +Theorem lt_exists_pred : + forall z n : N, z < n -> exists k : N, n == S k /\ z <= k. +Proof NZlt_exists_pred. + +Theorem lt_succ_iter_r : + forall (n : nat) (m : N), m < NZsucc_iter (Datatypes.S n) m. +Proof NZlt_succ_iter_r. + +Theorem neq_succ_iter_l : + forall (n : nat) (m : N), NZsucc_iter (Datatypes.S n) m ~= m. +Proof NZneq_succ_iter_l. + +(** Stronger variant of induction with assumptions n >= 0 (n < 0) +in the induction step *) -Theorem lt_trichotomy : forall n m, n < m \/ n == m \/ m < n. +Theorem right_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, z <= n -> A n. +Proof NZright_induction. + +Theorem left_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, n <= z -> A n. +Proof NZleft_induction. + +Theorem central_induction : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, A z -> + (forall n : N, z <= n -> A n -> A (S n)) -> + (forall n : N, n < z -> A (S n) -> A n) -> + forall n : N, A n. +Proof NZcentral_induction. + +Theorem right_induction' : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> A n -> A (S n)) -> + forall n : N, A n. +Proof NZright_induction'. + +Theorem strong_right_induction' : + forall A : N -> Prop, predicate_wd E A -> + forall z : N, + (forall n : N, n <= z -> A n) -> + (forall n : N, z <= n -> (forall m : N, z <= m -> m < n -> A m) -> A n) -> + forall n : N, A n. +Proof NZstrong_right_induction'. + +(** Elimintation principle for < *) + +Theorem lt_ind : + forall A : N -> Prop, predicate_wd E A -> + forall n : N, + A (S n) -> + (forall m : N, n < m -> A m -> A (S m)) -> + forall m : N, n < m -> A m. +Proof NZlt_ind. + +(** Elimintation principle for <= *) + +Theorem le_ind : + forall A : N -> Prop, predicate_wd E A -> + forall n : N, + A n -> + (forall m : N, n <= m -> A m -> A (S m)) -> + forall m : N, n <= m -> A m. +Proof NZle_ind. + +(** Theorems that are true for natural numbers but not for integers *) + +Theorem le_0_l : forall n : N, 0 <= 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_trans with (m := n); [assumption | apply lt_n_Sn]. +induct n. +now le_intro2. +intros; now apply le_le_succ. Qed. -(** The law of excluded middle for < *) -Theorem lt_em : forall n m, n < m \/ ~ n < m. +Theorem nle_succ_0 : forall n, ~ (S n <= 0). 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_irr. -right; intro; apply (lt_asymm n m); split; assumption. +intros n H; apply <- lt_le_succ in H; false_hyp H nlt_0_r. Qed. -Theorem not_lt : forall n m, ~ (n < m) <-> n >= m. +Theorem le_0_eq_0 : forall n, n <= 0 -> n == 0. Proof. -intros n m; split; intro H. -destruct (lt_trichotomy n m) as [H1 | [H1 | H1]]. -false_hyp H1 H. rewrite H1; apply le_refl. now le_intro1. -intro; now apply (le_lt_trans m n m) in H; [false_hyp H lt_irr |]. +intros n H; le_elim H; [false_hyp H nlt_0_r | assumption]. Qed. -Theorem lt_or_ge : forall n m, n < m \/ n >= m. +Theorem lt_0_succ : forall n, 0 < S n. Proof. -intros n m; rewrite <- not_lt; apply lt_em. +induct n; [apply lt_succ_r | intros n H; now apply lt_lt_succ]. Qed. -Theorem nat_total_order : forall n m, n # m -> n < m \/ m < n. +Theorem lt_lt_0 : forall n m, n < m -> 0 < m. Proof. -intros n m H; destruct (lt_trichotomy n m) as [A | A]; [now left |]. -now destruct A as [A | A]; [elim H | right]. +intros n m; induct n. +trivial. +intros n IH H. apply IH; now apply lt_succ_lt. Qed. -Theorem lt_exists_pred : forall n m, m < n -> exists p, n == S p. +Theorem neq_0_lt_0 : forall n, 0 ~= n -> 0 < n. Proof. -nondep_induct n. -intros m H; false_hyp H lt_0. -intros n _ _; now exists n. +nondep_induct n. intro H; now elim H. intros; apply lt_0_succ. 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. +Lemma Acc_nonneg_lt : forall n : N, + Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n. 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. +intros n H; induction H as [n _ H2]; +constructor; intros y H; apply H2; split; [apply le_0_l | assumption]. Qed. -Theorem lt_ind : - Q (S n) -> - (forall m, n < m -> Q m -> Q (S m)) -> - forall m, n < m -> Q m. +Theorem lt_wf : well_founded lt. 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. +unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf. Qed. -End Induction1. +(** Elimination principlies for < and <= for relations *) -Section Induction2. +Section RelElim. -(* Variable Q : relation N. -- does not work !!! *) -Variable Q : N -> N -> Prop. -Hypothesis Q_wd : rel_wd E Q. +(* FIXME: Variable R : relation N. -- does not work *) -Add Morphism Q with signature E ==> E ==> iff as Q_morph2. -Proof Q_wd. +Variable R : N -> N -> Prop. +Hypothesis R_wd : rel_wd E E R. + +Add Morphism R with signature E ==> E ==> iff as R_morph2. +Proof R_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. + (forall m, R 0 m) -> + (forall n m, n <= m -> R n m -> R (S n) (S m)) -> + forall n m, n <= m -> R 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]. +intros n IH m H. elim H using le_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now le_intro2. +intros k H1 H2. apply le_succ_le in H1. auto. 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. + (forall m, R 0 (S m)) -> + (forall n m, n < m -> R n m -> R (S n) (S m)) -> + forall n m, n < m -> R n m. Proof. intros Base Step; induct n. -intros m H. apply lt_exists_pred in H; destruct H as [m' H]. +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]. +intros n IH m H. elim H using lt_ind. +solve_predicate_wd. +apply Step; [| apply IH]; now apply lt_succ_r. +intros k H1 H2. apply lt_succ_lt in H1. auto. Qed. -End Induction2. +End RelElim. + +End NOrderPropFunct. + -End NOrderProperties. +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NOtherInd.v b/theories/Numbers/Natural/Axioms/NOtherInd.v index cf6738750..9b01e5143 100644 --- a/theories/Numbers/Natural/Axioms/NOtherInd.v +++ b/theories/Numbers/Natural/Axioms/NOtherInd.v @@ -8,7 +8,7 @@ Parameter S : N -> N. Notation "0" := O. Definition induction := -forall P : N -> Prop, pred_wd E P -> +forall P : N -> Prop, predicate_wd E P -> P 0 -> (forall n : N, P n -> P (S n)) -> forall n : N, P n. Definition other_induction := @@ -19,20 +19,20 @@ forall P : N -> Prop, Theorem other_ind_implies_ind : other_induction -> induction. Proof. -unfold induction, other_induction; intros OI P P_wd Base Step. -apply OI; unfold pred_wd in P_wd. -intros; now apply -> (P_wd 0). -intros n Pn m EmSn; now apply -> (P_wd (S n)); [apply Step|]. +unfold induction, other_induction; intros OI P predicate_wd Base Step. +apply OI; unfold predicate_wd in predicate_wd. +intros; now apply -> (predicate_wd 0). +intros n Pn m EmSn; now apply -> (predicate_wd (S n)); [apply Step|]. Qed. Theorem ind_implies_other_ind : induction -> other_induction. Proof. intros I P Base Step. -set (Q := fun n => forall m, m == n -> P m). -cut (forall n, Q n). -unfold Q; intros H n; now apply (H n). +set (A := fun n => forall m, m == n -> P m). +cut (forall n, A n). +unfold A; intros H n; now apply (H n). apply I. -unfold pred_wd, Q. intros x y Exy. +unfold predicate_wd, A. intros x y Exy. split; intros H m Em; apply H; [now rewrite Exy | now rewrite <- Exy]. exact Base. intros n Qn m EmSn; now apply Step with (n := n); [apply Qn |]. @@ -42,14 +42,14 @@ Qed. other_induction and we proved the base case and the induction step, we can in fact show that the predicate in question is well-defined, and therefore we can turn this other induction into the standard one. *) -Theorem other_ind_implies_pred_wd : +Theorem other_ind_implies_predicate_wd : other_induction -> forall P : N -> Prop, (forall n : N, n == 0 -> P n) -> (forall n : N, P n -> forall m : N, m == S n -> P m) -> - pred_wd E P. + predicate_wd E P. Proof. -intros OI P Base Step; unfold pred_wd. +intros OI P Base Step; unfold predicate_wd. intros x; pattern x; apply OI; clear x. (* Base case *) intros x H1 y H2. @@ -87,7 +87,7 @@ Axiom recursion_0 : forall (a : A) (f : N -> A -> A), EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. -Axiom recursion_S : +Axiom recursion_succ : forall (a : A) (f : N -> A -> A), EA a a -> fun2_wd E EA EA f -> forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). @@ -114,10 +114,10 @@ now apply EA_trans with (y := a'). intros x IH y H y' H1. rewrite H in H1; symmetry in H1. assert (EA (recursion a f y) (f x (recursion a f x))). -apply recursion_S. now apply EA_neighbor with (a' := a'). +apply recursion_succ. now apply EA_neighbor with (a' := a'). assumption. now symmetry. assert (EA (f' x (recursion a' f' x)) (recursion a' f' y')). -symmetry; apply recursion_S. now apply EA_neighbor with (a' := a). assumption. +symmetry; apply recursion_succ. now apply EA_neighbor with (a' := a). assumption. now symmetry. assert (EA (f x (recursion a f x)) (f' x (recursion a' f' x))). apply Eff'. reflexivity. apply IH. reflexivity. @@ -130,7 +130,7 @@ Axiom recursion_0' : forall (a : A) (f : N -> A -> A), forall x : N, x == 0 -> recursion a f x = a. -Axiom recursion_S' : +Axiom recursion_succ' : forall (a : A) (f : N -> A -> A), EA a a -> fun2_wd E EA EA f -> forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). @@ -147,10 +147,10 @@ intros x Ex0 x' Exx'. rewrite Ex0 in Exx'. symmetry in Exx'. replace (recursion a f x) with a. replace (recursion a' f' x') with a'. assumption. symmetry; now apply recursion_0'. symmetry; now apply recursion_0'. intros x IH y EySx y' Eyy'. rewrite EySx in Eyy'. symmetry in Eyy'. -apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_S'. +apply EA_trans with (y := (f x (recursion a f x))). now apply recursion_succ'. apply EA_trans with (y := (f' x (recursion a' f' x))). apply Eff'. reflexivity. now apply IH. -symmetry; now apply recursion_S'. +symmetry; now apply recursion_succ'. Qed. @@ -158,3 +158,10 @@ Qed. End Recursion. Implicit Arguments recursion [A]. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NPlus.v b/theories/Numbers/Natural/Axioms/NPlus.v index 3a7c19b62..5f5a88bca 100644 --- a/theories/Numbers/Natural/Axioms/NPlus.v +++ b/theories/Numbers/Natural/Axioms/NPlus.v @@ -1,208 +1,138 @@ -Require Export NAxioms. +Require Import NZPlus. +Require Export NBase. -Module Type NPlusSignature. -Declare Module Export NatModule : NatSignature. +Module Type NPlusSig. + +Declare Module Export NBaseMod : NBaseSig. Open Local Scope NatScope. -Parameter (*Inline*) plus : N -> N -> N. +Parameter Inline plus : N -> N -> N. Notation "x + y" := (plus x y) : NatScope. Add Morphism plus with signature E ==> E ==> E as plus_wd. -Axiom plus_0_l : forall n, 0 + n == n. -Axiom plus_S_l : forall n m, (S n) + m == S (n + m). +Axiom plus_0_l : forall n : N, 0 + n == n. +Axiom plus_succ_l : forall n m : N, (S n) + m == S (n + m). -End NPlusSignature. +End NPlusSig. -Module NPlusProperties - (NatMod : NatSignature) - (Import NPlusModule : NPlusSignature with Module NatModule := NatMod). -Module Export NatPropertiesModule := NatProperties NatModule. -Import NatMod. +Module NPlusPropFunct (Import NPlusMod : NPlusSig). +Module Export NBasePropMod := NBasePropFunct NBaseMod. Open Local Scope NatScope. -(* If H1 : t1 == u1 and H2 : t2 == u2 then "add_equations H1 H2 as H3" -adds the hypothesis H3 : t1 + t2 == u1 + u2 *) -Tactic Notation "add_equations" constr(H1) constr(H2) "as" ident(H3) := -match (type of H1) with -| ?t1 == ?u1 => match (type of H2) with - | ?t2 == ?u2 => pose proof (plus_wd t1 u1 H1 t2 u2 H2) as H3 - | _ => fail 2 ":" H2 "is not an equation" - end -| _ => fail 1 ":" H1 "is not an equation" -end. - -Theorem plus_0_r : forall n, n + 0 == n. -Proof. -induct n. -now rewrite plus_0_l. -intros x IH. -rewrite plus_S_l. -now rewrite IH. -Qed. +(*Theorem plus_wd : fun2_wd E E E plus. +Proof plus_wd. -Theorem plus_S_r : forall n m, n + S m == S (n + m). -Proof. -intros n m; generalize n; clear n. induct n. -now repeat rewrite plus_0_l. -intros x IH. -repeat rewrite plus_S_l; now rewrite IH. -Qed. +Theorem plus_0_l : forall n : N, 0 + n == n. +Proof plus_0_l. -Theorem plus_S_l : forall n m, S n + m == S (n + m). -Proof. -intros. -now rewrite plus_S_l. -Qed. +Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m). +Proof plus_succ_l.*) -Theorem plus_comm : forall n m, n + m == m + n. -Proof. -intros n m; generalize n; clear n. induct n. -rewrite plus_0_l; now rewrite plus_0_r. -intros x IH. -rewrite plus_S_l; rewrite plus_S_r; now rewrite IH. -Qed. +Module NZPlusMod <: NZPlusSig. -Theorem plus_assoc : forall n m p, n + (m + p) == (n + m) + p. -Proof. -intros n m p; generalize n; clear n. induct n. -now repeat rewrite plus_0_l. -intros x IH. -repeat rewrite plus_S_l; now rewrite IH. -Qed. +Module NZBaseMod <: NZBaseSig := NZBaseMod. -Theorem plus_shuffle1 : forall n m p q, (n + m) + (p + q) == (n + p) + (m + q). -Proof. -intros n m p q. -rewrite <- (plus_assoc n m (p + q)). rewrite (plus_comm m (p + q)). -rewrite <- (plus_assoc p q m). rewrite (plus_assoc n p (q + m)). -now rewrite (plus_comm q m). -Qed. +Definition NZplus := plus. -Theorem plus_shuffle2 : forall n m p q, (n + m) + (p + q) == (n + q) + (m + p). -Proof. -intros n m p q. -rewrite <- (plus_assoc n m (p + q)). rewrite (plus_assoc m p q). -rewrite (plus_comm (m + p) q). now rewrite <- (plus_assoc n q (m + p)). -Qed. +(* Axioms*) +Add Morphism NZplus with signature E ==> E ==> E as NZplus_wd. +Proof plus_wd. +Definition NZplus_0_l := plus_0_l. +Definition NZplus_succ_l := plus_succ_l. -Theorem plus_1_l : forall n, 1 + n == S n. -Proof. -intro n; rewrite plus_S_l; now rewrite plus_0_l. -Qed. +End NZPlusMod. -Theorem plus_1_r : forall n, n + 1 == S n. -Proof. -intro n; rewrite plus_comm; apply plus_1_l. -Qed. +Module Export NZPlusPropMod := NZPlusPropFunct NZPlusMod. -Theorem plus_cancel_l : forall n m p, p + n == p + m -> n == m. -Proof. -induct p. -do 2 rewrite plus_0_l; trivial. -intros p IH H. do 2 rewrite plus_S_l in H. apply S_inj in H. now apply IH. -Qed. +(** Theorems that are valid for both natural numbers and integers *) -Theorem plus_cancel_r : forall n m p, n + p == m + p -> n == m. -Proof. -intros n m p. -rewrite plus_comm. -set (k := p + n); rewrite plus_comm; unfold k. -apply plus_cancel_l. -Qed. +Theorem plus_0_r : forall n : N, n + 0 == n. +Proof NZplus_0_r. -Theorem plus_eq_0 : forall n m, n + m == 0 -> n == 0 /\ m == 0. -Proof. -intros n m; induct n. -rewrite plus_0_l; now split. -intros n IH H. rewrite plus_S_l in H. -absurd_hyp H; [|assumption]. unfold not; apply S_0. -Qed. +Theorem plus_succ_r : forall n m : N, n + S m == S (n + m). +Proof NZplus_succ_r. -Theorem plus_eq_S : - forall n m p, n + m == S p -> (exists n', n == S n') \/ (exists m', m == S m'). -Proof. -intros n m p; nondep_induct n. -intro H; rewrite plus_0_l in H; right; now exists p. -intros n _; left; now exists n. -Qed. +Theorem plus_comm : forall n m : N, n + m == m + n. +Proof NZplus_comm. -Theorem succ_plus_discr : forall n m, m # S (n + m). -Proof. -intro n; induct m. -intro H. apply S_0 with (n := (n + 0)). now apply (proj2 (proj2 E_equiv)). (* symmetry *) -intros m IH H. apply S_inj in H. rewrite plus_S_r in H. -unfold not in IH; now apply IH. -Qed. +Theorem plus_assoc : forall n m p : N, n + (m + p) == (n + m) + p. +Proof NZplus_assoc. -(* The following section is devoted to defining a function that, given -two numbers whose some equals 1, decides which number equals 1. The -main property of the function is also proved .*) - -(* First prove a theorem with ordinary disjunction *) -Theorem plus_eq_1 : - forall m n, m + n == 1 -> (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0). -induct m. -intros n H; rewrite plus_0_l in H; left; now split. -intros n IH m H; rewrite plus_S_l in H; apply S_inj in H; -apply plus_eq_0 in H; destruct H as [H1 H2]; -now right; split; [apply S_wd |]. -Qed. +Theorem plus_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q). +Proof NZplus_shuffle1. -Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m. +Theorem plus_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p). +Proof NZplus_shuffle2. -Theorem plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false). -Proof. -unfold fun2_wd; intros. unfold eq_bool. reflexivity. -Qed. +Theorem plus_1_l : forall n : N, 1 + n == S n. +Proof NZplus_1_l. + +Theorem plus_1_r : forall n : N, n + 1 == S n. +Proof NZplus_1_r. + +Theorem plus_cancel_l : forall n m p : N, p + n == p + m <-> n == m. +Proof NZplus_cancel_l. + +Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m. +Proof NZplus_cancel_r. + +(** Theorems that are valid for natural numbers but cannot be proved for NZ *) -Add Morphism plus_eq_1_dec with signature E ==> E ==> eq_bool as plus_eq_1_dec_wd. +Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. Proof. -unfold fun2_wd, plus_eq_1_dec. -intros x x' Exx' y y' Eyy'. -apply recursion_wd with (EA := eq_bool). -unfold eq_bool; reflexivity. -unfold eq_fun2; unfold eq_bool; reflexivity. -assumption. +intros n m; induct n. +(* The next command does not work with the axiom plus_0_l from NPlusSig *) +rewrite plus_0_l. intuition reflexivity. +intros n IH. rewrite plus_succ_l. +rewrite_false (S (n + m) == 0) succ_neq_0. +rewrite_false (S n == 0) succ_neq_0. tauto. Qed. -Theorem plus_eq_1_dec_0 : forall n, plus_eq_1_dec 0 n = true. +Theorem plus_eq_succ : + forall n m : N, (exists p : N, n + m == S p) <-> + (exists n' : N, n == S n') \/ (exists m' : N, m == S m'). Proof. -intro n. unfold plus_eq_1_dec. -now apply recursion_0. +intros n m; nondep_induct n. +split; intro H. +destruct H as [p H]. rewrite plus_0_l in H; right; now exists p. +destruct H as [[n' H] | [m' H]]. +symmetry in H; false_hyp H succ_neq_0. +exists m'; now rewrite plus_0_l. +intro n; split; intro H. +left; now exists n. +exists (n + m); now rewrite plus_succ_l. Qed. -Theorem plus_eq_1_dec_S : forall m n, plus_eq_1_dec (S n) m = false. +Theorem plus_eq_1 : forall n m : N, + n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1. Proof. -intros n m. unfold plus_eq_1_dec. -now rewrite (recursion_S eq_bool); -[| unfold eq_bool | apply plus_eq_1_dec_step_wd]. +intros n m H. +assert (H1 : exists p : N, n + m == S p) by now exists 0. +apply -> plus_eq_succ in H1. destruct H1 as [[n' H1] | [m' H1]]. +left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H. +apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split. +right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H. +apply -> plus_eq_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split. Qed. -Theorem plus_eq_1_dec_correct : - forall m n, m + n == 1 -> - (plus_eq_1_dec m n = true -> m == 0 /\ n == 1) /\ - (plus_eq_1_dec m n = false -> m == 1 /\ n == 0). +Theorem succ_plus_discr : forall n m : N, m ~= S (n + m). Proof. -intros m n; induct m. -intro H. rewrite plus_0_l in H. -rewrite plus_eq_1_dec_0. -split; [intros; now split | intro H1; discriminate H1]. -intros m _ H. rewrite plus_eq_1_dec_S. -split; [intro H1; discriminate | intros _ ]. -rewrite plus_S_l in H. apply S_inj in H. -apply plus_eq_0 in H; split; [apply S_wd | ]; tauto. +intro n; induct m. +apply neq_symm. apply succ_neq_0. +intros m IH H. apply succ_inj in H. rewrite plus_succ_r in H. +unfold not in IH; now apply IH. Qed. -(* One could define n <= m := exists p, p + n == m. Then we have +(* One could define n <= m as exists p : N, p + n == m. Then we have dichotomy: -forall n m, n <= m \/ m <= n, +forall n m : N, n <= m \/ m <= n, i.e., -forall n m, (exists p, p + n == m) \/ (exists p, p + m == n) (1) +forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1) We will need (1) in the proof of induction principle for integers constructed as pairs of natural numbers. The formula (1) can be proved @@ -213,17 +143,24 @@ for integers constructed from natural numbers we do not need to require implementations of order and minus; it is enough to prove (1) here. *) -Theorem plus_dichotomy : forall n m, (exists p, p + n == m) \/ (exists p, p + m == n). +Theorem plus_dichotomy : + forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n). Proof. intros n m; induct n. left; exists m; apply plus_0_r. intros n IH. -(* destruct IH as [p H | p H]. does not print a goal in ProofGeneral *) destruct IH as [[p H] | [p H]]. -destruct (O_or_S p) as [H1 | [p' H1]]; rewrite H1 in H. -rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_S_l; now rewrite plus_0_l. -left; exists p'; rewrite plus_S_r; now rewrite plus_S_l in H. -right; exists (S p). rewrite plus_S_l; now rewrite H. +destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H. +rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_succ_l; now rewrite plus_0_l. +left; exists p'; rewrite plus_succ_r; now rewrite plus_succ_l in H. +right; exists (S p). rewrite plus_succ_l; now rewrite H. Qed. -End NPlusProperties. +End NPlusPropFunct. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NPlusOrder.v b/theories/Numbers/Natural/Axioms/NPlusOrder.v index 4119e3c24..c3e8cb663 100644 --- a/theories/Numbers/Natural/Axioms/NPlusOrder.v +++ b/theories/Numbers/Natural/Axioms/NPlusOrder.v @@ -1,11 +1,13 @@ Require Export NPlus. Require Export NOrder. +Require Import NZPlusOrder. -Module NPlusOrderProperties (Import NPlusModule : NPlusSignature) - (Import NOrderModule : NOrderSignature with - Module NatModule := NPlusModule.NatModule). -Module Export NPlusPropertiesModule := NPlusProperties NatModule NPlusModule. -Module Export NOrderPropertiesModule := NOrderProperties NOrderModule. +Module NPlusOrderPropFunct + (Import NPlusMod : NPlusSig) + (Import NOrderMod : NOrderSig with Module NBaseMod := NPlusMod.NBaseMod). +Module Export NPlusPropMod := NPlusPropFunct NPlusMod. +Module Export NOrderPropMod := NOrderPropFunct NOrderMod. +Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod. Open Local Scope NatScope. (* Print All locks up here !!! *) @@ -14,14 +16,14 @@ Proof. intros n m p; induct p. now rewrite plus_0_r. intros x IH H. -rewrite plus_S_r. apply lt_closed_S. apply IH; apply H. +rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H. Qed. Theorem 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_l; assumption. -intros x IH. do 2 rewrite plus_S_l. now apply <- lt_resp_S. +intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ. Qed. Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. @@ -43,7 +45,7 @@ Proof. intros p n m; induct p. now do 2 rewrite plus_0_l. intros p IH. -do 2 rewrite plus_S_l. now rewrite lt_resp_S. +do 2 rewrite plus_succ_l. now rewrite lt_resp_succ. Qed. Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m. @@ -72,11 +74,20 @@ rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1. now rewrite plus_comm in H1. Qed. -Theorem plus_gt_S : - forall n m p, n + m > S p -> (exists n', n == S n') \/ (exists m', m == S m'). +Theorem plus_gt_succ : + forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m'). Proof. -intros n m p H. apply lt_exists_pred in H. destruct H as [q H]. -now apply plus_eq_S in H. +intros n m p H. +apply <- lt_le_succ in H. +apply lt_exists_pred in H. destruct H as [q H]. +now apply plus_eq_succ in H. Qed. End NPlusOrderProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NPred.v b/theories/Numbers/Natural/Axioms/NPred.v index d3da22660..711d6b883 100644 --- a/theories/Numbers/Natural/Axioms/NPred.v +++ b/theories/Numbers/Natural/Axioms/NPred.v @@ -4,42 +4,49 @@ Require Export NAxioms. 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 +NBasePropFunct functor, we would not be able to use it in other signatures. *) Module Type NPredSignature. -Declare Module Export NatModule : NatSignature. +Declare Module Export NBaseMod : NBaseSig. Open Local Scope NatScope. Parameter Inline P : N -> N. -Add Morphism P with signature E ==> E as P_wd. +Add Morphism P with signature E ==> E as pred_wd. -Axiom P_0 : P 0 == 0. -Axiom P_S : forall n, P (S n) == n. +Axiom pred_0 : P 0 == 0. +Axiom pred_succ : forall n, P (S n) == n. End NPredSignature. -Module NDefPred (Import NM : NatSignature) <: NPredSignature. -Module NatModule := NM. +Module NDefPred (Import NM : NBaseSig) <: NPredSignature. +Module NBaseMod := 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. +Add Morphism P with signature E ==> E as pred_wd. Proof. intros; unfold P. now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |]. Qed. -Theorem P_0 : P 0 == 0. +Theorem pred_0 : P 0 == 0. Proof. unfold P; now rewrite recursion_0. Qed. -Theorem P_S : forall n, P (S n) == n. +Theorem pred_succ : forall n, P (S n) == n. Proof. -intro n; unfold P; now rewrite (recursion_S E); [| unfold fun2_wd; now intros |]. +intro n; unfold P; now rewrite (recursion_succ E); [| unfold fun2_wd; now intros |]. Qed. End NDefPred. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NRec.v b/theories/Numbers/Natural/Axioms/NRec.v new file mode 100644 index 000000000..d74660c4a --- /dev/null +++ b/theories/Numbers/Natural/Axioms/NRec.v @@ -0,0 +1,259 @@ +Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A. + +Implicit Arguments recursion [A]. + +(* Suppose the codomain A has a setoid equality relation EA. If A is a +function space C -> D, it makes sense to consider extensional +functional equality as EA. Indeed, suppose, for example, that we say +[Definition g (x : N) : C -> D := (recursion ... x ...)]. We would +like to show that the function g of two arguments is well-defined. +This requirement is the same as the requirement that the functions of +one argument (g x) and (g x') are extensionally equal whenever x == +x', i.e., + +forall x x' : N, x == x' -> eq_fun (g x) (g x'), + +which is the same as + +forall x x' : N, x == x' -> forall y y' : C, EC y y' -> ED (g x y) (g x' y') + +where EC and ED are setoid equalities on C and D, respectively. + +Now, if we consider EA to be extensional equality on the function +space, we cannot require that EA is reflexive. Indeed, reflexivity of +EA: + +forall f : C -> D, eq_fun f f + +or + +forall f : C -> D, forall x x', EC x x' -> ED (f x) (f x') + +means that every function f ; C -> D is well-defined, which is in +general false. We can expect that EA is symmetric and transitive, +i.e., that EA is a partial equivalence relation (PER). However, there +seems to be no need to require this in the following axioms. + +When we defined a function by recursion, the arguments of this +function may occur in the recursion's base case a, the counter x, or +the step function f. For example, in the following definition: + +Definition plus (x y : N) := recursion y (fun _ p => S p) x. + +one argument becomes the base case and the other becomes the counter. + +In the definitions of times: + +Definition times (x y : N) := recursion 0 (fun x p => plus y p) x. + +the argument y occurs in the step function. Thus it makes sense to +formulate an axiom saying that (recursion a f x) is equal to +(recursion a' f' x') whenever (EA a a'), x == x', and eq_fun2 f f'. We +need to vary all three arguments; for example, claiming that +(recursion a f x) equals (recursion a' f x') with the same f whenever +(EA a a') and x == x' is not enough to prove well-defidedness of +multiplication defined above. + +This leads to the axioms given below. There is a question if it is +possible to formulate simpler axioms that would imply this statement +for any implementation. Indeed, the proof seems to have to proceed by +straighforward induction on x. The difficulty is that we cannot prove +(EA (recursion a f x) (recursion a' f' x')) using the induction axioms +above because recursion is not declared to be a setoid morphism: +that's what we are proving! Therefore, this has to be proved by +induction inside each particular implementation. *) + +Axiom recursion_wd : forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x == x' -> + EA (recursion a f x) (recursion a' f' x'). + +(* Can we instead declare recursion as a morphism? It does not seem +so. For this, we need to register the relation EA, and for this we +need to declare it as a variable in a section. But information about +morhisms is lost when sections are closed. *) + +(* When the function recursion is polymorphic on the codomain A, there +seems no other option than to return the given base case a when the +counter is 0. Therefore, we can formulate the following axioms with +Leibniz equality. *) + +Axiom recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. + +Axiom recursion_succ : + forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). + +(* It may be possible to formulate recursion_0 and recursion_succ as follows: +Axiom recursion_0 : + forall (a : A) (f : N -> A -> A), + EA a a -> forall x : N, x == 0 -> EA (recursion a f x) a. + +Axiom recursion_succ : + forall (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n m : N, n == S m -> EA (recursion a f n) (f m (recursion a f m)). + +Then it is possible to prove recursion_wd (see IotherInd.v). This +raises some questions: + +(1) Can the axioms recursion_wd, recursion_0 and recursion_succ (both +variants) proved for all reasonable implementations? + +(2) Can these axioms be proved without assuming that EA is symmetric +and transitive? In OtherInd.v, recursion_wd can be proved from +recursion_0 and recursion_succ by assuming symmetry and transitivity. + +(2) Which variant requires proving less for each implementation? Can +it be that proving all three axioms about recursion has some common +parts which have to be repeated? *) + +Implicit Arguments recursion_wd [A]. +Implicit Arguments recursion_0 [A]. +Implicit Arguments recursion_succ [A]. + +Definition if_zero (A : Set) (a b : A) (n : N) : A := + recursion a (fun _ _ => b) n. + +Add Morphism if_zero with signature LE_succet ==> LE_succet ==> E ==> LE_succet as if_zero_wd. +Proof. +unfold LE_succet. +intros; unfold if_zero; now apply recursion_wd with (EA := (@eq A)); +[| unfold eq_fun2; now intros |]. +Qed. + +Theorem if_zero_0 : forall (A : Set) (a b : A), if_zero A a b 0 = a. +Proof. +unfold if_zero; intros; now rewrite recursion_0. +Qed. + +Theorem if_zero_succ : forall (A : Set) (a b : A) (n : N), if_zero A a b (S n) = b. +Proof. +intros; unfold if_zero. +now rewrite (recursion_succ (@eq A)); [| | unfold fun2_wd; now intros]. +Qed. + +Implicit Arguments if_zero [A]. + +(* To prove this statement, we need to provably different terms, +e.g., true and false *) +Theorem succ_0 : forall n, ~ S n == 0. +Proof. +intros n H. +assert (true = false); [| discriminate]. +replace true with (if_zero false true (S n)) by apply if_zero_succ. +pattern false at 2; replace false with (if_zero false true 0) by apply if_zero_0. +change (LE_succet bool (if_zero false true (S n)) (if_zero false true 0)). +rewrite H. unfold LE_succet. reflexivity. +Qed. + +Theorem succ_inj : forall m n, S m == S n -> m == n. +Proof. +intros m n H. +setoid_replace m with (A (S m)) by (symmetry; apply pred_succ). +setoid_replace n with (A (S n)) by (symmetry; apply pred_succ). +now apply pred_wd. +Qed. + +(* The following section is devoted to defining a function that, given +two numbers whose some equals 1, decides which number equals 1. The +main property of the function is also proved .*) + +(* First prove a theorem with ordinary disjunction *) +Theorem plus_eq_1 : + forall m n : N, m + n == 1 -> (m == 0 /\ n == 1) \/ (m == 1 /\ n == 0). +induct m. +intros n H; rewrite plus_0_l in H; left; now split. +intros n IH m H; rewrite plus_succ_l in H; apply succ_inj in H; +apply plus_eq_0 in H; destruct H as [H1 H2]; +now right; split; [apply succ_wd |]. +Qed. + +Definition plus_eq_1_dec (m n : N) : bool := recursion true (fun _ _ => false) m. + +Theorem plus_eq_1_dec_step_wd : fun2_wd E eq_bool eq_bool (fun _ _ => false). +Proof. +unfold fun2_wd; intros. unfold eq_bool. reflexivity. +Qed. + +Add Morphism plus_eq_1_dec with signature E ==> E ==> eq_bool as plus_eq_1_dec_wd. +Proof. +unfold fun2_wd, plus_eq_1_dec. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +unfold eq_bool; reflexivity. +unfold eq_fun2; unfold eq_bool; reflexivity. +assumption. +Qed. + +Theorem plus_eq_1_dec_0 : forall n : N, plus_eq_1_dec 0 n = true. +Proof. +intro n. unfold plus_eq_1_dec. +now apply recursion_0. +Qed. + +Theorem plus_eq_1_dec_succ : forall m n : N, plus_eq_1_dec (S n) m = false. +Proof. +intros n m. unfold plus_eq_1_dec. +now rewrite (recursion_succ eq_bool); +[| unfold eq_bool | apply plus_eq_1_dec_step_wd]. +Qed. + +Theorem plus_eq_1_dec_correct : + forall m n : N, m + n == 1 -> + (plus_eq_1_dec m n = true -> m == 0 /\ n == 1) /\ + (plus_eq_1_dec m n = false -> m == 1 /\ n == 0). +Proof. +intros m n; induct m. +intro H. rewrite plus_0_l in H. +rewrite plus_eq_1_dec_0. +split; [intros; now split | intro H1; discriminate H1]. +intros m _ H. rewrite plus_eq_1_dec_succ. +split; [intro H1; discriminate | intros _ ]. +rewrite plus_succ_l in H. apply succ_inj in H. +apply plus_eq_0 in H; split; [apply succ_wd | ]; tauto. +Qed. + +Definition times_eq_0_dec (n m : N) : bool := + recursion true (fun _ _ => recursion false (fun _ _ => false) m) n. + +Lemma times_eq_0_dec_wd_step : + forall y y', y == y' -> + eq_bool (recursion false (fun _ _ => false) y) + (recursion false (fun _ _ => false) y'). +Proof. +intros y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +now unfold eq_bool. +unfold eq_fun2. intros. now unfold eq_bool. +assumption. +Qed. + +Add Morphism times_eq_0_dec with signature E ==> E ==> eq_bool +as times_eq_0_dec_wd. +unfold fun2_wd, times_eq_0_dec. +intros x x' Exx' y y' Eyy'. +apply recursion_wd with (EA := eq_bool). +now unfold eq_bool. +unfold eq_fun2; intros. now apply times_eq_0_dec_wd_step. +assumption. +Qed. + +Theorem times_eq_0_dec_correct : + forall n m, n * m == 0 -> + (times_eq_0_dec n m = true -> n == 0) /\ + (times_eq_0_dec n m = false -> m == 0). +Proof. +nondep_induct n; nondep_induct m; unfold times_eq_0_dec. +rewrite recursion_0; split; now intros. +intro n; rewrite recursion_0; split; now intros. +intro; rewrite recursion_0; rewrite (recursion_succ eq_bool); +[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros]. +intro m; rewrite (recursion_succ eq_bool). +rewrite times_succ_l. rewrite plus_succ_r. intro H; now apply succ_0 in H. +now unfold eq_bool. +unfold fun2_wd; intros; now unfold eq_bool. +Qed. diff --git a/theories/Numbers/Natural/Axioms/NStrongRec.v b/theories/Numbers/Natural/Axioms/NStrongRec.v index 5c9a65781..c35a6693b 100644 --- a/theories/Numbers/Natural/Axioms/NStrongRec.v +++ b/theories/Numbers/Natural/Axioms/NStrongRec.v @@ -1,7 +1,7 @@ Require Export NAxioms. -Module StrongRecProperties (Import NatModule : NatSignature). -Module Export NatPropertiesModule := NatProperties NatModule. +Module StrongRecProperties (Import NBaseMod : NBaseSig). +Module Export NBasePropMod := NBasePropFunct NBaseMod. Open Local Scope NatScope. Section StrongRecursion. @@ -66,3 +66,10 @@ End StrongRecursion. Implicit Arguments strong_rec [A]. End StrongRecProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NTimes.v b/theories/Numbers/Natural/Axioms/NTimes.v index 1d1644891..94bd8d26e 100644 --- a/theories/Numbers/Natural/Axioms/NTimes.v +++ b/theories/Numbers/Natural/Axioms/NTimes.v @@ -1,10 +1,11 @@ Require Export Ring. -(* Since we define a ring here, it should be possible to call the tactic +(* Since we define a ring below, it should be possible to call the tactic ring in the modules that use this module. Hence Export, not Import. *) Require Export NPlus. +Require Import NZTimes. -Module Type NTimesSignature. -Declare Module Export NPlusModule : NPlusSignature. +Module Type NTimesSig. +Declare Module Export NPlusMod : NPlusSig. Open Local Scope NatScope. Parameter Inline times : N -> N -> N. @@ -14,7 +15,7 @@ Notation "x * y" := (times x y) : NatScope. Add Morphism times with signature E ==> E ==> E as times_wd. Axiom times_0_r : forall n, n * 0 == 0. -Axiom times_S_r : forall n m, n * (S m) == n * m + n. +Axiom times_succ_r : forall n m, n * (S m) == n * m + n. (* Here recursion is done on the second argument to conform to the usual definition of ordinal multiplication in set theory, which is not @@ -29,71 +30,63 @@ 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 NTimesSignature. +End NTimesSig. -Module NTimesProperties (Import NTimesModule : NTimesSignature). -Module Export NPlusPropertiesModule := NPlusProperties NPlusModule.NatModule NPlusModule. +Module NTimesPropFunct (Import NTimesMod : NTimesSig). +Module Export NPlusPropMod := NPlusPropFunct NPlusMod. Open Local Scope NatScope. -Theorem times_0_l : forall n, 0 * n == 0. -Proof. -induct n. -now rewrite times_0_r. -intros x IH. -rewrite times_S_r. now rewrite plus_0_r. -Qed. +(*Theorem times_wd : fun2_wd E E E times. +Proof times_wd. -Theorem times_S_l : forall n m, (S n) * m == n * m + m. -Proof. -intros n m; induct m. -do 2 rewrite times_0_r; now rewrite plus_0_l. -intros m IH. do 2 rewrite times_S_r. rewrite IH. -do 2 rewrite <- plus_assoc. repeat rewrite plus_S_r. -now setoid_replace (m + n) with (n + m); [| apply plus_comm]. -Qed. +Theorem times_0_r : forall n, n * 0 == 0. +Proof times_0_r. -Theorem times_comm : forall n m, n * m == m * n. -Proof. -intros n m. induct n. -rewrite times_0_l; now rewrite times_0_r. -intros n IH. rewrite times_S_l; rewrite times_S_r. now rewrite IH. -Qed. +Theorem times_succ_r : forall n m, n * (S m) == n * m + n. +Proof times_succ_r.*) -Theorem times_plus_distr_r : forall n m p, (n + m) * p == n * p + m * p. -Proof. -intros n m p; induct n. -rewrite times_0_l. now do 2 rewrite plus_0_l. -intros n IH. rewrite plus_S_l. do 2 rewrite times_S_l. rewrite IH. -do 2 rewrite <- plus_assoc. apply plus_wd. reflexivity. apply plus_comm. -Qed. +Module NZTimesMod <: NZTimesSig. +Module NZPlusMod <: NZPlusSig := NZPlusMod. +Definition NZtimes := times. -Theorem times_plus_distr_l : forall n m p, n * (m + p) == n * m + n * p. -Proof. -intros n m p. -setoid_replace (n * (m + p)) with ((m + p) * n); [| apply times_comm]. -rewrite times_plus_distr_r. -setoid_replace (n * m) with (m * n); [| apply times_comm]. -now setoid_replace (n * p) with (p * n); [| apply times_comm]. -Qed. +(* Axioms *) -Theorem times_assoc : forall n m p, n * (m * p) == (n * m) * p. -Proof. -intros n m p; induct n. -now repeat rewrite times_0_l. -intros n IH. do 2 rewrite times_S_l. rewrite IH. now rewrite times_plus_distr_r. -Qed. +Add Morphism NZtimes with signature E ==> E ==> E as NZtimes_wd. +Proof times_wd. +Definition NZtimes_0_r := times_0_r. +Definition NZtimes_succ_r := times_succ_r. -Theorem times_1_l : forall n, 1 * n == n. -Proof. -intro n. rewrite times_S_l; rewrite times_0_l. now rewrite plus_0_l. -Qed. +End NZTimesMod. -Theorem times_1_r : forall n, n * 1 == n. -Proof. -intro n; rewrite times_comm; apply times_1_l. -Qed. +Module Export NZTimesPropMod := NZTimesPropFunct NZTimesMod. + +(** Theorems that are valid for both natural numbers and integers *) + +Theorem times_0_l : forall n : N, 0 * n == 0. +Proof NZtimes_0_l. + +Theorem times_succ_l : forall n m : N, (S n) * m == n * m + m. +Proof NZtimes_succ_l. -Lemma semi_ring : semi_ring_theory 0 (S 0) plus times E. +Theorem times_comm : forall n m : N, n * m == m * n. +Proof NZtimes_comm. + +Theorem times_plus_distr_r : forall n m p : N, (n + m) * p == n * p + m * p. +Proof NZtimes_plus_distr_r. + +Theorem times_plus_distr_l : forall n m p : N, n * (m + p) == n * m + n * p. +Proof NZtimes_plus_distr_l. + +Theorem times_assoc : forall n m p : N, n * (m * p) == (n * m) * p. +Proof NZtimes_assoc. + +Theorem times_1_l : forall n : N, 1 * n == n. +Proof NZtimes_1_l. + +Theorem times_1_r : forall n : N, n * 1 == n. +Proof NZtimes_1_r. + +Lemma semi_ring : semi_ring_theory 0 1 plus times E. Proof. constructor. exact plus_0_l. @@ -108,66 +101,28 @@ Qed. Add Ring SR : semi_ring. +(** Theorems that cannot be proved in NZTimes *) + Theorem times_eq_0 : forall n m, n * m == 0 -> n == 0 \/ m == 0. Proof. induct n; induct m. intros; now left. intros; now left. intros; now right. -intros m IH H1. rewrite times_S_l in H1. rewrite plus_S_r in H1. now apply S_0 in H1. -Qed. - -Definition times_eq_0_dec (n m : N) : bool := - recursion true (fun _ _ => recursion false (fun _ _ => false) m) n. - -Lemma times_eq_0_dec_wd_step : - forall y y', y == y' -> - eq_bool (recursion false (fun _ _ => false) y) - (recursion false (fun _ _ => false) y'). -Proof. -intros y y' Eyy'. -apply recursion_wd with (EA := eq_bool). -now unfold eq_bool. -unfold eq_fun2. intros. now unfold eq_bool. -assumption. -Qed. - -Add Morphism times_eq_0_dec with signature E ==> E ==> eq_bool -as times_eq_0_dec_wd. -unfold fun2_wd, times_eq_0_dec. -intros x x' Exx' y y' Eyy'. -apply recursion_wd with (EA := eq_bool). -now unfold eq_bool. -unfold eq_fun2; intros. now apply times_eq_0_dec_wd_step. -assumption. -Qed. - -Theorem times_eq_0_dec_correct : - forall n m, n * m == 0 -> - (times_eq_0_dec n m = true -> n == 0) /\ - (times_eq_0_dec n m = false -> m == 0). -Proof. -nondep_induct n; nondep_induct m; unfold times_eq_0_dec. -rewrite recursion_0; split; now intros. -intro n; rewrite recursion_0; split; now intros. -intro; rewrite recursion_0; rewrite (recursion_S eq_bool); -[split; now intros | now unfold eq_bool | unfold fun2_wd; unfold eq_bool; now intros]. -intro m; rewrite (recursion_S eq_bool). -rewrite times_S_l. rewrite plus_S_r. intro H; now apply S_0 in H. -now unfold eq_bool. -unfold fun2_wd; intros; now unfold eq_bool. +intros m IH H1. rewrite times_succ_l in H1. +rewrite plus_succ_r in H1. now apply succ_neq_0 in H1. Qed. Theorem times_eq_1 : forall n m, n * m == 1 -> n == 1 /\ m == 1. Proof. -nondep_induct n; nondep_induct m. -intro H; rewrite times_0_l in H; symmetry in H; now apply S_0 in H. -intros n H; rewrite times_0_l in H; symmetry in H; now apply S_0 in H. -intro H; rewrite times_0_r in H; symmetry in H; now apply S_0 in H. -intros m H; rewrite times_S_l in H; rewrite plus_S_r in H; -apply S_inj in H; rewrite times_comm in H; rewrite times_S_l in H; -apply plus_eq_0 in H; destruct H as [H1 H2]. -apply plus_eq_0 in H1; destruct H1 as [_ H3]; rewrite H2; rewrite H3; now split. +intros n m; induct n. +intro H; rewrite times_0_l in H; symmetry in H; false_hyp H succ_neq_0. +intros n IH H. rewrite times_succ_l in H. apply plus_eq_1 in H. +destruct H as [[H1 H2] | [H1 H2]]. +apply IH in H1. destruct H1 as [_ H1]. rewrite H1 in H2; false_hyp H2 succ_neq_0. +apply times_eq_0 in H1. destruct H1 as [H1 | H1]. +rewrite H1; now split. +rewrite H2 in H1; false_hyp H1 succ_neq_0. Qed. (* In proving the correctness of the definition of multiplication on @@ -194,11 +149,18 @@ do 2 rewrite times_plus_distr_l in H2. symmetry in H2; add_equations H1 H2 as H3. stepl (a * n + (u + a * n' + a * m)) in H3 by ring. stepr (a * n + (a * m + v + a * m')) in H3 by ring. -apply plus_cancel_l in H3. +apply -> plus_cancel_l in H3. stepl (a * m + (u + a * n')) in H3 by ring. stepr (a * m + (v + a * m')) in H3 by ring. -apply plus_cancel_l in H3. +apply -> plus_cancel_l in H3. stepl (u + a * n') by ring. now stepr (v + a * m') by ring. Qed. -End NTimesProperties. +End NTimesPropFunct. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Axioms/NTimesOrder.v b/theories/Numbers/Natural/Axioms/NTimesOrder.v index ea189c60f..3e7c3f2b2 100644 --- a/theories/Numbers/Natural/Axioms/NTimesOrder.v +++ b/theories/Numbers/Natural/Axioms/NTimesOrder.v @@ -1,30 +1,30 @@ Require Export NTimes. Require Export NPlusOrder. -Module NTimesOrderProperties (Import NTimesModule : NTimesSignature) - (Import NOrderModule : NOrderSignature with - Module NatModule := NTimesModule.NPlusModule.NatModule). -Module Export NTimesPropertiesModule := NTimesProperties NTimesModule. +Module NTimesOrderProperties (Import NTimesMod : NTimesSig) + (Import NOrderModule : NOrderSig with + Module NBaseMod := NTimesMod.NPlusMod.NBaseMod). +Module Export NTimesPropertiesModule := NTimesPropFunct NTimesMod. Module Export NPlusOrderPropertiesModule := - NPlusOrderProperties NTimesModule.NPlusModule NOrderModule. + NPlusOrderProperties NTimesMod.NPlusMod NOrderModule. Open Local Scope NatScope. -Lemma times_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. +Lemma times_succ_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. Proof. intros n m p; induct n. now do 2 rewrite times_1_l. intros x IH H. -rewrite times_S_l. -set (k := S x * m); rewrite times_S_l; unfold k; clear k. +rewrite times_succ_l. +set (k := S x * m); rewrite times_succ_l; unfold k; clear k. apply plus_lt_compat; [apply IH; assumption | assumption]. Qed. -Lemma times_S_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n). +Lemma times_succ_lt_compat_r : forall n m p, m < p -> m * (S n) < p * (S n). Proof. intros n m p H. set (k := (p * (S n))); rewrite times_comm; unfold k; clear k. set (k := ((S n) * m)); rewrite times_comm; unfold k; clear k. -now apply times_S_lt_compat_l. +now apply times_succ_lt_compat_l. Qed. Lemma times_lt_compat_l : forall m n p, n < m -> 0 < p -> p * n < p * m. @@ -32,7 +32,7 @@ Proof. intros n m p H1 H2. apply (lt_exists_pred p) in H2. destruct H2 as [q H]. repeat rewrite H. -now apply times_S_lt_compat_l. +now apply times_succ_lt_compat_l. Qed. Lemma times_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. @@ -40,7 +40,7 @@ Proof. intros n m p H1 H2. apply (lt_exists_pred p) in H2. destruct H2 as [q H]. repeat rewrite H. -now apply times_S_lt_compat_r. +now apply times_succ_lt_compat_r. Qed. Lemma times_positive : forall n m, 0 < n -> 0 < m -> 0 < n * m. @@ -56,8 +56,15 @@ intros; rewrite times_0_l; apply times_positive; [assumption | apply lt_positive with (n := p); assumption]. intros x IH H1 H2. apply lt_trans with (m := ((S x) * q)). -now apply times_S_lt_compat_l; assumption. +now apply times_succ_lt_compat_l; assumption. now apply times_lt_compat_r; [| apply lt_positive with (n := p)]. Qed. End NTimesOrderProperties. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 956c8b28c..46973db7f 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -34,22 +34,22 @@ as E_rel. End NBinaryDomain. -Module BinaryNat <: NatSignature. +Module BinaryNat <: NBaseSig. Module Export NDomainModule := NBinaryDomain. Definition O := N0. Definition S := Nsucc. -Add Morphism S with signature E ==> E as S_wd. +Add Morphism S with signature E ==> E as succ_wd. Proof. congruence. Qed. Theorem induction : - forall P : N -> Prop, pred_wd E P -> + forall P : N -> Prop, predicate_wd E P -> P 0 -> (forall n, P n -> P (S n)) -> forall n, P n. Proof. -intros P P_wd; apply Nind. +intros P predicate_wd; apply Nind. Qed. Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) := @@ -79,7 +79,7 @@ Proof. intros A a f; unfold recursion; unfold Nrec; now rewrite Nrect_base. Qed. -Theorem recursion_S : +Theorem recursion_succ : forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), EA a a -> fun2_wd E EA EA f -> forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). @@ -94,7 +94,7 @@ End BinaryNat. Module NBinaryDepRec <: NDepRecSignature. Module Export NDomainModule := NBinaryDomain. -Module Export NatModule := BinaryNat. +Module Export NBaseMod := BinaryNat. Definition dep_recursion := Nrec. @@ -105,7 +105,7 @@ Proof. intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base. Qed. -Theorem dep_recursion_S : +Theorem dep_recursion_succ : 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). Proof. @@ -114,8 +114,8 @@ Qed. End NBinaryDepRec. -Module NBinaryPlus <: NPlusSignature. -Module Export NatModule := BinaryNat. +Module NBinaryPlus <: NPlusSig. +Module Export NBaseMod := BinaryNat. Definition plus := Nplus. @@ -129,15 +129,15 @@ Proof. exact Nplus_0_l. Qed. -Theorem plus_S_l : forall n m, (S n) + m = S (n + m). +Theorem plus_succ_l : forall n m, (S n) + m = S (n + m). Proof. exact Nplus_succ. Qed. End NBinaryPlus. -Module NBinaryTimes <: NTimesSignature. -Module Export NPlusModule := NBinaryPlus. +Module NBinaryTimes <: NTimesSig. +Module Export NPlusMod := NBinaryPlus. Definition times := Nmult. @@ -151,16 +151,16 @@ Proof. intro n; rewrite Nmult_comm; apply Nmult_0_l. Qed. -Theorem times_S_r : forall n m, n * (S m) = n * m + n. +Theorem times_succ_r : forall n m, n * (S m) = n * m + n. Proof. -intros n m; rewrite Nmult_comm; rewrite Nmult_Sn_m. +intros n m; rewrite Nmult_comm; rewrite Nmult_succn_m. rewrite Nplus_comm; now rewrite Nmult_comm. Qed. End NBinaryTimes. -Module NBinaryOrder <: NOrderSignature. -Module Export NatModule := BinaryNat. +Module NBinaryOrder <: NOrderSig. +Module Export NBaseMod := BinaryNat. Definition lt (m n : N) := comp_bool (Ncompare m n) Lt. Definition le (m n : N) := let c := (Ncompare m n) in orb (comp_bool c Lt) (comp_bool c Eq). @@ -188,14 +188,14 @@ Proof. unfold lt; destruct x as [|x]; simpl; now intro. Qed. -Theorem lt_S : forall x y, lt x (S y) <-> le x y. +Theorem lt_succ : forall x y, lt x (S y) <-> le x y. Proof. intros x y. rewrite le_lt. assert (H1 : lt x (S y) <-> Ncompare x (S y) = Lt); [unfold lt, comp_bool; destruct (x ?= S y); simpl; split; now intro |]. assert (H2 : lt x y <-> Ncompare x y = Lt); [unfold lt, comp_bool; destruct (x ?= y); simpl; split; now intro |]. -pose proof (Ncompare_n_Sm x y) as H. tauto. +pose proof (Ncompare_n_succm x y) as H. tauto. Qed. End NBinaryOrder. @@ -226,3 +226,10 @@ match n with end. *) (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index c1fc14a8a..0240f29b1 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -1,10 +1,10 @@ -Require Import Minus. +(*Require Import Minus.*) Require Export NPlus. -Require Export NDepRec. +(*Require Export NDepRec. Require Export NTimesOrder. Require Export NMinus. -Require Export NMiscFunct. +Require Export NMiscFunct.*) (* First we define the functions that will be suppled as implementations. The parameters in module types, to which these @@ -57,85 +57,69 @@ end. Delimit Scope NatScope with Nat. Open Scope NatScope. -(* Domain *) +Module NPeanoBaseMod <: NBaseSig. -Module Export NPeanoDomain <: NDomainEqSignature. +Theorem E_equiv : equiv nat (@eq nat). +Proof (eq_equiv nat). -Definition N := nat. -Definition E := (@eq nat). -Definition e := e. - -Theorem E_equiv_e : forall x y : N, E x y <-> e x y. +Theorem succ_wd : fun_wd (@eq nat) (@eq nat) S. Proof. -induction x; destruct y; simpl; try now split; intro. -rewrite <- IHx; split; intro H; [now injection H | now rewrite H]. +congruence. Qed. -Definition E_equiv : equiv N E := eq_equiv N. - -Add Relation N 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 NPeanoDomain. - -Module Export PeanoNat <: NatSignature. -Module (*Import*) NDomainModule := NPeanoDomain. - -Definition O := 0. -Definition S := S. +Theorem succ_inj : forall n1 n2 : nat, S n1 = S n2 -> n1 = n2. +Proof. +intros n1 n2 H; now simplify_eq H. +Qed. -Add Morphism S with signature E ==> E as S_wd. +Theorem succ_neq_0 : forall n : nat, S n <> 0. Proof. -congruence. +intros n H; simplify_eq H. Qed. Theorem induction : - forall P : nat -> Prop, pred_wd (@eq nat) P -> - P 0 -> (forall n, P n -> P (S n)) -> forall n, P n. + forall A : nat -> Prop, predicate_wd (@eq nat) A -> + A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n. Proof. -intros P W Base Step n; elim n; assumption. +intros; now apply nat_ind. Qed. -Definition recursion := fun A : Set => nat_rec (fun _ => A). -Implicit Arguments recursion [A]. +Definition N := nat. +Definition E := (@eq nat). +Definition O := 0. +Definition S := S. -Theorem recursion_wd : -forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> - forall x x' : N, x = x' -> - EA (recursion a f x) (recursion a' f' x'). +End NPeanoBaseMod. + +Module NPeanoPlusMod <: NPlusSig. +Module NBaseMod := NPeanoBaseMod. + +Theorem plus_wd : fun2_wd (@eq nat) (@eq nat) (@eq nat) plus. Proof. -unfold fun2_wd, E. -intros A EA a a' Eaa' f f' Eff'. -induction x as [| n IH]; intros x' H; rewrite <- H; simpl. -assumption. -apply Eff'; [reflexivity | now apply IH]. +congruence. Qed. -Theorem recursion_0 : - forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a. +Theorem plus_0_l : forall n, 0 + n = n. Proof. reflexivity. Qed. -Theorem recursion_S : -forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), - EA a a -> fun2_wd E EA EA f -> - forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). +Theorem plus_succ_l : forall n m, (S n) + m = S (n + m). Proof. -intros A EA a f EAaa f_wd. unfold fun2_wd, E in *. -induction n; simpl; now apply f_wd. +reflexivity. Qed. -End PeanoNat. +Definition plus := plus. + +End NPeanoPlusMod. + +Module Export NPeanoBasePropMod := NBasePropFunct NPeanoBaseMod. +Module Export NPeanoPlusPropMod := NPlusPropFunct NPeanoPlusMod. + Module Export NPeanoDepRec <: NDepRecSignature. Module Import NDomainModule := NPeanoDomain. -Module Import NatModule := PeanoNat. +Module Import NBaseMod := PeanoNat. Definition dep_recursion := nat_rec. @@ -146,7 +130,7 @@ Proof. reflexivity. Qed. -Theorem dep_recursion_S : +Theorem dep_recursion_succ : 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). Proof. @@ -155,8 +139,8 @@ Qed. End NPeanoDepRec. -Module Export NPeanoOrder <: NOrderSignature. -Module Import NatModule := PeanoNat. +Module Export NPeanoOrder <: NOrderSig. +Module Import NBaseMod := PeanoNat. Definition lt := lt. Definition le := le. @@ -189,7 +173,7 @@ Proof. destruct x as [|x]; simpl; now intro. Qed. -Lemma lt_S_bool : forall x y, lt x (S y) = le x y. +Lemma lt_succ_bool : forall x y, lt x (S y) = le x y. Proof. unfold lt, le; induction x as [| x IH]; destruct y as [| y]; simpl; try reflexivity. @@ -197,39 +181,15 @@ destruct x; now simpl. apply IH. Qed. -Theorem lt_S : forall x y, lt x (S y) <-> le x y. +Theorem lt_succ : forall x y, lt x (S y) <-> le x y. Proof. -intros; rewrite <- eq_true_iff; apply lt_S_bool. +intros; rewrite <- eq_true_iff; apply lt_succ_bool. Qed. End NPeanoOrder. -Module Export NPeanoPlus <: NPlusSignature. -Module (*Import*) NatModule := PeanoNat. - -Definition plus := plus. - -Notation "x + y" := (plus x y) : NatScope. - -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Proof. -unfold E; congruence. -Qed. - -Theorem plus_0_l : forall n, 0 + n = n. -Proof. -reflexivity. -Qed. - -Theorem plus_S_l : forall n m, (S n) + m = S (n + m). -Proof. -reflexivity. -Qed. - -End NPeanoPlus. - -Module Export NPeanoTimes <: NTimesSignature. -Module Import NPlusModule := NPeanoPlus. +Module Export NPeanoTimes <: NTimesSig. +Module Import NPlusMod := NPeanoPlus. Definition times := mult. @@ -243,7 +203,7 @@ Proof. auto. Qed. -Theorem times_S_r : forall n m, n * (S m) = n * m + n. +Theorem times_succ_r : forall n m, n * (S m) = n * m + n. Proof. auto. Qed. @@ -251,7 +211,7 @@ Qed. End NPeanoTimes. Module Export NPeanoPred <: NPredSignature. -Module Export NatModule := PeanoNat. +Module Export NBaseMod := PeanoNat. Definition P (n : nat) := match n with @@ -259,17 +219,17 @@ match n with | S n' => n' end. -Add Morphism P with signature E ==> E as P_wd. +Add Morphism P with signature E ==> E as pred_wd. Proof. unfold E; congruence. Qed. -Theorem P_0 : P 0 = 0. +Theorem pred_0 : P 0 = 0. Proof. reflexivity. Qed. -Theorem P_S : forall n, P (S n) = n. +Theorem pred_succ : forall n, P (S n) = n. Proof. now intro. Qed. @@ -291,7 +251,7 @@ Proof. now destruct n. Qed. -Theorem minus_S_r : forall n m, n - (S m) = P (n - m). +Theorem minus_succ_r : forall n m, n - (S m) = P (n - m). Proof. induction n as [| n IH]; simpl. now intro. @@ -311,6 +271,44 @@ Module Export NPeanoMinusProperties := Module MiscFunctModule := MiscFunctFunctor PeanoNat. (* The instruction above adds about 0.5M to the size of the .vo file !!! *) +Theorem E_equiv_e : forall x y : N, E x y <-> e x y. +Proof. +induction x; destruct y; simpl; try now split; intro. +rewrite <- IHx; split; intro H; [now injection H | now rewrite H]. +Qed. + +Definition recursion := fun A : Set => nat_rec (fun _ => A). +Implicit Arguments recursion [A]. + +Theorem recursion_wd : +forall (A : Set) (EA : relation A), + forall a a' : A, EA a a' -> + forall f f' : N -> A -> A, eq_fun2 E EA EA f f' -> + forall x x' : N, x = x' -> + EA (recursion a f x) (recursion a' f' x'). +Proof. +unfold fun2_wd, E. +intros A EA a a' Eaa' f f' Eff'. +induction x as [| n IH]; intros x' H; rewrite <- H; simpl. +assumption. +apply Eff'; [reflexivity | now apply IH]. +Qed. + +Theorem recursion_0 : + forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a. +Proof. +reflexivity. +Qed. + +Theorem recursion_succ : +forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), + EA a a -> fun2_wd E EA EA f -> + forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). +Proof. +intros A EA a f EAaa f_wd. unfold fun2_wd, E in *. +induction n; simpl; now apply f_wd. +Qed. + (*Lemma e_implies_E : forall n m, e n m = true -> n = m. Proof. intros n m H; rewrite <- eq_true_unfold_pos in H; @@ -320,3 +318,10 @@ Qed. Add Ring SR : semi_ring (decidable e_implies_E). Goal forall x y : nat, x + y = y + x. intros. ring.*) + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index c59690887..fd9e9aa8b 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -4,13 +4,12 @@ Require Export Bool. importing the current file wants to use. e.g., Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2, then it needs to know about bool and have a notation ||. *) - +Require Export QRewrite. (* Contents: - Coercion from bool to Prop - Extension of the tactics stepl and stepr -- An attempt to extend setoid rewrite to formulas with quantifiers - Extentional properties of predicates, relations and functions (well-definedness and equality) - Relations on cartesian product @@ -21,7 +20,8 @@ Contents: Definition eq_bool := (@eq bool). -Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. +(*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*) +(* This has been added to theories/Datatypes.v *) Coercion eq_true : bool >-> Sortclass. Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true. @@ -84,145 +84,13 @@ end. Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r]. -(** An attempt to extend setoid rewrite to formulas with quantifiers *) - -(* The following algorithm was explained to me by Bruno Barras. - -In the future, we need to prove that some predicates are -well-defined w.r.t. a setoid relation, i.e., we need to prove theorems -of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it -makes sense to do induction only on predicates that satisfy this -property. Ideally, such goal should be proved by saying "intros x y H; -rewrite H; reflexivity". - -Now, such predicates P may contain quantifiers besides setoid -morphisms. However, the tactic "rewrite" (which in this case stands -for "setoid_rewrite") currently cannot handle universal quantifiers as -well as lambda abstractions, which are part of the existential -quantifier notation (recall that "exists x, P" stands for "ex (fun x -=> p)"). - -Therefore, to prove that P x <-> P y, we proceed as follows. Suppose -that P x is C[forall z, Q[x,z]] where C is a context, i.e., a term -with a hole. We assume that the hole of C does not occur inside -another quantifier, i.e., that forall z, Q[x,z] is a top-level -quantifier in P. The notation Q[x,z] means that the term Q contains -free occurrences of variables x and z. We prove that forall z, Q[x,z] -<-> forall z, Q[y,z]. To do this, we show that forall z, Q[x,z] <-> -Q[y,z]. After performing "intro z", this goal is handled recursively, -until no more quantifiers are left in Q. - -After we obtain the goal - -H : x == y -H1 : forall z, Q[x,z] <-> forall z, Q[y,z] -================================= -C[forall z, Q[x,z]] <-> C[forall z, Q[y,z]] - -we say "rewrite H1". Repeating this for other quantifier subformulas -in P, we make them all identical in P x and P y. After that, saying -"rewrite H" solves the goal. - -To implement this algorithm, we need the following theorems: - -Theorem forall_morphism : - forall (A : Set) (P Q : A -> Prop), - (forall x : A, P x <-> Q x) -> ((forall x : A, P x) <-> (forall x : A, Q x)). - -Theorem exists_morphism : - forall (A : Set) (P Q : A -> Prop), - (forall x : A, P x <-> Q x) -> (ex P <-> ex Q) - -Below, we obtain them by registering the universal and existential -quantifiers as setoid morphisms, though they can be proved without any -reference to setoids. Ideally, registering quantifiers as morphisms -should take care of setoid rewriting in the presence of quantifiers, -but as described above, this is currently not so, and we have to -handle quantifiers manually. - -The job of deriving P x <-> P y from x == y is done by the tactic -qmorphism x y below. *) - -Section Quantifiers. - -Variable A : Set. - -Definition predicate := A -> Prop. - -Definition equiv_predicate : relation predicate := - fun (P1 P2 : predicate) => forall x : A, P1 x <-> P2 x. - -Theorem equiv_predicate_refl : reflexive predicate equiv_predicate. -Proof. -unfold reflexive, equiv_predicate. reflexivity. -Qed. - -Theorem equiv_predicate_symm : symmetric predicate equiv_predicate. -Proof. -firstorder. -Qed. - -Theorem equiv_predicate_trans : transitive predicate equiv_predicate. -Proof. -firstorder. -Qed. - -Add Relation predicate equiv_predicate - reflexivity proved by equiv_predicate_refl - symmetry proved by equiv_predicate_symm - transitivity proved by equiv_predicate_trans -as equiv_predicate_rel. - -Add Morphism (@ex A) - with signature equiv_predicate ==> iff - as exists_morphism. -Proof. -firstorder. -Qed. - -Add Morphism (fun P : predicate => forall x : A, P x) - with signature equiv_predicate ==> iff - as forall_morphism. -Proof. -firstorder. -Qed. - -End Quantifiers. - -(* replace x by y in t *) -Ltac repl x y t := -match t with -| context C [x] => let t' := (context C [y]) in repl x y t' -| _ => t -end. - -Ltac qmorphism x y := -lazymatch goal with -| |- ?P <-> ?P => reflexivity -| |- context [ex ?P] => - match P with - | context [x] => - let P' := repl x y P in - setoid_replace (ex P) with (ex P') using relation iff; - [qmorphism x y | - apply exists_morphism; unfold equiv_predicate; intros; qmorphism x y] - end -| |- context [forall z, @?P z] => - match P with - | context [x] => - let P' := repl x y P in - setoid_replace (forall z, P z) with (forall z, P' z) using relation iff; - [qmorphism x y | - apply forall_morphism; unfold equiv_predicate; intros; qmorphism x y] - end -| _ => setoid_replace x with y; [reflexivity | assumption] -end. - (** Extentional properties of predicates, relations and functions *) +Definition predicate (A : Type) := A -> Prop. + Section ExtensionalProperties. -Variables A B C : Set. +Variables A B C : Type. Variable EA : relation A. Variable EB : relation B. Variable EC : relation C. @@ -234,12 +102,6 @@ Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y). Definition fun2_wd (f : A -> B -> C) := forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y'). -Definition pred_wd (P : predicate A) := - forall x y, EA x y -> (P x <-> P y). - -Definition rel_wd (R : relation A) := - forall x x', EA x x' -> forall y y', EA y y' -> (R x y <-> R x' y'). - Definition eq_fun : relation (A -> B) := fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x'). @@ -256,8 +118,32 @@ Implicit Arguments fun_wd [A B]. Implicit Arguments fun2_wd [A B C]. Implicit Arguments eq_fun [A B]. Implicit Arguments eq_fun2 [A B C]. -Implicit Arguments pred_wd [A]. -Implicit Arguments rel_wd [A]. + +Definition predicate_wd (A : Type) (EA : relation A) := fun_wd EA iff. + +Definition rel_wd (A B : Type) (EA : relation A) (EB : relation B) := + fun2_wd EA EB iff. + +Implicit Arguments predicate_wd [A]. +Implicit Arguments rel_wd [A B]. + +Ltac solve_predicate_wd := +unfold predicate_wd; +let x := fresh "x" in +let y := fresh "y" in +let H := fresh "H" in + intros x y H; qiff x y H. + +(* The following tactic uses solve_predicate_wd to solve the goals +relating to well-defidedness that are produced by applying induction. +We declare it to take the tactic that applies the induction theorem +and not the induction theorem itself because the tactic may, for +example, supply additional arguments, as does NZinduct_center in +NZBase.v *) +Ltac induction_maker n t := + try intros until n; + pattern n; t; clear n; + [solve_predicate_wd | ..]. (** Relations on cartesian product. Used in MiscFunct for defining functions whose domain is a product of sets by primitive recursion *) @@ -307,6 +193,69 @@ Implicit Arguments prod_rel_equiv [A B]. (** Miscellaneous *) +Theorem neg_false : forall P : Prop, ~ P <-> (P <-> False). +Proof. +intro P; unfold not; split; intro H; [split; intro H1; +[apply H; assumption | elim H1] | apply (proj1 H)]. +Qed. + +(* This tactic replaces P in the goal with False. +The goal ~ P should be solvable by "apply H". *) +Ltac rewrite_false P H := +setoid_replace P with False using relation iff; +[| apply -> neg_false; apply H]. + +Tactic Notation "symmetry" constr(Eq) := +lazymatch Eq with +| ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff; + [| split; intro; symmetry; assumption] +| _ => fail Eq "does not have the form (E t1 t2)" +end. + +Theorem and_cancel_l : forall A B C : Prop, + (B -> A) -> (C -> A ) -> ((A /\ B <-> A /\ C) <-> (B <-> C)). +Proof. +intros; tauto. +Qed. + +Theorem and_cancel_r : forall A B C : Prop, + (B -> A) -> (C -> A ) -> ((B /\ A <-> C /\ A) <-> (B <-> C)). +Proof. +intros; tauto. +Qed. + +Theorem or_cancel_l : forall A B C : Prop, + (B -> ~A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)). +Proof. +intros; tauto. +Qed. + +Theorem or_cancel_r : forall A B C : Prop, + (B -> ~A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)). +Proof. +intros; tauto. +Qed. + +Theorem or_iff_compat_l : forall A B C : Prop, + (B <-> C) -> (A \/ B <-> A \/ C). +Proof. +intros; tauto. +Qed. + +Theorem or_iff_compat_r : forall A B C : Prop, + (B <-> C) -> (B \/ A <-> C \/ A). +Proof. +intros; tauto. +Qed. + +Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B). +Proof. +intros; tauto. +Qed. + +Declare Left Step iff_stepl. +Declare Right Step iff_trans. + Definition comp_bool (x y : comparison) : bool := match x, y with | Lt, Lt => true @@ -335,3 +284,9 @@ Add Relation (fun A : Set => A) LE_Set symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A)))) transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A)))) as EA_rel. + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/QRewrite.v b/theories/Numbers/QRewrite.v new file mode 100644 index 000000000..a781411a2 --- /dev/null +++ b/theories/Numbers/QRewrite.v @@ -0,0 +1,173 @@ +Require Import List. +Require Import Setoid. + +(** An attempt to extend setoid rewrite to formulas with quantifiers *) + +(* The following algorithm was explained to me by Bruno Barras. + +In the future, we need to prove that some predicates are +well-defined w.r.t. a setoid relation, i.e., we need to prove theorems +of the form "forall x y, x == y -> (P x <-> P y)". The reason is that it +makes sense to do induction only on predicates P that satisfy this +property. Ideally, such goal should be proved by saying "intros x y H; +rewrite H; reflexivity". + +Such predicates P may contain quantifiers besides setoid morphisms. +Unfortunately, the tactic "rewrite" (which in this case stands for +"setoid_rewrite") currently cannot handle universal quantifiers as well +as lambda abstractions, which are part of the existential quantifier +notation (recall that "exists x, P" stands for "ex (fun x => p)"). + +Therefore, to prove that P x <-> P y, we proceed as follows. Suppose +that P x is C[forall z, A[x,z]] where C is a context, i.e., a term with +a hole. We assume that the hole of C does not occur inside another +quantifier, i.e., that forall z, A[x,z] is a top-level quantifier in P. +The notation A[x,z] means that x and z occur freely in A. We prove that +forall z, A[x,z] <-> forall z, A[y,z]. To do this, we show that +forall z, A[x,z] <-> A[y,z]. After performing "intro z", this goal is +handled recursively, until no more quantifiers are left in A. + +After we obtain the goal + +H : x == y +H1 : forall z, A[x,z] <-> forall z, A[y,z] +================================= +C[forall z, A[x,z]] <-> C[forall z, A[y,z]] + +we say "rewrite H1". The tactic setoid_rewrite can handle this because +"forall z" is a top-level quantifier. Repeating this for other +quantifier subformulas in P, we make them all identical in P x and P y. +After that, saying "rewrite H" solves the goal. + +The job of deriving P x <-> P y from x == y is done by the tactic +qmorphism x y below. *) + +Section Quantifiers. + +Variable A : Set. + +Theorem exists_morph : forall P1 P2 : A -> Prop, + (forall x : A, P1 x <-> P2 x) -> (ex P1 <-> ex P2). +Proof. +(intros P1 P2 H; split; intro H1; destruct H1 as [x H1]; +exists x); [now rewrite <- H | now rewrite H]. +Qed. + +Theorem forall_morph : forall P1 P2 : A -> Prop, + (forall x : A, P1 x <-> P2 x) -> ((forall x : A, P1 x) <-> (forall x : A, P2 x)). +Proof. +(intros P1 P2 H; split; intros H1 x); [now apply -> H | now apply <- H]. +Qed. + +End Quantifiers. + +(* replace x by y in t *) +Ltac repl x y t := +match t with +| context C [x] => let t' := (context C [y]) in repl x y t' +| _ => t +end. + +(* The tactic qiff x y H solves the goal P[x] <-> P[y] from H : E x y +where E is a registered setoid relation, P may contain quantifiers, +and x and y are arbitrary terms *) +Ltac qiff x y H := +match goal with +| |- ?P <-> ?P => reflexivity +(* The clause above is needed because if the goal is trivial, i.e., x +and y do not occur in P, "setoid_replace x with y" below would produce +an error. *) +| |- context [ex ?P] => + lazymatch P with + | context [x] => + let P' := repl x y P in + setoid_replace (ex P) with (ex P') using relation iff; + [qiff x y H | apply exists_morph; intro; qiff x y H] + end +| |- context [forall z, @?P z] => + lazymatch P with + | context [x] => + let P' := repl x y P in + setoid_replace (forall z, P z) with (forall z, P' z) using relation iff; + [qiff x y H | apply forall_morph; intro; qiff x y H] + end +| _ => setoid_rewrite H; reflexivity +end. + +Ltac qsetoid_rewrite H := +lazymatch (type of H) with +| ?E ?t1 ?t2 => + lazymatch goal with + | |- (fun x => @?G x) t1 => + let H1 := fresh in + let H2 := fresh in + let x1 := fresh "x" in + let x2 := fresh "x" in + set (x1 := t1); set (x2 := t2); + assert (H1 : E x1 x2); [apply H |]; + assert (H2 : (fun x => G x) x1 <-> (fun x => G x) x2); [qiff x1 x2 H1 |]; + unfold x1 in *; unfold x2 in *; apply <- H2; + clear H1 H2 x1 x2 + | _ => pattern t1; qsetoid_rewrite H + end +| _ => fail "The type of" H "does not have the form (E t1 t2)" +end. + +Tactic Notation "qsetoid_rewrite" "<-" constr(H) := +let H1 := fresh in + pose proof H as H1; + symmetry in H1; + qsetoid_rewrite H1; + clear H1. + +Tactic Notation "qsetoid_replace" constr(t1) "with" constr(t2) + "using" "relation" constr(E) := +let H := fresh in +lazymatch goal with +| |- ?G => + cut (E t1 t2); [intro H; change G; qsetoid_rewrite H; clear H |] +end. + +(* For testing *) + +(*Parameter E : nat -> nat -> Prop. +Axiom E_equiv : equiv nat E. + +Add Relation nat E + reflexivity proved by (proj1 E_equiv) + symmetry proved by (proj2 (proj2 E_equiv)) + transitivity proved by (proj1 (proj2 E_equiv)) +as E_rel. + +Notation "x == y" := (E x y) (at level 70). + +Add Morphism plus with signature E ==> E ==> E as plus_morph. Admitted. + +Goal forall x, x == x + x -> + (exists y, forall z, y == y + z -> exists u, x == u) /\ x == 0. +intros x H1. pattern x at 1. +qsetoid_rewrite H1. qsetoid_rewrite <- H1. +Admitted.*) + +(* For the extension that deals with multiple equalities. The idea is +to give qiff a list of hypothesis instead of just one H. *) + +(*Inductive EqList : Type := +| eqnil : EqList +| eqcons : forall A : Prop, A -> EqList -> EqList. + +Implicit Arguments eqcons [A]. + +Ltac ra L := +lazymatch L with +| eqnil => reflexivity +| eqcons ?H ?T => rewrite H; ra T +end. + +ra (eqcons H0 (eqcons H1 eqnil)).*) + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) |