Require Import logical. Require Import algebra. Require Import naturals. Require Import fractions. Require Import prats. (** * Dedekind cuts *) (** ** Definition of cuts *) Definition p1_set {R:Type} (s:R->Prop) := exists x, s x. Definition p2_set {R:Type} (s:R->Prop) := exists x, ~ s x. Definition p3_set {R:Type} (s:R->Prop) (lt:R->R->bool) := forall x y, s y -> lt x y -> s x. Definition p4_set {R:Type} (s:R->Prop) (lt:R->R->bool) := forall x, s x -> exists y, s y /\ lt x y. Record cut := Cut {pcut : prat -> Prop; p1 : p1_set pcut; p2 : p2_set pcut; p3 : p3_set pcut lt_prat; p4 : p4_set pcut lt_prat}. Definition CE : Prop := forall x y : cut, (forall a, pcut x a <-> pcut y a) -> x = y. (** To prove certain properties of cuts we need xm and ce as assumptions. *) Variable ce : CE. Variable xm : XM. Lemma p3_equiv {pcut:prat->Prop} : p3_set pcut lt_prat -> forall a b, pcut a -> ~ pcut b -> a < b. intros p A a b B C. destruct (satz81H0 a b) as [D|[D|D]]. exact D. subst a. destruct (C B). destruct (C (A _ _ B D)). Qed. (** * Equality of cuts *) (** Two cuts are considered to be the same iff their sets contain the same positive rational numbers. *) Definition eq_cut (x y:cut) := forall a, pcut x a <-> pcut y a. Notation "x == y":=(eq_cut x y). (** This equality is an equivalence relation. *) Theorem satz116 : reflexive cut eq_cut. intros x a. tauto. Qed. Theorem satz117 : symmetric cut eq_cut. intros x y A a. split; intros B. apply (A _). exact B. apply (A _). exact B. Qed. Theorem satz118 : transitive cut eq_cut. intros x y z A B a. split; intros C. apply (B _), (A _). exact C. apply (A _), (B _). exact C. Qed. Lemma cut_order_equiv_a {x y:cut} : x = y -> x == y. intros x y A. rewrite A. apply satz116. Qed. Lemma cut_order_equiv_b {x y:cut} : x == y -> x = y. apply ce. Qed. (** Given a certain cut and two positive rational numbers. *) Theorem satz119 {x:cut} {a b:prat} : ~ pcut x a -> a < b -> ~ pcut x b. intros [x x1 x2 x3 x4] a b A B C. simpl in *. contradiction (A (x3 _ _ C B)). Qed. (** ** Order *) Definition lt_cut (x y:cut) := exists z, pcut y z /\ ~ pcut x z. Notation "x < y":=(lt_cut x y). Theorem satz123H0 : trichotomy cut lt_cut. intros x y. destruct (xm (lt_cut x y)) as [A|A]. tauto. destruct (xm (lt_cut y x)) as [B|B]. tauto. right. left. apply cut_order_equiv_b. intros a. split; intros C. destruct (xm (pcut y a)). apply H. contradiction B. exists a. tauto. destruct (xm (pcut x a)). apply H. contradiction A. exists a. tauto. Qed. Theorem satz123H1 {x y:cut} : x < y -> x = y -> False. intros x y [u [A B]] C. rewrite <- C in A. destruct (B A). Qed. Theorem satz123H2 {x y:cut} : x < y -> y < x -> False. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [u [A B]] [v [C D]]. simpl in *. contradiction (satz81H2 (p3_equiv y3 _ _ A D) (p3_equiv x3 _ _ C B)). Qed. Theorem satz123H3 {x y:cut} : y < x -> x = y -> False. intros x y A B. symmetry in B. apply (satz123H1 A B). Qed. Theorem satz126 : transitive cut lt_cut. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4] [a [A B]] [b [C D]]. unfold lt_cut in *. exists b. split. apply C. intros E. apply (satz81H2 (p3_equiv y3 _ _ A D) (p3_equiv x3 _ _ E B)). Qed. Lemma lt_cut_irreflexive : irreflexive cut lt_cut. intros x A. apply (satz123H2 A). tauto. Qed. Notation "x <= y":=(x < y \/ x = y). Theorem satz127a {x y z:cut} : x <= y -> y < z -> x < z. intros x y z [A|A] B. apply (satz126 _ _ _ A B). rewrite A. apply B. Qed. Theorem satz127b {x y z:cut} : x < y -> y <= z -> x < z. intros x y z A [B|B]. apply (satz126 _ _ _ A B). rewrite<- B. apply A. Qed. Theorem satz128 : transitive cut (fun x y => x <= y). intros x y z A [B|B]. left. apply (satz127a A B). rewrite<- B. apply A. Qed. Theorem leq_cut_reflexive : reflexive cut (fun x y => x <= y). intros x. tauto. Qed. (** ** Addition of Cuts *) Definition add_set (p q : prat->Prop):= fun u:prat => exists x, exists y, p x /\ q y /\ u = x+y. Lemma p1_add_proof {x y:cut} : p1_set (add_set (pcut x) (pcut y)). intros [x [u A] x2 x3 x4] [y [v B] y2 y3 y4]. simpl. exists (u+v). unfold add_set. exists u. exists v. split. apply A. split. apply B. reflexivity. Qed. Lemma p2_add_proof {x y:cut} : p2_set (add_set (pcut x) (pcut y)). intros [x x1 [u A] x3 x4] [y y1 [v B] y3 y4]. simpl. exists (u+v). unfold add_set. intros [a [b [C [D E]]]]. contradiction (satz81H1 (satz98 (p3_equiv x3 _ _ C A) (p3_equiv y3 _ _ D B)) E). Qed. Lemma p3_add_proof {x y:cut} : p3_set (add_set (pcut x) (pcut y)) lt_prat. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a b [v [w [A [B C]]]] D. exists (quotient_prat a (v+w) * v). exists (quotient_prat a (v+w) * w). simpl in *. split. apply (x3 _ v). apply A. rewrite C in D. rewrite <- (@mul_prat_identity_l (v+w)) in D. rewrite <-(@quotient_prat_correct_a a (v+w)) in D. generalize (satz106a D); intros F. generalize (@satz105a _ _ v F); intros G. rewrite mul_prat_identity_l in G. apply G. split. apply (y3 _ w). apply B. rewrite C in D. rewrite <- (@mul_prat_identity_l (v+w)) in D. rewrite <-(@quotient_prat_correct_a a (v+w)) in D. generalize (satz106a D); intros F. generalize (@satz105a _ _ w F); intros G. rewrite mul_prat_identity_l in G. apply G. rewrite <- satz104. symmetry. apply quotient_prat_correct_a. Qed. Lemma p4_add_proof {x y:cut} : p4_set (add_set (pcut x) (pcut y)) lt_prat. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a [v [w [A [B C]]]]. simpl in *. destruct (x4 _ A) as [r [D E]]. destruct (y4 _ B) as [s [F G]]. exists (r+s). split. exists r. exists s. split. apply D. split. apply F. reflexivity. rewrite C. apply (satz98 E G). Qed. Definition add_cut (x y:cut) := Cut (add_set (pcut x) (pcut y)) p1_add_proof p2_add_proof p3_add_proof p4_add_proof. Notation "x + y":=(add_cut x y). Theorem satz130 (x y:cut) : x + y = y + x. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4]. apply cut_order_equiv_b. unfold eq_cut. unfold add_cut. simpl. intros a. split. intros [v [w [A [B C]]]]. exists w. exists v. split. apply B. split. apply A. rewrite C. apply satz92. intros [v [w [A [B C]]]]. exists w. exists v. split. apply B. split. apply A. rewrite C. apply satz92. Qed. Theorem satz131 (x y z:cut) : (x + y) + z = x + (y + z). intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4]. apply cut_order_equiv_b. unfold eq_cut. unfold add_cut. simpl. intros a. split. intros [t [u [[v [w [A [B C]]]] [D E]]]]. exists v. exists (add_prat w u). split. apply A. split. exists w. exists u. tauto. subst t a. apply satz93. intros [t [u [A [[v [w [B [C D]]]] E]]]]. exists (add_prat t v). exists w. split. exists t. exists v. tauto. split. apply C. subst u a. symmetry. apply satz93. Qed. Lemma satz132 (a:prat) (x:cut) : exists l, exists u, exists k, pcut x l /\ ~ pcut x u /\ sub_prat u l k = a. intros a [x [b A] [c B] x3 x4]. destruct (@satz115 a c) as [n C]. generalize (@satz95 _ _ b C); intros D. cut (lt_prat c (add_prat c b)). intros E. generalize (satz86 c _ _ E D); intros F. rewrite satz92 in F. cut (~ x (add_prat b (mul_prat n a))). intros G. destruct (@XM_WP xm (fun i => ~ x (add_prat b (mul_prat i a)))) as [u H]. exists n. apply G. destruct u. exists b. exists (add_prat b a). exists (satz94). simpl. destruct H as [I J]. rewrite mul_prat_identity_l in I. split. apply A. split. apply I. apply (@satz97b _ _ b). rewrite satz92,(sub_prat_correct_a). apply satz92. exists (add_prat b (mul_prat u a)). exists (add_prat b (mul_prat (S u) a)). simpl. assert (L:lt_prat (add_prat b (mul_prat u a)) (add_prat b (mul_prat (S u) a))). repeat rewrite (satz92 b _). apply satz95. apply satz105a. rewrite <-nat_to_prat_S. apply satz94. destruct H as [I J]. exists L. split. destruct (xm (x (add_prat b (mul_prat u a)))) as [K|K]. apply K. contradiction (lt_nat_irreflexive (J _ K)). split. apply I. apply (@satz97b _ _ (add_prat b (mul_prat u a))). rewrite satz92, sub_prat_correct_a. rewrite <- nat_to_prat_S. rewrite (satz102 _ a),satz104,(satz102 a O),mul_prat_identity_l. rewrite <-satz93,(satz102 a u). apply satz92. intros G. contradiction (B (x3 _ _ G F)). apply satz94. Qed. Lemma satz133 {x y:cut} : x < x + y. intros [x x1 x2 x3 x4] [y [a A] y2 y3 y4]. unfold lt_cut. simpl. destruct (satz132 a (Cut x x1 x2 x3 x4)) as [l [u [K [B [C D]]]]]. simpl in *. exists u; split. exists l. exists a. rewrite satz92. split. tauto. split. tauto. rewrite <-D. rewrite satz92. symmetry. apply sub_prat_correct_a. apply C. Qed. Lemma satz134 {x y z:cut} : x < y -> x + z < y + z. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4] [u [A B]]. simpl in *. destruct (y4 _ A) as [v [C D]]. destruct (@satz101a v u D) as [a E]. destruct (satz132 a (Cut z z1 z2 z3 z4)) as [b [c [K[F [G H]]]]]. simpl in *. assert (I: add_prat u c = add_prat v b). generalize (@satz96 _ _ b H); clear H; intros H. rewrite satz92 in H. rewrite sub_prat_correct_a in H. subst c. subst v. symmetry. apply satz93. exists (add_prat v b). simpl. split. exists v. exists b. tauto. rewrite <- I. intros [d [e [J[M L]]]]. contradiction (satz81H1 (satz98 (p3_equiv x3 _ _ J B) (p3_equiv z3 _ _ M G)) L). Qed. Lemma satz135 {x y z:cut} : x = y -> x + z = y + z. intros x y z A. rewrite A. reflexivity. Qed. Lemma satz136a {x y z:cut} : x + z < y + z -> x < y. intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]]. apply B. contradiction (satz123H1 A (satz135 B)). contradiction (satz123H2 A (satz134 B)). Qed. Lemma satz136b {x y z:cut} : x + z = y + z -> x = y. intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]]. contradiction (satz123H1 (satz134 B) A). apply B. contradiction (satz123H3 (satz134 B) A). Qed. Lemma satz137 {x y z u:cut} : x < y -> z < u -> x + z < y + u. intros x y z u A B. apply (satz126 _ _ _ (satz134 A)). repeat (rewrite (satz130 y _)). apply (satz134 B). Qed. Lemma satz138a {x y z u:cut} : x < y -> z <= u -> x + z < y + u. intros x y z u A [B|B]. apply (satz137 A B). subst z. apply (satz134 A). Qed. Lemma satz138b {x y z u:cut} : x <= y -> z < u -> x + z < y + u. intros x y z u [A|A] B. apply (satz137 A B). subst x. repeat (rewrite (satz130 y)). apply (satz134 B). Qed. Lemma satz139 {x y z u:cut} : x <= y -> z <= u -> x + z <= y + u. intros x y z u [A|A] B. left. apply (satz138a A B). destruct B as [B|B]. left. apply satz138b. tauto. apply B. right. rewrite A,B. reflexivity. Qed. (** ** Subtraction of Cuts *) Definition sub_cut_set (p q:prat->Prop) (a:prat) := exists b, exists c, exists l, p b /\ ~ q c /\ a = sub_prat b c l. Lemma p1_sub_proof {x y:cut} {l:y pcut x a -> pcut y a. intros x y a [z [A B]] C. apply (p3 y _ _ A (p3_equiv (p3 x) _ _ C B)). Qed. (***satz140a***) Lemma sub_cut_correct_a {x y:cut} {l:x < y} : x + (@sub_cut y x l) = y. intros x y l; symmetry. apply ce. intros a; split. intros A. destruct (xm (pcut x a)) as [M|M]. apply (@satz140H0 x (x + sub_cut y x l)). apply satz133. apply M. destruct (p4 y _ A) as [u [D E]]. destruct (satz132 (sub_prat u a E) x) as [b [c [K [F [G H]]]]]. generalize (@satz96 _ _ b H); intros I. rewrite (satz92 (sub_prat c b K)),sub_prat_correct_a in I. generalize (p3_equiv (p3 x) _ _ F M); intros J. generalize (@satz96 _ _ (sub_prat a b J) I); intros L. cut (lt_prat c u). intros O. rewrite satz93,(sub_prat_correct_a _ _ J), (satz92 _ a),(sub_prat_correct_a _ _ E),<-(sub_prat_correct_a c u O) in L. repeat rewrite (satz92 c) in L. generalize (satz97b L); clear L; intros L. generalize (@satz96 _ _ b L); intros N. rewrite (satz92 (sub_prat a b J)),(sub_prat_correct_a _ _ J) in N. exists b. exists (sub_prat u c O). split. apply F. split. exists u. exists c. exists O. tauto. rewrite N. apply satz92. rewrite I. apply (@satz97a _ _ a). rewrite satz93,(satz92 b a),<-satz93,(satz92 _ a),(sub_prat_correct_a _ _ E). repeat rewrite (satz92 u _). apply (satz95 J). intros [b [c [A [[d [e [K [B [C D]]]]] E]]]]. rewrite D in E. generalize (p3_equiv (p3 x) _ _ A C); intros F. cut (lt_prat (add_prat (sub_prat d e K) b) d). intros G. rewrite E. rewrite satz92 in G. apply (p3 y _ _ B G). cut (add_prat (add_prat (sub_prat d e K) b) (sub_prat e b F) = d). intros H. apply (@satz97a _ _ (sub_prat e b F)). rewrite H. apply satz94. rewrite satz93,(sub_prat_correct_a _ _ F),satz92. apply (sub_prat_correct_a _ _ K). Qed. Lemma satz140b {x y:cut} : x < y -> exists z, x + z = y. intros x y l. exists (sub_cut y x l). apply sub_cut_correct_a. Qed. Lemma sub_cut_PI {x y:cut} {m n:lt_cut y x} : sub_cut x y m = sub_cut x y n. intros x y m n. apply ce. unfold sub_cut. simpl. tauto. Qed. (** ** Multiplication of Cuts *) Definition mul_set (p q : prat->Prop):= fun u:prat => exists x, exists y, p x /\ q y /\ u = x*y. Lemma p1_mul_proof {x y:cut} : p1_set (mul_set (pcut x) (pcut y)). intros [x [u A] x2 x3 x4] [y [v B] y2 y3 y4]. simpl. exists (u*v). unfold mul_set. exists u. exists v. split. apply A. split. apply B. reflexivity. Qed. Lemma p2_mul_proof {x y:cut} : p2_set (mul_set (pcut x) (pcut y)). intros [x x1 [u A] x3 x4] [y y1 [v B] y3 y4]. simpl. exists (u*v). unfold mul_set. intros [a [b [C [D E]]]]. contradiction (satz81H1 (satz107 (p3_equiv x3 _ _ C A) (p3_equiv y3 _ _ D B)) E). Qed. Lemma p3_mul_proof {x y:cut} : forall a b, mul_set (pcut x) (pcut y) b -> lt_prat a b -> mul_set (pcut x) (pcut y) a. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a b [v [w [A [B C]]]] D. simpl in *. rewrite C in D. cut (mul_prat v (quotient_prat a v) = a). intros E. cut (lt_prat (quotient_prat a v) w). intros F. exists v. exists (quotient_prat a v). split. apply A. split. apply (y3 _ _ B F). symmetry. apply E. rewrite<- (mul_prat_identity_l w). rewrite <-(@quotient_prat_correct_a O v). rewrite satz103. rewrite quotient_prat_correct_b. repeat (rewrite (satz102 (quotient_prat O v))). apply (satz105a D). symmetry. rewrite satz102. symmetry. apply quotient_prat_correct_a. Qed. Lemma p4_mul_proof {x y:cut} : forall a, mul_set (pcut x) (pcut y) a -> exists b, mul_set (pcut x) (pcut y) b /\ lt_prat a b. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] a [v [w [A [B C]]]]. simpl in *. destruct (x4 _ A) as [l [D E]]. exists (mul_prat l w). split. exists l. exists w. tauto. rewrite C. apply (satz105a E). Qed. Definition mul_cut (x y:cut) := Cut (mul_set (pcut x) (pcut y)) p1_mul_proof p2_mul_proof p3_mul_proof p4_mul_proof. Notation "x * y":=(mul_cut x y). (* mul_cut_commutative *) Theorem satz142 : commutative cut mul_cut. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4]. apply cut_order_equiv_b. unfold eq_cut. intros a; split; intros [b [c [A [B C]]]]; simpl in *. exists c. exists b. rewrite C. rewrite satz102. tauto. exists c. exists b. rewrite C. rewrite satz102. tauto. Qed. (* mul_cut_associative *) Theorem satz143 : associative cut mul_cut. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4]. apply cut_order_equiv_b. unfold eq_cut. intros a; split; intros [b [c [A [C D]]]]; simpl in *. destruct A as [d [e [E [F G]]]]. exists d. exists (mul_prat e c). split. apply E. split. exists e. exists c. tauto. rewrite D,G. apply satz103. destruct C as [d [e [E [F G]]]]. exists (mul_prat b d). exists e. split. exists b. exists d. tauto. rewrite D,G. rewrite satz103. tauto. Qed. Theorem satz144 : distributes cut add_cut mul_cut. intros [x x1 x2 x3 x4] [y y1 y2 y3 y4] [z z1 z2 z3 z4]. apply cut_order_equiv_b. unfold eq_cut. simpl in *. intros a; split. intros [b [c [A [[d [e [B [C D]]]] E]]]]. exists (mul_prat b d). exists (mul_prat b e). split. exists b. exists d. tauto. split. exists b. exists e. tauto. rewrite E,D. apply satz104. intros [b [c [[d [e [A [B C]]]] [[f [g [E [F G]]]] H]]]]. destruct (@satz81H0 d f) as [J|[J|J]]. destruct (satz101a J) as [h K]. symmetry in K. rewrite K in G. apply (@p3_mul_proof (Cut x x1 x2 x3 x4) (Cut y y1 y2 y3 y4 + Cut z z1 z2 z3 z4) _ (add_prat a (mul_prat h e))). simpl. exists f. exists (add_prat e g). split. apply E. split. exists e. exists g. tauto. rewrite H,C,G,K. rewrite satz104, (satz102 (add_prat d h) e), (satz102 _ g), satz104, satz104. rewrite (satz102 e d),(satz102 e h),(satz93 (mul_prat d e)), (satz92 _ (mul_prat h e)), <-(satz93). reflexivity. apply satz94. subst d. exists f. exists (add_prat e g). split. apply E. split. exists e. exists g. tauto. rewrite H,C,G. symmetry. apply satz104. destruct (satz101a J) as [h K]. symmetry in K. rewrite K in C. apply (@p3_mul_proof (Cut x x1 x2 x3 x4) (Cut y y1 y2 y3 y4 + Cut z z1 z2 z3 z4) _ (add_prat a (mul_prat h g))). simpl. exists d. exists (add_prat e g). split. apply A. split. exists e. exists g. tauto. rewrite H,C,G,K. rewrite satz104,(satz102 (add_prat f h) g),(satz104). repeat (rewrite (satz102 _ g)). apply satz93. apply satz94. Qed. Theorem satz145a {x y z:cut} : x < y -> x * z < y * z. intros x y z A. destruct (satz140b A) as [a B]. rewrite <-B. rewrite (satz142 (x+a)),(satz144),(satz142). apply satz133. Qed. Theorem satz145b {x y z:cut} : x = y -> x * z = y * z. intros x y z A. rewrite A. reflexivity. Qed. Theorem satz146a {x y z:cut} : x * z < y * z -> x < y. intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]]. apply B. contradiction (satz123H1 A (satz145b B)). contradiction (satz123H2 A (satz145a B)). Qed. Theorem satz146b {x y z:cut} : x * z = y * z -> x = y. intros x y z A. destruct (@satz123H0 x y) as [B|[B|B]]. contradiction (satz123H1 (satz145a B) A). apply B. contradiction (satz123H3 (satz145a B) A). Qed. Theorem satz147 {x y z u:cut} : x < y -> z < u -> x * z < y * u. intros x y z u A B. apply (satz126 _ (x*u)). repeat (rewrite (satz142 x)). apply (satz145a B). apply (satz145a A). Qed. Theorem satz148a {x y z u:cut} : x <= y -> z < u -> x * z < y * u. intros x y z u [A|A] B. apply (satz147 A B). rewrite A,(satz142 y),(satz142 y). apply (satz145a B). Qed. Theorem satz148b {x y z u:cut} : x < y -> z <= u -> x * z < y * u. intros x y z u A [B|B]. apply (satz147 A B). rewrite B. apply (satz145a A). Qed. Theorem satz149 {x y z u:cut} : x <= y -> z <= u -> x * z <= y * u. intros x y z u [A|A] B. left. apply (satz148b A B). destruct B as [B|B]. left. apply satz148a. right. apply A. apply B. right. rewrite A,B. reflexivity. Qed. (** ** Prat to Cuts *) Definition prat_cut_set (a:prat) := fun b => lt_prat b a. Lemma p1_prat_cut_proof {a:prat} : exists b, prat_cut_set a b. exact @satz90. Qed. Lemma p2_prat_cut_proof {a:prat} : exists b, ~ prat_cut_set a b. intros a. destruct (@satz89 a) as [b A]. exists b. intros B. exact (satz81H2 A B). Qed. Lemma p3_prat_cut_proof {a:prat} : forall x y, prat_cut_set a y -> lt_prat x y -> prat_cut_set a x. intros a x y A B. apply (satz86 _ _ _ B A). Qed. Lemma p4_prat_cut_proof {a:prat} : forall x, prat_cut_set a x -> exists y, prat_cut_set a y /\ lt_prat x y. intros a x A. unfold prat_cut_set. destruct (satz91 A) as [y [B C]]. exists y. split. apply C. apply B. Qed. Definition prat_to_cut (a:prat) := Cut (prat_cut_set a) p1_prat_cut_proof p2_prat_cut_proof p3_prat_cut_proof p4_prat_cut_proof. Coercion prat_to_cut : prat >-> cut. Definition is_rational_cut (x:cut) := exists a:prat, x = a. Definition is_irrational_cut (x:cut) := ~ is_rational_cut x. Theorem satz151 : identity_l cut O mul_cut. intros [x x1 x2 x3 x4]. unfold mul_cut. simpl. unfold prat_cut_set. unfold mul_set. apply cut_order_equiv_b. unfold eq_cut. simpl. split. intros [b [c [A [B C]]]]. rewrite C. apply (x3 _ _ B). generalize (@satz105a b O c A); intros D. rewrite mul_prat_identity_l in D. apply D. intros A. destruct (x4 _ A) as [b [B C]]. exists (mul_prat (quotient_prat O b) a). exists b. split. rewrite satz102. generalize (@satz105a _ _ (quotient_prat O b) C); intros D. rewrite (satz102 b) in D. rewrite quotient_prat_correct_a in D. apply D. split. apply B. rewrite satz102,<-satz103,(satz102 b). rewrite quotient_prat_correct_a. symmetry. apply mul_prat_identity_l. Qed. Definition inv_set (q:prat->Prop) (a:prat) := exists b, ~ q b /\ lt_prat b (inv_mul_prat a). Lemma p1_inv_proof {x:cut} : p1_set (inv_set (pcut x)). intros x. destruct (p2 x) as [a A]. exists (inv_mul_prat (add_prat a a)). exists a. split. apply A. rewrite inv_mul_prat_correct_b. apply satz94. Qed. Lemma p2_inv_proof {x:cut} : p2_set (inv_set (pcut x)). intros x. destruct (p1 x) as [a A]. exists (inv_mul_prat a). intros [b [B C]]. rewrite inv_mul_prat_correct_b in C. apply B. apply (p3 x b a A). apply C. Qed. Lemma p3_inv_proof {x:cut} : p3_set (inv_set (pcut x)) lt_prat. intros x a b [c [A B]] C. generalize (@satz105a _ _ (inv_mul_prat b) C); intros D. rewrite (satz102 b),inv_mul_prat_correct_a in D. rewrite <-(inv_mul_prat_correct_a a),satz102 in D. generalize (satz106a D); clear D; intros D. exists (inv_mul_prat b). split. intros E. apply A, (p3 x c _ E B). apply D. Qed. Lemma p4_inv_proof {x:cut} : p4_set (inv_set (pcut x)) lt_prat. intros x a [b [A B]]. destruct (satz91 B) as [d [E F]]. exists (inv_mul_prat d). split. exists b. split. apply A. rewrite inv_mul_prat_correct_b. apply E. rewrite <-(inv_mul_prat_correct_b a). apply (inv_mul_prat_correct_c _ _ F). Qed. Definition inv_cut (x:cut) := Cut (inv_set (pcut x)) p1_inv_proof p2_inv_proof p3_inv_proof p4_inv_proof. Theorem satz152a {x:cut} : x * inv_cut x = O. intros x. apply ce. intros a. split. intros [b [c [A [[d [B C]] D]]]]. rewrite <-(inv_mul_prat_correct_a c),D. simpl. apply satz105a. apply (satz86 _ _ _ (p3_equiv (p3 x) _ _ A B) C). intros A. destruct (p1 x) as [b B]. destruct (satz132 (mul_prat (sub_prat O a A) b) x) as [l [u [K [C [D E]]]]]. generalize (p3_equiv (p3 x) _ _ B D); intros F. generalize (@satz105a _ _ (sub_prat O a A) F); clear F; intros F. rewrite (satz102 b),<-E,(satz102 u) in F. generalize (@satz95 _ _ (mul_prat a u) F); clear F; intros F. rewrite (satz102 _ u),(satz102 (sub_prat O a A)),<-satz104 in F. unfold pcut,prat_to_cut,prat_cut_set in A. rewrite (satz92 _ a),(sub_prat_correct_a _ _ A) in F. rewrite (satz102 _ O),mul_prat_identity_l in F. rewrite (satz92 (sub_prat u l K)) in F. assert (G:(lt_prat (add_prat (mul_prat u a) (sub_prat u l K)) (add_prat l (sub_prat u l K)))). rewrite sub_prat_correct_a. apply F. generalize (satz97a G); clear F; clear G; intros F. cut (lt_prat u (quotient_prat l a)). intros G. exists l. exists (inv_mul_prat (quotient_prat l a)). split. apply C. split. exists u. split. apply D. rewrite inv_mul_prat_correct_b. apply G. apply (@satz106b _ _ (quotient_prat l a)). rewrite (satz102 a),quotient_prat_correct_a,satz103. rewrite inv_mul_prat_correct_a. symmetry. rewrite satz102. apply mul_prat_identity_l. apply (@satz106a _ _ a). rewrite quotient_prat_correct_a. apply F. Qed. Theorem satz152b {x:cut} : exists y, x * y = O. intros x. exists (inv_cut x). apply satz152a. Qed. Definition quotient_cut (x y:cut) := x * inv_cut y. Theorem satz153a {x y:cut} : x * quotient_cut y x = y. intros x y. unfold quotient_cut. rewrite (satz142 y),<-satz143,<-satz151,satz152a. reflexivity. Qed. Theorem satz153b {x y:cut} : exists z, x * z = y. intros x y. exists (quotient_cut y x). apply satz153a. Qed. Theorem satz153c {x y u v} : x * u = y -> x * v = y -> u = v. intros x y u v A B. rewrite <-A in B. rewrite (satz142 x),(satz142 x) in B. symmetry. apply (satz146b B). Qed. Theorem satz154a {x y:prat} : lt_prat x y -> x < y. intros x y A. exists x. unfold prat_to_cut,pcut. split. apply A. unfold prat_cut_set. generalize (lt_prat_irreflexive x). tauto. Qed. Theorem satz154b {x y:prat} : x < y -> lt_prat x y. intros x y [a [A B]]. unfold prat_to_cut,pcut,prat_cut_set in *. destruct (@satz81H0 x y) as [H|[H|H]]. apply H. subst x. destruct (B A). destruct (B (satz86 _ _ _ A H)). Qed. Theorem satz154c {x y:prat} : x = y -> @eq cut x y. intros x y A. rewrite A. reflexivity. Qed. Theorem satz154d {x y:prat} : @eq cut x y -> x = y. intros x y A. destruct (@satz81H0 x y) as [B|[B|B]]. contradiction (satz123H1 (satz154a B) A). apply B. contradiction (satz123H3 (satz154a B) A). Qed. Theorem satz155a {x y:prat} : @eq cut (add_prat x y) (x + y). intros x y. apply ce. intros a. split. unfold add_cut,prat_to_cut,add_set,prat_cut_set,pcut. intros A. rewrite <-(mul_prat_identity_l (add_prat x y)), <-(quotient_prat_correct_a _ (add_prat x y)) in A. generalize (@satz106a _ _ _ A); clear A; intros A. exists (mul_prat x (quotient_prat a (add_prat x y))). exists (mul_prat y (quotient_prat a (add_prat x y))). split. generalize (@satz105a _ _ x A); intros B. rewrite mul_prat_identity_l,satz102 in B. apply B. split. generalize (@satz105a _ _ y A); intros B. rewrite mul_prat_identity_l,satz102 in B. apply B. rewrite (satz102 x),(satz102 y),<-satz104,satz102. rewrite satz102. symmetry. apply quotient_prat_correct_a. unfold add_cut,prat_to_cut,add_set,prat_cut_set,pcut. intros [b [c [A [B C]]]]. rewrite C. apply (satz98 A B). Qed. Theorem satz155b {x y:prat} {k:lt_prat y x} {l: y < x} : @eq cut (sub_prat x y k) (@sub_cut x y l). intros x y k l. generalize (@satz155a (sub_prat x y k) y); intros A. rewrite satz92,(sub_prat_correct_a _ _ k) in A. rewrite <-(@sub_cut_correct_a y x l),satz130 in A. symmetry. apply (satz136b A). Qed. Theorem satz155c {x y:prat} : @eq cut (mul_prat x y) (x * y). intros x y; apply ce; intros a. split. intros A. destruct (satz91 A) as [b [B C]]. rewrite <-(mul_prat_identity_l b),<-(quotient_prat_correct_a a b) in B. generalize (satz106a B); intros D. generalize (@satz105a _ _ y D); clear D; intros D. rewrite mul_prat_identity_l in D. rewrite <-(quotient_prat_correct_a b y) in C. generalize (satz106a C); intros E. exists (quotient_prat b y). exists (mul_prat y (quotient_prat a b)). split. apply E. split. rewrite satz102 in D. apply D. rewrite <-satz103,quotient_prat_correct_a. rewrite satz102. symmetry. apply quotient_prat_correct_a. intros [b [c [A [B C]]]]. rewrite C. apply (satz107 A B). Qed. Theorem satz155d {x y:prat} : @eq cut (quotient_prat x y) (quotient_cut x y). intros x y. apply (@satz146b _ _ y). rewrite <-satz155c. rewrite quotient_prat_correct_a. rewrite satz142,satz153a. reflexivity. Qed. Theorem satz158a {x:cut} {a:prat} : pcut x a -> a < x. intros x a. intros A. exists a. split. apply A. intros B. destruct (lt_prat_irreflexive _ B). Qed. Theorem satz158b {x:cut} {a:prat} : a < x -> pcut x a. intros x a. intros [b [A B]]. destruct (@satz81H0 a b) as [H|[H|H]]. apply (p3 x _ _ A H). rewrite H. apply A. destruct (B H). Qed. Theorem satz158c {x:cut} {a:prat} : ~ pcut x a -> x <= a. intros x a A. destruct (@satz123H0 x a) as [B|[B|B]]; try tauto. destruct (A (satz158b B)). Qed. Theorem satz158d {x:cut} {a:prat} : x <= a -> ~ pcut x a. intros x a [A|A] B. destruct (satz123H2 A (satz158a B)). destruct (satz123H3 (satz158a B) A). Qed. Definition lub (x:cut) (m:prat) := forall a, pcut x a <-> lt_prat a m. Definition lub' (x:cut) (m:prat) := ~ pcut x m /\ forall a, ~ pcut x a -> leq_prat m a. Lemma lub_equiv (x:cut) (m:prat) : lub x m <-> lub' x m. intros x m. apply conj. intros A. apply conj. intros B. destruct (A m) as [C _]. apply (satz81H1 (C B) (refl_equal _)). intros a B. destruct (A a) as [C D]. apply frac_order_equiv_d. destruct (@satz81H0 a m) as [E|[E|E]]. destruct (B (D E)). left. rewrite E. apply satz37. right. apply E. intros [A B] a. apply conj. intros C. apply satz154b. apply (satz127b (satz158a C) (satz158c A)). intros C. destruct (xm (pcut x a)). apply H. destruct (frac_order_equiv_c (B a H)) as [D|D]. destruct (satz81H1 C). apply (eq_prat_equiv_f D). destruct (satz81H2 C D). Qed. Theorem satz157a {x:prat} : lub x x. intros x a. tauto. Qed. Theorem satz157b {x:prat} : exists m, lub x m. intros x. exists x. apply satz157a. Qed. Theorem satz157c {x:cut} {a:prat} : lub x a -> x = a. intros x a. exact (ce x a). Qed. Theorem satz157d {x:cut} : (exists m, lub x m) -> exists a : prat, x = a. intros x [m A]. exists m. apply (satz157c A). Qed. Theorem satz159 {x y:cut} : x < y -> exists a : prat, x < a /\ a < y. intros x y [a [A B]]. destruct (p4 y _ A) as [b [C D]]. exists b. split. apply (@satz127a _ a). destruct (@satz123H0 x a) as [H|[H|H]]. left. apply H. right. apply H. destruct (B (satz158b H)). apply (satz154a D). apply (satz158a C). Qed. Lemma ex_min_cut (x y:cut) : exists z, z<=x /\ z<=y. intros x y. destruct (@satz123H0 x y) as [A|[A|A]]. exists x. tauto. exists x. tauto. exists y. tauto. Qed. Theorem satz160 {x y:cut} {a:prat} : x * y < a -> exists b:prat, exists c:prat, @eq cut a (b * c) /\ x <= b /\ y <= c. intros x y a A. destruct (ex_min_cut O (quotient_cut (sub_cut a (x * y) A) (x + y + O))) as [d [B1 B2]]. destruct (@satz159 x (x+d) satz133) as [b [C D]]. destruct (@satz159 y (y+d) satz133) as [c [E F]]. generalize (satz147 D F); clear D; clear F; intros G. rewrite satz144,(satz142 _ y) in G. rewrite satz144,(satz142 y),(satz142 y) in G. rewrite satz131,(satz142 _ d),<-satz144,<-satz131,(satz130 y x) in G. generalize (@satz149 _ _ (x+y+O) (x+y+O) B2 (leq_cut_reflexive _)); intros H. rewrite (satz142 (quotient_cut _ _) (x+y+O)),satz153a in H. generalize (@satz149 d _ _ _ (leq_cut_reflexive _) (@satz139 (x+y) _ _ _ (leq_cut_reflexive _) B1)). intros K. generalize (@satz127b _ _ _ G (@satz139 (x*y) _ _ _ (leq_cut_reflexive _) K)); clear G; clear K; intros G. generalize (satz127b G (@satz139 (x*y) (x*y)_ _ (leq_cut_reflexive _) H)); clear G; clear H; intros G. rewrite sub_cut_correct_a in G. exists (quotient_prat a c). exists c. split. symmetry. rewrite satz142,satz155d. apply satz153a. split. left. apply (satz126 _ _ _ C). apply (@satz146a _ _ c). rewrite (satz142 (quotient_prat a c)). rewrite satz155d,(satz153a). apply G. left. apply E. Qed. Definition sqrt_set (x:cut) (a:prat) := a * a < x. Lemma p1_sqrt_proof (x:cut) : p1_set (sqrt_set x). intros x. destruct (@satz123H0 O x) as [A|[A|A]]. exists O. unfold sqrt_set. rewrite satz151. apply A. exists (O/(S O)). rewrite <-(satz151 x). rewrite <-A. apply satz147; apply satz158a; exact I. destruct (p1 x) as [a B]. exists a. rewrite <-(satz151 x). apply (satz147 (satz126 _ _ _ (satz158a B) A) (satz158a B)). Qed. Lemma p2_sqrt_proof (x:cut) : p2_set (sqrt_set x). intros x. rewrite <-(satz151 x). destruct (@satz123H0 O x) as [A|[A|A]]. destruct (p2 x) as [a B]. exists a. unfold sqrt_set. intros C. rewrite (satz151 x) in C. cut (a < a * a). intros D. apply B. apply satz158b. apply (satz126 _ _ _ D C). cut (pcut x O). intros D. generalize (p3_equiv (p3 x) _ _ D B). intros E. generalize (@satz105a _ _ a E). rewrite mul_prat_identity_l. intros F. rewrite <-satz155c. apply (satz154a F). apply (satz158b A). rewrite <-A. exists O. exact (lt_cut_irreflexive _). exists O. unfold sqrt_set. repeat rewrite (satz151 _). intros B. contradiction (satz123H2 A B). Qed. Lemma p3_sqrt_proof (x:cut) : p3_set (sqrt_set x) lt_prat. intros x a b A B. unfold sqrt_set in *. apply (satz126 _ (b*b)). apply (satz147 (satz154a B) (satz154a B)). apply A. Qed. Lemma ex_less_cut (x y:cut) : exists z:prat, z w * w = y -> v = w. intros v w y A B. rewrite <-B in A. destruct (@satz123H0 v w) as [C|[C|C]]. contradiction (satz123H1 (satz147 C C) A). apply C. contradiction (satz123H3 (satz147 C C) A). Qed. Lemma satz162H0 {x y z u:cut} : x = y -> z = u -> x * z = y * u. intros x y z u A B. rewrite A,B. reflexivity. Qed. Lemma satz162H1 {x y:nat} : leq_nat (S (mul_nat x x)) (mul_nat y y) -> leq_nat (S x) y. intros x y A. destruct (satz10H0 x y) as [B|[B|B]]. apply B. subst x. destruct (lt_nat_irreflexive A). destruct (satz10H2 _ _ A (satz34 B B)). Qed. Theorem satz162 : exists x, is_irrational_cut x. exists (sqrt_cut (S O)). intros [[[a1 a2] arp] A]. generalize (satz162H0 A A); clear A; intros A. rewrite satz161a in A. rewrite <-satz155c in A. unfold mul_prat,rep,mul_frac in A. generalize (eq_prat_equiv_a (satz154d A)); clear A; intros A. unfold eq_prat_a in A. unfold frac_to_prat, nat_to_frac, rep in A. generalize (redAx1_rev _ _ A); clear A; intros A. unfold eq_frac_prop in A. symmetry in A. rewrite <-satz31 in A. apply (sqrt_two A). Qed. Theorem dense_cut : dense cut lt_cut. intros x y [a [A B]]. destruct (p4 y a A) as [b [C D]]. exists b. split. destruct (@satz123H0 x b) as [E|[E|E]]. apply E. subst x. destruct (B D). destruct B. apply satz158b. apply (satz126 _ b). apply (satz154a D). apply E. exists b. split. apply C. exact (lt_prat_irreflexive b). Qed. (** Logical stuff - to prove the need of certain assumptions we need a cut depending on a proposition X*) Definition pset (X:Prop) := fun a : prat => if lt_prat a (S O) then True else if lt_prat a (S (S O)) then X else False. Lemma pset_p1 (X:Prop) : p1_set (pset X). intros X. exists O. exact I. Qed. Lemma pset_p2 (X:Prop) : p2_set (pset X). intros X. exists (S (S O)). intros []. Qed. Lemma pset_p3 (X:Prop) : p3_set (pset X) lt_prat. intros X a b A B. unfold pset in *. case_eq (lt_prat b (S O)); intros C. rewrite (reflect_eq1 (satz86 _ _ _ B (reflect_eq2 C))). exact I. rewrite C in A. case_eq (lt_prat b (S (S O))); intros D. rewrite D in A. rewrite (reflect_eq1 (satz86 _ _ _ B (reflect_eq2 D))). case_eq (lt_prat a (S O)); tauto. rewrite D in A. contradiction A. Qed. Lemma pset_p4 (X:Prop) : p4_set (pset X) lt_prat. intros X a A. unfold pset in *. case_eq (lt_prat a (S O)); intros B. destruct (p4 (S O) a (reflect_eq2 B)) as [b [C D]]. exists b. unfold pcut,prat_to_cut,prat_cut_set in C. rewrite (reflect_eq1 C). tauto. rewrite B in A. case_eq (lt_prat a (S (S O))); intros C. rewrite C in A. destruct (p4 (S (S O)) a (reflect_eq2 C)) as [b [D E]]. exists b. unfold pcut,prat_to_cut,prat_cut_set in D. rewrite (reflect_eq1 D). case_eq (lt_prat b (S O)); tauto. rewrite C in A. contradiction A. Qed. Definition cp (X:Prop) := Cut (pset X) (pset_p1 X) (pset_p2 X) (pset_p3 X) (pset_p4 X). Lemma TR_XM : trichotomy cut lt_cut -> XM. intros tr x. destruct (tr (cp x) (cp (~x))) as [A|[A|A]]. destruct A as [a [A B]]. unfold cp,pset in *;simpl in *. case_eq (lt_prat a (S O)); intros C; rewrite C in *. tauto. case_eq (lt_prat a (S(S O))); intros D; rewrite D in *. tauto. tauto. generalize (cut_order_equiv_a A (S O)); intros B. unfold eq_cut,cp,pset in B;simpl in *. tauto. destruct A as [a [A B]]. unfold cp,pset in *;simpl in *. case_eq (lt_prat a (S O)); intros C; rewrite C in *. tauto. case_eq (lt_prat a (S(S O))); intros D; rewrite D in *. tauto. tauto. Qed. Lemma fe_inv (p q:prat -> Prop) : p = q -> forall a, p a = q a. intros p q A. rewrite A. tauto. Qed. Lemma CE_PE : CE -> PE. intros cex x y A. cut (forall a, pcut (cp x) a <-> pcut (cp y) a). intros B. generalize (cex (cp x) (cp y) B). intros C. injection C. clear C; intros C. generalize (fe_inv _ _ C). intros D. exact (D (S O)). simpl in *. intros a. unfold pset. destruct (lt_prat a (S O)). tauto. destruct (lt_prat a (S (S O))); tauto. Qed. Lemma CE_PI : CE -> PI. exact (fun x => PE_PI (CE_PE x)). Qed. Lemma SE_CE : SE -> CE. intros se [x x1 x2 x3 x4] [y y1 y2 y3 y4] A. generalize (se _ _ _ A); intros B. simpl in *. subst x. generalize (PE_PI (SE_PE se)); intros pi. rewrite (pi _ x1 y1), (pi _ x2 y2), (pi _ x3 y3), (pi _ x4 y4). reflexivity. Qed. Lemma FE_PE_CE : FE -> PE ->CE. intros fe pe [x x1 x2 x3 x4] [y y1 y2 y3 y4] A. generalize (FE_PE_SE fe pe _ _ _ A); intros B. simpl in *. subst x. generalize (PE_PI pe); intros pi. rewrite (pi _ x1 y1), (pi _ x2 y2), (pi _ x3 y3), (pi _ x4 y4). reflexivity. Qed. (* End of cuts *)