Library fractions

Require Import algebra.
Require Import logical.
Require Import naturals.

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<y1*x2
end.

Definition eq_frac_prop (x y:frac) := match (x,y) with
(x1/x2 , y1/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).

Theorem satz37 : reflexive frac eq_frac_prop.
intros [x1 x2].
reflexivity.
Qed.

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.

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.

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.

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.

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<y). simpl; tauto.
case_eq (x~~y); intros C. left. apply frac_order_equiv_b.
rewrite C. exact I.
intros B. rewrite B,C in A. contradiction A.
Qed.

Lemma frac_order_equiv_d {x y:frac} : x ~ y \/ x < y -> x <~ y.
intros x y A.
case_eq (x~~y); intros B. exact I.
case_eq (x<y); intros C. exact I.
simpl.
destruct A as [A|A].
generalize (frac_order_equiv_a A); intros D.
rewrite B in D. contradiction D.
rewrite C in A. contradiction A.
Qed.

Lemma eq_frac_lemma {x y:frac} : x=y -> 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.

Theorem satz41H0 (x y:frac) : x<y\/x~y\/y<x.
intros [x1 x2] [y1 y2]. unfold eq_frac_prop. unfold lt_frac.
apply satz10H0.
Qed.

Theorem satz41H1 (x y:frac) : y<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 -> x<y -> False.
intros [x1 x2] [y1 y2]. unfold lt_frac. apply satz10H2.
Qed.

Theorem satz41H3 (x y:frac) : x<y -> 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<y -> x~z -> y~u -> z<u.
intros [x1 x2] [y1 y2] [z1 z2] [u1 u2] A B C.
unfold lt_frac in A. unfold eq_frac_prop in B. unfold eq_frac_prop in C. unfold lt_frac.
assert (D:(y1*u2)*(z1*x2)=(u1*y2)*(x1*z2)).
rewrite B. exact (satz32b _ _ _ C).
rewrite (satz39H0 y1 u2 z1 x2) in D. rewrite (satz39H0 u1 y2 x1 z2) in D.
assert (E: leq_nat (S((u1*z2)*(x1*y2))) ((u1*z2)*(y1*x2))).
rewrite satz29,(satz29 (u1*z2)). apply (satz32a A).
rewrite<- D in E. rewrite (satz29 (mul_nat y1 x2)) in E. apply (satz33a E).
Qed.

