blob: d3d22651cd51c81045602e7260d112a87aff8c2c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
Require Export NAxioms.
(* We would like to have a signature for the predecessor: first, to be
able to provide an efficient implementation, and second, to be able to
use this function in the signatures defining other functions, e.g.,
subtraction. If we just define predecessor by recursion in
NBasePropFunct functor, we would not be able to use it in other
signatures. *)
Module Type NPredSignature.
Declare Module Export NBaseMod : NBaseSig.
Open Local Scope NatScope.
Parameter Inline P : N -> N.
Add Morphism P with signature E ==> E as pred_wd.
Axiom pred_0 : P 0 == 0.
Axiom pred_succ : forall n, P (S n) == n.
End NPredSignature.
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 pred_wd.
Proof.
intros; unfold P.
now apply recursion_wd with (EA := E); [| unfold eq_fun2; now intros |].
Qed.
Theorem pred_0 : P 0 == 0.
Proof.
unfold P; now rewrite recursion_0.
Qed.
Theorem pred_succ : forall n, P (S n) == n.
Proof.
intro n; unfold P; now rewrite (recursion_succ E); [| unfold fun2_wd; now intros |].
Qed.
End NDefPred.
|
