helm/software/matita/contribs/procedural/Coq/Init/Logic.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: Logic.v,v 1.29.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
  34
  35 (* UNEXPORTED
  36 Set Implicit Arguments.
  37 *)
  38
  39 include "Init/Notations.ma".
  40
  41 (*#* * Propositional connectives *)
  42
  43 (*#* [True] is the always true proposition *)
  44
  45 inline procedural "cic:/Coq/Init/Logic/True.ind".
  46
  47 (*#* [False] is the always false proposition *)
  48
  49 inline procedural "cic:/Coq/Init/Logic/False.ind".
  50
  51 (*#* [not A], written [~A], is the negation of [A] *)
  52
  53 inline procedural "cic:/Coq/Init/Logic/not.con" as definition.
  54
  55 (* NOTATION
  56 Notation "~ x" := (not x) : type_scope.
  57 *)
  58
  59 (* UNEXPORTED
  60 Hint Unfold not: core.
  61 *)
  62
  63 inline procedural "cic:/Coq/Init/Logic/and.ind".
  64
  65 (* UNEXPORTED
  66 Section Conjunction
  67 *)
  68
  69 (*#* [and A B], written [A /\ B], is the conjunction of [A] and [B]
  70
  71       [conj p q] is a proof of [A /\ B] as soon as
  72       [p] is a proof of [A] and [q] a proof of [B]
  73
  74       [proj1] and [proj2] are first and second projections of a conjunction *)
  75
  76 (* UNEXPORTED
  77 cic:/Coq/Init/Logic/Conjunction/A.var
  78 *)
  79
  80 (* UNEXPORTED
  81 cic:/Coq/Init/Logic/Conjunction/B.var
  82 *)
  83
  84 inline procedural "cic:/Coq/Init/Logic/proj1.con" as theorem.
  85
  86 inline procedural "cic:/Coq/Init/Logic/proj2.con" as theorem.
  87
  88 (* UNEXPORTED
  89 End Conjunction
  90 *)
  91
  92 (*#* [or A B], written [A \/ B], is the disjunction of [A] and [B] *)
  93
  94 inline procedural "cic:/Coq/Init/Logic/or.ind".
  95
  96 (*#* [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
  97
  98 inline procedural "cic:/Coq/Init/Logic/iff.con" as definition.
  99
 100 (* NOTATION
 101 Notation "A <-> B" := (iff A B) : type_scope.
 102 *)
 103
 104 (* UNEXPORTED
 105 Section Equivalence
 106 *)
 107
 108 inline procedural "cic:/Coq/Init/Logic/iff_refl.con" as theorem.
 109
 110 inline procedural "cic:/Coq/Init/Logic/iff_trans.con" as theorem.
 111
 112 inline procedural "cic:/Coq/Init/Logic/iff_sym.con" as theorem.
 113
 114 (* UNEXPORTED
 115 End Equivalence
 116 *)
 117
 118 (*#* [(IF_then_else P Q R)], written [IF P then Q else R] denotes
 119     either [P] and [Q], or [~P] and [Q] *)
 120
 121 inline procedural "cic:/Coq/Init/Logic/IF_then_else.con" as definition.
 122
 123 (* NOTATION
 124 Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
 125   (at level 200) : type_scope.
 126 *)
 127
 128 (*#* * First-order quantifiers
 129   - [ex A P], or simply [exists x, P x], expresses the existence of an
 130       [x] of type [A] which satisfies the predicate [P] ([A] is of type
 131       [Set]). This is existential quantification.
 132   - [ex2 A P Q], or simply [exists2 x, P x & Q x], expresses the
 133       existence of an [x] of type [A] which satisfies both the predicates
 134       [P] and [Q].
 135   - Universal quantification (especially first-order one) is normally
 136     written [forall x:A, P x]. For duality with existential quantification,
 137     the construction [all P] is provided too.
 138 *)
 139
 140 inline procedural "cic:/Coq/Init/Logic/ex.ind".
 141
 142 inline procedural "cic:/Coq/Init/Logic/ex2.ind".
 143
 144 inline procedural "cic:/Coq/Init/Logic/all.con" as definition.
 145
 146 (* Rule order is important to give printing priority to fully typed exists *)
 147
 148 (* NOTATION
 149 Notation "'exists' x , p" := (ex (fun x => p))
 150   (at level 200, x ident) : type_scope.
 151 *)
 152
 153 (* NOTATION
 154 Notation "'exists' x : t , p" := (ex (fun x:t => p))
 155   (at level 200, x ident, format "'exists'  '/  ' x  :  t ,  '/  ' p")
 156   : type_scope.
 157 *)
 158
 159 (* NOTATION
 160 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
 161   (at level 200, x ident, p at level 200) : type_scope.
 162 *)
 163
 164 (* NOTATION
 165 Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))
 166   (at level 200, x ident, t at level 200, p at level 200,
 167    format "'exists2'  '/  ' x  :  t ,  '/  ' '[' p  &  '/' q ']'")
 168   : type_scope.
 169 *)
 170
 171 (*#* Derived rules for universal quantification *)
 172
 173 (* UNEXPORTED
 174 Section universal_quantification
 175 *)
 176
 177 (* UNEXPORTED
 178 cic:/Coq/Init/Logic/universal_quantification/A.var
 179 *)
 180
 181 (* UNEXPORTED
 182 cic:/Coq/Init/Logic/universal_quantification/P.var
 183 *)
 184
 185 inline procedural "cic:/Coq/Init/Logic/inst.con" as theorem.
 186
 187 inline procedural "cic:/Coq/Init/Logic/gen.con" as theorem.
 188
 189 (* UNEXPORTED
 190 End universal_quantification
 191 *)
 192
 193 (*#* * Equality *)
 194
 195 (*#* [eq x y], or simply [x=y], expresses the (Leibniz') equality
 196     of [x] and [y]. Both [x] and [y] must belong to the same type [A].
 197     The definition is inductive and states the reflexivity of the equality.
 198     The others properties (symmetry, transitivity, replacement of
 199     equals) are proved below. The type of [x] and [y] can be made explicit
 200     using the notation [x = y :> A] *)
 201
 202 inline procedural "cic:/Coq/Init/Logic/eq.ind".
 203
 204 (* NOTATION
 205 Notation "x = y" := (x = y :>_) : type_scope.
 206 *)
 207
 208 (* NOTATION
 209 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 210 *)
 211
 212 (* NOTATION
 213 Notation "x <> y" := (x <> y :>_) : type_scope.
 214 *)
 215
 216 (* UNEXPORTED
 217 Implicit Arguments eq_ind [A].
 218 *)
 219
 220 (* UNEXPORTED
 221 Implicit Arguments eq_rec [A].
 222 *)
 223
 224 (* UNEXPORTED
 225 Implicit Arguments eq_rect [A].
 226 *)
 227
 228 (* UNEXPORTED
 229 Hint Resolve I conj or_introl or_intror refl_equal: core v62.
 230 *)
 231
 232 (* UNEXPORTED
 233 Hint Resolve ex_intro ex_intro2: core v62.
 234 *)
 235
 236 (* UNEXPORTED
 237 Section Logic_lemmas
 238 *)
 239
 240 inline procedural "cic:/Coq/Init/Logic/absurd.con" as theorem.
 241
 242 (* UNEXPORTED
 243 Section equality
 244 *)
 245
 246 (* UNEXPORTED
 247 cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var
 248 *)
 249
 250 (* UNEXPORTED
 251 cic:/Coq/Init/Logic/Logic_lemmas/equality/B.var
 252 *)
 253
 254 (* UNEXPORTED
 255 cic:/Coq/Init/Logic/Logic_lemmas/equality/f.var
 256 *)
 257
 258 (* UNEXPORTED
 259 cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var
 260 *)
 261
 262 (* UNEXPORTED
 263 cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var
 264 *)
 265
 266 (* UNEXPORTED
 267 cic:/Coq/Init/Logic/Logic_lemmas/equality/z.var
 268 *)
 269
 270 inline procedural "cic:/Coq/Init/Logic/sym_eq.con" as theorem.
 271
 272 (* UNEXPORTED
 273 Opaque sym_eq.
 274 *)
 275
 276 inline procedural "cic:/Coq/Init/Logic/trans_eq.con" as theorem.
 277
 278 (* UNEXPORTED
 279 Opaque trans_eq.
 280 *)
 281
 282 inline procedural "cic:/Coq/Init/Logic/f_equal.con" as theorem.
 283
 284 (* UNEXPORTED
 285 Opaque f_equal.
 286 *)
 287
 288 inline procedural "cic:/Coq/Init/Logic/sym_not_eq.con" as theorem.
 289
 290 inline procedural "cic:/Coq/Init/Logic/sym_equal.con" as definition.
 291
 292 inline procedural "cic:/Coq/Init/Logic/sym_not_equal.con" as definition.
 293
 294 inline procedural "cic:/Coq/Init/Logic/trans_equal.con" as definition.
 295
 296 (* UNEXPORTED
 297 End equality
 298 *)
 299
 300 (* Is now a primitive principle
 301   Theorem eq_rect: (A:Type)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y).
 302   Proof.
 303    Intros.
 304    Cut (identity A x y).
 305    NewDestruct 1; Auto.
 306    NewDestruct H; Auto.
 307   Qed.
 308 *)
 309
 310 inline procedural "cic:/Coq/Init/Logic/eq_ind_r.con" as definition.
 311
 312 inline procedural "cic:/Coq/Init/Logic/eq_rec_r.con" as definition.
 313
 314 inline procedural "cic:/Coq/Init/Logic/eq_rect_r.con" as definition.
 315
 316 (* UNEXPORTED
 317 End Logic_lemmas
 318 *)
 319
 320 inline procedural "cic:/Coq/Init/Logic/f_equal2.con" as theorem.
 321
 322 inline procedural "cic:/Coq/Init/Logic/f_equal3.con" as theorem.
 323
 324 inline procedural "cic:/Coq/Init/Logic/f_equal4.con" as theorem.
 325
 326 inline procedural "cic:/Coq/Init/Logic/f_equal5.con" as theorem.
 327
 328 (* UNEXPORTED
 329 Hint Immediate sym_eq sym_not_eq: core v62.
 330 *)
 331