# Library Q_misc

``` Set Implicit Arguments. Require Import ZArith. Require Import Znumtheory. Require Import Z_misc. Require Import QArith. Require Import Decidable. Require Import misc. Definition Q_of_nat (n:nat) := (inject_Z (Z_of_nat n)). Coercion Local Q_of_nat : nat >-> Q. Coercion Local inject_Z : Z >-> Q. Definition in_Z (x: Q) :=   exists y:Z, x == inject_Z y.   forall x: Q,   decidable (in_Z x). *) Property nat_in_Z:   forall n: nat,   in_Z (Q_of_nat n). Proof.   intro.   exists (Z_of_nat n).   unfold Qeq, Q_of_nat.   reflexivity. Qed. Property Qplus_in_Z_compat:   forall q: Q,   forall x: Z,   in_Z q -> in_Z (q + x). Proof.   intros q x H_in_Z.   unfold in_Z in *.   elim H_in_Z.   intros q' H_q'.   exists (q' + x)%Z.   rewrite H_q'.   unfold Qeq, Q_of_nat, Qplus.   simpl.   repeat rewrite Zmult_1_r.   reflexivity. Qed. Lemma n_plus_1_eq_S_n:   forall n: nat, (n + 1)%Q = S n. Proof.   intro n.   unfold Q_of_nat, inject_Z, Z_of_nat.   destruct n; [reflexivity |].   do 2 rewrite Zpos_P_of_succ_nat.   rewrite inj_S.   unfold Qplus; simpl; apply f_equal2; auto.   ring. Qed. Theorem S_n_m_1_eq_n: forall n : nat, ((S n) - 1)%Q = n. Proof.   intros.   rewrite <- n_plus_1_eq_S_n.   unfold Q_of_nat, inject_Z, Z_of_nat.   destruct n; [reflexivity |].   rewrite Zpos_P_of_succ_nat.   unfold Qminus;   unfold Qplus; simpl.   apply f_equal2; auto.   ring. Qed. Lemma Zplus_eq_Qplus:   forall x y: Z,   ((x + y)%Z == x + y)%Q. Proof.   intros; unfold Qeq; simpl; omega. Qed. Lemma Qmult_lt_0_lt_reg_r : forall x y z, 0 < z -> x*z < y*z -> x < y. Proof.   intros (a1,a2) (b1,b2) (c1,c2); unfold Qlt; simpl.   Open Scope Z_scope.   simpl_mult.   replace (a1*c1*('b2*'c2)) with ((a1*'b2)*(c1*'c2)) by ring.   replace (b1*c1*('a2*'c2)) with ((b1*'a2)*(c1*'c2)) by ring.   intros; apply Zmult_lt_reg_r with (c1*'c2); auto with zarith.   ring_simplify in H.   assert (0 = 0 * c1).     compute.     trivial.   rewrite H1.   replace (c1 * 'c2) with ('c2 * c1) by ring.   eapply Zmult_lt_compat_r; auto.   compute.   trivial.   Close Scope Z_scope. Qed. Lemma Qinv_pos_strict:   forall x,   forall H_x_pos: x > 0,   0 < / x. Proof.   intros.   apply Qmult_lt_0_lt_reg_r with x; auto.   ring_simplify.   rewrite Qmult_inv_r.     unfold Q_of_nat, Qlt.     simpl.     auto with zarith.     unfold Qlt in H_x_pos.     simpl in H_x_pos.     ring_simplify in H_x_pos.     unfold Q_of_nat, Qeq.     simpl.     auto with zarith. Qed. Lemma Qinv_pos:   forall x,   forall H_x_pos: x > 0,   0 <= / x. Proof.   intros.   apply Qmult_lt_0_le_reg_r with x; auto.   apply Qle_trans with 0; ring_simplify.     apply Qle_refl.   rewrite Qmult_comm.   rewrite Qmult_inv_r.     unfold Q_of_nat, Qle.     simpl.     auto with zarith arith.     unfold Qlt in H_x_pos.     simpl in H_x_pos.     ring_simplify in H_x_pos.     unfold Q_of_nat, Qeq.     simpl.     auto with zarith. Qed. Theorem Qinv_ge_inv:   forall x,   forall H_x: x >= 1,   / x <= 1. Proof.   intros.   simpl in H_x.   assert (H_x_pos: x > 0).     assert (0 < 1).       unfold Q_of_nat, Qlt; simpl; auto with zarith.     apply (Qlt_le_trans 0 1 x H H_x).   apply (Qmult_lt_0_le_reg_r (/x) 1 x H_x_pos).   ring_simplify.   rewrite Qmult_comm.   rewrite Qmult_inv_r.   assumption.   unfold Qlt in H_x_pos.   unfold Qeq.   auto with zarith. Qed. Theorem Qdiv_le_compat:   forall x y z,   forall H_z_pos: z > 0,   forall H_x_le_y: x <= y,   x / z <= y / z. Proof.   intros.   unfold Qdiv.   apply Qmult_le_compat_r; auto with qarith.   eapply Qinv_pos.   assumption. Qed. Theorem le_impl_Qle:   forall (x:nat) (y: nat),   forall H_nat: (x <= y)%nat,     x <= y. Proof.   intros.   unfold Q_of_nat, Qle.   simpl.   ring_simplify.   auto with zarith arith. Qed. Theorem ge_impl_Qge:   forall (x:nat) (y: nat),   forall H_nat: (x >= y)%nat,     x >= y. Proof.   intros.   unfold Q_of_nat.   unfold Qle.   simpl.   ring_simplify.   auto with zarith arith. Qed. Theorem Qle_impl_le:   forall (x:nat) (y: nat),   forall H_Q: x <= y,     (x <= y)%nat. Proof.   intros.   unfold Q_of_nat, Qle in H_Q.   simpl in H_Q.   replace ((Z_of_nat x * 1)%Z) with ((Z_of_nat x)%Z) in H_Q by ring.   replace ((Z_of_nat y * 1)%Z) with ((Z_of_nat y)%Z) in H_Q by ring.   apply inj_le_rev.   assumption. Qed. Theorem Zle_impl_Qle:   forall (x:Z) (y: Z),   forall H_Z: (x <= y)%Z,     inject_Z x <= inject_Z y. Proof.   intros.   unfold Q_of_nat, Qle.   simpl.   ring_simplify.   auto with zarith arith. Qed. Theorem Qle_impl_Zle:   forall (x:Z) (y: Z),   forall H_Q: (x <= y)%Q,     (x <= y)%Z. Proof.   intros.   unfold Q_of_nat, Qle in H_Q.   simpl in H_Q.   ring_simplify in H_Q.   auto with zarith arith. Qed. Theorem Qeq_impl_Zeq:   forall (x:Z) (y: Z),   forall H_Q: (x == y)%Q,     (x = y)%Z. Proof.   intros.   unfold Q_of_nat, Qeq in H_Q.   simpl in H_Q.   ring_simplify in H_Q.   auto with zarith arith. Qed. Theorem lt_impl_Qlt:   forall (x:nat) (y:nat),   forall H_Z: (x < y)%nat,     Q_of_nat x < Q_of_nat y. Proof.   intros.   unfold Q_of_nat, Qlt.   simpl.   ring_simplify.   auto with zarith arith. Qed. Theorem Zlt_impl_Qlt:   forall (x:Z) (y: Z),   forall H_Z: (x < y)%Z,     inject_Z x < inject_Z y. Proof.   intros.   unfold Q_of_nat, Qlt.   simpl.   ring_simplify.   auto with zarith arith. Qed. Theorem Qlt_impl_Zlt:   forall (x:Z) (y: Z),   forall H_Q: inject_Z x < inject_Z y,     (x < y)%Z. Proof.   intros.   unfold Q_of_nat, Qlt in H_Q.   simpl in H_Q.   ring_simplify in H_Q.   auto with zarith arith. Qed. Theorem Qlt_impl_lt:   forall (x:nat) (y: nat),   forall H_Q: Q_of_nat x < Q_of_nat y,     (x < y)%nat. Proof.   intros.   unfold Q_of_nat, Qlt in H_Q.   simpl in H_Q.   ring_simplify in H_Q.   auto with zarith arith. Qed. Theorem le_impl_Zle:   forall (x:nat) (y: nat),   forall H_nat: (x <= y)%nat,     (Z_of_nat x <= Z_of_nat y)%Z. Proof.   intros.   apply inj_le.   assumption. Qed. Theorem abs_le_compat:   forall x y,   forall a d r,   forall H_r: r > 0,   forall H_x_le_y: x <= y,   forall H_a_le_x_m_d_div_r: a <= (x - d) / r,   a <= (y - d) / r. Proof.   intros.   simpl in H_a_le_x_m_d_div_r.   eapply (Qle_trans a ((x - d) / r) ((y - d) / r)); auto.   eapply Qdiv_le_compat; auto.   unfold Qminus.   eapply Qplus_le_compat; auto.   eapply Qle_refl. Qed. Theorem abs_le_compat_prim:   forall x y,   forall a d r,   forall H_r: r >= 0,   forall H_x_le_y: x <= y,   forall H_a_le_x_m_d_div_r: a <= (x - d) * r,   a <= (y - d) * r. Proof.   intros.   simpl in H_a_le_x_m_d_div_r.   eapply (Qle_trans a ((x - d) * r) ((y - d) * r)); auto.   eapply Qmult_le_compat_r; auto.   unfold Qminus.   eapply Qplus_le_compat; auto.   eapply Qle_refl. Qed. Theorem Qplus_eq_compat:   forall a b x y,   forall H_a_eq_b: a == b,   forall H_x_eq_y: x == y,   a + x == b + y. Proof.   intros.   rewrite H_x_eq_y.   rewrite H_a_eq_b.   apply Qeq_refl. Qed. Theorem Qplus_lt_compat_l:   forall a x y,   forall H_x_eq_y: x < y,   a + x < a + y. Proof.   intros.   apply <- Qlt_minus_iff.   assert (H_aux: a + y + - (a + x) == y + - x).     ring.   rewrite H_aux; clear H_aux.   apply -> Qlt_minus_iff.   assumption. Qed. Theorem Qle_plus:   forall a x y,   forall H_x_le_y: a + x <= a + y,   x <= y. Proof.   intros.   assert (H_m_a_le_m_a: -a <= -a).     apply Qle_refl.   generalize (Qplus_le_compat (-a) (-a) (a+x) (a+y) H_m_a_le_m_a H_x_le_y).   intro H_cc.   ring_simplify in H_cc.   exact H_cc. Qed. Theorem Qlt_plus:   forall a x y,   a + x < a + y <-> x < y. Proof.   intros.   split.     intros.     apply <- Qlt_minus_iff.     assert (H_aux: (y + - x) == ((a + y) + - (a + x))).       ring.     rewrite H_aux; clear H_aux.     apply -> Qlt_minus_iff; assumption.     intros.     apply <- Qlt_minus_iff.     assert (H_aux: (y + - x) == ((a + y) + - (a + x))).       ring.     rewrite <- H_aux; clear H_aux.     apply -> Qlt_minus_iff; assumption. Qed. Lemma plus_impl_Qplus:   forall x y: nat,     (x + y)% nat == (x + y)%Q. Proof.   intros.   induction x.     simpl.     rewrite Qplus_0_l.     reflexivity.     assert (H_aux: (S x + y = S (x + y))%nat);       auto with arith.     rewrite H_aux; clear H_aux.     rewrite <- n_plus_1_eq_S_n.     rewrite <- n_plus_1_eq_S_n.     assert (H_aux: x + 1 + y == (x + y) + 1).       ring.     rewrite H_aux; clear H_aux.     apply Qplus_eq_compat; auto.     apply Qeq_refl. Qed. Lemma minus_impl_Qminus:   forall x y: nat,   forall H_x_le_y: (x <= y)%nat,     (y - x)% nat == (y - x)%Q. Proof.   intros.   induction x.     unfold Q_of_nat, Qminus, Qeq, Qplus.     simpl.     ring_simplify.     rewrite <- minus_n_O.     trivial.     assert (H_x'_le_y: (x <= y)%nat).       apply le_Sn_le.       assumption.     rewrite <- n_plus_1_eq_S_n.     assert (H_aux: y - (x + 1) == (y - 1) - x).       ring.     rewrite H_aux; clear H_aux.    case_eq y.      intro H_y.      rewrite H_y in H_x_le_y.      generalize (le_Sn_O x).      congruence.      intros y' H_y.      assert (H_aux: S y' - 1 = y').        eapply (S_n_m_1_eq_n y').      rewrite H_aux; clear H_aux.      simpl.      unfold Q_of_nat, Qeq, Qminus, Qplus; simpl.      ring_simplify.      rewrite inj_minus1; auto.      rewrite H_y in H_x_le_y.      auto with arith. Qed. Theorem simply_1:   forall d1 r1 d2 r2 i,   forall H_r1_pos: r1 > 0,   forall H_r2_pos: r2 > 0,   ((i - d1) / r1 - d2) / r2 == (i - (d1 + d2 * r1)) / (r1 * r2). Proof.   intros.   field.   simpl in H_r1_pos.   simpl in H_r2_pos.   unfold Qlt in H_r1_pos.   unfold Qlt in H_r2_pos.   unfold Qeq.   split; auto with zarith. Qed. Theorem simply_1_prim:   forall d1 r1 d2 r2 i,   forall H_r1_non_null: ~ r1 == 0,   ((i - d1) * r1 - d2) * r2 == (i - (d1 + d2 / r1)) * (r1 * r2). Proof.   intros.   field.   assumption. Qed. Property QDen_Qred_def:   forall x: Q,   (QDen (Qred x) = Zdiv (QDen x) (Zgcd (Qnum x) (QDen x)))%Z. Proof.   intros.   unfold Qred.   destruct x.   case_eq (Zggcd Qnum (Zpos Qden)).   intros z [r1 r2] H_eq.   rewrite <- Zggcd_gcd.   simpl.   rewrite H_eq.   simpl.   assert (H:= Zggcd_correct_divisors Qnum (Zpos Qden) ).   rewrite H_eq in H; destruct H.   rewrite H0.   rewrite Zmult_comm.   assert (0 < z)%Z.     assert (H_gcd:= Zgcd_gt_0_r Qnum (Zpos Qden)).     rewrite <- Zggcd_gcd in H_gcd.     rewrite H_eq in H_gcd.     simpl in H_gcd.     apply H_gcd.     compute.     reflexivity.   rewrite Z_div_mult_full.   assert (0 < r2)%Z.     assert (H_z:= Zsgn_Zmult z r2).     rewrite <- H0 in H_z.     simpl in H_z.     rewrite <- Zsgn_pos in H1.     rewrite H1 in H_z.     rewrite Zmult_1_l in H_z.     symmetry in H_z.     rewrite Zsgn_pos in H_z.     assumption.     destruct r2; compute in H1; try discriminate; auto.   intro abs.   subst.   exact (Zlt_irrefl 0 H1). Qed. Property QDen_Qred_x_le_QDen_x:   forall x: Q,   (QDen (Qred x) <= QDen x)%Z. Proof.   intros.   rewrite QDen_Qred_def.   assert ((0 < Zgcd (Qnum x) (' Qden x))%Z).     apply Zgcd_gt_0_r.     compute.     reflexivity.   apply Zdiv_le_upper_bound; auto with zarith.   rewrite <- (Zmult_1_r (Zpos (Qden x))) at 1.   apply Zmult_le_compat_l.   2: (compute; intro; discriminate).   omega. Qed. Property inv_Qden_x_le_inv_Qden_Qred_x:   forall x: Q,   (1 # Qden x <= 1 # Qden (Qred x)). Proof.   intros.   unfold Qle, Qnum, Qden.   fold (Qden x).   fold (Qden (Qred x)).   repeat rewrite Zmult_1_l.   apply QDen_Qred_x_le_QDen_x. Qed. Definition Qmin (n m:Q) :=   match n ?= m with     | Eq | Lt => n     | Gt => m   end. Lemma Qle_min_l:   forall n m : Q, Qmin n m <= n. Proof.   intros.   unfold Qmin.   case_eq (n ?= m); try solve [ intros; apply Qle_refl ].   rewrite <- Qgt_alt.   apply Qlt_le_weak. Qed. Lemma Qle_min_r:   forall n m : Q, Qmin n m <= m. Proof.   intros.   unfold Qmin.   case_eq (n ?= m); try solve [ intros; apply Qle_refl ].     rewrite <- Qeq_alt.     intro H_cmp; rewrite H_cmp; apply Qle_refl.     rewrite <- Qlt_alt.     apply Qlt_le_weak. Qed. Lemma Qmin_dec : forall n m:Q, {Qmin n m = n} + {Qmin n m = m}. Proof.   unfold Qmin in |- *; intros; elim (n ?= m); auto. Qed. Lemma Qmin_irreducible : forall n m:Q, Qmin n m = n \/ Qmin n m = m. Proof.   intros n m; destruct (Qmin_dec n m); [left|right]; trivial. Qed. Definition Qmax (m n:Q) :=   match m ?= n with     | Eq | Gt => m     | Lt => n   end. Lemma Qle_max_l:   forall n m : Q, n <= Qmax n m. Proof.   intros.   unfold Qmax.   case_eq (n ?= m); try solve [ intros; apply Qle_refl ].   rewrite <- Qlt_alt.   apply Qlt_le_weak. Qed. Lemma Qle_max_r:   forall n m : Q, m <= Qmax n m. Proof.   intros.   unfold Qmax.   case_eq (n ?= m); try solve [ intros; apply Qle_refl ].     rewrite <- Qeq_alt.     intro H_cmp; rewrite H_cmp; apply Qle_refl.     rewrite <- Qgt_alt.     apply Qlt_le_weak. Qed. Lemma Qmax_dec : forall n m:Q, {Qmax n m = n} + {Qmax n m = m}. Proof.   unfold Qmax in |- *; intros; elim (n ?= m); auto. Qed. Lemma Qmax_irreducible : forall n m:Q, Qmax n m = n \/ Qmax n m = m. Proof.   intros n m; destruct (Qmax_dec n m); [left|right]; trivial. Qed. Lemma den_r_le_den_r_i_p_b:   forall r: Q,   forall i: nat,   forall b: Q,   forall H_wf_b: Qden b = Qden r,   1 # Qden r <= 1 # Qden (Qred (r * i + b)). Proof.   intros.   unfold Qle, Qnum, Qden.   fold (Qden (Qred (r * i + b))).   fold (Qden r).   repeat rewrite Zmult_1_l.   simpl.   rewrite H_wf_b.   rewrite Pmult_1_r.   assert (H_aux:     (Zplus       (Zmult (Zmult (Qnum r) (Z_of_nat i)) (Zpos (Qden r)))       (Zmult (Qnum b) (Zpos (Qden r))))     =     (Zmult       (Zplus         (Zmult (Qnum r) (Z_of_nat i))         (Qnum b))       (Zpos (Qden r)))).     ring.   rewrite H_aux; clear H_aux.   case_eq (Zggcd ((Qnum r * (Z_of_nat i) + Qnum b) * ' Qden r) (' (Qden r * Qden r)));   intros z [r1 r2] H_eq; simpl.   pose (H:= Zgcd_is_gcd ((Qnum r * (Z_of_nat i) + Qnum b) * ' Qden r) (' (Qden r * Qden r))).   rewrite <- Zggcd_gcd in H.   rewrite H_eq in H; simpl in H.   inversion_clear H.   assert (H_z: ((Zpos (Qden r)) | z)%Z).     apply H2.     exists (Qnum r * (Z_of_nat i) + Qnum b)%Z; auto.     exists (Zpos (Qden r))%Z; auto with zarith.   assert (Zpos (Qden r) <= z)%Z.     apply Zdivide_le; auto.     compute; intros; discriminate.     change (0 < fst (z, (r1, r2)))%Z; rewrite <- H_eq; rewrite Zggcd_gcd.     apply Zgcd_gt_0_r.     compute; reflexivity.     match goal with     | H_eq : (Zggcd ?X ?Y) = _ |- _ =>       assert (Hcd := Zggcd_correct_divisors X Y); rewrite H_eq in Hcd;         destruct Hcd as [_ Hcd]; revert Hcd H; clear; intros     end.     rewrite Zpos_mult_morphism in Hcd.     assert (H_Qden_r: (0 < Zpos (Qden r))).       compute; reflexivity.     assert (H_cc:       ((Zpos (Qden r) * Zpos (Qden r)) / (Zpos (Qden r)) >= (z * r2) / z)%Z).       rewrite Hcd.       apply Zdiv_le_denom; auto.       rewrite <- Hcd.       apply Zle_ge.       replace 0%Z with (0 * Zpos (Qden r))%Z by omega.       apply Zmult_le_compat_r; apply Zlt_le_weak; assumption.       rewrite Z_div_mult_full in H_cc.       rewrite Zmult_comm in H_cc.       rewrite Z_div_mult_full in H_cc.       rewrite Z2P_correct.       apply Zge_le.       assumption.       apply -> Zsgn_pos.       rewrite <- (Zmult_1_l (Zsgn r2)).       assert (H_z: (Zsgn z = 1)%Z).         apply <- Zsgn_pos.         apply (Zlt_le_trans           0           (Zpos (Qden r))           z); auto.       rewrite <- H_z at 1.       rewrite <- Zsgn_Zmult.       rewrite <- Hcd.       apply <- Zsgn_pos.       replace 0%Z with (0 * Zpos (Qden r))%Z by omega.       apply Zmult_lt_compat_r;         try solve [ compute; reflexivity ].       intro.       symmetry in H0.       absurd (0%Z = z); auto.       apply Zlt_not_eq.       apply (Zlt_le_trans         0         (Zpos (Qden r))         z); auto.       intro.       symmetry in H0.       absurd (0%Z = Zpos (Qden r)); auto.       apply Zlt_not_eq.       compute; reflexivity. Qed. Lemma den_r_i_p_b_le_den_r:   forall r: Q,   forall i: nat,   forall b: Q,   forall H_wf_b: Qden b = Qden r,    1 # Qden (r * i + b) <= 1 # Qden r. Proof.   intros.   unfold Qle, Qnum, Qden.   fold (Qden (r * i + b)).   fold (Qden r).   repeat rewrite Zmult_1_l.   simpl.   rewrite H_wf_b.   rewrite Pmult_1_r.   rewrite <- (Pmult_1_r (Qden r)) at 1.   repeat rewrite Zpos_mult_morphism.   apply Zmult_le_compat_l.     apply Zlt_impl_Zle.     assert (H_aux: (Zpos xH) = (0 + 1)%Z).       auto.     rewrite H_aux; clear H_aux.     apply Zplus_lt_compat_r.     apply Zgt_lt.     apply Zgt_pos_0.     apply Zle_0_pos. Qed. ```