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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Import DecidableType2 OrderedType2.
Require Export NumPrelude.
Delimit Scope NumScope with Num.
Local Open Scope NumScope.
(** Axiomatization of a domain with zero, successor, predecessor,
and a bi-directional induction principle. We require [P (S n) = n]
but not the other way around, since this domain is meant
to be either N or Z. In fact it can be a few other things,
for instance [Z/nZ] (See file [NZDomain for a study of that).
*)
Module Type NZDomain (Import E : EqualityType).
(** [E] provides [t], [eq], [eq_equiv : Equivalence eq] *)
Notation "x == y" := (eq x y) (at level 70) : NumScope.
Notation "x ~= y" := (~ eq x y) (at level 70) : NumScope.
Parameter Inline zero : t.
Parameter Inline succ : t -> t.
Parameter Inline pred : t -> t.
Notation "0" := zero : NumScope.
Notation S := succ.
Notation P := pred.
Notation "1" := (S 0) : NumScope.
Instance succ_wd : Proper (eq ==> eq) S.
Instance pred_wd : Proper (eq ==> eq) P.
Axiom pred_succ : forall n, P (S n) == n.
Axiom bi_induction :
forall A : t -> Prop, Proper (eq==>iff) A ->
A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
End NZDomain.
Module Type NZDomainSig := EqualityType <+ NZDomain.
(** A version with decidable type *)
Module Type NZDecDomainSig := DecidableType <+ NZDomain.
(** Axiomatization of basic operations : [+] [-] [*] *)
Module Type NZHasBasicFuns (Import NZ : NZDomainSig).
Parameter Inline add : t -> t -> t.
Parameter Inline sub : t -> t -> t.
Parameter Inline mul : t -> t -> t.
Notation "x + y" := (add x y) : NumScope.
Notation "x - y" := (sub x y) : NumScope.
Notation "x * y" := (mul x y) : NumScope.
Instance add_wd : Proper (eq ==> eq ==> eq) add.
Instance sub_wd : Proper (eq ==> eq ==> eq) sub.
Instance mul_wd : Proper (eq ==> eq ==> eq) mul.
Axiom add_0_l : forall n, (0 + n) == n.
Axiom add_succ_l : forall n m, (S n) + m == S (n + m).
Axiom sub_0_r : forall n, n - 0 == n.
Axiom sub_succ_r : forall n m, n - (S m) == P (n - m).
Axiom mul_0_l : forall n, 0 * n == 0.
Axiom mul_succ_l : forall n m, S n * m == n * m + m.
End NZHasBasicFuns.
Module Type NZBasicFunsSig := NZDomainSig <+ NZHasBasicFuns.
(** Old name for the same interface: *)
Module Type NZAxiomsSig := NZBasicFunsSig.
(** Axiomatization of order *)
Module Type NZHasOrd (Import NZ : NZDomainSig).
Parameter Inline lt : t -> t -> Prop.
Parameter Inline le : t -> t -> Prop.
Notation "x < y" := (lt x y) : NumScope.
Notation "x <= y" := (le x y) : NumScope.
Notation "x > y" := (lt y x) (only parsing) : NumScope.
Notation "x >= y" := (le y x) (only parsing) : NumScope.
Instance lt_wd : Proper (eq ==> eq ==> iff) lt.
(** Compatibility of [le] can be proved later from [lt_wd]
and [lt_eq_cases] *)
Axiom lt_eq_cases : forall n m, n <= m <-> n < m \/ n == m.
Axiom lt_irrefl : forall n, ~ (n < n).
Axiom lt_succ_r : forall n m, n < S m <-> n <= m.
End NZHasOrd.
Module Type NZOrdSig := NZDomainSig <+ NZHasOrd.
(** Axiomatization of minimum and maximum *)
Module Type NZHasMinMax (Import NZ : NZOrdSig).
Parameter Inline min : t -> t -> t.
Parameter Inline max : t -> t -> t.
(** Compatibility of [min] and [max] can be proved later *)
Axiom min_l : forall n m, n <= m -> min n m == n.
Axiom min_r : forall n m, m <= n -> min n m == m.
Axiom max_l : forall n m, m <= n -> max n m == n.
Axiom max_r : forall n m, n <= m -> max n m == m.
End NZHasMinMax.
Module Type NZOrdAxiomsSig :=
NZDomainSig <+ NZHasBasicFuns <+ NZHasOrd <+ NZHasMinMax.
|
