Require Import algebra. Require Import logical. Require Import naturals. (** ** Fractions In this chapter we introduce the fractions and their basic properties. *) (** *** 1 Definition and equivalence of fractions *) Inductive frac: Type := over : nat->nat->frac. Notation "n / m" := (over n m). Definition lt_frac (x y:frac) := match(x,y) with (x1/x2 , y1/y2) => x1*y2 x1*y2=y1*x2 end. Definition eq_frac_bool (x y:frac) := match (x,y) with (x1/x2 , y1/y2) => x1*y2==y1*x2 end. Notation "x ~ y":=(eq_frac_prop x y)(at level 70, no associativity). Notation "x ~~ y":=(eq_frac_bool x y)(at level 70, no associativity). Notation "x < y":=(lt_frac x y). Notation "x <~ y":=(orb (x ~~ y) (x < y))(at level 70, no associativity). (** Reflexivity of ~ *) Theorem satz37 : reflexive frac eq_frac_prop. intros [x1 x2]. reflexivity. Qed. (** Symmetry of ~ *) Theorem satz38 : symmetric frac eq_frac_prop. intros [x1 x2] [y1 y2]. unfold eq_frac_prop. intros A. rewrite A. reflexivity. Qed. Lemma satz39H0 (x y z u:nat) : (x*y)*(z*u) = (x*u)*(z*y). intros x y z u. rewrite (satz31 x y (z*u)). rewrite <-(satz31 y z u). rewrite (satz29 (y*z) u). rewrite <-(satz31 x u (y*z)). rewrite (satz29 y z). reflexivity. Qed. (** Transitivity of ~ *) Theorem satz39 : transitive frac eq_frac_prop. intros [x1 x2] [y1 y2] [z1 z2]. unfold eq_frac_prop. intros A B. assert (C:(x1*y2)*(y1*z2)=(y1*x2)*(z1*y2)). rewrite<- B. exact ((satz32b (x1*y2) (y1*x2) (y1*z2)) A). rewrite (satz39H0 x1 y2 y1 z2),(satz39H0 y1 x2 z1 y2) in C. rewrite (satz29 (y1*y2) (z1*x2)) in C. exact (satz33b C). Qed. (** Canceling *) Theorem satz40 {x1 x2 x:nat}: x1/x2 ~ (x1*x)/(x2*x). intros x1 x2 x. unfold eq_frac_prop. rewrite (satz29 x2 x). rewrite (satz31 x1 x x2). reflexivity. Qed. (** *** Projection functions for the numerator and denominator of a fraction. *) Definition num (x:frac) := match x with x1/_ => x1 end. Definition den (x:frac) := match x with _/x2 => x2 end. Lemma frac_equal_num (x y:frac) : x ~ y -> num x = num y -> x=y. intros [x1 x2] [y1 y2] A B. simpl in *. subst x1. unfold eq_frac_prop in A. repeat (rewrite (satz29 y1) in A). rewrite (satz33b A). reflexivity. Qed. Lemma frac_equal_den (x y:frac) : x ~ y -> den x = den y -> x = y. intros [x1 x2] [y1 y2] A B. simpl in *. subst x2. unfold eq_frac_prop in A. rewrite (satz33b A). reflexivity. Qed. (** ** 2 Order of fractions *) (* Order equivalences *) Lemma frac_order_equiv_a {x y:frac} : x ~ y -> x ~~ y. intros [x1 x2] [y1 y2]. apply nat_order_equiv_c. Qed. Lemma frac_order_equiv_b {x y:frac} : x ~~ y -> x ~ y. intros [x1 x2] [y1 y2]. apply nat_order_equiv_d. Qed. Lemma frac_order_equiv_c {x y:frac} : x <~ y -> x ~ y \/ x < y. intros x y. intros A. case_eq (x x <~ y. intros x y A. case_eq (x~~y); intros B. exact I. case_eq (x x~y. intros x y A. rewrite A. apply satz37. Qed. Definition equal_frac (x y:frac):bool := match x, y with (x1/x2), (y1/y2) => andb (x1==y1) (x2==y2) end. Lemma equal_frac_ref {x:frac} : equal_frac x x. intros [x1 x2]. induction x1. induction x2. exact I. exact IHx2. exact IHx1. Qed. Lemma eq_frac_equiv_a {x y:frac} : x = y -> equal_frac x y. intros x y A. rewrite A. exact equal_frac_ref. Qed. Lemma eq_frac_equiv_b {x y:frac} : equal_frac x y -> x = y. intros [x1 x2] [y1 y2]. unfold equal_frac. case_eq (x1==y1); intros A; case_eq (x2==y2); intros B; simpl; try tauto. intros _. rewrite (nat_order_equiv_d (reflect_eq2 A)). rewrite (nat_order_equiv_d (reflect_eq2 B)). reflexivity. Qed. Lemma lt_frac_irreflexive : irreflexive frac lt_frac. intros [x1 x2]. apply lt_nat_irreflexive. Qed. Lemma leq_frac_reflexive : reflexive frac (fun x y => x <~ y). intros [x1 x2]. apply frac_order_equiv_d. left. apply satz37. Qed. (** Trichotomy *) Theorem satz41H0 (x y:frac) : x x~y -> False. intros [x1 x2] [y1 y2]. unfold lt_frac, eq_frac_prop. apply satz10H1. Qed. Theorem satz41H2 (x y:frac) : y x False. intros [x1 x2] [y1 y2]. unfold lt_frac. apply satz10H2. Qed. Theorem satz41H3 (x y:frac) : x x~y -> False. intros [x1 x2] [y1 y2]. unfold lt_frac, eq_frac_prop. apply satz10H3. Qed. Theorem satz44 {x y z u:frac} : x x~z -> y~u -> z x~z -> y~u -> z<~u. intros x y z u A B C. apply frac_order_equiv_d. destruct (frac_order_equiv_c A) as [D|D]. left. apply (satz39 _ _ _ (satz39 _ _ _ (satz38 _ _ B) D) C). right. apply (satz44 D B C). Qed. Theorem satz47 {x y z u:frac} : x<~y -> x~z -> y~u -> z<~u. intros x y z u A B C. apply frac_order_equiv_d. destruct (frac_order_equiv_c A) as [D|D]. left. apply (satz39 _ _ _ (satz39 _ _ _ (satz38 _ _ B) D) C). right. apply (satz44 D B C). Qed. (** Transitivity of > *) Theorem satz50 : transitive frac (fun x y => x < y). intros [x1 x2] [y1 y2] [z1 z2] A B. unfold lt_frac in A. unfold lt_frac in B. unfold lt_frac. assert (C:leq_nat (S((x1*y2)*(y1*z2))) ((y1*x2)*(z1*y2))). apply (satz34 A B). rewrite (satz29 (y1*x2)) in C. rewrite satz39H0 in C. rewrite (satz39H0 z1) in C. exact (satz33a C). Qed. Theorem satz51a {x y z:frac} : x<~y -> y x y<~z -> x x <~y). intros x y z A B. apply frac_order_equiv_d. destruct (frac_order_equiv_c A) as [C|C]. destruct (frac_order_equiv_c B) as [D|D]. left. apply (satz39 _ _ _ C D). right. apply (satz44 D (satz38 _ _ C) (satz37 _)). right. exact (satz51b C B). Qed. Theorem satz53 {x:frac} : exists y, x exists z, x ((x1*y2+y1*x2)/(x2*y2)) end. Notation "x + y":=(add_frac x y). Theorem satz56 {x y z u:frac} : x~y -> z~u -> x+z ~ y+u. intros [x1 x2] [y1 y2] [z1 z2] [u1 u2] A B. unfold eq_frac_prop. unfold add_frac. unfold eq_frac_prop in A. unfold eq_frac_prop in B. repeat rewrite satz30'. rewrite (satz31 z1). rewrite <-(satz31 x2),(satz29 (x2*y2) u2), <-(satz31 z1 u2),(satz32b _ _ _ B),(satz39H0 u1 y2). rewrite satz31,<-(satz31 z2),(satz29 z2 y2). rewrite (satz31 y1 u2),(satz29 u2), (satz31 x2),<-(satz31 y1). rewrite satz31,<-satz31. apply (satz19b _ _ _ (satz32b _ _ _ A)). Qed. Theorem satz57 {x1 x2 x:nat} : x1/x + x2/x ~ (add_nat x1 x2)/x. intros x1 x2 x. unfold eq_frac_prop. unfold add_frac. rewrite<- satz30',satz31. reflexivity. Qed. Theorem satz58 (x y:frac) : x+y ~ y+x. intros [x1 x2] [y1 y2]. unfold eq_frac_prop. unfold add_frac. rewrite satz6,(satz29 x2 y2). reflexivity. Qed. Theorem satz59 {x y z} : (x+y)+z ~ x+(y+z). intros [x1 x2] [y1 y2] [z1 z2]. unfold add_frac. rewrite <- (satz31 x2 y2 z2),(satz29 x2 y2),satz30'. rewrite (satz31 x1 y2 z2),(satz29 y1 x2),<-(satz31 z1 y2 x2). rewrite (satz31 x2 y1 z2). rewrite (satz29 x2 (y1*z2)),(satz5 (x1*(y2*z2)) _ _). rewrite <-satz30'. reflexivity. Qed. Theorem satz60 {x y:frac} : x x+z x+z x+z~y+z. intros x y z A. exact (satz56 A (satz37 _)). Qed. Theorem satz63a {x y z:frac} : x+z x x~y. intros x y z A. destruct (satz41H0 x y) as [B|[B|B]]. contradiction (satz41H3 _ _ (satz62a B) A). exact B. contradiction (satz41H1 _ _ (satz62a B) A). Qed. Theorem satz64 {x y z u:frac} : x z x+z z x+z z<~u -> x+z z<~u -> x+z<~y+u. intros x y z u A B. apply frac_order_equiv_d. destruct (frac_order_equiv_c A) as [C|C]. destruct (frac_order_equiv_c B) as [D|D]. left. exact (satz56 C D). right. exact (satz65a A D). right. exact (satz65b C B). Qed. Theorem satz67a {x y:frac} : y exists u, y+u~x. intros [x1 x2] [y1 y2] A. unfold lt_frac in A. destruct (nat_order_equiv_b A) as [u B]. exists (u/(x2*y2)). assert (C:y1/y2+u/(x2*y2)~(y1*x2)/(x2*y2)+u/(x2*y2)). rewrite satz29. exact (satz56 satz40 (satz37 _)). assert (D: (x1*y2)/(x2*y2) ~ x1/x2). apply (satz38 _ _ satz40). rewrite B in D. exact (satz39 _ _ _ (satz39 _ _ _ C satz57) D). Qed. Theorem satz67b {x y v w:frac} : v+y~x -> w+y~x -> v~w. intros x y v w A B. exact (satz63b (satz39 _ _ _ A (satz38 _ _ B))). Qed. Theorem satz67c {x y:frac} : x<~y -> forall u, y+u~x -> False. intros x y A u B. exact (satz41H3 _ _ (satz44 (satz51a A satz60) (satz38 _ _ B) (satz37 _)) (satz37 (y+u))). Qed. (* Definition of Minus: u from satz67 is x-y *) Fixpoint sub_frac (x y:frac) : y frac := match x,y with | (x1/x2), (y1/y2) => fun (l:y1/y2 (sub_nat (x1*y2) (y1*x2) l)/(x2*y2) end. Theorem sub_frac_correct_a (x y:frac) (l: x < y) : y ~ x + (sub_frac y x l). intros [x1 x2] [y1 y2] A. unfold eq_frac_prop. unfold add_frac. simpl. rewrite <-(satz31 x1 y2 x2). rewrite (satz29 (x1*y2) x2), (satz29 (sub_nat (y1*x2) (x1*y2) A) x2). rewrite <- (@satz30 x2). rewrite sub_nat_correct_a. rewrite <-(satz31 y1 x2),(satz29 y1 x2),(satz31 x2 y1),(satz29 y2 x2). rewrite <-(satz31 y1 x2),(satz29 y1 x2),<-(satz31 x2 _ y2). reflexivity. Qed. (** ** 4 Multiplication of fractions *) Definition mul_frac (x y:frac) := match x,y with x1/x2 , y1/y2 => (x1*y1)/(x2*y2) end. Notation "x * y" :=(mul_frac x y). Lemma satz68' (x y z u:nat) : mul_nat (mul_nat x y)(mul_nat z u) = mul_nat (mul_nat x z)(mul_nat y u). intros x y z u. rewrite satz31. rewrite <-(satz31 y z u). rewrite (satz29 y z). rewrite satz31,<-satz31. reflexivity. Qed. Theorem satz68 {x y z u:frac} : x~y -> z~u -> x*z~y*u. intros [x1 x2] [y1 y2] [z1 z2] [u1 u2]. unfold mul_frac. unfold eq_frac_prop. intros A B. rewrite satz68',(satz68' y1 u1 x2 z2). rewrite B. exact (satz32b _ _ _ A). Qed. Theorem satz69 (x y:frac) : x*y ~ y*x. intros [x1 x2] [y1 y2]. unfold mul_frac. rewrite (satz29 x1 y1),(satz29 x2 y2). apply satz37. Qed. Theorem satz70 {x y z:frac} : (x*y)*z ~ x*(y*z). intros [x1 x2] [y1 y2] [z1 z2]. unfold mul_frac. rewrite (satz31 x1 y1 z1),(satz31 x2 y2 z2). apply satz37. Qed. Theorem satz71 {x y z:frac} : x*(y+z) ~ x*y + x*z. intros [x1 x2] [y1 y2] [z1 z2]. assert (A: (mul_nat (mul_nat x1 y1) z2)/(mul_nat (mul_nat x2 y2) z2) +(mul_nat (mul_nat x1 z1) y2)/(mul_nat (mul_nat x2 z2) y2) ~ (mul_nat x1 y1)/(mul_nat x2 y2)+(mul_nat x1 z1)/(mul_nat x2 z2)). exact (satz38 _ _ (satz56 satz40 satz40)). unfold mul_frac. assert (B: (mul_nat x1 (add_nat (mul_nat y1 z2) (mul_nat z1 y2))/ (mul_nat x2 (mul_nat y2 z2)) ~(add_nat (mul_nat x1 (mul_nat y1 z2)) (mul_nat x1 (mul_nat z1 y2)))/ (mul_nat x2 (mul_nat y2 z2)))). rewrite satz30. apply satz37. repeat rewrite satz31 in A. rewrite (satz29 z2 y2) in A. apply (satz39 _ _ _ (satz39 _ _ _ B (satz38 _ _ satz57)) A). Qed. Theorem satz72a (x y z:frac) : x x*z x*z~y*z. intros x y z A. exact (satz68 A (satz37 z)). Qed. Theorem satz73a {x y z:frac} : x*z x x~y. intros x y z A. destruct (satz41H0 x y) as [B|[B|B]]. contradiction (satz41H3 _ _ (satz72a _ _ _ B) A). exact B. contradiction (satz41H1 _ _ (satz72a _ _ _ B) A). Qed. Theorem satz74a {x y z u:frac} : x z x*z z x*z z<~u -> x*z z<~u -> x*z<~y*u. intros x y z u A B. apply frac_order_equiv_d. destruct (frac_order_equiv_c A) as [C|C]. destruct (frac_order_equiv_c B) as [D|D]. left. exact (satz68 C D). right. exact (satz75a A D). right. exact (satz75b C B). Qed. Theorem satz77a {x y:frac} : exists u, y*u~x. intros [x1 x2] [y1 y2]. exists ((mul_nat x1 y2)/(mul_nat x2 y1)). assert (A:(mul_nat x1 y2)/(mul_nat x2 y1)*(y1/y2) ~ (mul_nat x1 (mul_nat y1 y2))/(mul_nat x2 (mul_nat y1 y2))). unfold mul_frac. rewrite satz31,satz31,(satz29 y2 y1). apply satz37. exact (satz39 _ _ _ (satz69 _ _) (satz39 _ _ _ A (satz38 _ _ satz40))). Qed. Theorem satz77b {x y v w:frac} : v*y~x -> w*y~x -> v~w. intros x y v w A B. exact (satz73b (satz39 _ _ _ A (satz38 _ _ B))). Qed. Coercion nat_to_frac (x:nat) := x/O. Definition inv_mul_frac (x:frac) := match x with x1/x2 => x2/x1 end. Lemma inv_mul_frac_correct (x:frac) : inv_mul_frac x * x ~ O. intros [x1 x2]; unfold inv_mul_frac. simpl. rewrite satz29. exact (satz29 _ _). Qed. (* End of fractions *)