From 4b993912cc6c6135e41ea959f934fa73d1da05ab Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 4 Oct 2009 10:05:11 +0000 Subject: Some new lemmas on max and min and a fix for a wrongly stated lemma in r12358. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12370 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rbasic_fun.v | 106 +++++++++++++++++++++++++++++++++----------- theories/ZArith/Zmax.v | 16 +++++++ theories/ZArith/Zmin.v | 12 +++++ 3 files changed, 108 insertions(+), 26 deletions(-) diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 08e6323ea..f5570286d 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -34,8 +34,14 @@ Definition Rmin (x y:R) : R := (*********) Lemma Rmin_case : forall r1 r2 (P:R -> Type), P r1 -> P r2 -> P (Rmin r1 r2). Proof. - intros r1 r2 P H1 H2; unfold Rmin in |- *; case (Rle_dec r1 r2); - auto with arith. + intros r1 r2 P H1 H2; unfold Rmin; case (Rle_dec r1 r2); auto. +Qed. + +(*********) +Lemma Rmin_case_strong : forall r1 r2 (P:R -> Type), + (r1 <= r2 -> P r1) -> (r2 <= r1 -> P r2) -> P (Rmin r1 r2). +Proof. + intros r1 r2 P H1 H2; unfold Rmin; destruct (Rle_dec r1 r2); auto with real. Qed. (*********) @@ -80,9 +86,33 @@ Proof. Qed. (*********) -Lemma Rmin_comm : forall a b:R, Rmin a b = Rmin b a. +Lemma Rmin_left : forall x y, x <= y -> Rmin x y = x. Proof. - intros; unfold Rmin in |- *; case (Rle_dec a b); case (Rle_dec b a); intros; + intros; apply Rmin_case_strong; auto using Rle_antisym. +Qed. + +(*********) +Lemma Rmin_right : forall x y, y <= x -> Rmin x y = y. +Proof. + intros; apply Rmin_case_strong; auto using Rle_antisym. +Qed. + +(*********) +Lemma Rle_min_compat_r : forall x y z, x <= y -> Rmin x z <= Rmin y z. +Proof. + intros; do 2 (apply Rmin_case_strong; intro); eauto using Rle_trans, Rle_refl. +Qed. + +(*********) +Lemma Rle_min_compat_l : forall x y z, x <= y -> Rmin z x <= Rmin z y. +Proof. + intros; do 2 (apply Rmin_case_strong; intro); eauto using Rle_trans, Rle_refl. +Qed. + +(*********) +Lemma Rmin_comm : forall x y:R, Rmin x y = Rmin y x. +Proof. + intros; unfold Rmin; case (Rle_dec x y); case (Rle_dec y x); intros; try reflexivity || (apply Rle_antisym; assumption || auto with real). Qed. @@ -100,15 +130,15 @@ Proof. Qed. (*********) -Lemma Rmin_glb : forall a b c:R, a <= b -> a <= c -> a <= Rmin b c. +Lemma Rmin_glb : forall x y z:R, z <= x -> z <= y -> z <= Rmin x y. Proof. - intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption. + intros; unfold Rmin in |- *; case (Rle_dec x y); intro; assumption. Qed. (*********) -Lemma Rmin_glb_lt : forall a b c:R, a < b -> a < c -> a < Rmin b c. +Lemma Rmin_glb_lt : forall x y z:R, z < x -> z < y -> z < Rmin x y. Proof. - intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption. + intros; unfold Rmin in |- *; case (Rle_dec x y); intro; assumption. Qed. (*******************************) @@ -125,8 +155,14 @@ Definition Rmax (x y:R) : R := (*********) Lemma Rmax_case : forall r1 r2 (P:R -> Type), P r1 -> P r2 -> P (Rmax r1 r2). Proof. - intros r1 r2 P H1 H2; unfold Rmax in |- *; case (Rle_dec r1 r2); - auto with arith. + intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto. +Qed. + +(*********) +Lemma Rmax_case_strong : forall r1 r2 (P:R -> Type), + (r2 <= r1 -> P r1) -> (r1 <= r2 -> P r2) -> P (Rmax r1 r2). +Proof. + intros r1 r2 P H1 H2; unfold Rmax; case (Rle_dec r1 r2); auto with real. Qed. (*********) @@ -141,17 +177,7 @@ Proof. apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)). Qed. -Lemma RmaxLess1 : forall r1 r2, r1 <= Rmax r1 r2. -Proof. - intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real. -Qed. - -Lemma RmaxLess2 : forall r1 r2, r2 <= Rmax r1 r2. -Proof. - intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real. -Qed. - -Lemma Rmax_comm : forall p q:R, Rmax p q = Rmax q p. +Lemma Rmax_comm : forall x y:R, Rmax x y = Rmax y x. Proof. intros p q; unfold Rmax in |- *; case (Rle_dec p q); case (Rle_dec q p); auto; intros H1 H2; apply Rle_antisym; auto with real. @@ -175,6 +201,35 @@ Proof. [ right; reflexivity | auto with real ]. Qed. +(* begin hide *) +Notation RmaxLess1 := Rmax_l (only parsing). +Notation RmaxLess2 := Rmax_r (only parsing). +(* end hide *) + +(*********) +Lemma Rmax_left : forall x y, y <= x -> Rmax x y = x. +Proof. + intros; apply Rmax_case_strong; auto using Rle_antisym. +Qed. + +(*********) +Lemma Rmax_right : forall x y, x <= y -> Rmax x y = y. +Proof. + intros; apply Rmax_case_strong; auto using Rle_antisym. +Qed. + +(*********) +Lemma Rle_max_compat_r : forall x y z, x <= y -> Rmax x z <= Rmax y z. +Proof. + intros; do 2 (apply Rmax_case_strong; intro); eauto using Rle_trans, Rle_refl. +Qed. + +(*********) +Lemma Rle_max_compat_l : forall x y z, x <= y -> Rmax z x <= Rmax z y. +Proof. + intros; do 2 (apply Rmax_case_strong; intro); eauto using Rle_trans, Rle_refl. +Qed. + (*********) Lemma RmaxRmult : forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q. @@ -198,15 +253,15 @@ Proof. Qed. (*********) -Lemma Rmax_lub : forall a b c:R, a <= b -> a <= c -> a <= Rmax b c. +Lemma Rmax_lub : forall x y z:R, x <= z -> y <= z -> Rmax x y <= z. Proof. - intros; unfold Rmax in |- *; case (Rle_dec b c); intro; assumption. + intros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed. (*********) -Lemma Rmax_lub_lt : forall a b c:R, a < b -> a < c -> a < Rmax b c. +Lemma Rmax_lub_lt : forall x y z:R, x < z -> y < z -> Rmax x y < z. Proof. - intros; unfold Rmax in |- *; case (Rle_dec b c); intro; assumption. + intros; unfold Rmax; case (Rle_dec x y); intro; assumption. Qed. (*********) @@ -216,7 +271,6 @@ Proof. case (Rle_dec x y); intro; assumption. Qed. - (*******************************) (** * Rabsolu *) (*******************************) diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v index b7911181f..07eca7765 100644 --- a/theories/ZArith/Zmax.v +++ b/theories/ZArith/Zmax.v @@ -67,14 +67,18 @@ Proof. intros; apply Zmax_case_strong; auto with zarith. Qed. +(* begin hide *) Notation Zmax1 := Zle_max_l (only parsing). +(* end hide *) Lemma Zle_max_r : forall n m:Z, m <= Zmax n m. Proof. intros; apply Zmax_case_strong; auto with zarith. Qed. +(* begin hide *) Notation Zmax2 := Zle_max_r (only parsing). +(* end hide *) Lemma Zmax_lub : forall n m p:Z, n <= p -> m <= p -> Zmax n m <= p. Proof. @@ -86,6 +90,18 @@ Proof. intros; apply Zmax_case; assumption. Qed. +(** * Compatibility with order *) + +Lemma Zle_max_compat_r : forall n m p, n <= m -> Zmax n p <= Zmax m p. +Proof. + intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl. +Qed. + +Lemma Zle_max_compat_l : forall n m p, n <= m -> Zmax p n <= Zmax p m. +Proof. + intros; do 2 (apply Zmax_case_strong; intro); eauto using Zle_trans, Zle_refl. +Qed. + (** * Semi-lattice properties of max *) Lemma Zmax_idempotent : forall n:Z, Zmax n n = n. diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v index dd35cd139..de83af137 100644 --- a/theories/ZArith/Zmin.v +++ b/theories/ZArith/Zmin.v @@ -80,6 +80,18 @@ Proof. intros; apply Zmin_case; assumption. Qed. +(** * Compatibility with order *) + +Lemma Zle_min_compat_r : forall n m p, n <= m -> Zmin n p <= Zmin m p. +Proof. + intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl. +Qed. + +Lemma Zle_min_compat_l : forall n m p, n <= m -> Zmin p n <= Zmin p m. +Proof. + intros; do 2 (apply Zmin_case_strong; intro); eauto using Zle_trans, Zle_refl. +Qed. + (** * Semi-lattice properties of min *) Lemma Zmin_idempotent : forall n:Z, Zmin n n = n. -- cgit v1.2.3