helm/software/matita/contribs/procedural/Coq/Init/Specif.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Specif.v,v 1.25.2.1 2004/07/16 19:31:04 herbelin Exp $ i*)
  34
  35 (* UNEXPORTED
  36 Set Implicit Arguments.
  37 *)
  38
  39 (*#* Basic specifications : Sets containing logical information *)
  40
  41 include "Init/Notations.ma".
  42
  43 include "Init/Datatypes.ma".
  44
  45 include "Init/Logic.ma".
  46
  47 (*#* Subsets *)
  48
  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]. *)
  53
  54 inline procedural "cic:/Coq/Init/Specif/sig.ind".
  55
  56 inline procedural "cic:/Coq/Init/Specif/sig2.ind".
  57
  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)}]. *)
  61
  62 inline procedural "cic:/Coq/Init/Specif/sigS.ind".
  63
  64 inline procedural "cic:/Coq/Init/Specif/sigS2.ind".
  65
  66 (* UNEXPORTED
  67 Arguments Scope sig [type_scope type_scope].
  68 *)
  69
  70 (* UNEXPORTED
  71 Arguments Scope sig2 [type_scope type_scope type_scope].
  72 *)
  73
  74 (* UNEXPORTED
  75 Arguments Scope sigS [type_scope type_scope].
  76 *)
  77
  78 (* UNEXPORTED
  79 Arguments Scope sigS2 [type_scope type_scope type_scope].
  80 *)
  81
  82 (* NOTATION
  83 Notation "{ x : A  |  P }" := (sig (fun x:A => P)) : type_scope.
  84 *)
  85
  86 (* NOTATION
  87 Notation "{ x : A  |  P  &  Q }" := (sig2 (fun x:A => P) (fun x:A => Q)) :
  88   type_scope.
  89 *)
  90
  91 (* NOTATION
  92 Notation "{ x : A  &  P }" := (sigS (fun x:A => P)) : type_scope.
  93 *)
  94
  95 (* NOTATION
  96 Notation "{ x : A  &  P  &  Q }" := (sigS2 (fun x:A => P) (fun x:A => Q)) :
  97   type_scope.
  98 *)
  99
 100 (* NOTATION
 101 Add Printing Let sig.
 102 *)
 103
 104 (* NOTATION
 105 Add Printing Let sig2.
 106 *)
 107
 108 (* NOTATION
 109 Add Printing Let sigS.
 110 *)
 111
 112 (* NOTATION
 113 Add Printing Let sigS2.
 114 *)
 115
 116 (*#* Projections of sig *)
 117
 118 (* UNEXPORTED
 119 Section Subset_projections
 120 *)
 121
 122 (* UNEXPORTED
 123 cic:/Coq/Init/Specif/Subset_projections/A.var
 124 *)
 125
 126 (* UNEXPORTED
 127 cic:/Coq/Init/Specif/Subset_projections/P.var
 128 *)
 129
 130 inline procedural "cic:/Coq/Init/Specif/proj1_sig.con" as definition.
 131
 132 inline procedural "cic:/Coq/Init/Specif/proj2_sig.con" as definition.
 133
 134 (* UNEXPORTED
 135 End Subset_projections
 136 *)
 137
 138 (*#* Projections of sigS *)
 139
 140 (* UNEXPORTED
 141 Section Projections
 142 *)
 143
 144 (* UNEXPORTED
 145 cic:/Coq/Init/Specif/Projections/A.var
 146 *)
 147
 148 (* UNEXPORTED
 149 cic:/Coq/Init/Specif/Projections/P.var
 150 *)
 151
 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)] *)
 156
 157 inline procedural "cic:/Coq/Init/Specif/projS1.con" as definition.
 158
 159 inline procedural "cic:/Coq/Init/Specif/projS2.con" as definition.
 160
 161 (* UNEXPORTED
 162 End Projections
 163 *)
 164
 165 (*#* Extended_booleans *)
 166
 167 inline procedural "cic:/Coq/Init/Specif/sumbool.ind".
 168
 169 (* NOTATION
 170 Add Printing If sumbool.
 171 *)
 172
 173 inline procedural "cic:/Coq/Init/Specif/sumor.ind".
 174
 175 (* NOTATION
 176 Add Printing If sumor.
 177 *)
 178
 179 (*#* Choice *)
 180
 181 (* UNEXPORTED
 182 Section Choice_lemmas
 183 *)
 184
 185 (*#* The following lemmas state various forms of the axiom of choice *)
 186
 187 (* UNEXPORTED
 188 cic:/Coq/Init/Specif/Choice_lemmas/S.var
 189 *)
 190
 191 (* UNEXPORTED
 192 cic:/Coq/Init/Specif/Choice_lemmas/S'.var
 193 *)
 194
 195 (* UNEXPORTED
 196 cic:/Coq/Init/Specif/Choice_lemmas/R.var
 197 *)
 198
 199 (* UNEXPORTED
 200 cic:/Coq/Init/Specif/Choice_lemmas/R'.var
 201 *)
 202
 203 (* UNEXPORTED
 204 cic:/Coq/Init/Specif/Choice_lemmas/R1.var
 205 *)
 206
 207 (* UNEXPORTED
 208 cic:/Coq/Init/Specif/Choice_lemmas/R2.var
 209 *)
 210
 211 inline procedural "cic:/Coq/Init/Specif/Choice.con" as lemma.
 212
 213 inline procedural "cic:/Coq/Init/Specif/Choice2.con" as lemma.
 214
 215 inline procedural "cic:/Coq/Init/Specif/bool_choice.con" as lemma.
 216
 217 (* UNEXPORTED
 218 End Choice_lemmas
 219 *)
 220
 221 (*#* A result of type [(Exc A)] is either a normal value of type [A] or
 222      an [error] :
 223      [Inductive Exc [A:Set] : Set := value : A->(Exc A) | error : (Exc A)]
 224      it is implemented using the option type. *)
 225
 226 inline procedural "cic:/Coq/Init/Specif/Exc.con" as definition.
 227
 228 inline procedural "cic:/Coq/Init/Specif/value.con" as definition.
 229
 230 inline procedural "cic:/Coq/Init/Specif/error.con" as definition.
 231
 232 (* UNEXPORTED
 233 Implicit Arguments error [A].
 234 *)
 235
 236 inline procedural "cic:/Coq/Init/Specif/except.con" as definition.
 237
 238 (* for compatibility with previous versions *)
 239
 240 (* UNEXPORTED
 241 Implicit Arguments except [P].
 242 *)
 243
 244 inline procedural "cic:/Coq/Init/Specif/absurd_set.con" as theorem.
 245
 246 (* UNEXPORTED
 247 Hint Resolve left right inleft inright: core v62.
 248 *)
 249
 250 (*#* Sigma Type at Type level [sigT] *)
 251
 252 inline procedural "cic:/Coq/Init/Specif/sigT.ind".
 253
 254 (* UNEXPORTED
 255 Section projections_sigT
 256 *)
 257
 258 (* UNEXPORTED
 259 cic:/Coq/Init/Specif/projections_sigT/A.var
 260 *)
 261
 262 (* UNEXPORTED
 263 cic:/Coq/Init/Specif/projections_sigT/P.var
 264 *)
 265
 266 inline procedural "cic:/Coq/Init/Specif/projT1.con" as definition.
 267
 268 inline procedural "cic:/Coq/Init/Specif/projT2.con" as definition.
 269
 270 (* UNEXPORTED
 271 End projections_sigT
 272 *)
 273