helm/software/matita/contribs/procedural/Coq/Init/Peano.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: Peano.v,v 1.23.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
  34
  35 (*#* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
  36
  37 (*#* This module defines the following operations on natural numbers :
  38     - predecessor [pred]
  39     - addition [plus]
  40     - multiplication [mult]
  41     - less or equal order [le]
  42     - less [lt]
  43     - greater or equal [ge]
  44     - greater [gt]
  45
  46    This module states various lemmas and theorems about natural numbers,
  47    including Peano's axioms of arithmetic (in Coq, these are in fact provable)
  48    Case analysis on [nat] and induction on [nat * nat] are provided too *)
  49
  50 include "Init/Notations.ma".
  51
  52 include "Init/Datatypes.ma".
  53
  54 include "Init/Logic.ma".
  55
  56 (* UNEXPORTED
  57 Open Scope nat_scope.
  58 *)
  59
  60 inline procedural "cic:/Coq/Init/Peano/eq_S.con" as definition.
  61
  62 (* UNEXPORTED
  63 Hint Resolve (f_equal S): v62.
  64 *)
  65
  66 (* UNEXPORTED
  67 Hint Resolve (f_equal (A:=nat)): core.
  68 *)
  69
  70 (*#* The predecessor function *)
  71
  72 inline procedural "cic:/Coq/Init/Peano/pred.con" as definition.
  73
  74 (* UNEXPORTED
  75 Hint Resolve (f_equal pred): v62.
  76 *)
  77
  78 inline procedural "cic:/Coq/Init/Peano/pred_Sn.con" as theorem.
  79
  80 inline procedural "cic:/Coq/Init/Peano/eq_add_S.con" as theorem.
  81
  82 (* UNEXPORTED
  83 Hint Immediate eq_add_S: core v62.
  84 *)
  85
  86 (*#* A consequence of the previous axioms *)
  87
  88 inline procedural "cic:/Coq/Init/Peano/not_eq_S.con" as theorem.
  89
  90 (* UNEXPORTED
  91 Hint Resolve not_eq_S: core v62.
  92 *)
  93
  94 inline procedural "cic:/Coq/Init/Peano/IsSucc.con" as definition.
  95
  96 inline procedural "cic:/Coq/Init/Peano/O_S.con" as theorem.
  97
  98 (* UNEXPORTED
  99 Hint Resolve O_S: core v62.
 100 *)
 101
 102 inline procedural "cic:/Coq/Init/Peano/n_Sn.con" as theorem.
 103
 104 (* UNEXPORTED
 105 Hint Resolve n_Sn: core v62.
 106 *)
 107
 108 (*#* Addition *)
 109
 110 inline procedural "cic:/Coq/Init/Peano/plus.con" as definition.
 111
 112 (* UNEXPORTED
 113 Hint Resolve (f_equal2 plus): v62.
 114 *)
 115
 116 (* UNEXPORTED
 117 Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
 118 *)
 119
 120 (* NOTATION
 121 Infix "+" := plus : nat_scope.
 122 *)
 123
 124 inline procedural "cic:/Coq/Init/Peano/plus_n_O.con" as lemma.
 125
 126 (* UNEXPORTED
 127 Hint Resolve plus_n_O: core v62.
 128 *)
 129
 130 inline procedural "cic:/Coq/Init/Peano/plus_O_n.con" as lemma.
 131
 132 inline procedural "cic:/Coq/Init/Peano/plus_n_Sm.con" as lemma.
 133
 134 (* UNEXPORTED
 135 Hint Resolve plus_n_Sm: core v62.
 136 *)
 137
 138 inline procedural "cic:/Coq/Init/Peano/plus_Sn_m.con" as lemma.
 139
 140 (*#* Multiplication *)
 141
 142 inline procedural "cic:/Coq/Init/Peano/mult.con" as definition.
 143
 144 (* UNEXPORTED
 145 Hint Resolve (f_equal2 mult): core v62.
 146 *)
 147
 148 (* NOTATION
 149 Infix "*" := mult : nat_scope.
 150 *)
 151
 152 inline procedural "cic:/Coq/Init/Peano/mult_n_O.con" as lemma.
 153
 154 (* UNEXPORTED
 155 Hint Resolve mult_n_O: core v62.
 156 *)
 157
 158 inline procedural "cic:/Coq/Init/Peano/mult_n_Sm.con" as lemma.
 159
 160 (* UNEXPORTED
 161 Hint Resolve mult_n_Sm: core v62.
 162 *)
 163
 164 (*#* Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
 165
 166 inline procedural "cic:/Coq/Init/Peano/minus.con" as definition.
 167
 168 (* NOTATION
 169 Infix "-" := minus : nat_scope.
 170 *)
 171
 172 (*#* Definition of the usual orders, the basic properties of [le] and [lt]
 173     can be found in files Le and Lt *)
 174
 175 (*#* An inductive definition to define the order *)
 176
 177 inline procedural "cic:/Coq/Init/Peano/le.ind".
 178
 179 (* NOTATION
 180 Infix "<=" := le : nat_scope.
 181 *)
 182
 183 (* UNEXPORTED
 184 Hint Constructors le: core v62.
 185 *)
 186
 187 (*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
 188
 189 inline procedural "cic:/Coq/Init/Peano/lt.con" as definition.
 190
 191 (* UNEXPORTED
 192 Hint Unfold lt: core v62.
 193 *)
 194
 195 (* NOTATION
 196 Infix "<" := lt : nat_scope.
 197 *)
 198
 199 inline procedural "cic:/Coq/Init/Peano/ge.con" as definition.
 200
 201 (* UNEXPORTED
 202 Hint Unfold ge: core v62.
 203 *)
 204
 205 (* NOTATION
 206 Infix ">=" := ge : nat_scope.
 207 *)
 208
 209 inline procedural "cic:/Coq/Init/Peano/gt.con" as definition.
 210
 211 (* UNEXPORTED
 212 Hint Unfold gt: core v62.
 213 *)
 214
 215 (* NOTATION
 216 Infix ">" := gt : nat_scope.
 217 *)
 218
 219 (* NOTATION
 220 Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
 221 *)
 222
 223 (* NOTATION
 224 Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 225 *)
 226
 227 (* NOTATION
 228 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 229 *)
 230
 231 (* NOTATION
 232 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 233 *)
 234
 235 (*#* Pattern-Matching on natural numbers *)
 236
 237 inline procedural "cic:/Coq/Init/Peano/nat_case.con" as theorem.
 238
 239 (*#* Principle of double induction *)
 240
 241 inline procedural "cic:/Coq/Init/Peano/nat_double_ind.con" as theorem.
 242
 243 (*#* Notations *)
 244