(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                 Peano.v                                  *)
(****************************************************************************)

(* 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 *)

Require Export Logic.
Require Export LogicSyntax.
Require Export Datatypes.

Theorem eq_S : (n,m:nat) n=m -> (S n)=(S m).
Proof.
 Intros; Apply (f_equal nat) ; Auto.
Qed.
Hint eq_S.

(* The predecessor function *)

Definition pred : nat->nat 
     := [n:nat](Cases n of O => O | (S u) => u end).

Theorem pred_Sn : (m:nat) m=(pred (S m)).
 Proof.
Auto.
Qed.

Theorem eq_add_S : (n,m:nat) (S n)=(S m) -> n=m.
Proof.
 Intros n m H ; Change (pred (S n))=(pred (S m)).
Apply (f_equal nat); Auto.
Qed.
Immediate eq_add_S.

(* A consequence of the previous axioms *)

Theorem not_eq_S : (n,m:nat) ~(n=m) -> ~((S n)=(S m)).
Proof.
 Red; Auto.
Qed.
Hint not_eq_S.

Definition IsSucc : nat->Prop
  := [n:nat]Cases n of O => False | (S p) => True end.


Theorem O_S : (n:nat)~(O=(S n)).
Proof.
Red;Intros n H.
Change (IsSucc O).
Elim (sym_eq nat O (S n));[Exact I | Assumption].
Qed.
Hint O_S.

Theorem n_Sn : (n:nat) ~(n=(S n)).
Proof.
 Induction n ; Auto.
Qed.
Hint n_Sn.

(*************************************************)
(*      Addition                                 *)
(*************************************************)

Fixpoint plus [n:nat] : nat -> nat := 
   [m:nat]Cases n of 
      O   => m 
  | (S p) => (S (plus p m)) end.

Lemma plus_n_O : (n:nat) n=(plus n O).
Proof.
 Induction n ; Simpl ; Auto.
Qed.
Hint plus_n_O.

Lemma plus_n_Sm : (n,m:nat) (S (plus n m))=(plus n (S m)).
Proof.
 Intros m n; Elim m; Simpl; Auto.
Qed.
Hint plus_n_Sm.

(***************************************)
(*      Multiplication                 *)
(***************************************)

Fixpoint  mult [n:nat] : nat -> nat := 
   [m:nat]Cases n of O => O 
               | (S p) => (plus m (mult p m)) end.

Lemma mult_n_O : (n:nat) O=(mult n O).
Proof.
 Induction n; Simpl; Auto.
Qed.
Hint mult_n_O.

Lemma mult_n_Sm : (n,m:nat) (plus (mult n m) n)=(mult n (S m)).
Proof.
 Intros; Elim n; Simpl; Auto.
 Intros p H; Case H; Elim plus_n_Sm; Apply eq_S.
 Pattern 1 3 m; Elim m; Simpl; Auto.
Qed.
Hint mult_n_Sm.

(***********************************************************************)
(* 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 *)

Inductive le [n:nat] : nat -> Prop
    := le_n : (le n n)
     | le_S : (m:nat)(le n m)->(le n (S m)).

Hint le_n le_S.

Definition lt := [n,m:nat](le (S n) m).
Hint Unfold lt.

Definition ge := [n,m:nat](le m n).
Hint Unfold ge.

Definition gt := [n,m:nat](lt m n).
Hint Unfold gt.

(*********************************************************)
(* Pattern-Matching on natural numbers                   *)
(*********************************************************)

Theorem nat_case : (n:nat)(P:nat->Prop)(P O)->((m:nat)(P (S m)))->(P n).
Proof.
 Induction n ; Auto.
Qed.

(**********************************************************)
(* Principle of double induction                          *)
(**********************************************************)

Theorem nat_double_ind : (R:nat->nat->Prop)
     ((n:nat)(R O n)) -> ((n:nat)(R (S n) O))
     -> ((n,m:nat)(R n m)->(R (S n) (S m)))
     -> (n,m:nat)(R n m).
Proof.
 Induction n; Auto.
 Induction m; Auto.
Qed.


(* $Id: Peano.v,v 1.10 1998/04/30 16:45:51 mohring Exp $ *)
