X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FInit%2FPeano.mma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FInit%2FPeano.mma;h=f23ce2532f2809f7eb95cc83753f5de3a69964d5;hb=29714797b01e0ac8c22e4df2827b1785a759f482;hp=0000000000000000000000000000000000000000;hpb=1fb0f39de8b87920d2f15f9e33929d372fa518dd;p=helm.git

diff --git a/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma b/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma
new file mode 100644
index 000000000..f23ce2532
--- /dev/null
+++ b/helm/software/matita/contribs/procedural/Coq/Init/Peano.mma
@@ -0,0 +1,244 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 *)
+