Library completeness

Require Import algebra.
Require Import logical.
Require Import naturals.
Require Import fractions.
Require Import prats.
Require Import cuts.
Require Import reals.

Definition lt (p q:real->Prop) := forall x y, p x -> q y -> x < y.

Definition all (p q:real->Prop) := forall x, p x \/ q x.


Definition gbetw (p q:real->Prop) (x:real) := forall y, (y < x -> ~ q y) /\ (x < y -> ~ p y).


Definition dbetw (p q:real->Prop) (x:real) := forall y, (y < x -> p y) /\ (x < y -> q y).


Definition GF : Prop :=
forall p q:real->Prop,
   ex p ->
   ex q ->
   lt p q ->
   exists x, gbetw p q x.


Definition DF : Prop :=
forall p q:real->Prop,
   ex p ->
   ex q ->
   all p q ->
   lt p q ->
   exists x, dbetw p q x.


Definition TF := TAcompleteness real lt_real.

Section general1.

Variable p q:real->Prop.

Variable ex_p : ex p.
Variable ex_q : ex q.

Variable lt_pq : lt p q.


Definition pc_set (a:prat) := exists x :cut, p x /\ lt_cut a x.

Lemma pc_p1 : (exists a : cut, p a) -> p1_set pc_set.
intros [a A].
destruct (p1 a) as [b B].
exists b. exists a. split.
apply A.
apply (satz158a B).
Qed.

Lemma pc_p2 : p2_set pc_set.
destruct ex_q as [[|a|a] A].
exists O.
intros [b [B C]].
apply (satz167H2 O Z).
apply (lt_pq _ _ B A).
exact I.
destruct (p2 a) as [b B].
exists b.
intros [c [C D]].
apply B.
apply (satz158b (satz126 _ _ _ D (lt_pq _ _ C A))).
exists O.
intros [b [B C]].
destruct (satz167H2 O Z).
apply (lt_pq _ _ B A).
exact I.
Qed.

Lemma pc_p3 : p3_set pc_set lt_prat.
intros x y [a [A B]] C.
exists a. split. apply A.
apply (satz126 _ y _ (satz154a C) B).
Qed.

Lemma pc_p4 : p4_set pc_set lt_prat.
intros x [a [A B]].
destruct (satz159 B) as [y [C D]].
exists y. split.
exists a. tauto.
apply (satz154b C).
Qed.

Definition pc (A:exists a:cut, p a):= Cut pc_set (pc_p1 A) pc_p2 pc_p3 pc_p4.


Lemma gfH0 : (exists a:cut, p a) -> exists x, gbetw p q x.
intros A. exists (pc A).
intros [|b|b]. split.
intros _ B. destruct A as [a A]. apply (lt_pq _ _ A B).
intros [].
split. intros B C. simpl in B.
destruct B as [c [D E]].
simpl in D. destruct D as [d [F G]].
apply (@satz123H2 b d).
apply (@satz127a _ c).
destruct (@satz123H0 b c) as [H|[H|H]]; try tauto.
destruct E. apply (satz158b H).
apply G. apply (lt_pq d b). apply F. apply C.
intros B C.
destruct B as [c [D E]].
destruct E. exists b. split. apply C.
apply (satz158a D).
split.
intros _ B. destruct A as [a A]. apply (lt_pq _ _ A B).
intros [].
Qed.

End general1.

Section general2.

