--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* This file was automatically generated: do not edit *********************)
+
+include "Coq.ma".
+
+(*#**********************************************************************)
+
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+
+(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
+
+(* \VV/ *************************************************************)
+
+(* // * This file is distributed under the terms of the *)
+
+(* * GNU Lesser General Public License Version 2.1 *)
+
+(*#**********************************************************************)
+
+(*i $Id: Peano.v,v 1.23 2003/11/29 17:28:30 herbelin Exp $ i*)
+
+(*#* Natural numbers [nat] built from [O] and [S] are defined in Datatypes.v *)
+
+(*#* This module defines the following operations on natural numbers :
+ - predecessor [pred]
+ - addition [plus]
+ - multiplication [mult]
+ - less or equal order [le]
+ - less [lt]
+ - greater or equal [ge]
+ - greater [gt]
+
+ This module states various lemmas and theorems about natural numbers,
+ including Peano's axioms of arithmetic (in Coq, these are in fact provable)
+ Case analysis on [nat] and induction on [nat * nat] are provided too *)
+
+include "Init/Notations.ma".
+
+include "Init/Datatypes.ma".
+
+include "Init/Logic.ma".
+
+(* UNEXPORTED
+Open Scope nat_scope.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/eq_S.con" as definition.
+
+(* UNEXPORTED
+Hint Resolve (f_equal S): v62.
+*)
+
+(* UNEXPORTED
+Hint Resolve (f_equal (A:=nat)): core.
+*)
+
+(*#* The predecessor function *)
+
+inline procedural "cic:/Coq/Init/Peano/pred.con" as definition.
+
+(* UNEXPORTED
+Hint Resolve (f_equal pred): v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/pred_Sn.con" as theorem.
+
+inline procedural "cic:/Coq/Init/Peano/eq_add_S.con" as theorem.
+
+(* UNEXPORTED
+Hint Immediate eq_add_S: core v62.
+*)
+
+(*#* A consequence of the previous axioms *)
+
+inline procedural "cic:/Coq/Init/Peano/not_eq_S.con" as theorem.
+
+(* UNEXPORTED
+Hint Resolve not_eq_S: core v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/IsSucc.con" as definition.
+
+inline procedural "cic:/Coq/Init/Peano/O_S.con" as theorem.
+
+(* UNEXPORTED
+Hint Resolve O_S: core v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/n_Sn.con" as theorem.
+
+(* UNEXPORTED
+Hint Resolve n_Sn: core v62.
+*)
+
+(*#* Addition *)
+
+inline procedural "cic:/Coq/Init/Peano/plus.con" as definition.
+
+(* UNEXPORTED
+Hint Resolve (f_equal2 plus): v62.
+*)
+
+(* UNEXPORTED
+Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+*)
+
+(* NOTATION
+Infix "+" := plus : nat_scope.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/plus_n_O.con" as lemma.
+
+(* UNEXPORTED
+Hint Resolve plus_n_O: core v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/plus_O_n.con" as lemma.
+
+inline procedural "cic:/Coq/Init/Peano/plus_n_Sm.con" as lemma.
+
+(* UNEXPORTED
+Hint Resolve plus_n_Sm: core v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/plus_Sn_m.con" as lemma.
+
+(*#* Multiplication *)
+
+inline procedural "cic:/Coq/Init/Peano/mult.con" as definition.
+
+(* UNEXPORTED
+Hint Resolve (f_equal2 mult): core v62.
+*)
+
+(* NOTATION
+Infix "*" := mult : nat_scope.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/mult_n_O.con" as lemma.
+
+(* UNEXPORTED
+Hint Resolve mult_n_O: core v62.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/mult_n_Sm.con" as lemma.
+
+(* UNEXPORTED
+Hint Resolve mult_n_Sm: core v62.
+*)
+
+(*#* Definition of subtraction on [nat] : [m-n] is [0] if [n>=m] *)
+
+inline procedural "cic:/Coq/Init/Peano/minus.con" as definition.
+
+(* NOTATION
+Infix "-" := minus : nat_scope.
+*)
+
+(*#* Definition of the usual orders, the basic properties of [le] and [lt]
+ can be found in files Le and Lt *)
+
+(*#* An inductive definition to define the order *)
+
+inline procedural "cic:/Coq/Init/Peano/le.ind".
+
+(* NOTATION
+Infix "<=" := le : nat_scope.
+*)
+
+(* UNEXPORTED
+Hint Constructors le: core v62.
+*)
+
+(*i equivalent to : "Hints Resolve le_n le_S : core v62." i*)
+
+inline procedural "cic:/Coq/Init/Peano/lt.con" as definition.
+
+(* UNEXPORTED
+Hint Unfold lt: core v62.
+*)
+
+(* NOTATION
+Infix "<" := lt : nat_scope.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/ge.con" as definition.
+
+(* UNEXPORTED
+Hint Unfold ge: core v62.
+*)
+
+(* NOTATION
+Infix ">=" := ge : nat_scope.
+*)
+
+inline procedural "cic:/Coq/Init/Peano/gt.con" as definition.
+
+(* UNEXPORTED
+Hint Unfold gt: core v62.
+*)
+
+(* NOTATION
+Infix ">" := gt : nat_scope.
+*)
+
+(* NOTATION
+Notation "x <= y <= z" := (x <= y /\ y <= z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
+*)
+
+(* NOTATION
+Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
+*)
+
+(*#* Pattern-Matching on natural numbers *)
+
+inline procedural "cic:/Coq/Init/Peano/nat_case.con" as theorem.
+
+(*#* Principle of double induction *)
+
+inline procedural "cic:/Coq/Init/Peano/nat_double_ind.con" as theorem.
+
+(*#* Notations *)
+
projects / helm.git / blobdiff