# Library Coqtail.Reals.Reirr

Section eirr.
Require Import Max.

Require Import Rseries_facts.
Require Import Rsequence_facts.
Require Import Rsequence_subsequence.
Require Import Rpser_usual.
Require Import Reals.
Require Import Rsequence_tactics.
Require Import Rtactic.

Require Import Fourier.

Open Scope R_scope.

Definition e := exp 1.

Definition partial_e n := sum_f_R0 (fun n/INR (fact n)) n.

Lemma sum_integer_INR_div : n, {m |
sum_f_R0 (fun i : nat/ INR (fact i) × INR (fact n)) n = INR m}.
Proof.
induction n.
1%nat. simpl. field.

destruct IHn as (m1, Hm1).
rewrite tech5. rewrite fact_simpl. rewrite mult_INR.
(S n × m1 + 1)%nat.
rewrite <- scal_sum.
rewrite <- scal_sum in Hm1. rewrite Rmult_assoc. rewrite Hm1.
rewrite plus_INR. rewrite mult_INR. do 2 rewrite S_INR. simpl.
field.

split.
apply INR_fact_neq_0.
assert (INR n 0) by intuition ; intro H1 ; fourier.
Qed.

Lemma integer_exp_minus_sum : a b : nat,
b Oe = INR a / INR b
{n | INR (fact b) × (e - partial_e b) = IZR n}.
Proof.
intros a b Hb0 Habs.
rewrite Habs.
rewrite Rmult_minus_distr_l.
unfold partial_e.
rewrite scal_sum.
unfold Rdiv. rewrite Rmult_comm. rewrite Rmult_assoc.
rewrite (integer_INR_div b Hb0).
destruct (sum_integer_INR_div b) as (m1, Hm1).
rewrite Hm1.
(Z_of_nat a × Z_of_nat (fact (b-1)) - Z_of_nat m1)%Z.
unfold Zminus. rewrite plus_IZR. rewrite mult_IZR.
rewrite Ropp_Ropp_IZR. repeat rewrite <- INR_IZR_INZ.
ring.
Qed.

Lemma sum_max : b N f,
( n, f n > 0) → (sum_f_R0 f b <
sum_f_R0 f (max N (S b))).
Proof.
intros b N f Hpos.
assert (b < max N (S b))%nat by intuition.
induction H.
replace (sum_f_R0 f b) with (sum_f_R0 f b + 0) by ring.
simpl. apply Rplus_le_lt_compat.
right. reflexivity.

apply Hpos.
simpl.
replace (sum_f_R0 f b) with (sum_f_R0 f b + 0) by ring.
apply Rplus_le_lt_compat.
left. apply IHle.

apply Hpos.
Qed.

Lemma inv_INR_fact_pos : n, (/INR (fact n)) > 0.
Proof.
intros n.
assert (INR (fact n) > 0).
induction n.
simpl. fourier.

simpl. rewrite plus_INR. replace 0 with (0 + 0) by intuition.
apply Rplus_gt_ge_compat. apply IHn. intuition.
apply Rinv_0_lt_compat. intuition.
Qed.

Lemma Rminus_lt_plus : a b c, a - b < ca < b + c.
Proof.
intros.
fourier.
Qed.

Lemma Rplus_lt_minus : a b c, a < b + ca - b < c.
Proof.
intros.
fourier.
Qed.

Lemma sum_max1 : N b f,
( n, f n 0) →
sum_f_R0 f (max N (S b))
sum_f_R0 f (S b).
Proof.
intros N b f Hpos.
assert (H : (S b max N (S b))%nat) by intuition.
induction H.
intuition.

rewrite tech5.
replace (sum_f_R0 f (S b)) with (sum_f_R0 f (S b) + 0) by ring.
apply Rplus_ge_compat. apply IHle. apply Hpos.
Qed.

Lemma minus_exp_sum_pos : a b : nat,
b O
INR (fact b) × (e - partial_e b) > 0.
Proof.
intros a b Hb0.
unfold e, partial_e, exp.
destruct (exist_exp 1) as (y, Hexp). unfold exp_in in ×. simpl.
apply Rmult_gt_0_compat ; [apply INR_fact_lt_0|].
unfold infinite_sum in Hexp.
assert (H : y sum_f_R0 (fun n : nat/ INR (fact n)) bFalse).
intro Habs.
assert (H1 : /INR (fact (S b)) > 0) by (apply inv_INR_fact_pos).
generalize (Hexp (/INR (fact (S b))) H1) ; clear Hexp ; intro Hexp.
destruct Hexp as (N, Hexp).
assert (Hmax : ((max N (S b)) N)%nat). intuition.
generalize (Hexp (max N (S b)) Hmax). clear Hexp. intros Hexp.
unfold R_dist in ×. unfold Rabs in ×.
replace (sum_f_R0 (fun i : nat/ INR (fact i) × 1 ^ i) (max N (S b)))
with (sum_f_R0 (fun n : nat/ INR (fact n)) (max N (S b))) in × by
(apply Rseq_sum_ext ; intros n; rewrite pow1; ring).
destruct (Rcase_abs (sum_f_R0 (fun i : nat/ INR (fact i)) (max N (S b)) - y)) as [H|H].
apply Rle_minus in Habs.
assert (sum_f_R0 (fun n : nat/ INR (fact n)) b - y <
sum_f_R0 (fun i : nat/ INR (fact i)) (max N (S b)) - y).
unfold Rminus. apply Rplus_lt_compat_r.
apply sum_max. intuition. apply inv_INR_fact_pos.