Theorem gf : GF.
intros p q ex_p ex_q lt_pq.
destruct (xm (exists a:cut, p a)) as [A|A].
apply (gfH0 p q ex_q lt_pq A).
destruct (xm (exists a:cut, q (N a))) as [B|B].
set (p':= fun n => p (inv_add_real n)).
set (q':= fun n => q (inv_add_real n)).
destruct (gfH0 q' p') as [x C].
destruct ex_p as [x C].
exists (inv_add_real x); unfold p'.
rewrite satz177; apply C.
intros x y C D.
rewrite <-satz177,<-(@satz177 y).
apply (satz183a (lt_pq (inv_add_real y) (inv_add_real x) D C)).
apply B.
exists (inv_add_real x).
intros y; destruct (C (inv_add_real y)) as [D E].
unfold p',q' in D,E.
rewrite satz177 in D,E.
split.
intros F.
apply E.
rewrite <-(@satz177 x).
apply (satz183a F).
intros F.
apply D.
rewrite <-(@satz177 x).
apply (satz183a F).
exists Z.
intros [|a|a]. tauto. split.
intros []. intros _ C.
destruct A. exists a. apply C.
split. intros _ C. apply B. exists a. apply C.
intros [].
Qed.

End general2.

Section dedekind.

Variable p q : real -> Prop.

Variable ex_p : ex p.
Variable ex_q : ex q.


Variable all_pq : all p q.

Variable lt_pq : lt p q.

Definition FT_exist := exists x, dbetw p q x.

Definition FT_unique := forall x y, dbetw p q x -> dbetw p q y -> x = y.


Lemma DBETW_GBETW : forall x, dbetw p q x -> gbetw p q x.
intros x A y.
destruct (A y) as [B C].
split; intros D E.
apply (satz167H1 _ _ (lt_pq _ _ (B D) E)).
reflexivity.
apply (satz167H1 _ _ (lt_pq _ _ E (C D))).
reflexivity.
Qed.

Lemma GBETW_DBETW : forall x, gbetw p q x -> dbetw p q x.
intros x A y.
destruct (A y) as [B C].
destruct (all_pq y) as [D|D].
split; intros E.
apply D.
destruct (C E D).
split; intros E.
destruct (B E D).
apply D.
Qed.

Lemma dfuH0 : forall x y, dbetw p q x -> dbetw p q y -> x < y -> False.
intros x y A B C.
destruct (A (quotient_real (x + y) (O + O) I)) as [_ D].
destruct (B (quotient_real (x + y) (O + O) I)) as [E _].
destruct (satz167H1 (quotient_real (x + y) (O + O) I) (quotient_real (x + y) (O + O) I)).
apply (lt_pq (quotient_real (x + y) (O + O) I) (quotient_real (x + y) (O + O) I)).
apply E.
apply (@satz203d _ _ (O+O)).
rewrite (satz194 (quotient_real _ (O+O) _)).
rewrite satz204a. rewrite satz201.
rewrite (satz194 _ O).
rewrite satz195.
apply (satz188a C).
apply I.
apply D.
apply (@satz203d _ _ (O+O)).
rewrite (satz194 (quotient_real _ (O+O) _)).
rewrite satz204a. rewrite satz201.
rewrite (satz194 _ O).
rewrite satz195,(satz175 _ y).
apply (satz188a C).
apply I.
reflexivity.
Qed.

Lemma dfu : FT_unique.
intros x y A B.
destruct (satz167H0 x y) as [C|[C|C]].
destruct (dfuH0 _ _ A B C).
apply C.
destruct (dfuH0 _ _ B A C).
Qed.

Lemma p_a : forall x y, p y -> x < y -> p x.
intros x y A B.
destruct (all_pq x) as [C|C]. apply C.
destruct (satz167H2 _ _ B (lt_pq _ _ A C)).
Qed.

Lemma q_a : forall x y, q x -> x < y -> q y.
intros x y A B.
destruct (all_pq y) as [C|C].
destruct (satz167H2 _ _ B (lt_pq _ _ C A)).
apply C.
Qed.

Lemma dfe : FT_exist.
destruct (gf p q ex_p ex_q lt_pq) as [x A].
exists x. apply GBETW_DBETW.
apply A.
Qed.

End dedekind.

Theorem df : DF.
exact dfe.
Qed.


Theorem tf : TF.
intros p q l.
destruct (xm (ex p)) as [A|A].
destruct (xm (ex q)) as [B|B].
destruct (gf p q A B l) as [z C].
exists z.
intros x y D E F G.
split.
destruct (satz167H0 x z) as [H|[H|H]].
apply H. destruct (F H).
destruct (C x) as [_ K].
destruct (K H D).
destruct (satz167H0 y z) as [H|[H|H]].
destruct (C y) as [K _].
destruct (K H E).
subst y; destruct G; reflexivity.
apply H.
exists Z.
intros x y C D.
destruct B. exists y. apply D.
exists Z.
intros x y C.
destruct A. exists x. apply C.
Qed.

Lemma HAsup : HAsupremum real lt_real.
intros p [x A] [y B].
destruct (df (fun x => exists y, p y /\ x < y) (fun x => ~ exists y, p y /\ x < y)) as [z C].
destruct (ninpl x) as [z C].
exists z; exists x. tauto.
destruct (ninpr y) as [z C].
exists z. intros [u [D E]].
generalize (B u D); intros F.
destruct (satz167H2 y z C).
apply (satz172b E F).
intros z.
apply xm.
intros u v [z [C D]] E.
destruct (satz167H0 u v) as [F|[F|F]].
apply F.
destruct E.
subst v. exists z. tauto.
destruct E.
exists z. split. apply C.
apply (satz171 _ _ _ F D).
exists z.
split.
intros u D.
destruct (satz167H0 u z) as [E|[E|E]].
left. apply E.
right. apply E.
destruct (tarski3 _ _ E) as [w [F G]].
destruct (C w) as [_ H].
destruct (H F).
exists u. tauto.
intros u D.
destruct (C u) as [E _].
destruct (satz167H0 u z) as [F|[F|F]].
destruct (E F) as [v [G H]].
destruct (D v G) as [J|J].
destruct (satz167H2 _ _ H J).
destruct (satz167H1 _ _ H J).
right. symmetry. apply F.
left. apply F.
Qed.



Section NestedIntervals.


Variable a : Datatypes.nat -> real.
Variable b : Datatypes.nat -> real.


Variable interval : forall n, a n <= b n.


Variable isotonic_a : forall n, a n <= a (Datatypes.S n).
Variable antitonic_b : forall n, b (Datatypes.S n) <= b n.

Fixpoint lt_dnat (n m:Datatypes.nat) := match n,m with
| _ , Datatypes.O => false
| Datatypes.O , _ => true
| Datatypes.S n, Datatypes.S m => lt_dnat n m
end.
Notation "n < m":=(lt_dnat n m).

Lemma lt_equiv n m : n < Datatypes.S m -> n = m \/ n < m.
fix IHx 1.
intros [|n] [|m]. tauto. tauto.
destruct n; tauto.
intros A.
destruct (IHx n m A).
left. apply (f_equal _ H).
tauto.
Qed.

Lemma a_1 : forall n m, n < m -> a n <= a m.
induction m.
destruct n; intros [].
intros A. destruct (lt_equiv n m A) as [B|B].
subst n. apply isotonic_a.
apply (satz173 _ _ _ (IHm B) (isotonic_a _)).
Qed.

Lemma b_1 : forall n m, n < m -> b m <= b n.
induction m.
destruct n; intros [].
intros A. destruct (lt_equiv n m A) as [B|B].
subst n. apply antitonic_b.
apply (satz173 _ _ _ (antitonic_b _) (IHm B)).
Qed.

Lemma b_2 : forall n, b n <= b Datatypes.O.
induction n. right. tauto.
exact (satz173 _ _ _ (antitonic_b n) IHn).
Qed.

Lemma tri : trichotomy Datatypes.nat lt_dnat.
unfold trichotomy.
fix IHx 1. intros [|x] [|y].
tauto. simpl; tauto. simpl;tauto.
destruct (IHx x y) as [H|[H|H]]; try tauto.
right. left.
apply (f_equal _ H).
Qed.

Lemma le : forall n m, a n <= b m.
intros n m.
destruct (tri n m) as [A|[A|A]].
apply (satz173 _ _ _ (a_1 _ _ A) (interval _)).
subst n. apply interval.
apply (satz173 _ _ _ (interval _) (b_1 _ _ A)).
Qed.

Lemma NI : exists x, forall n, a n <= x /\ x <= b n.
destruct (HAsup (fun x => exists n, x <= a n)) as [x [A B]].
exists (a Datatypes.O). exists Datatypes.O. right. reflexivity.
exists (b Datatypes.O).
intros x [n A].
apply (satz173 _ _ _ (satz173 _ _ _ A (le n n)) (b_2 _)).
exists x.
intros n. split.
apply A. exists n. right. tauto.
apply B.
intros y [m C].
apply (satz173 _ _ _ C (le _ _)).
Qed.

End NestedIntervals.


Section Archimedian.

Coercion dnat_to_real n := iter real add_real O n.

Definition nats := fun x :real => exists n:Datatypes.nat, x = n.

Lemma natnotbound : forall x:real, exists n:Datatypes.nat, x < n.
intros x.
destruct (xm (exists n:Datatypes.nat, x < n)).
apply H.
destruct (HAsup nats) as [y [A B]].
exists O. exists Datatypes.O.
reflexivity.
exists x.
intros y [z A].
destruct (satz167H0 y x) as [B|[B|B]].
tauto. tauto.
subst y.
destruct H.
exists z. apply B.
destruct (xm (exists n:Datatypes.nat, y-O<n)) as [[n C]|C].
cut (y < n + O). intros D.
destruct (A (n+O)).
exists (Datatypes.S n). reflexivity.
destruct (satz167H2 _ _ D H0).
destruct (satz167H1 _ _ D H0).
rewrite <-(sub_real_correct y O).
apply (@satz188a _ _ O C).
destruct (B (y-O)) as [D|D].
intros z [n D].
destruct (satz167H0 z (y-O)) as [E|[E|E]].
tauto. tauto.
subst z.
destruct C. exists n. apply E.
generalize (satz182d D).
unfold sub_real.
rewrite satz175,<-satz186,satz179.
intros [].
symmetry in D.
generalize (satz182e D).
unfold sub_real.
rewrite satz175,<-satz186,satz179.
intros E. discriminate E.
Qed.

Lemma Arch : JDarchimedean real Z add_real leq_real.
intros x A B y C.
destruct x. contradiction B. reflexivity.
destruct (natnotbound (quotient_real y (P c) I)).
exists x.
left.
cut (y < (P c)*x).
intros D.
cut (P c * x = iter real add_real (P c) x).
intros E; rewrite <-E; apply D.
generalize x.
fix IHz 1.
intros [|z].
unfold dnat_to_real,iter.
rewrite satz194,satz195. reflexivity.
unfold dnat_to_real,iter. fold iter.
rewrite satz201,(satz194 _ O),satz195,<-(IHz z).
reflexivity.
generalize (satz203a _ _ (P c) H I).
rewrite quotient_real_correct,satz194.
tauto.
destruct A. destruct H. discriminate H.
Qed.

End Archimedian.