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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
|
(************************************************************************)
(* 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 *)
(************************************************************************)
(*i $Id: Datatypes.v 11073 2008-06-08 20:24:51Z herbelin $ i*)
Set Implicit Arguments.
Require Import Notations.
Require Import Logic.
(** [unit] is a singleton datatype with sole inhabitant [tt] *)
Inductive unit : Set :=
tt : unit.
(** [bool] is the datatype of the boolean values [true] and [false] *)
Inductive bool : Set :=
| true : bool
| false : bool.
Add Printing If bool.
Delimit Scope bool_scope with bool.
Bind Scope bool_scope with bool.
(** Basic boolean operators *)
Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
Definition orb (b1 b2:bool) : bool := if b1 then true else b2.
Definition implb (b1 b2:bool) : bool := if b1 then b2 else true.
Definition xorb (b1 b2:bool) : bool :=
match b1, b2 with
| true, true => false
| true, false => true
| false, true => true
| false, false => false
end.
Definition negb (b:bool) := if b then false else true.
Infix "||" := orb : bool_scope.
Infix "&&" := andb : bool_scope.
(*******************************)
(** * Properties of [andb] *)
(*******************************)
Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
Proof.
destruct a; destruct b; intros; split; try (reflexivity || discriminate).
Qed.
Hint Resolve andb_prop: bool v62.
Lemma andb_true_intro :
forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
Proof.
destruct b1; destruct b2; simpl in |- *; tauto || auto with bool.
Qed.
Hint Resolve andb_true_intro: bool v62.
(** Interpretation of booleans as propositions *)
Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
(** [nat] is the datatype of natural numbers built from [O] and successor [S];
note that the constructor name is the letter O.
Numbers in [nat] can be denoted using a decimal notation;
e.g. [3%nat] abbreviates [S (S (S O))] *)
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
Delimit Scope nat_scope with nat.
Bind Scope nat_scope with nat.
Arguments Scope S [nat_scope].
(** [Empty_set] has no inhabitant *)
Inductive Empty_set : Set :=.
(** [identity A a] is the family of datatypes on [A] whose sole non-empty
member is the singleton datatype [identity A a a] whose
sole inhabitant is denoted [refl_identity A a] *)
Inductive identity (A:Type) (a:A) : A -> Type :=
refl_identity : identity (A:=A) a a.
Hint Resolve refl_identity: core v62.
Implicit Arguments identity_ind [A].
Implicit Arguments identity_rec [A].
Implicit Arguments identity_rect [A].
(** [option A] is the extension of [A] with an extra element [None] *)
Inductive option (A:Type) : Type :=
| Some : A -> option A
| None : option A.
Implicit Arguments None [A].
Definition option_map (A B:Type) (f:A->B) o :=
match o with
| Some a => Some (f a)
| None => None
end.
(** [sum A B], written [A + B], is the disjoint sum of [A] and [B] *)
Inductive sum (A B:Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
Notation "x + y" := (sum x y) : type_scope.
(** [prod A B], written [A * B], is the product of [A] and [B];
the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
Inductive prod (A B:Type) : Type :=
pair : A -> B -> prod A B.
Add Printing Let prod.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Section projections.
Variables A B : Type.
Definition fst (p:A * B) := match p with
| (x, y) => x
end.
Definition snd (p:A * B) := match p with
| (x, y) => y
end.
End projections.
Hint Resolve pair inl inr: core v62.
Lemma surjective_pairing :
forall (A B:Type) (p:A * B), p = pair (fst p) (snd p).
Proof.
destruct p; reflexivity.
Qed.
Lemma injective_projections :
forall (A B:Type) (p1 p2:A * B),
fst p1 = fst p2 -> snd p1 = snd p2 -> p1 = p2.
Proof.
destruct p1; destruct p2; simpl in |- *; intros Hfst Hsnd.
rewrite Hfst; rewrite Hsnd; reflexivity.
Qed.
Definition prod_uncurry (A B C:Type) (f:prod A B -> C)
(x:A) (y:B) : C := f (pair x y).
Definition prod_curry (A B C:Type) (f:A -> B -> C)
(p:prod A B) : C := match p with
| pair x y => f x y
end.
(** Comparison *)
Inductive comparison : Set :=
| Eq : comparison
| Lt : comparison
| Gt : comparison.
Definition CompOpp (r:comparison) :=
match r with
| Eq => Eq
| Lt => Gt
| Gt => Lt
end.
(** Identity *)
Definition ID := forall A:Type, A -> A.
Definition id : ID := fun A x => x.
(* begin hide *)
(* Compatibility *)
Notation prodT := prod (only parsing).
Notation pairT := pair (only parsing).
Notation prodT_rect := prod_rect (only parsing).
Notation prodT_rec := prod_rec (only parsing).
Notation prodT_ind := prod_ind (only parsing).
Notation fstT := fst (only parsing).
Notation sndT := snd (only parsing).
Notation prodT_uncurry := prod_uncurry (only parsing).
Notation prodT_curry := prod_curry (only parsing).
(* end hide *)
|
