Max.v

(***************************************************************************                  The Calculus of Inductive Constructions                                                                                                                              Projet Coq                                                                                                                                 INRIA        LRI-CNRS        ENS-CNRS                               Rocquencourt         Orsay          Lyon                                                                                                                                 Coq V6.2                                                                 May 1st 1998                                                                                                           **************************************************************************                                   Min.v                                    ***************************************************************************)
Require Export Arith.
(* maximum of two natural numbers *)

Fixpoint max[n:nat]: nat ->nat :=
   [m:nat]
      Cases n m of
          O _ => m
         | _ O => n
         | (S n') (S m') => (S (max n' m'))
      end.

Lemma max_SS: (n, m:nat)(S (max n m))=(max (S n) (S m)).
Proof.
Auto.
Qed.

Lemma max_0_n : (n:nat)(max O n)=n.
Intros;Case n;Auto.
Qed.
Hint max_0_n.

Lemma max_sym: (n, m:nat)(max n m)=(max m n).
Induction n; Induction m; Simpl; Auto.
Qed.
Hint max_SS.

Lemma max_incr_l: (n, m:nat)(le (max n m) (max (S n) m)).
Induction n.
Intro m; Case m.
Simpl; Auto.
Intro m0; Case m0; Simpl; Auto.
Intros; Case m.
Simpl; Auto.
Intro m0; Repeat Rewrite <- max_SS; Auto.
Qed.

Lemma max_incr_r: (n, m:nat)(le (max n m) (max n (S m))).
Intros.
Rewrite (max_sym n (S m)).
Rewrite (max_sym n m).
Apply max_incr_l.
Qed.
Hint max_incr_l max_incr_r.

Lemma le_max_l: (n, m:nat)(le n (max n m)).
Proof.
Induction n; Intros; Simpl; Auto.
Elim m; Intros; Simpl; Auto.
Qed.
Hint le_max_l.

Lemma le_max_r: (n, m:nat)(le m (max n m)).
Proof.
Induction n; Intros; Simpl; Auto.
Elim m; Intros; Simpl; Auto.
Case m; Simpl; Auto.
Qed.
Hint le_max_r.
(* max n m is equal to n or m *)

Lemma max_case: (n, m:nat) (P:nat ->Set) (P n) -> (P m) ->(P (max n m)).
Proof.
Induction n; Auto.
Induction m; Intros; Simpl; Auto.
Induction m; Intros; Auto.
Rewrite <- max_SS; Auto.
Apply (H n1 [n:nat](P (S n))); Auto.
Qed.

Lemma max_case_Prop: (n, m:nat) (P:nat ->Prop) (P n) -> (P m) ->(P (max n m)).
Induction n; Auto.
Induction m; Intros; Simpl; Auto.
Induction m; Intros; Auto.
Rewrite <- max_SS; Auto.
Apply (H n1 [n:nat](P (S n))); Auto.
Qed.

14/09/98, 09:21