fourier.

apply Rminus_lt_plus in Hexp.
apply (Rplus_le_compat_r (/ INR (fact (S b)))) in Habs.
assert (sum_f_R0 (fun i : nat/ INR (fact i)) (max N (S b))
sum_f_R0 (fun n : nat/ INR (fact n)) b + / INR (fact (S b))).
rewrite <- tech5. apply sum_max1. intros. left. apply inv_INR_fact_pos.
assert (H2 : (sum_f_R0 (fun i : nat/ INR (fact i)) (max N (S b)) <
sum_f_R0 (fun n : nat/ INR (fact n)) b + / INR (fact (S b)))).
eapply Rlt_le_trans. apply Hexp. apply Habs.
apply Rlt_not_ge in H2. apply H2.
assumption.

apply Rgt_minus. apply Rlt_gt.
apply Rfourier_not_le_gt. assumption.
Qed.

Lemma geometric_sum : (k:R),
Rabs k < 1 → infinite_sum (fun i:natk ^ i) (1 / (1 - k)).
Proof.
intros k H0k1.
intros eps Heps.
assert (Hpos : 0 < eps × (1 - k)).
apply Rmult_lt_0_compat ; [apply Heps |].
unfold Rabs in ×. destruct (Rcase_abs k) ; fourier.
destruct (pow_lt_1_zero k H0k1 (eps × (1 - k)) Hpos) as (N, HN).
N.
intros n Hn.
rewrite tech3.
unfold R_dist, Rdiv.
field_simplify ((1 - k ^ S n) × / (1 - k) - 1 × / (1 - k)).
rewrite Rabs_div. rewrite Rabs_Ropp. unfold Rabs. destruct (Rcase_abs (-k + 1)) as [H|[H|H]].
assert (H1 : (N N)%nat) by intuition. generalize (HN N H1). intros.
assert (eps × (1 - k) < 0). replace 0 with (eps × 0) by intuition.
apply Rmult_lt_compat_l. apply Heps. fourier. fourier.
replace eps with (eps × (1 - k) × / (-k + 1)).
unfold Rdiv. apply Rmult_lt_compat_r.
apply Rinv_0_lt_compat. fourier.

apply HN. intuition. field. intros H3. fourier.

unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; fourier.
intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; fourier.
intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; fourier.
intro H2. unfold Rabs in H0k1 ; destruct (Rcase_abs k) ; fourier.
Qed.

Lemma exp_remain_sum : n,
n OINR (fact n) × (e - partial_e n) < 1 / INR n.
Proof.
intros b Hb0.
unfold partial_e, e, exp.
destruct (exist_exp 1) as (x, Hexp). simpl.
unfold exp_in in ×.
assert (Hgeom : (infinite_sum (fun i(/INR (S b)) ^ i) (1 / (1 - /INR (S b))))).
apply (geometric_sum (/INR (S b))).
unfold Rabs. destruct (Rcase_abs (/INR (S b))) as [H1|[H1|H1]].
assert (H : (- /INR (S b) < 0 )) by intuition.
eapply (Rlt_trans) ; [apply H|intuition].

replace 1 with (/1) by intuition.
apply Rinv_lt_contravar.
rewrite Rmult_1_l. intuition.

destruct b.
destruct Hb0. reflexivity.

rewrite S_INR. assert (INR (S b) > 0) by intuition. fourier.

rewrite H1. fourier.

assert (He : (infinite_sum (fun i : nat/ INR (fact i)) x)).
intros eps Heps. destruct (Hexp eps Heps) as (N, Hexp1).
N. intros n Hn. generalize (Hexp1 n Hn). intros H1.
assert (Hrew : (sum_f_R0 (fun i : nat/ INR (fact i) × 1 ^ i) n =
sum_f_R0 (fun i : nat/ INR (fact i)) n)).
apply sum_eq. intros. rewrite pow1. intuition.

rewrite <- Hrew. apply H1. clear Hexp.

pose (Un := fun n : nat/ INR (fact (n))).
pose (UUn := fun n : natUn (S b + n)%nat).
assert (Hluu : Rser_cv UUn (x - sum_f_R0 Un b)).
apply (Rser_cv_shifts b Un). assumption.

assert (Hlu : Rser_cv Un x). apply He.

