diff options
Diffstat (limited to 'theories/Reals/Rlogic.v')
| -rw-r--r-- | theories/Reals/Rlogic.v | 364 |
1 files changed, 135 insertions, 229 deletions
diff --git a/theories/Reals/Rlogic.v b/theories/Reals/Rlogic.v index 14dea1c6..07792942 100644 --- a/theories/Reals/Rlogic.v +++ b/theories/Reals/Rlogic.v @@ -1,261 +1,137 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** * This module proves some logical properties of the axiomatics of Reals +(** This module proves some logical properties of the axiomatic of Reals. -1. Decidablity of arithmetical statements from - the axiom that the order of the real numbers is decidable. - -2. Derivability of the archimedean "axiom" +- Decidability of arithmetical statements. +- Derivability of the Archimedean "axiom". +- Decidability of negated formulas. *) -(** 1- Proof of the decidablity of arithmetical statements from -excluded middle and the axiom that the order of the real numbers is -decidable. *) +Require Import RIneq. -(** Assuming a decidable predicate [P n], A series is constructed whose -[n]th term is 1/2^n if [P n] holds and 0 otherwise. This sum reaches 2 -only if [P n] holds for all [n], otherwise the sum is less than 2. -Comparing the sum to 2 decides if [forall n, P n] or [~forall n, P n] *) +(** * Decidability of arithmetical statements *) (** One can iterate this lemma and use classical logic to decide any statement in the arithmetical hierarchy. *) -(** Contributed by Cezary Kaliszyk and Russell O'Connor *) - -Require Import ConstructiveEpsilon. -Require Import Rfunctions. -Require Import PartSum. -Require Import SeqSeries. -Require Import RiemannInt. -Require Import Fourier. - Section Arithmetical_dec. Variable P : nat -> Prop. Hypothesis HP : forall n, {P n} + {~P n}. -Let ge_fun_sums_ge_lemma : (forall (m n : nat) (f : nat -> R), (lt m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n). -Proof. -intros m n f mn fpos. -replace (sum_f_R0 f m) with (sum_f_R0 f m + 0) by ring. -rewrite (tech2 f m n mn). -apply Rplus_le_compat_l. - induction (n - S m)%nat; simpl in *. - apply fpos. -replace 0 with (0 + 0) by ring. -apply (Rplus_le_compat _ _ _ _ IHn0 (fpos (S (m + S n0)%nat))). -Qed. - -Let ge_fun_sums_ge : (forall (m n : nat) (f : nat -> R), (le m n) -> (forall i : nat, 0 <= f i) -> sum_f_R0 f m <= sum_f_R0 f n). -Proof. -intros m n f mn pos. - elim (le_lt_or_eq _ _ mn). - intro; apply ge_fun_sums_ge_lemma; assumption. -intro H; rewrite H; auto with *. -Qed. - -Let f:=fun n => (if HP n then (1/2)^n else 0)%R. - -Lemma cauchy_crit_geometric_dec_fun : Cauchy_crit_series f. +Lemma sig_forall_dec : {n | ~P n} + {forall n, P n}. Proof. -intros e He. -assert (X:(Pser (fun n:nat => 1) (1/2) (/ (1 - (1/2))))%R). - apply GP_infinite. - apply Rabs_def1; fourier. -assert (He':e/2 > 0) by fourier. -destruct (X _ He') as [N HN]. -clear X. -exists N. -intros n m Hn Hm. -replace e with (e/2 + e/2)%R by field. -set (g:=(fun n0 : nat => 1 * (1 / 2) ^ n0)) in *. -assert (R_dist (sum_f_R0 g n) (sum_f_R0 g m) < e / 2 + e / 2). - apply Rle_lt_trans with (R_dist (sum_f_R0 g n) 2+R_dist 2 (sum_f_R0 g m))%R. - apply R_dist_tri. - replace (/(1 - 1/2)) with 2 in HN by field. - cut (forall n, (n >= N)%nat -> R_dist (sum_f_R0 g n) 2 < e/2)%R. - intros Z. - apply Rplus_lt_compat. - apply Z; assumption. - rewrite R_dist_sym. - apply Z; assumption. - clear - HN He. - intros n Hn. - apply HN. - auto. -eapply Rle_lt_trans;[|apply H]. -clear -ge_fun_sums_ge n. -cut (forall n m, (m <= n)%nat -> R_dist (sum_f_R0 f n) (sum_f_R0 f m) <= R_dist (sum_f_R0 g n) (sum_f_R0 g m)). - intros H. - destruct (le_lt_dec m n). - apply H; assumption. - rewrite R_dist_sym. - rewrite (R_dist_sym (sum_f_R0 g n)). - apply H; auto with *. -clear n m. -intros n m Hnm. -unfold R_dist. -cut (forall i : nat, (1 / 2) ^ i >= 0). intro RPosPow. -rewrite Rabs_pos_eq. - rewrite Rabs_pos_eq. - cut (sum_f_R0 g m - sum_f_R0 f m <= sum_f_R0 g n - sum_f_R0 f n). - intros; fourier. - do 2 rewrite <- minus_sum. - apply (ge_fun_sums_ge m n (fun i : nat => g i - f i) Hnm). - intro i. - unfold f, g. - elim (HP i); intro; ring_simplify; auto with *. - cut (sum_f_R0 g m <= sum_f_R0 g n). - intro; fourier. - apply (ge_fun_sums_ge m n g Hnm). - intro. unfold g. - ring_simplify. - apply Rge_le. - apply RPosPow. - cut (sum_f_R0 f m <= sum_f_R0 f n). - intro; fourier. - apply (ge_fun_sums_ge m n f Hnm). - intro; unfold f. - elim (HP i); intro; simpl. - apply Rge_le. - apply RPosPow. - auto with *. -intro i. -apply Rle_ge. -apply pow_le. -fourier. -Qed. - -Lemma forall_dec : {forall n, P n} + {~forall n, P n}. -Proof. -destruct (cv_cauchy_2 _ cauchy_crit_geometric_dec_fun). - cut (2 <= x <-> forall n : nat, P n). - intro H. - elim (Rle_dec 2 x); intro X. - left; tauto. - right; tauto. -assert (A:Rabs(1/2) < 1) by (apply Rabs_def1; fourier). -assert (A0:=(GP_infinite (1/2) A)). -symmetry. - split; intro. - replace 2 with (/ (1 - (1 / 2))) by field. - unfold Pser, infinite_sum in A0. - eapply Rle_cv_lim;[|unfold Un_cv; apply A0 |apply u]. - intros n. - clear -n H. - induction n; unfold f;simpl. - destruct (HP 0); auto with *. - elim n; auto. - apply Rplus_le_compat; auto. - destruct (HP (S n)); auto with *. - elim n0; auto. -intros n. -destruct (HP n); auto. -elim (RIneq.Rle_not_lt _ _ H). -assert (B:0< (1/2)^n). - apply pow_lt. - fourier. -apply Rle_lt_trans with (2-(1/2)^n);[|fourier]. -replace (/(1-1/2))%R with 2 in A0 by field. -set (g:= fun m => if (eq_nat_dec m n) then (1/2)^n else 0). -assert (Z: Un_cv (fun N : nat => sum_f_R0 g N) ((1/2)^n)). - intros e He. - exists n. - intros a Ha. - replace (sum_f_R0 g a) with ((1/2)^n). - rewrite (R_dist_eq); assumption. - symmetry. - cut (forall a : nat, ((a >= n)%nat -> sum_f_R0 g a = (1 / 2) ^ n) /\ ((a < n)%nat -> sum_f_R0 g a = 0))%R. - intros H0. - destruct (H0 a). - auto. - clear - g. - induction a. - split; - intros H; - simpl; unfold g; - destruct (eq_nat_dec 0 n) as [t|f]; try reflexivity. - elim f; auto with *. - exfalso; omega. - destruct IHa as [IHa0 IHa1]. - split; - intros H; - simpl; unfold g at 2; - destruct (eq_nat_dec (S a) n). - rewrite IHa1. - ring. - omega. - ring_simplify. - apply IHa0. - omega. - exfalso; omega. - ring_simplify. - apply IHa1. - omega. -assert (C:=CV_minus _ _ _ _ A0 Z). -eapply Rle_cv_lim;[|apply u |apply C]. -clear - n0 B. -intros m. -simpl. -induction m. - simpl. - unfold f, g. - destruct (eq_nat_dec 0 n). - destruct (HP 0). - elim n0. - congruence. - clear -n. - induction n; simpl; fourier. - destruct (HP); simpl; fourier. -cut (f (S m) <= 1 * ((1 / 2) ^ (S m)) - g (S m)). - intros L. - eapply Rle_trans. +assert (Hi: (forall n, 0 < INR n + 1)%R). + intros n. + apply Rle_lt_0_plus_1, pos_INR. +set (u n := (if HP n then 0 else / (INR n + 1))%R). +assert (Bu: forall n, (u n <= 1)%R). + intros n. + unfold u. + case HP ; intros _. + apply Rle_0_1. + rewrite <- S_INR, <- Rinv_1. + apply Rinv_le_contravar with (1 := Rlt_0_1). + apply (le_INR 1), le_n_S, le_0_n. +set (E y := exists n, y = u n). +destruct (completeness E) as [l [ub lub]]. + exists R1. + intros y [n ->]. + apply Bu. + exists (u O). + now exists O. +assert (Hnp: forall n, not (P n) -> ((/ (INR n + 1) <= l)%R)). + intros n Hp. + apply ub. + exists n. + unfold u. + now destruct (HP n). +destruct (Rle_lt_dec l 0) as [Hl|Hl]. + right. + intros n. + destruct (HP n) as [H|H]. + exact H. + exfalso. + apply Rle_not_lt with (1 := Hl). + apply Rlt_le_trans with (/ (INR n + 1))%R. + now apply Rinv_0_lt_compat. + now apply Hnp. +left. +set (N := Zabs_nat (up (/l) - 2)). +assert (H1l: (1 <= /l)%R). + rewrite <- Rinv_1. + apply Rinv_le_contravar with (1 := Hl). + apply lub. + now intros y [m ->]. +assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). + unfold N. + rewrite INR_IZR_INZ. + rewrite inj_Zabs_nat. + replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R. + apply (f_equal (fun v => IZR v + 1)%R). + apply Zabs_eq. + apply Zle_minus_le_0. + apply (Zlt_le_succ 1). + apply lt_IZR. + apply Rle_lt_trans with (1 := H1l). + apply archimed. + rewrite minus_IZR. simpl. - apply Rplus_le_compat. - apply IHm. - apply L. - simpl; fourier. -unfold f, g. -destruct (eq_nat_dec (S m) n). - destruct (HP (S m)). - elim n0. - congruence. - rewrite e. - fourier. -destruct (HP (S m)). - fourier. + ring. +assert (Hl': (/ (INR (S N) + 1) < l)%R). + rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. + apply Rinv_1_lt_contravar with (1 := H1l). + rewrite S_INR. + rewrite HN. + ring_simplify. + apply archimed. +exists N. +intros H. +apply Rle_not_lt with (2 := Hl'). +apply lub. +intros y [n ->]. +unfold u. +destruct (HP n) as [_|Hp]. + apply Rlt_le. + now apply Rinv_0_lt_compat. +apply Rinv_le_contravar. +apply Hi. +apply Rplus_le_compat_r. +apply le_INR. +destruct (le_or_lt n N) as [Hn|Hn]. + 2: now apply lt_le_S. +exfalso. +destruct (le_lt_or_eq _ _ Hn) as [Hn'| ->]. +2: now apply Hp. +apply Rlt_not_le with (2 := Hnp _ Hp). +rewrite <- (Rinv_involutive l) by now apply Rgt_not_eq. +apply Rinv_1_lt_contravar. +rewrite <- S_INR. +apply (le_INR 1), le_n_S, le_0_n. +apply Rlt_le_trans with (INR N + 1)%R. +apply Rplus_lt_compat_r. +now apply lt_INR. +rewrite HN. +apply Rplus_le_reg_r with (-/l + 1)%R. ring_simplify. -apply pow_le. -fourier. -Qed. - -Lemma sig_forall_dec : {n | ~P n}+{forall n, P n}. -Proof. -destruct forall_dec. - right; assumption. -left. -apply constructive_indefinite_ground_description_nat; auto. - clear - HP. - firstorder. -apply Classical_Pred_Type.not_all_ex_not. -assumption. +apply archimed. Qed. End Arithmetical_dec. -(** 2- Derivability of the Archimedean axiom *) +(** * Derivability of the Archimedean axiom *) -(* This is a standard proof (it has been taken from PlanetMath). It is +(** This is a standard proof (it has been taken from PlanetMath). It is formulated negatively so as to avoid the need for classical -logic. Using a proof of {n | ~P n}+{forall n, P n} (the one above or a -variant of it that does not need classical axioms) , we can in -principle also derive [up] and its [specification] *) +logic. Using a proof of [{n | ~P n}+{forall n, P n}], we can in +principle also derive [up] and its specification. The proof above +cannot be used for that purpose, since it relies on the [archimed] axiom. *) Theorem not_not_archimedean : forall r : R, ~ (forall n : nat, (INR n <= r)%R). @@ -296,3 +172,33 @@ rewrite (Rplus_comm (INR n) 0) in H6. rewrite Rplus_0_l in H6. assumption. Qed. + +(** * Decidability of negated formulas *) + +Lemma sig_not_dec : forall P : Prop, {not (not P)} + {not P}. +Proof. +intros P. +set (E := fun x => x = R0 \/ (x = R1 /\ P)). +destruct (completeness E) as [x H]. + exists R1. + intros x [->|[-> _]]. + apply Rle_0_1. + apply Rle_refl. + exists R0. + now left. +destruct (Rle_lt_dec 1 x) as [H'|H']. +- left. + intros HP. + elim Rle_not_lt with (1 := H'). + apply Rle_lt_trans with (2 := Rlt_0_1). + apply H. + intros y [->|[_ Hy]]. + apply Rle_refl. + now elim HP. +- right. + intros HP. + apply Rlt_not_le with (1 := H'). + apply H. + right. + now split. +Qed. |