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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
Require Export NZAxioms NZPow NZSqrt NZLog NZDiv NZGcd.
(** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
Module Type NAxiom (Import NZ : NZDomainSig').
Axiom pred_0 : P 0 == 0.
End NAxiom.
Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom.
Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom.
(** Let's now add some more functions and their specification *)
(** Parity functions *)
Module Type Parity (Import N : NAxiomsMiniSig').
Parameter Inline even odd : t -> bool.
Definition Even n := exists m, n == 2*m.
Definition Odd n := exists m, n == 2*m+1.
Axiom even_spec : forall n, even n = true <-> Even n.
Axiom odd_spec : forall n, odd n = true <-> Odd n.
End Parity.
(** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon,
and add to that a N-specific constraint. *)
Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N).
Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b.
End NDivSpecific.
(** For gcd pow sqrt log2, the NZ axiomatizations are enough. *)
(** We now group everything together. *)
Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
<+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
<+ DivMod <+ NZDivCommon <+ NDivSpecific.
Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
<+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
<+ DivMod' <+ NZDivCommon <+ NDivSpecific.
(** It could also be interesting to have a constructive recursor function. *)
Module Type NAxiomsRec (Import NZ : NZDomainSig').
Parameter Inline recursion : forall {A : Type}, A -> (t -> A -> A) -> t -> A.
Declare Instance recursion_wd {A : Type} (Aeq : relation A) :
Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
Axiom recursion_0 :
forall {A} (a : A) (f : t -> A -> A), recursion a f 0 = a.
Axiom recursion_succ :
forall {A} (Aeq : relation A) (a : A) (f : t -> A -> A),
Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)).
End NAxiomsRec.
Module Type NAxiomsRecSig := NAxiomsMiniSig <+ NAxiomsRec.
Module Type NAxiomsRecSig' := NAxiomsMiniSig' <+ NAxiomsRec.
Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec.
Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec.
|
