1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
36 Set Implicit Arguments.
39 (*#* Basic specifications : Sets containing logical information *)
41 include "Init/Notations.ma".
43 include "Init/Datatypes.ma".
45 include "Init/Logic.ma".
49 (*#* [(sig A P)], or more suggestively [{x:A | (P x)}], denotes the subset
50 of elements of the Set [A] which satisfy the predicate [P].
51 Similarly [(sig2 A P Q)], or [{x:A | (P x) & (Q x)}], denotes the subset
52 of elements of the Set [A] which satisfy both [P] and [Q]. *)
54 inline procedural "cic:/Coq/Init/Specif/sig.ind".
56 inline procedural "cic:/Coq/Init/Specif/sig2.ind".
58 (*#* [(sigS A P)], or more suggestively [{x:A & (P x)}], is a subtle variant
59 of subset where [P] is now of type [Set].
60 Similarly for [(sigS2 A P Q)], also written [{x:A & (P x) & (Q x)}]. *)
62 inline procedural "cic:/Coq/Init/Specif/sigS.ind".
64 inline procedural "cic:/Coq/Init/Specif/sigS2.ind".
67 Arguments Scope sig [type_scope type_scope].
71 Arguments Scope sig2 [type_scope type_scope type_scope].
75 Arguments Scope sigS [type_scope type_scope].
79 Arguments Scope sigS2 [type_scope type_scope type_scope].
83 Notation "{ x : A | P }" := (sig (fun x:A => P)) : type_scope.
87 Notation "{ x : A | P & Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
92 Notation "{ x : A & P }" := (sigS (fun x:A => P)) : type_scope.
96 Notation "{ x : A & P & Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
101 Add Printing Let sig.
105 Add Printing Let sig2.
109 Add Printing Let sigS.
113 Add Printing Let sigS2.
116 (*#* Projections of sig *)
119 Section Subset_projections
123 cic:/Coq/Init/Specif/Subset_projections/A.var
127 cic:/Coq/Init/Specif/Subset_projections/P.var
130 inline procedural "cic:/Coq/Init/Specif/proj1_sig.con" as definition.
132 inline procedural "cic:/Coq/Init/Specif/proj2_sig.con" as definition.
135 End Subset_projections
138 (*#* Projections of sigS *)
145 cic:/Coq/Init/Specif/Projections/A.var
149 cic:/Coq/Init/Specif/Projections/P.var
152 (*#* An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] of
153 type [A] and of a proof [h] that [a] satisfies [P].
154 Then [(projS1 y)] is the witness [a]
155 and [(projS2 y)] is the proof of [(P a)] *)
157 inline procedural "cic:/Coq/Init/Specif/projS1.con" as definition.
159 inline procedural "cic:/Coq/Init/Specif/projS2.con" as definition.
165 (*#* Extended_booleans *)
167 inline procedural "cic:/Coq/Init/Specif/sumbool.ind".
170 Add Printing If sumbool.
173 inline procedural "cic:/Coq/Init/Specif/sumor.ind".
176 Add Printing If sumor.
182 Section Choice_lemmas
185 (*#* The following lemmas state various forms of the axiom of choice *)
188 cic:/Coq/Init/Specif/Choice_lemmas/S.var
192 cic:/Coq/Init/Specif/Choice_lemmas/S'.var
196 cic:/Coq/Init/Specif/Choice_lemmas/R.var
200 cic:/Coq/Init/Specif/Choice_lemmas/R'.var
204 cic:/Coq/Init/Specif/Choice_lemmas/R1.var
208 cic:/Coq/Init/Specif/Choice_lemmas/R2.var
211 inline procedural "cic:/Coq/Init/Specif/Choice.con" as lemma.
213 inline procedural "cic:/Coq/Init/Specif/Choice2.con" as lemma.
215 inline procedural "cic:/Coq/Init/Specif/bool_choice.con" as lemma.
221 (*#* A result of type [(Exc A)] is either a normal value of type [A] or
223 [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
224 it is implemented using the option type. *)
226 inline procedural "cic:/Coq/Init/Specif/Exc.con" as definition.
228 inline procedural "cic:/Coq/Init/Specif/value.con" as definition.
230 inline procedural "cic:/Coq/Init/Specif/error.con" as definition.
233 Implicit Arguments error [A].
236 inline procedural "cic:/Coq/Init/Specif/except.con" as definition.
238 (* for compatibility with previous versions *)
241 Implicit Arguments except [P].
244 inline procedural "cic:/Coq/Init/Specif/absurd_set.con" as theorem.
247 Hint Resolve left right inleft inright: core v62.
250 (*#* Sigma Type at Type level [sigT] *)
252 inline procedural "cic:/Coq/Init/Specif/sigT.ind".
255 Section projections_sigT
259 cic:/Coq/Init/Specif/projections_sigT/A.var
263 cic:/Coq/Init/Specif/projections_sigT/P.var
266 inline procedural "cic:/Coq/Init/Specif/projT1.con" as definition.
268 inline procedural "cic:/Coq/Init/Specif/projT2.con" as definition.