Arith's min and max placed in Peano (+basic specs max_l and co)

This allow for instance to remove the dependency of List.v toward Min.v
To prove max_l and co, we push Le.le_pred and Le.le_S_n into Peano.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12784 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 50 insertions, 0 deletions

diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 12a8f7a4b0..8779f2b452 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -201,6 +201,16 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
+Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
+Proof.
+induction 1; auto. destruct m; simpl; auto.
+Qed.
+
+Theorem le_S_n : forall n m, S n <= S m -> n <= m.
+Proof.
+intros n m. exact (le_pred (S n) (S m)).
+Qed.
+
 (** Case analysis *)
 
 Theorem nat_case :
@@ -220,3 +230,43 @@ Proof.
   induction n; auto.
   destruct m as [| n0]; auto.
 Qed.
+
+(** Maximum and minimum : definitions and specifications *)
+
+Fixpoint max n m : nat :=
+  match n, m with
+    | O, _ => m
+    | S n', O => n
+    | S n', S m' => S (max n' m')
+  end.
+
+Fixpoint min n m : nat :=
+  match n, m with
+    | O, _ => 0
+    | S n', O => 0
+    | S n', S m' => S (min n' m')
+  end.
+
+Theorem max_l : forall n m : nat, m <= n -> max n m = n.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem max_r : forall n m : nat, n <= m -> max n m = m.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem min_l : forall n m : nat, n <= m -> min n m = n.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.
+
+Theorem min_r : forall n m : nat, m <= n -> min n m = m.
+Proof.
+induction n; destruct m; simpl; auto. inversion 1.
+intros. apply f_equal. apply IHn. apply le_S_n. trivial.
+Qed.