diff options
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAxioms.v | 151 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZBase.v | 99 | ||||
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZPairsOrder1.v | 114 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPlus.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 39 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NBase.v | 121 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMiscFunct.v | 6 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 33 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NPlus.v | 12 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimes.v | 15 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimesOrder.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 250 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 383 | ||||
| -rw-r--r-- | theories/Numbers/QRewrite1.v | 173 |
17 files changed, 335 insertions, 1103 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 4019b4774..d3c0410ea 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -4,154 +4,17 @@ Require Export NZAxioms. Set Implicit Arguments. Module Type ZAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. +Open Local Scope NatIntScope. -Parameter Inline Z : Set. -Parameter Inline ZE : Z -> Z -> Prop. -Parameter Inline Z0 : Z. -Parameter Inline Zsucc : Z -> Z. -Parameter Inline Zpred : Z -> Z. -Parameter Inline Zplus : Z -> Z -> Z. -Parameter Inline Zminus : Z -> Z -> Z. -Parameter Inline Ztimes : Z -> Z -> Z. -Parameter Inline Zlt : Z -> Z -> Prop. -Parameter Inline Zle : Z -> Z -> Prop. +Notation Z := NZ (only parsing). +Notation E := NZE (only parsing). -Delimit Scope IntScope with Int. -Open Local Scope IntScope. -Notation "x == y" := (ZE x y) (at level 70, no associativity) : IntScope. -Notation "x ~= y" := (~ ZE x y) (at level 70, no associativity) : IntScope. -Notation "0" := Z0 : IntScope. -Notation "'S'" := Zsucc : IntScope. -Notation "'P'" := Zpred : IntScope. -Notation "1" := (S 0) : IntScope. -Notation "x + y" := (Zplus x y) : IntScope. -Notation "x - y" := (Zminus x y) : IntScope. -Notation "x * y" := (Ztimes x y) : IntScope. -Notation "x < y" := (Zlt x y) : IntScope. -Notation "x <= y" := (Zle x y) : IntScope. -Notation "x > y" := (Zlt y x) (only parsing) : IntScope. -Notation "x >= y" := (Zle y x) (only parsing) : IntScope. +(** Integers are obtained by postulating that every number has a predecessor *) +Axiom S_P : forall n : Z, S (P n) == n. -Axiom ZE_equiv : equiv Z ZE. +End ZAxiomsSig. -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. - -Add Morphism Zsucc with signature ZE ==> ZE as Zsucc_wd. -Add Morphism Zpred with signature ZE ==> ZE as Zpred_wd. -Add Morphism Zplus with signature ZE ==> ZE ==> ZE as Zplus_wd. -Add Morphism Zminus with signature ZE ==> ZE ==> ZE as Zminus_wd. -Add Morphism Ztimes with signature ZE ==> ZE ==> ZE as Ztimes_wd. -Add Morphism Zlt with signature ZE ==> ZE ==> iff as Zlt_wd. -Add Morphism Zle with signature ZE ==> ZE ==> iff as Zle_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. (* Local Variables: diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v index e0b753d4e..8f5c284e7 100644 --- a/theories/Numbers/Integer/Abstract/ZBase.v +++ b/theories/Numbers/Integer/Abstract/ZBase.v @@ -1,98 +1,29 @@ -Require Export NumPrelude. -Require Import NZBase. +Require Export ZAxioms. +Require Import NZTimesOrder. -Module Type ZBaseSig. +Module ZBasePropFunct (Import ZAxiomsMod : ZAxiomsSig). +Open Local Scope NatIntScope. -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. +Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. 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 : forall n1 n2 : Z, S n1 == S n2 -> n1 == n2. +Proof NZsucc_inj. -Theorem Zsucc_inj_wd : forall n m, S n == S m <-> n == m. +Theorem Zsucc_inj_wd : forall n1 n2 : Z, S n1 == S n2 <-> n1 == n2. Proof NZsucc_inj_wd. -Theorem Zsucc_inj_neg : forall n m, S n ~= S m <-> n ~= m. +Theorem Zsucc_inj_wd_neg : forall n m : Z, 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). +Theorem Zcentral_induction : +forall A : Z -> Prop, predicate_wd E A -> + forall z : Z, A z -> + (forall n : Z, A n <-> A (S n)) -> + forall n : Z, A n. +Proof NZcentral_induction. End ZBasePropFunct. diff --git a/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v b/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v deleted file mode 100644 index 5c6e50c1d..000000000 --- a/theories/Numbers/Integer/NatPairs/ZPairsOrder1.v +++ /dev/null @@ -1,114 +0,0 @@ -Require Import NPlusOrder. -Require Export ZPlusOrder. -Require Export ZPairsPlus. - -Module NatPairsOrder (Import NPlusMod : NPlusSig) - (Import NOrderModule : NOrderSig - with Module NBaseMod := NPlusMod.NBaseMod) <: ZOrderSignature. -Module Import NPlusOrderPropertiesModule := - NPlusOrderProperties NPlusMod NOrderModule. -Module Export IntModule := NatPairsInt NPlusMod. -Open Local Scope NatScope. - -Definition lt (p1 p2 : Z) := (fst p1) + (snd p2) < (fst p2) + (snd p1). -Definition le (p1 p2 : Z) := (fst p1) + (snd p2) <= (fst p2) + (snd p1). - -Notation "x < y" := (lt x y) : IntScope. -Notation "x <= y" := (le x y) : IntScope. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -unfold lt, E; intros x1 y1 H1 x2 y2 H2; simpl. -rewrite eq_true_iff; split; intro H. -stepr (snd y1 + fst y2) by apply plus_comm. -apply (plus_lt_repl_pair (fst x1) (snd x1)); [| assumption]. -stepl (snd y2 + fst x1) by apply plus_comm. -stepr (fst y2 + snd x1) by apply plus_comm. -apply (plus_lt_repl_pair (snd x2) (fst x2)). -now stepl (fst x1 + snd x2) by apply plus_comm. -stepl (fst y2 + snd x2) by apply plus_comm. now stepr (fst x2 + snd y2) by apply plus_comm. -stepr (snd x1 + fst x2) by apply plus_comm. -apply (plus_lt_repl_pair (fst y1) (snd y1)); [| now symmetry]. -stepl (snd x2 + fst y1) by apply plus_comm. -stepr (fst x2 + snd y1) by apply plus_comm. -apply (plus_lt_repl_pair (snd y2) (fst y2)). -now stepl (fst y1 + snd y2) by apply plus_comm. -stepl (fst x2 + snd y2) by apply plus_comm. now stepr (fst y2 + snd x2) by apply plus_comm. -Qed. - -(* Below is a very long explanation why it would be useful to be -able to use the fold tactic in hypotheses. -We will prove the following statement not from scratch, like lt_wd, -but expanding <= to < and == and then using lt_wd. The theorem we need -to prove is (x1 <= x2) = (y1 <= y2) for all x1 == y1 and x2 == y2 : Z. -To be able to express <= through < and ==, we need to expand <=%Int to -<=%Nat, since we have not proved yet the properties of <=%Int. But -then it would be convenient to fold back equalities from -(fst x1 + snd x2 == fst x2 + snd x1)%Nat to (x1 == x2)%Int. -The reason is that we will need to show that (x1 == x2)%Int <-> -(y1 == y2)%Int from (x1 == x2)%Int and (y1 == y2)%Int. If we fold -equalities back to Int, then we could do simple rewriting, since we have -already showed that ==%Int is an equivalence relation. On the other hand, -if we leave equalities expanded to Nat, we will have to apply the -transitivity of ==%Int by hand. *) - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -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 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 (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 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 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" *) -assert (H2' : (x2 == y2)%Int); [exact H2 |]. -rewrite H1'; rewrite H2'. reflexivity. -Qed. - -Open Local Scope IntScope. - -Theorem le_lt : forall n m : Z, n <= m <-> n < m \/ n == m. -Proof. -intros n m; unfold lt, le, E; simpl. apply le_lt. (* refers to NOrderModule.le_lt *) -Qed. - -Theorem lt_irr : forall n : Z, ~ (n < n). -Proof. -intros n; unfold lt, E; simpl. apply lt_irr. -(* refers to NPlusOrderPropertiesModule.NOrderPropFunctModule.lt_irr *) -Qed. - -Theorem lt_S : forall n m, n < (S m) <-> n <= m. -Proof. -intros n m; unfold lt, le, E; simpl. rewrite plus_S_l; apply lt_S. -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 (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. - -(* - Local Variables: - tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" - End: -*) diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index fa0bd21a3..0a89132ea 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -8,6 +8,7 @@ Parameter Inline NZ0 : NZ. Parameter Inline NZsucc : NZ -> NZ. Parameter Inline NZpred : NZ -> NZ. Parameter Inline NZplus : NZ -> NZ -> NZ. +Parameter Inline NZminus : NZ -> NZ -> NZ. Parameter Inline NZtimes : NZ -> NZ -> NZ. Axiom NZE_equiv : equiv NZ NZE. @@ -20,6 +21,7 @@ as NZE_rel. Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. +Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. Delimit Scope NatIntScope with NatInt. @@ -31,6 +33,7 @@ Notation "'S'" := NZsucc : NatIntScope. Notation "'P'" := NZpred : NatIntScope. Notation "1" := (S 0) : NatIntScope. Notation "x + y" := (NZplus x y) : NatIntScope. +Notation "x - y" := (NZminus x y) : NatIntScope. Notation "x * y" := (NZtimes x y) : NatIntScope. Axiom NZpred_succ : forall n : NZ, P (S n) == n. @@ -42,6 +45,9 @@ Axiom NZinduction : Axiom NZplus_0_l : forall n : NZ, 0 + n == n. Axiom NZplus_succ_l : forall n m : NZ, (S n) + m == S (n + m). +Axiom NZminus_0_r : forall n : NZ, n - 0 == n. +Axiom NZminus_succ_r : forall n m : NZ, n - (S m) == P (n - m). + Axiom NZtimes_0_r : forall n : NZ, n * 0 == 0. Axiom NZtimes_succ_r : forall n m : NZ, n * (S m) == n * m + n. @@ -59,6 +65,8 @@ Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. Notation "x < y" := (NZlt x y) : NatIntScope. Notation "x <= y" := (NZle x y) : NatIntScope. +Notation "x > y" := (NZlt y x) (only parsing) : NatIntScope. +Notation "x >= y" := (NZle y x) (only parsing) : NatIntScope. Axiom NZle_lt_or_eq : forall n m : NZ, n <= m <-> n < m \/ n == m. Axiom NZlt_irrefl : forall n : NZ, ~ (n < n). diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 64cf68489..fbccf049c 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -69,8 +69,8 @@ End CentralInduction. Tactic Notation "NZinduct" ident(n) := induction_maker n ltac:(apply NZinduction). -Tactic Notation "NZinduct" ident(n) constr(z) := - induction_maker n ltac:(apply NZcentral_induction with (z := z)). +Tactic Notation "NZinduct" ident(n) constr(u) := + induction_maker n ltac:(apply NZcentral_induction with (z := u)). End NZBasePropFunct. diff --git a/theories/Numbers/NatInt/NZPlus.v b/theories/Numbers/NatInt/NZPlus.v index d333274ba..061ab84bb 100644 --- a/theories/Numbers/NatInt/NZPlus.v +++ b/theories/Numbers/NatInt/NZPlus.v @@ -5,17 +5,6 @@ Module NZPlusPropFunct (Import NZAxiomsMod : NZAxiomsSig). Module Export NZBasePropMod := NZBasePropFunct NZAxiomsMod. Open Local Scope NatIntScope. -(** 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 => assert (H3 : t1 + t2 == u1 + u2); [now apply NZplus_wd |] - | _ => fail 2 ":" H2 "is not an equation" - end -| _ => fail 1 ":" H1 "is not an equation" -end. - Theorem NZplus_0_r : forall n : NZ, n + 0 == n. Proof. NZinduct n. now rewrite NZplus_0_l. @@ -81,6 +70,11 @@ intros n m p. rewrite (NZplus_comm n p); rewrite (NZplus_comm m p). apply NZplus_cancel_l. Qed. +Theorem NZminus_1_r : forall n : NZ, n - 1 == P n. +Proof. +intro n; rewrite NZminus_succ_r; now rewrite NZminus_0_r. +Qed. + End NZPlusPropFunct. diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v new file mode 100644 index 000000000..a30c81682 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -0,0 +1,39 @@ +Require Export NumPrelude. +Require Export NZAxioms. + +Set Implicit Arguments. + +Module Type NAxiomsSig. +Declare Module Export NZOrdAxiomsMod : NZOrdAxiomsSig. +Open Local Scope NatIntScope. + +Notation N := NZ (only parsing). +Notation E := NZE (only parsing). + +Parameter Inline recursion : forall A : Set, A -> (N -> A -> A) -> N -> A. +Implicit Arguments recursion [A]. + +Axiom pred_0 : P 0 == 0. + +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'). + +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)). + +End NAxiomsSig. + + +(* + Local Variables: + tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" + End: +*) diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v index b8940027c..b999240fb 100644 --- a/theories/Numbers/Natural/Abstract/NBase.v +++ b/theories/Numbers/Natural/Abstract/NBase.v @@ -2,13 +2,12 @@ Require Export NAxioms. Require Import NZTimesOrder. (* The last property functor on NZ, which subsumes all others *) Module NBasePropFunct (Import NAxiomsMod : NAxiomsSig). -Open Local Scope NatScope. +Open Local Scope NatIntScope. (* We call the last property functor on NZ, which includes all the previous ones, to get all properties of NZ at once. This way we will include them only one time. *) -Module NZOrdAxiomsMod := NNZFunct NAxiomsMod. Module Export NZTimesOrderMod := NZTimesOrderPropFunct NZOrdAxiomsMod. (* Here we probably need to re-prove all axioms declared in NAxioms.v to @@ -20,20 +19,12 @@ this way, one only has to consult, for example, NPlus.v to see all available properties for plus (i.e., one does not have to go to NAxioms.v and NZPlus.v). *) -Theorem E_equiv : equiv N E. -Proof E_equiv. - -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. +Theorem pred_succ : forall n : N, P (S n) == n. +Proof NZpred_succ. Theorem pred_0 : P 0 == 0. Proof pred_0. -Theorem pred_succ : forall n : N, P (S n) == n. -Proof pred_succ. - Theorem neq_symm : forall n m : N, n ~= m -> m ~= n. Proof NZneq_symm. @@ -46,37 +37,79 @@ Proof NZsucc_inj_wd. Theorem succ_inj_wd_neg : forall n m : N, S n ~= S m <-> n ~= m. Proof NZsucc_inj_wd_neg. +(* Now we prove that the successor of a number is not zero by defining a +function (by recursion) that maps 0 to false and the successor to true *) + +Definition if_zero (A : Set) (a b : A) (n : N) : A := + recursion a (fun _ _ => b) n. + +Add Morphism if_zero with signature @eq ==> @eq ==> E ==> @eq as if_zero_wd. +Proof. +intros; unfold if_zero. apply recursion_wd with (EA := (@eq A)). +reflexivity. unfold eq_fun2; now intros. assumption. +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 A (@eq A)); [| | unfold fun2_wd; now intros]. +Qed. + +Implicit Arguments if_zero [A]. + +Theorem neq_succ_0 : forall n : 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. +now rewrite H. +Qed. + +(* Next, we show that all numbers are nonnegative and recover regular induction +from the bidirectional induction on NZ *) + +Theorem le_0_l : forall n : N, 0 <= n. +Proof. +NZinduct n. +le_equal. +intro n; split. +apply NZle_le_succ. +intro H; apply -> NZle_succ_le_or_eq_succ in H; destruct H as [H | H]. +assumption. +symmetry in H; false_hyp H neq_succ_0. +Qed. + +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. +intros A A_wd A0 AS n; apply NZright_induction with 0; try assumption. +intros; auto; apply le_0_l. apply le_0_l. +Qed. + (* The theorems NZinduction, NZcentral_induction and the tactic NZinduct -refer to bidirectional induction, which is not so useful on natural +refer to bidirectional induction, which is not useful on natural numbers. Therefore, we define a new induction tactic for natural numbers. We do not have to call "Declare Left Step" and "Declare Right Step" commands again, since the data for stepl and stepr tactics is inherited -from NZ. *) +from N. *) -Tactic Notation "induct" ident(n) := induction_maker n ltac:(apply induction). -(* FIXME: "Ltac induct n := induction_maker n ltac:(apply induction)" does not work (bug 1703) *) +Ltac induct n := induction_maker n ltac:(apply induction). -(* Now we add properties peculiar to natural numbers *) - -Theorem nondep_induction : +Theorem case_analysis : 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. -Tactic Notation "nondep_induct" ident(n) := - induction_maker n ltac:(apply nondep_induction). - -(* The fact "forall n : N, S n ~= 0" can be proved either by building a -function (using recursion) that maps 0 ans S n to two provably different -terms, or from the axioms of order *) - -Theorem neq_succ_0 : forall n : N, S n ~= 0. -Proof. -intros n H. apply nlt_0_r with n. rewrite <- H. -apply <- lt_succ_le. apply <- le_lt_or_eq. now right. -Qed. +Ltac cases n := induction_maker n ltac:(apply case_analysis). Theorem neq_0 : ~ forall n, n == 0. Proof. @@ -85,19 +118,21 @@ Qed. Theorem neq_0_succ : forall n, n ~= 0 <-> exists m, n == S m. Proof. -nondep_induct n. split; intro H; +cases n. split; intro H; [now elim H | destruct H as [m H]; symmetry in H; false_hyp H neq_succ_0]. intro n; split; intro H; [now exists n | apply neq_succ_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]. +cases n. +now left. +intro n; right; now exists n. Qed. Theorem eq_pred_0 : forall n : N, P n == 0 <-> n == 0 \/ n == 1. Proof. -nondep_induct n. +cases n. rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto. split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H]. intro n. rewrite pred_succ. rewrite_false (S n == 0) neq_succ_0. @@ -106,18 +141,18 @@ Qed. Theorem succ_pred : forall n : N, n ~= 0 -> S (P n) == n. Proof. -nondep_induct n. +cases n. intro H; elimtype False; now apply H. intros; now rewrite pred_succ. Qed. Theorem pred_inj : forall n m : N, n ~= 0 -> m ~= 0 -> P n == P m -> n == m. Proof. -intros n m; nondep_induct n. +intros n m; cases n. intros H; elimtype False; now apply H. -intros n H1; nondep_induct m. +intros n _; cases m. intros H; elimtype False; now apply H. -intros m H2 H3. do 2 rewrite pred_succ in H3. now apply succ_wd. +intros m H2 H3. do 2 rewrite pred_succ in H3. now rewrite H3. Qed. (* The following induction principle is useful for reasoning about, e.g., @@ -144,7 +179,7 @@ Qed. End PairInduction. -Tactic Notation "pair_induct" ident(n) := induction_maker n ltac:(apply pair_induction). +(*Ltac pair_induct n := induction_maker n ltac:(apply pair_induction).*) (* The following is useful for reasoning about, e.g., Ackermann function *) Section TwoDimensionalInduction. @@ -171,11 +206,11 @@ Qed. End TwoDimensionalInduction. -Tactic Notation "two_dim_induct" ident(n) ident(m) := +(*Ltac two_dim_induct n m := try intros until n; try intros until m; pattern n, m; apply two_dim_induction; clear n m; - [solve_rel_wd | | | ]. + [solve_rel_wd | | | ].*) Section DoubleInduction. @@ -193,12 +228,12 @@ Theorem double_induction : (forall n m : N, R n m -> R (S n) (S m)) -> forall n m : N, R n m. Proof. intros H1 H2 H3; induct n; auto. -intros n IH; nondep_induct m; auto. +intros n H; cases m; auto. Qed. End DoubleInduction. -Tactic Notation "double_induct" ident(n) ident(m) := +Ltac double_induct n m := try intros until n; try intros until m; pattern n, m; apply double_induction; clear n m; diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index 0af5c22fd..811126123 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -2,13 +2,13 @@ Require Export NTimesOrder. Module NMinusPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NTimesOrderPropMod := NTimesOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. +Open Local Scope NatIntScope. Theorem minus_0_r : forall n : N, n - 0 == n. -Proof minus_0_r. +Proof NZminus_0_r. Theorem minus_succ_r : forall n m : N, n - (S m) == P (n - m). -Proof minus_succ_r. +Proof NZminus_succ_r. Theorem minus_1_r : forall n : N, n - 1 == P n. Proof. @@ -85,7 +85,7 @@ intros n m p H; double_induct n m. intros m H1; rewrite minus_0_l in H1. symmetry in H1; false_hyp H1 H. intro n; rewrite minus_0_r; now rewrite plus_0_l. intros n m IH H1. rewrite minus_succ in H1. apply IH in H1. -rewrite plus_succ_l; now apply succ_wd. +rewrite plus_succ_l; now rewrite H1. Qed. Theorem minus_plus_distr : forall n m p : N, n - (m + p) == (n - m) - p. @@ -126,7 +126,7 @@ Qed. Theorem times_pred_r : forall n m : N, n * (P m) == n * m - n. Proof. -intro n; nondep_induct m. +intros n m; cases m. now rewrite pred_0, times_0_r, minus_0_l. intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc. le_equal. diff --git a/theories/Numbers/Natural/Abstract/NMiscFunct.v b/theories/Numbers/Natural/Abstract/NMiscFunct.v index 82a922453..362dc0516 100644 --- a/theories/Numbers/Natural/Abstract/NMiscFunct.v +++ b/theories/Numbers/Natural/Abstract/NMiscFunct.v @@ -164,7 +164,7 @@ Qed. Theorem lt_0 : forall n, ~ lt n 0. Proof. -nondep_induct n. +ases/g rewrite lt_base_eq; rewrite if_zero_0; now intro. intros n; rewrite lt_step_eq. rewrite recursion_0. now intro. Qed. @@ -196,10 +196,10 @@ 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; +ases/g [split; intro; [now right | apply lt_0_1] | intro n; split; intro; [left |]; apply lt_0_succn]. -intros n IH. nondep_induct n0. +ases/g split. intro. assert (H1 : lt n 0); [now apply -> lt_succn_succm | false_hyp H1 lt_0]. intro H; destruct H as [H | H]. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 773f5d97e..e8311c63c 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -2,20 +2,17 @@ Require Export NTimes. Module NOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NTimesPropMod := NTimesPropFunct NAxiomsMod. -Open Local Scope NatScope. +Open Local Scope NatIntScope. (* The tactics le_less, le_equal and le_elim are inherited from NZOrder.v *) (* Axioms *) Theorem le_lt_or_eq : forall x y, x <= y <-> x < y \/ x == y. -Proof le_lt_or_eq. - -Theorem nlt_0_r : forall x, ~ (x < 0). -Proof nlt_0_r. +Proof NZle_lt_or_eq. Theorem lt_succ_le : forall x y, x < S y <-> x <= y. -Proof lt_succ_le. +Proof NZlt_succ_le. (* Renaming theorems from NZOrder.v *) @@ -195,11 +192,11 @@ Proof NZle_ind. (** Theorems that are true for natural numbers but not for integers *) -Theorem le_0_l : forall n : N, 0 <= n. +(* "le_0_l : forall n : N, 0 <= n" was proved in NBase.v *) + +Theorem nlt_0_r : forall n : N, ~ n < 0. Proof. -induct n. -now le_equal. -intros; now apply le_le_succ. +intro n; apply -> le_nlt. apply le_0_l. Qed. Theorem nle_succ_0 : forall n, ~ (S n <= 0). @@ -228,19 +225,19 @@ Qed. Theorem neq_0_lt_0 : forall n, n ~= 0 <-> 0 < n. Proof. -nondep_induct n. +cases n. split; intro H; [now elim H | intro; now apply lt_irrefl with 0]. intro n; split; intro H; [apply lt_0_succ | apply neq_succ_0]. Qed. Lemma Acc_nonneg_lt : forall n : N, - Acc (fun n m => 0 <= n /\ n < m) n -> Acc lt n. + Acc (fun n m => 0 <= n /\ n < m) n -> Acc NZlt n. Proof. intros n H; induction H as [n _ H2]; constructor; intros y H; apply H2; split; [apply le_0_l | assumption]. Qed. -Theorem lt_wf : well_founded lt. +Theorem lt_wf : well_founded NZlt. Proof. unfold well_founded; intro n; apply Acc_nonneg_lt. apply NZlt_wf. Qed. @@ -296,14 +293,14 @@ Qed. Theorem le_pred_l : forall n : N, P n <= n. Proof. -nondep_induct n. +cases n. rewrite pred_0; le_equal. intros; rewrite pred_succ; apply le_succ_r. Qed. Theorem lt_pred_l : forall n : N, n ~= 0 -> P n < n. Proof. -nondep_induct n. +cases n. intro H; elimtype False; now apply H. intros; rewrite pred_succ; apply lt_succ_r. Qed. @@ -320,14 +317,14 @@ Qed. Theorem lt_le_pred : forall n m : N, n < m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intro n; nondep_induct m. +intro n; cases m. intro H; false_hyp H nlt_0_r. intros m IH. rewrite pred_succ; now apply -> lt_succ_le. Qed. Theorem lt_pred_le : forall n m : N, P n < m -> n <= m. (* Converse is false for n == m == 0 *) Proof. -intros n m; nondep_induct n. +intros n m; cases n. rewrite pred_0; intro H; le_less. intros n IH. rewrite pred_succ in IH. now apply -> lt_le_succ. Qed. @@ -378,7 +375,7 @@ Qed. Theorem le_pred_le_succ : forall n m : N, P n <= m <-> n <= S m. Proof. -intros n m; nondep_induct n. +intros n m; cases n. rewrite pred_0. split; intro H; apply le_0_l. intro n. rewrite pred_succ. apply succ_le_mono. Qed. diff --git a/theories/Numbers/Natural/Abstract/NPlus.v b/theories/Numbers/Natural/Abstract/NPlus.v index 67a2766ba..f1e0e6ace 100644 --- a/theories/Numbers/Natural/Abstract/NPlus.v +++ b/theories/Numbers/Natural/Abstract/NPlus.v @@ -2,13 +2,13 @@ Require Export NBase. Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NBasePropMod := NBasePropFunct NAxiomsMod. -Open Local Scope NatScope. +Open Local Scope NatIntScope. Theorem plus_0_l : forall n : N, 0 + n == n. -Proof plus_0_l. +Proof NZplus_0_l. Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m). -Proof plus_succ_l. +Proof NZplus_succ_l. (** Theorems that are valid for both natural numbers and integers *) @@ -42,7 +42,7 @@ 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 *) +(** Theorems that are valid for natural numbers but cannot be proved for N *) Theorem plus_eq_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0. Proof. @@ -58,7 +58,7 @@ 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. -intros n m; nondep_induct n. +intros n m; cases 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]]. @@ -91,7 +91,7 @@ Qed. Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m). Proof. -intros n m; nondep_induct n. +intros n m; cases n. intro H; now elim H. intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ. Qed. diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index 7d42a812c..a0d255892 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -5,13 +5,13 @@ Require Export NPlus. Module NTimesPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NPlusPropMod := NPlusPropFunct NAxiomsMod. -Open Local Scope NatScope. +Open Local Scope NatIntScope. Theorem times_0_r : forall n, n * 0 == 0. -Proof times_0_r. +Proof NZtimes_0_r. Theorem times_succ_r : forall n m, n * (S m) == n * m + n. -Proof times_succ_r. +Proof NZtimes_succ_r. (** Theorems that are valid for both natural numbers and integers *) @@ -39,7 +39,7 @@ 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. +Lemma semi_ring : semi_ring_theory 0 1 NZplus NZtimes E. Proof. constructor. exact plus_0_l. @@ -97,9 +97,10 @@ Theorem plus_times_repl_pair : forall a n m n' m' u v, a * n + u == a * m + v -> n + m' == n' + m -> a * n' + u == a * m' + v. Proof. intros a n m n' m' u v H1 H2. -apply (@times_wd a a) in H2; [| reflexivity]. -do 2 rewrite times_plus_distr_l in H2. -symmetry in H2; add_equations H1 H2 as H3. +apply (@NZtimes_wd a a) in H2; [| reflexivity]. +do 2 rewrite times_plus_distr_l in H2. symmetry in H2. +assert (H3 : (a * n + u) + (a * n' + a * m) == (a * m + v) + (a * n + a * m')) + by now apply NZplus_wd. 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. diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v index 19b9e0ae4..68c6c4494 100644 --- a/theories/Numbers/Natural/Abstract/NTimesOrder.v +++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v @@ -2,7 +2,7 @@ Require Export NOrder. Module NTimesOrderPropFunct (Import NAxiomsMod : NAxiomsSig). Module Export NOrderPropMod := NOrderPropFunct NAxiomsMod. -Open Local Scope NatScope. +Open Local Scope NatIntScope. Theorem plus_lt_mono_l : forall n m p : N, n < m <-> p + n < p + m. Proof NZplus_lt_mono_l. @@ -48,7 +48,7 @@ Qed. Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m. Proof. -intro n; nondep_induct m. +intros n m; cases m. intro H; elimtype False; now apply H. intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r. Qed. diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v index 165c1211f..90b338773 100644 --- a/theories/Numbers/Natural/Binary/NBinary.v +++ b/theories/Numbers/Natural/Binary/NBinary.v @@ -2,128 +2,106 @@ Require Import NArith. Require Import NMinus. Module NBinaryAxiomsMod <: NAxiomsSig. - Open Local Scope N_scope. - -Definition N := N. -Definition E := (@eq N). -Definition O := 0. -Definition S := Nsucc. - -(*Definition Npred (n : N) := match n with -| 0 => 0 -| Npos p => match p with - | xH => 0 - | _ => Npos (Ppred p) - end -end.*) - -Definition P := Npred. -Definition plus := Nplus. -Definition minus := Nminus. - -(*Definition minus (n m : N) := -match n, m with -| N0, _ => N0 -| n, N0 => n -| Npos n', Npos m' => - match Pminus_mask n' m' with - | IsPos p => Npos p - | _ => N0 - end -end.*) - -Definition times := Nmult. -Definition lt := Nlt. -Definition le := Nle. - -Theorem E_equiv : equiv N E. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := N. +Definition NZE := (@eq N). +Definition NZ0 := 0. +Definition NZsucc := Nsucc. +Definition NZpred := Npred. +Definition NZplus := Nplus. +Definition NZminus := Nminus. +Definition NZtimes := Nmult. + +Theorem NZE_equiv : equiv N NZE. Proof (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. +Add Relation N 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 S with signature E ==> E as succ_wd. +Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. Proof. congruence. Qed. -Add Morphism P with signature E ==> E as pred_wd. +Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. Proof. congruence. Qed. -Add Morphism plus with signature E ==> E ==> E as plus_wd. +Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. Proof. congruence. Qed. -Add Morphism minus with signature E ==> E ==> E as minus_wd. +Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. Proof. congruence. Qed. -Add Morphism times with signature E ==> E ==> E as times_wd. +Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. Proof. congruence. Qed. -Add Morphism lt with signature E ==> E ==> iff as lt_wd. -Proof. -unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism le with signature E ==> E ==> iff as le_wd. -Proof. -unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Theorem induction : - forall A : N -> Prop, predicate_wd E A -> - A 0 -> (forall n, A n -> A (Nsucc n)) -> forall n, A n. +Theorem NZinduction : + forall A : N -> Prop, predicate_wd NZE A -> + A 0 -> (forall n, A n <-> A (Nsucc n)) -> forall n : N, A n. Proof. -intros A predicate_wd; apply Nind. +intros A A_wd A0 AS. apply Nind. assumption. intros; now apply -> AS. Qed. -Theorem pred_0 : Npred 0 = 0. -Proof. -reflexivity. -Qed. - -Theorem pred_succ : forall n : N, Npred (Nsucc n) = n. +Theorem NZpred_succ : forall n : N, Npred (Nsucc n) = n. Proof. destruct n as [| p]; simpl. reflexivity. case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ). intro H; false_hyp H Psucc_not_one. Qed. -Theorem plus_0_l : forall n : N, 0 + n = n. +Theorem NZplus_0_l : forall n : N, 0 + n = n. Proof Nplus_0_l. -Theorem plus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m). +Theorem NZplus_succ_l : forall n m : N, (Nsucc n) + m = Nsucc (n + m). Proof Nplus_succ. -Theorem minus_0_r : forall n : N, n - 0 = n. +Theorem NZminus_0_r : forall n : N, n - 0 = n. Proof Nminus_0_r. -Theorem minus_succ_r : forall n m : N, n - (S m) = P (n - m). +Theorem NZminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m). Proof Nminus_succ_r. -Theorem times_0_r : forall n : N, n * 0 = 0. +Theorem NZtimes_0_r : forall n : N, n * 0 = 0. Proof. intro n; rewrite Nmult_comm; apply Nmult_0_l. Qed. -Theorem times_succ_r : forall n m : N, n * (Nsucc m) = n * m + n. +Theorem NZtimes_succ_r : forall n m : N, n * (Nsucc m) = n * m + n. Proof. intros n m; rewrite Nmult_comm, Nmult_Sn_m. now rewrite Nplus_comm, Nmult_comm. Qed. -Theorem le_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m. +End NZAxiomsMod. + +Definition NZlt := Nlt. +Definition NZle := Nle. + +Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. +Proof. +unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. +Proof. +unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. +Qed. + +Theorem NZle_lt_or_eq : forall n m : N, n <= m <-> n < m \/ n = m. Proof. intros n m. assert (H : (n ?= m) = Eq <-> n = m). @@ -133,29 +111,37 @@ destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now now elim H1. destruct H1; discriminate. Qed. -Theorem nlt_0_r : forall n : N, ~ (n < 0). -Proof. -unfold Nlt; destruct n as [| p]; simpl; discriminate. -Qed. +Theorem NZlt_irrefl : forall n : N, ~ n < n. +Proof Nlt_irrefl. -Theorem lt_succ_le : forall n m : N, n < (S m) <-> n <= m. +Theorem NZlt_succ_le : forall n m : N, n < (Nsucc m) <-> n <= m. Proof. -intros x y. rewrite le_lt_or_eq. -unfold Nlt, Nle, S; apply Ncompare_n_Sm. +intros x y. rewrite NZle_lt_or_eq. +unfold Nlt, Nle; apply Ncompare_n_Sm. Qed. +End NZOrdAxiomsMod. + Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) := Nrec (fun _ => A) a f n. Implicit Arguments recursion [A]. +Theorem succ_neq_0 : forall n : N, Nsucc n <> 0. +Proof Nsucc_0. + +Theorem pred_0 : Npred 0 = 0. +Proof. +reflexivity. +Qed. + 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 f f' : N -> A -> A, eq_fun2 NZE EA EA f f' -> forall x x' : N, x = x' -> EA (recursion a f x) (recursion a' f' x'). Proof. -unfold fun2_wd, E, eq_fun2. +unfold fun2_wd, NZE, eq_fun2. intros A EA a a' Eaa' f f' Eff'. intro x; pattern x; apply Nind. intros x' H; now rewrite <- H. @@ -173,10 +159,10 @@ 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 -> + EA a a -> fun2_wd NZE EA EA f -> forall n : N, EA (recursion a f (Nsucc n)) (f n (recursion a f n)). Proof. -unfold E, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind. +unfold NZE, recursion, Nrec, fun2_wd; intros A EA a f EAaa f_wd n; pattern n; apply Nind. rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. clear n; intro n; do 2 rewrite Nrect_step; intro IH. apply f_wd; [reflexivity|]. now rewrite Nrect_step. @@ -186,102 +172,8 @@ End NBinaryAxiomsMod. Module Export NBinaryMinusPropMod := NMinusPropFunct NBinaryAxiomsMod. -(* -Module NBinaryDepRec <: NDepRecSignature. -Module Export NDomainModule := NBinaryDomain. -Module Export NBaseMod := BinaryNat. - -Definition dep_recursion := Nrec. - -Theorem 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. -Proof. -intros A a f; unfold dep_recursion; unfold Nrec; now rewrite Nrect_base. -Qed. - -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. -intros A a f n; unfold dep_recursion; unfold Nrec; now rewrite Nrect_step. -Qed. -End NBinaryDepRec. - -Module NBinaryPlus <: NPlusSig. -Module Export NBaseMod := BinaryNat. - -Definition plus := Nplus. - -Add Morphism plus with signature E ==> E ==> E as plus_wd. -Proof. -unfold E; congruence. -Qed. - -End NBinaryPlus. - -Module NBinaryTimes <: NTimesSig. -Module Export NPlusMod := NBinaryPlus. - -Definition times := Nmult. - -Add Morphism times with signature E ==> E ==> E as times_wd. -Proof. -unfold E; congruence. -Qed. - - -End NBinaryTimes. - -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). - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -unfold E; congruence. -Qed. - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -unfold E; congruence. -Qed. - -Theorem le_lt : forall n m, le n m <-> lt n m \/ n = m. -Proof. -intros n m. -assert (H : (n ?= m) = Eq <-> n = m). -(split; intro H); [now apply Ncompare_Eq_eq | rewrite H; apply Ncompare_refl]. -unfold le, lt; rewrite eq_true_or. repeat rewrite comp_bool_correct. now rewrite H. -Qed. - -Theorem lt_0 : forall x, ~ (lt x 0). -Proof. -unfold lt; destruct x as [|x]; simpl; now intro. -Qed. - -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 m x y) as H. tauto. -Qed. - -End NBinaryOrder. - -Module Export NBinaryTimesOrderProperties := NTimesOrderProperties NBinaryTimes NBinaryOrder. - -(* Todo: N implements NPred.v and NMinus.v *) - -(*Module Export BinaryRecEx := MiscFunctFunctor BinaryNat.*) - -(* Just some fun comparing the efficiency of the generic log defined +(* Some fun comparing the efficiency of the generic log defined by strong (course-of-value) recursion and the log defined by recursion on notation *) (* Time Eval compute in (log 100000). *) (* 98 sec *) @@ -302,7 +194,7 @@ end. *) (* Eval compute in (binlog 1000000000000000000). *) (* Works very fast *) -*) + (* Local Variables: tags-file-name: "~/coq/trunk/theories/Numbers/TAGS" diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index aa5ac99cf..2f6c13cac 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -2,416 +2,175 @@ Require Import Arith. Require Import NMinus. Module NPeanoAxiomsMod <: NAxiomsSig. - -Definition N := nat. -Definition E := (@eq nat). -Definition O := 0. -Definition S := S. -Definition P := pred. -Definition plus := plus. -Definition minus := minus. -Definition times := mult. -Definition lt := lt. -Definition le := le. -Definition recursion : forall A : Set, A -> (N -> A -> A) -> N -> A := - fun A : Set => nat_rec (fun _ => A). -Implicit Arguments recursion [A]. - -Theorem E_equiv : equiv nat E. +Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. +Module Export NZAxiomsMod <: NZAxiomsSig. + +Definition NZ := nat. +Definition NZE := (@eq nat). +Definition NZ0 := 0. +Definition NZsucc := S. +Definition NZpred := pred. +Definition NZplus := plus. +Definition NZminus := minus. +Definition NZtimes := mult. + +Theorem NZE_equiv : equiv nat NZE. Proof (eq_equiv nat). -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. +Add Relation nat NZE + reflexivity proved by (proj1 NZE_equiv) + symmetry proved by (proj2 (proj2 NZE_equiv)) + transitivity proved by (proj1 (proj2 NZE_equiv)) +as NZE_rel. -(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat E" +(* If we say "Add Relation nat (@eq nat)" instead of "Add Relation nat NZE" then the theorem generated for succ_wd below is forall x, succ x = succ x, which does not match the axioms in NAxiomsSig *) -Add Morphism S with signature E ==> E as succ_wd. +Add Morphism NZsucc with signature NZE ==> NZE as NZsucc_wd. Proof. congruence. Qed. -Add Morphism P with signature E ==> E as pred_wd. +Add Morphism NZpred with signature NZE ==> NZE as NZpred_wd. Proof. congruence. Qed. -Add Morphism plus with signature E ==> E ==> E as plus_wd. +Add Morphism NZplus with signature NZE ==> NZE ==> NZE as NZplus_wd. Proof. congruence. Qed. -Add Morphism minus with signature E ==> E ==> E as minus_wd. +Add Morphism NZminus with signature NZE ==> NZE ==> NZE as NZminus_wd. Proof. congruence. Qed. -Add Morphism times with signature E ==> E ==> E as times_wd. +Add Morphism NZtimes with signature NZE ==> NZE ==> NZE as NZtimes_wd. Proof. congruence. Qed. -Add Morphism lt with signature E ==> E ==> iff as lt_wd. -Proof. -unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Add Morphism le with signature E ==> E ==> iff as le_wd. -Proof. -unfold E; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. -Qed. - -Theorem induction : +Theorem NZinduction : forall A : nat -> Prop, predicate_wd (@eq nat) A -> - A 0 -> (forall n : nat, A n -> A (S n)) -> forall n : nat, A n. + A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. Proof. -intros; now apply nat_ind. +intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. Qed. -Theorem pred_0 : pred 0 = 0. -Proof. -reflexivity. -Qed. - -Theorem pred_succ : forall n : nat, pred (S n) = n. +Theorem NZpred_succ : forall n : nat, pred (S n) = n. Proof. reflexivity. Qed. -Theorem plus_0_l : forall n : nat, 0 + n = n. +Theorem NZplus_0_l : forall n : nat, 0 + n = n. Proof. reflexivity. Qed. -Theorem plus_succ_l : forall n m : nat, (S n) + m = S (n + m). +Theorem NZplus_succ_l : forall n m : nat, (S n) + m = S (n + m). Proof. reflexivity. Qed. -Theorem minus_0_r : forall n : nat, n - 0 = n. +Theorem NZminus_0_r : forall n : nat, n - 0 = n. Proof. intro n; now destruct n. Qed. -Theorem minus_succ_r : forall n m : nat, n - (S m) = pred (n - m). +Theorem NZminus_succ_r : forall n m : nat, n - (S m) = pred (n - m). Proof. -intros n m; induction n m using nat_double_ind; simpl; auto. apply minus_0_r. +intros n m; induction n m using nat_double_ind; simpl; auto. apply NZminus_0_r. Qed. -Theorem times_0_r : forall n : nat, n * 0 = 0. +Theorem NZtimes_0_r : forall n : nat, n * 0 = 0. Proof. exact mult_0_r. Qed. -Theorem times_succ_r : forall n m : nat, n * (S m) = n * m + n. +Theorem NZtimes_succ_r : forall n m : nat, n * (S m) = n * m + n. Proof. intros n m; symmetry; apply mult_n_Sm. Qed. -Theorem le_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m. -Proof. -intros n m; split. -apply le_lt_or_eq. -intro H; destruct H as [H | H]. -now apply lt_le_weak. rewrite H; apply le_refl. -Qed. - -Theorem nlt_0_r : forall n : nat, ~ (n < 0). -Proof. -exact lt_n_O. -Qed. - -Theorem lt_succ_le : forall n m : nat, n < S m <-> n <= m. -Proof. -intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm]. -Qed. - -Theorem recursion_wd : forall (A : Set) (EA : relation A), - forall a a' : A, EA a a' -> - forall f f' : N -> A -> A, eq_fun2 (@eq nat) EA EA f f' -> - forall n n' : N, n = n' -> - EA (recursion a f n) (recursion a' f' n'). -Proof. -unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. -Qed. - -Theorem recursion_0 : - forall (A : Set) (a : A) (f : N -> A -> A), recursion a f 0 = a. -Proof. -reflexivity. -Qed. - -Theorem recursion_succ : - forall (A : Set) (EA : relation A) (a : A) (f : N -> A -> A), - EA a a -> fun2_wd (@eq nat) EA EA f -> - forall n : N, EA (recursion a f (S n)) (f n (recursion a f n)). -Proof. -unfold eq_fun2; induction n; simpl; auto. -Qed. - -End NPeanoAxiomsMod. - -(* Now we apply the largest property functor *) - -Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod. - -(* - -Theorem succ_wd : fun_wd (@eq nat) (@eq nat) S. -Proof. -congruence. -Qed. - -Theorem succ_inj : forall n1 n2 : nat, S n1 = S n2 -> n1 = n2. -Proof. -intros n1 n2 H; now simplify_eq H. -Qed. - -Theorem succ_neq_0 : forall n : nat, S n <> 0. -Proof. -intros n H; simplify_eq H. -Qed. - - -Definition N := nat. -Definition E := (@eq nat). -Definition O := 0. -Definition S := S. - -End NPeanoBaseMod. - -Module NPeanoPlusMod <: NPlusSig. -Module NBaseMod := NPeanoBaseMod. - -Theorem plus_wd : fun2_wd (@eq nat) (@eq nat) (@eq nat) plus. -Proof. -congruence. -Qed. - -Theorem plus_0_l : forall n, 0 + n = n. -Proof. -reflexivity. -Qed. - -Theorem plus_succ_l : forall n m, (S n) + m = S (n + m). -Proof. -reflexivity. -Qed. - -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 NBaseMod := PeanoNat. - -Definition dep_recursion := nat_rec. - -Theorem 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. -Proof. -reflexivity. -Qed. - -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. -reflexivity. -Qed. - -End NPeanoDepRec. - -Module Export NPeanoOrder <: NOrderSig. -Module Import NBaseMod := PeanoNat. - -Definition lt := lt. -Definition le := le. - -Add Morphism lt with signature E ==> E ==> eq_bool as lt_wd. -Proof. -unfold E, eq_bool; congruence. -Qed. - -Add Morphism le with signature E ==> E ==> eq_bool as le_wd. -Proof. -unfold E, eq_bool; congruence. -Qed. - -(* It would be easier to prove the boolean lemma first because -|| is simplified by simpl unlike \/ *) -Lemma le_lt_bool : forall x y, le x y = (lt x y) || (e x y). -Proof. -induction x as [| x IH]; destruct y; simpl; (reflexivity || apply IH). -Qed. - -Theorem le_lt : forall x y, le x y <-> lt x y \/ x = y. -Proof. -intros; rewrite E_equiv_e; rewrite <- eq_true_or; -rewrite <- eq_true_iff; apply le_lt_bool. -Qed. +End NZAxiomsMod. -Theorem lt_0 : forall x, ~ (lt x 0). -Proof. -destruct x as [|x]; simpl; now intro. -Qed. +Definition NZlt := lt. +Definition NZle := le. -Lemma lt_succ_bool : forall x y, lt x (S y) = le x y. +Add Morphism NZlt with signature NZE ==> NZE ==> iff as NZlt_wd. Proof. -unfold lt, le; induction x as [| x IH]; destruct y as [| y]; -simpl; try reflexivity. -destruct x; now simpl. -apply IH. +unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. -Theorem lt_succ : forall x y, lt x (S y) <-> le x y. +Add Morphism NZle with signature NZE ==> NZE ==> iff as NZle_wd. Proof. -intros; rewrite <- eq_true_iff; apply lt_succ_bool. +unfold NZE; intros x1 x2 H1 y1 y2 H2; rewrite H1; now rewrite H2. Qed. -End NPeanoOrder. - -Module Export NPeanoTimes <: NTimesSig. -Module Import NPlusMod := NPeanoPlus. - -Definition times := mult. - -Add Morphism times with signature E ==> E ==> E as times_wd. +Theorem NZle_lt_or_eq : forall n m : nat, n <= m <-> n < m \/ n = m. Proof. -unfold E; congruence. +intros n m; split. +apply le_lt_or_eq. +intro H; destruct H as [H | H]. +now apply lt_le_weak. rewrite H; apply le_refl. Qed. -Theorem times_0_r : forall n, n * 0 = 0. +Theorem NZlt_irrefl : forall n : nat, ~ (n < n). Proof. -auto. +exact lt_irrefl. Qed. -Theorem times_succ_r : forall n m, n * (S m) = n * m + n. +Theorem NZlt_succ_le : forall n m : nat, n < S m <-> n <= m. Proof. -auto. +intros n m; split; [apply lt_n_Sm_le | apply le_lt_n_Sm]. Qed. -End NPeanoTimes. +End NZOrdAxiomsMod. -Module Export NPeanoPred <: NPredSignature. -Module Export NBaseMod := PeanoNat. - -Definition P (n : nat) := -match n with -| 0 => 0 -| S n' => n' -end. +Definition recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A := + fun A : Set => nat_rec (fun _ => A). +Implicit Arguments recursion [A]. -Add Morphism P with signature E ==> E as pred_wd. +Theorem succ_neq_0 : forall n : nat, S n <> 0. Proof. -unfold E; congruence. +intros; discriminate. Qed. -Theorem pred_0 : P 0 = 0. +Theorem pred_0 : pred 0 = 0. Proof. reflexivity. Qed. -Theorem pred_succ : forall n, P (S n) = n. -Proof. -now intro. -Qed. - -End NPeanoPred. - -Module Export NPeanoMinus <: NMinusSignature. -Module Import NPredModule := NPeanoPred. - -Definition minus := minus. - -Add Morphism minus with signature E ==> E ==> E as minus_wd. -Proof. -unfold E; congruence. -Qed. - -Theorem minus_0_r : forall n, n - 0 = n. -Proof. -now destruct n. -Qed. - -Theorem minus_succ_r : forall n m, n - (S m) = P (n - m). -Proof. -induction n as [| n IH]; simpl. -now intro. -destruct m; simpl; [apply minus_0_r | apply IH]. -Qed. - -End NPeanoMinus. - -(* Obtaining properties for +, *, <, and their combinations *) - -Module Export NPeanoTimesOrderProperties := NTimesOrderProperties NPeanoTimes NPeanoOrder. -Module Export NPeanoDepRecTimesProperties := - NDepRecTimesProperties NPeanoDepRec NPeanoTimes. -Module Export NPeanoMinusProperties := - NMinusProperties NPeanoMinus NPeanoPlus NPeanoOrder. - -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), +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'). + forall f f' : nat -> A -> A, eq_fun2 (@eq nat) EA EA f f' -> + forall n n' : nat, n = n' -> + EA (recursion a f n) (recursion a' f' n'). 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]. +unfold eq_fun2; induction n; intros n' Enn'; rewrite <- Enn' in *; simpl; auto. Qed. Theorem recursion_0 : - forall (A : Set) (a : A) (f : N -> A -> A), recursion a f O = a. + forall (A : Set) (a : A) (f : nat -> A -> A), recursion a f 0 = 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)). + forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A), + EA a a -> fun2_wd (@eq nat) EA EA f -> + forall n : nat, 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. +unfold eq_fun2; induction n; simpl; auto. 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; -now apply <- E_equiv_e. -Qed. +End NPeanoAxiomsMod. -Add Ring SR : semi_ring (decidable e_implies_E). +(* Now we apply the largest property functor *) -Goal forall x y : nat, x + y = y + x. intros. ring.*) -*) +Module Export NPeanoMinusPropMod := NMinusPropFunct NPeanoAxiomsMod. (* diff --git a/theories/Numbers/QRewrite1.v b/theories/Numbers/QRewrite1.v deleted file mode 100644 index a781411a2..000000000 --- a/theories/Numbers/QRewrite1.v +++ /dev/null @@ -1,173 +0,0 @@ -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: -*) |