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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \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.
Require Import Bool NZParity NZPow NZSqrt NZLog NZGcd NZDiv NZBits.
(** We obtain integers by postulating that successor of predecessor
is identity. *)
Module Type ZAxiom (Import Z : NZAxiomsSig').
Axiom succ_pred : forall n, S (P n) == n.
End ZAxiom.
(** For historical reasons, ZAxiomsMiniSig isn't just NZ + ZAxiom,
we also add an [opp] function, that can be seen as a shortcut
for [sub 0]. *)
Module Type Opp (Import T:Typ).
Parameter Inline opp : t -> t.
End Opp.
Module Type OppNotation (T:Typ)(Import O : Opp T).
Notation "- x" := (opp x) (at level 35, right associativity).
End OppNotation.
Module Type Opp' (T:Typ) := Opp T <+ OppNotation T.
Module Type IsOpp (Import Z : NZAxiomsSig')(Import O : Opp' Z).
Declare Instance opp_wd : Proper (eq==>eq) opp.
Axiom opp_0 : - 0 == 0.
Axiom opp_succ : forall n, - (S n) == P (- n).
End IsOpp.
Module Type OppCstNotation (Import A : NZAxiomsSig)(Import B : Opp A).
Notation "- 1" := (opp one).
Notation "- 2" := (opp two).
End OppCstNotation.
Module Type ZAxiomsMiniSig := NZOrdAxiomsSig <+ ZAxiom <+ Opp <+ IsOpp.
Module Type ZAxiomsMiniSig' := NZOrdAxiomsSig' <+ ZAxiom <+ Opp' <+ IsOpp
<+ OppCstNotation.
(** Other functions and their specifications *)
(** Absolute value *)
Module Type HasAbs(Import Z : ZAxiomsMiniSig').
Parameter Inline abs : t -> t.
Axiom abs_eq : forall n, 0<=n -> abs n == n.
Axiom abs_neq : forall n, n<=0 -> abs n == -n.
End HasAbs.
(** A sign function *)
Module Type HasSgn (Import Z : ZAxiomsMiniSig').
Parameter Inline sgn : t -> t.
Axiom sgn_null : forall n, n==0 -> sgn n == 0.
Axiom sgn_pos : forall n, 0<n -> sgn n == 1.
Axiom sgn_neg : forall n, n<0 -> sgn n == -1.
End HasSgn.
(** Divisions *)
(** First, the usual Coq convention of Truncated-Toward-Bottom
(a.k.a Floor). We simply extend the NZ signature. *)
Module Type ZDivSpecific (Import A:ZAxiomsMiniSig')(Import B : DivMod' A).
Axiom mod_pos_bound : forall a b, 0 < b -> 0 <= a mod b < b.
Axiom mod_neg_bound : forall a b, b < 0 -> b < a mod b <= 0.
End ZDivSpecific.
Module Type ZDiv (Z:ZAxiomsMiniSig) := NZDiv.NZDiv Z <+ ZDivSpecific Z.
Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z.
(** Then, the Truncated-Toward-Zero convention.
For not colliding with Floor operations, we use different names
*)
Module Type QuotRem (Import A : Typ).
Parameters Inline quot rem : t -> t -> t.
End QuotRem.
Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
Infix "÷" := quot (at level 40, left associativity).
Infix "rem" := rem (at level 40, no associativity).
End QuotRemNotation.
Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.
Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
Declare Instance quot_wd : Proper (eq==>eq==>eq) quot.
Declare Instance rem_wd : Proper (eq==>eq==>eq) B.rem.
Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b).
Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b).
Axiom rem_opp_r : forall a b, b ~= 0 -> a rem (-b) == a rem b.
End QuotRemSpec.
Module Type ZQuot (Z:ZAxiomsMiniSig) := QuotRem Z <+ QuotRemSpec Z.
Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z.
(** For all other functions, the NZ axiomatizations are enough. *)
(** Let's group everything *)
Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions
<+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd
<+ ZDiv <+ ZQuot <+ NZBits.NZBits <+ NZSquare.
Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions'
<+ HasAbs <+ HasSgn <+ NZParity.NZParity
<+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd'
<+ ZDiv' <+ ZQuot' <+ NZBits.NZBits' <+ NZSquare.
|
