diff options
Diffstat (limited to 'theories/Numbers/Natural/Axioms/NPred.v')
| -rw-r--r-- | theories/Numbers/Natural/Axioms/NPred.v | 29 |
1 files changed, 18 insertions, 11 deletions
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: +*) |