Theorem satz46 {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.

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.

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<z -> x<z.
intros x y z A B.
destruct (frac_order_equiv_c A) as [D|D].
exact (satz44 B (satz38 _ _ D) (satz37 _)).
exact (satz50 _ _ _ D B).
Qed.

Theorem satz51b {x y z:frac} : x<y -> y<~z -> x<z.
intros x y z A B.
destruct (frac_order_equiv_c B) as [C|C].
exact (satz44 A (satz37 _) C).
exact (satz50 _ _ _ A C).
Qed.

Theorem satz52a : transitive frac (fun x y => 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<y.
intros [x1 x2]. exists ((x1+x1)/x2). unfold lt_frac. rewrite (satz29 (x1+x1) _).
rewrite satz30, satz29. apply satz18.
Qed.

Theorem satz54 {x:frac} : exists y, y<x.
intros [x1 x2].
exists (x1/(x2+x2)). unfold lt_frac.
rewrite satz30. apply (satz18 _ _).
Qed.

Theorem satz55 {x y:frac} : x<y -> exists z, x<z /\z<y.
intros [x1 x2] [y1 y2] A. exists ((x1+y1)/(x2+y2)). unfold lt_frac in A.
split. unfold lt_frac.
rewrite satz30,(satz29 (x1+y1)),satz30,(satz29 x2),(satz29 x2),
satz6,(satz6 (x1*x2)).
exact (satz19a A).
unfold lt_frac. rewrite satz29. repeat rewrite satz30.
repeat rewrite (satz29 y2). exact (satz19a A).
Qed.

Definition add_frac (x y:frac) := match (x,y) with
(x1/x2 , y1/y2) => ((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+y.
intros [x1 x2] [y1 y2]. unfold lt_frac. unfold add_frac.
rewrite satz30',(satz31),(satz29 y2 x2). apply satz18.
Qed.

Lemma satz61' (x y z:nat) : (x*y)*z = (x*z)*y.
intros x y z. rewrite satz31,(satz29 y z),satz31. reflexivity.
Qed.

Theorem satz61 (x y z:frac) : x<y -> x+z<y+z.
intros [x1 x2] [y1 y2] [z1 z2] A. unfold add_frac. unfold lt_frac.
unfold lt_frac in A.
assert (B:leq_nat (S((x1*y2)*z2)) ((y1*x2)*z2)). apply (satz32a A).
rewrite (satz61' x1 y2 z2) in B.
rewrite (satz61' y1 x2 z2) in B.
assert (C:leq_nat (S((add_nat (x1*z2)(z1*x2))*y2)) ((add_nat (y1*z2)(z1*y2))*x2)).
rewrite satz30',satz30'.
assert (D:(z1*x2)*y2=(z1*y2)*x2).
exact (satz61' _ _ _).
rewrite D.
exact (satz19a B).
rewrite <-satz31,<-satz31. exact (satz32a C).
Qed.

Theorem satz62a {x y z:frac} : x<y -> x+z<y+z.
intros x y z. apply satz61.
Qed.

Theorem satz62b {x y z:frac} : x~y -> x+z~y+z.
intros x y z A. exact (satz56 A (satz37 _)).
Qed.

Theorem satz63a {x y z:frac} : x+z<y+z -> x<y.
intros x y z A. destruct (satz41H0 x y) as [B|[B|B]].
exact B.
contradiction (satz41H3 _ _ A (satz62b B)).
contradiction (satz41H2 _ _ A (satz62a B)).
Qed.

Theorem satz63b {x y z:frac} : x+z~y+z -> 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<y -> z<u -> x+z<y+u.
intros x y z u A B.
exact (satz50 _ _ _ (satz61 x y z A)
   (satz44 (satz61 z u y B) (satz58 z y) (satz58 u y))).
Qed.

Theorem satz65a {x y z u:frac} : x<~y -> z<u -> x+z<y+u.
intros x y z u A B.
destruct (frac_order_equiv_c A) as [C|C].
exact (satz44 (satz44 (satz61 _ _ x B) (satz58 z x)
   (satz58 u x)) (satz37 (x+z)) (satz56 C (satz37 u))).
exact (satz64 C B).
Qed.

Theorem satz65b {x y z u:frac} : x<y -> z<~u -> x+z<y+u.
intros x y z u A B.
destruct (frac_order_equiv_c B) as [C|C].
exact (satz44 (satz61 _ _ z A) (satz37 (x+z)) (satz56 (satz37 y) C)).
exact (satz64 A C).
Qed.

Theorem satz66a {x y z u:frac} : x<~y -> 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<x -> 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.


Fixpoint sub_frac (x y:frac) : y<x -> frac := match x,y with
| (x1/x2), (y1/y2) => fun (l:y1/y2<x1/x2) => (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.

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<y -> x*z<y*z.
intros [x1 x2] [y1 y2] [z1 z2] A.
unfold mul_frac. unfold lt_frac. unfold lt_frac in A.
rewrite (satz68' x1),(satz68' y1).
exact (satz32a A).
Qed.

Theorem satz72b (x y z:frac) : x~y -> x*z~y*z.
intros x y z A.
exact (satz68 A (satz37 z)).
Qed.

Theorem satz73a {x y z:frac} : x*z<y*z -> x<y.
intros x y z A.
destruct (satz41H0 x y) as [B|[B|B]].
exact B.
contradiction (satz41H3 _ _ A (satz72b _ _ _ B)).
contradiction (satz41H2 _ _ A (satz72a _ _ _ B)).
Qed.

Theorem satz73b {x y z:frac} : x*z~y*z -> 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<y -> z<u -> x*z<y*u.
intros x y z u A B.
exact (satz50 _ _ _ (satz72a _ _ _ A)
   (satz44 (satz72a _ _ _ B) (satz69 _ _) (satz69 _ _))).
Qed.

Theorem satz75a {x y z u:frac} : x<~y -> z<u -> x*z<y*u.
intros x y z u A B.
destruct (frac_order_equiv_c A) as [C|C].
exact (satz44 (satz44 (satz72a _ _ x B) (satz69 z x)
   (satz69 u x)) (satz37 (x*z)) (satz68 C (satz37 u))).
exact (satz74a C B).
Qed.

Theorem satz75b {x y z u:frac} : x<y -> z<~u -> x*z<y*u.
intros x y z u A B.
destruct (frac_order_equiv_c B) as [C|C].
exact (satz44 (satz72a _ _ z A) (satz37 (x*z)) (satz68 (satz37 y) C)).
exact (satz74a A C).
Qed.

Theorem satz76a {x y z u:frac} : x<~y -> 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.