assert (HRser : Rser_cv (fun kUn (S b+ k)%nat) (Rser_rem Un x Hlu b)).
apply (Rser_rem_cv Un).

assert (Rser_cv Un (Rser_rem Un x Hlu b + sum_f_R0 Un b)).
apply Rser_cv_shifts_rev. assumption.

assert (H1 : (x = Rser_rem Un x Hlu b + sum_f_R0 Un b)).
apply Rser_cv_unique with Un ; assumption.

rewrite H1. unfold Un. ring_simplify.
assert (Hlmachin : Rser_cv Un x). intuition.

apply Rser_cv_scal_compat_l with Un x (INR (fact b)) in Hlmachin.
fold Un. apply Rle_lt_trans with ((INR (fact b) × Rser_rem Un x Hlu)%Rseq b).
reflexivity. rewrite <- (Rser_rem_scal_compat_l Un x (INR (fact b)) Hlmachin).

pose (Vn := (fun n0 : natINR (fact b) × / INR (fact n0) )).
assert (Hlv : (Rser_cv Vn (INR (fact b) × x))).
unfold Vn. apply Rser_cv_scal_compat_l. assumption.

unfold Un. fold Vn.
pose (Wn := (fun i : nat/(INR (S b)) × (/ INR (S b)) ^ i)).
assert (Hlw : Rser_cv Wn (( /INR (S b) *(1/ (1 - / INR (S b)))))).
unfold Wn. apply Rser_cv_scal_compat_l.
apply Rser_cv_ext with (fun i : nat(/ INR (S b)) ^ i).
intro ; reflexivity.

apply Hgeom.

eapply Rlt_le_trans with (/ INR (S b) × (1 / (1 - / INR (S b)))).
apply (Rser_Rser_rem_lt_le Wn Vn _ _ _ _).
intros k Hkn.
unfold Vn, Wn. apply identite. assumption.

(S (S b)). intuition. unfold Vn, Wn. apply identite1.

apply Hlw.

field_simplify.
replace (INR (S b) - 1) with (INR b). right. reflexivity.

rewrite S_INR. ring.

intuition.

split.
apply not_0_INR.
intuition.

rewrite S_INR. unfold Rminus. rewrite Rplus_assoc.
intro H2. ring_simplify in H2. intuition.
Qed.

Lemma inv_inf_1 : x, x 0%nat/INR x 1.
Proof.
intros x Hx0.
assert (H : (INR x > 0)) by intuition.
assert (H1 : (INR x 1)).
induction x.
destruct Hx0. reflexivity.

replace 1 with (0 + 1) by intuition. rewrite S_INR.
apply Rplus_ge_compat. intuition. intuition.

rewrite <- Rinv_1.
apply Rle_Rinv. fourier. assumption.
intuition.
Qed.

Lemma minus_exp_sum_one : a b : nat,
b 0%nate = INR a / INR b
INR (fact b) × (e - partial_e b) < 1.
Proof.
intros a b Hb0 Habs.
eapply Rlt_le_trans.
apply exp_remain_sum. assumption.

unfold Rdiv. rewrite Rmult_1_l. apply inv_inf_1. assumption.
Qed.

Lemma integer_0_1 : x, 0 < IZR x < 1 → False.
Proof.
destruct x ; intros H.
intuition. simpl in ×. fourier.

simpl in ×.
induction (nat_of_P p).
simpl in ×. destruct H. fourier.

assert (INR (S n) 1). destruct n. simpl. right. reflexivity. intuition.
destruct H. fourier.

assert (IZR (Zneg p) 0). simpl. intuition.
destruct H. fourier.
Qed.

Lemma eirr : a b, b 0%nate = (INR a) / (INR b)False.
Proof.
intros a b Hb0 Habs.
pose (x := INR (fact b) × (e - partial_e b)).
assert (0 < x < 1).
split.
unfold x. apply (minus_exp_sum_pos a) ; intuition.

unfold x. apply (minus_exp_sum_one a) ; intuition.

destruct (integer_exp_minus_sum a b Hb0 Habs) as (m, Hm).
unfold x in ×.
rewrite Hm in H.
apply (integer_0_1 m). assumption.
Qed.

# Final result: e is irrational

Lemma e_is_irrational : (a : Z) (b : nat),
b Oe = (IZR a) / (INR b)False.
Proof.
intros [|a|a] b Hb He.
refine (eirr O b Hb _).
simpl in He; assumption.

refine (eirr (nat_of_P a) b Hb _).
simpl in He; assumption.

unfold IZR, e in ×.
assert (0 < INR (nat_of_P a) / INR b) by
(apply Rlt_mult_inv_pos; auto with real; INR_solve).
pose proof exp_pos 1 as Hpos.
rewrite He in Hpos.
apply (Rlt_not_le_frac_opp _ _ Hpos).
rewrite Ropp_involutive.
auto with real.
Qed.

End eirr.