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.
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.
Lemma Qmult_le_compat_l:
forall x y z : Q,
x <= y ->
0 <= z ->
z * x <= z * y.
Proof.
intros x y z H_x_le_y H_z_pos.
rewrite Qmult_comm.
assert (H_aux: z * y == y * z).
rewrite Qmult_comm.
reflexivity.
rewrite H_aux; clear H_aux.
apply Qmult_le_compat_r; auto.
Qed.
Lemma Qmult_lt_compat_l:
forall x y z : Q,
x < y ->
0 < z ->
z * x < z * y.
Proof.
intros x y z H_x_lt_y H_z_pos.
rewrite Qmult_comm.
assert (H_aux: z * y == y * z).
rewrite Qmult_comm.
reflexivity.
rewrite H_aux; clear H_aux.
apply Qmult_lt_compat_r; auto.
Qed.