diff options
Diffstat (limited to 'theories/Numbers/Natural')
19 files changed, 1211 insertions, 1171 deletions
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: +*) |