diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/Diaconescu.v | 9 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 3 | ||||
| -rw-r--r-- | theories/Reals/Rpower.v | 25 |
3 files changed, 25 insertions, 12 deletions
diff --git a/theories/Logic/Diaconescu.v b/theories/Logic/Diaconescu.v index c124e7141..6a1c88341 100644 --- a/theories/Logic/Diaconescu.v +++ b/theories/Logic/Diaconescu.v @@ -40,6 +40,7 @@ [[Carlström04]] Jesper Carlström, EM + Ext_ + AC_int is equivalent to AC_ext, Mathematical Logic Quaterly, vol 50(3), pp 236-240, 2004. *) +Require ClassicalFacts ChoiceFacts. (**********************************************************************) (** * Pred. Ext. + Rel. Axiom of Choice -> Excluded-Middle *) @@ -54,7 +55,7 @@ Definition PredicateExtensionality := (** From predicate extensionality we get propositional extensionality hence proof-irrelevance *) -Require Import ClassicalFacts. +Import ClassicalFacts. Variable pred_extensionality : PredicateExtensionality. @@ -76,7 +77,7 @@ Qed. (** From proof-irrelevance and relational choice, we get guarded relational choice *) -Require Import ChoiceFacts. +Import ChoiceFacts. Variable rel_choice : RelationalChoice. @@ -89,7 +90,7 @@ Qed. (** The form of choice we need: there is a functional relation which chooses an element in any non empty subset of bool *) -Require Import Bool. +Import Bool. Lemma AC_bool_subset_to_bool : exists R : (bool -> Prop) -> bool -> Prop, @@ -161,6 +162,8 @@ End PredExt_RelChoice_imp_EM. Section ProofIrrel_RelChoice_imp_EqEM. +Import ChoiceFacts. + Variable rel_choice : RelationalChoice. Variable proof_irrelevance : forall P:Prop , forall x y:P, x=y. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 7bcd2799a..bc82c3712 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1611,6 +1611,9 @@ Proof. Qed. Hint Resolve mult_INR: real. +Lemma pow_INR (m n: nat) : INR (m ^ n) = pow (INR m) n. +Proof. now induction n as [|n IHn];[ | simpl; rewrite mult_INR, IHn]. Qed. + (*********) Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n. Proof. diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a646104cd..301fe20b0 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -431,9 +431,9 @@ Proof. Qed. Theorem Rpower_lt : - forall x y z:R, 1 < x -> 0 <= y -> y < z -> x ^R y < x ^R z. + forall x y z:R, 1 < x -> y < z -> x ^R y < x ^R z. Proof. - intros x y z H H0 H1. + intros x y z H H1. unfold Rpower. apply exp_increasing. apply Rmult_lt_compat_r. @@ -488,11 +488,13 @@ Proof. Qed. Theorem Rle_Rpower : - forall e n m:R, 1 < e -> 0 <= n -> n <= m -> e ^R n <= e ^R m. + forall e n m:R, 1 <= e -> n <= m -> e ^R n <= e ^R m. Proof. - intros e n m H H0 H1; case H1. - intros H2; left; apply Rpower_lt; assumption. - intros H2; rewrite H2; right; reflexivity. + intros e n m [H | H]; intros H1. + case H1. + intros H2; left; apply Rpower_lt; assumption. + intros H2; rewrite H2; right; reflexivity. + now rewrite <- H; unfold Rpower; rewrite ln_1, !Rmult_0_r; apply Rle_refl. Qed. Theorem ln_lt_2 : / 2 < ln 2. @@ -707,13 +709,18 @@ intros x y z x0 y0; unfold Rpower. rewrite <- exp_plus, ln_mult, Rmult_plus_distr_l; auto. Qed. -Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> Rpower a c <= Rpower b c. +Lemma Rlt_Rpower_l a b c: 0 < c -> 0 < a < b -> a ^R c < b ^R c. +Proof. +intros c0 [a0 ab]; apply exp_increasing. +now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. +Qed. + +Lemma Rle_Rpower_l a b c: 0 <= c -> 0 < a <= b -> a ^R c <= b ^R c. Proof. intros [c0 | c0]; [ | intros; rewrite <- c0, !Rpower_O; [apply Rle_refl | |] ]. intros [a0 [ab|ab]]. - left; apply exp_increasing. - now apply Rmult_lt_compat_l; auto; apply ln_increasing; fourier. + now apply Rlt_le, Rlt_Rpower_l;[ | split]; fourier. rewrite ab; apply Rle_refl. apply Rlt_le_trans with a; tauto. tauto. |