Home

# Module LibPos

Require Export Coqlib.
Require Export ZArith.
Require Import Tactics.

Lemma Plt_rev_trans :forall a b,
Plt b a ->
forall c, Plt c b -> Plt c a.
Proof.
intros ; eauto using Plt_trans.
Qed.

Lemma Ple_Plt_trans:
forall (p q r: positive), Ple p q -> Plt q r -> Plt p r.
Proof.
unfold Plt, Ple; intros; omega.
Qed.

Lemma Ple_antisym : forall p q, Ple p q -> Ple q p -> p = q.
Proof.
unfold Ple.
intros.
assert (Zpos p = Zpos q) by omega.
congruence.
Qed.

Section Bounded_gt.

Variable p : positive.

Inductive bounded_gt : positive -> positive -> Prop :=
| bounded_gt_intro : forall a b,
Plt b a -> Plt a p -> bounded_gt a b.

Function bound_gt (q : positive) : nat :=
match (Zpos p - Zpos q)%Z with
| Zpos r => nat_of_P r
| _ => O
end.

Theorem bounded_gt_wf : well_founded bounded_gt.
Proof.
unfold well_founded.
cut (forall n q, bound_gt q = n -> Acc bounded_gt q).
intros.
eauto.
induction n using (well_founded_ind Wf_nat.lt_wf).
intros.
subst.
revert H.
unfold bound_gt.
case_eq (Zpos p - Zpos q)%Z.
intros.
assert (Zpos p = Zpos q) by omega.
injection H1.
intros ; subst q.
constructor.
inversion 1.
subst.
apply False_rect.
destruct (Plt_strict p).
eauto using Plt_trans.
intros.
constructor.
inversion 1.
subst.
unfold Plt in *.
assert (Zpos p > Zpos q)%Z.
cut (Zpos p - Zpos q > 0)%Z.
omega.
rewrite H.
compute.
trivial.
clear H4.
assert (Zpos p - Zpos y < Zpos p - Zpos q)%Z by omega.
assert (Zpos p - Zpos y > 0)%Z by omega.
generalize (H5).
case_eq (Zpos p - Zpos y)%Z ; intros until 1 ; compute ; try congruence.
intros _.
generalize (fun y0 Hq Hy => H0 y0 Hy y Hq).
rewrite H6.
intros.
eapply H7.
reflexivity.
apply nat_of_P_lt_Lt_compare_morphism.
rewrite H in H4.
rewrite H6 in H4.
unfold Zlt in H4.
simpl in H4.
assumption.
intros.
assert (Zpos p < Zpos q)%Z.
cut (Zpos p - Zpos q < 0)%Z.
omega.
rewrite H.
compute.
trivial.
assert (Plt p q).
assumption.
constructor.
inversion 1.
subst.
destruct (Plt_strict p).
eauto using Plt_trans.
Qed.

End Bounded_gt.

Section Bounded_exists.
Variable p : positive -> bool.

Lemma bounded_exists : forall n,
{j | Plt j n /\ p j = true} + {forall j, Plt j n -> p j = false}.
Proof.
intros.
induction n using Prec.
compute.
right.
destruct j ; simpl ; congruence.
case_eq (p n).
left.
exists n.
split.
apply Plt_succ.
assumption.
intros.
destruct IHn as [ [j [Hlt Hp]] | Hlt].
left.
exists j.
split.
eauto using Plt_succ, Plt_trans.
assumption.
right.
intros j Hlt_succ.
destruct (Plt_succ_inv _ _ Hlt_succ).
eauto.
congruence.
Qed.

End Bounded_exists.

Definition lcm a b := a * (b / Zgcd a b).

Lemma lcm_positive : forall a, 0 < a -> forall b, 0 < b -> 0 < lcm a b.
Proof.
intros.
unfold lcm.
replace 0 with (a * 0) by ring.
apply Zmult_lt_compat_l.
assumption.
generalize (Zgcd_is_gcd a b).
inversion 1.
destruct H3.
clear H1 H2 H4.
assert (Zgcd a b = 0 -> False).
intro.
generalize (Zgcd_inv_0_r _ _ H1).
omega.
pattern b at 1.
rewrite H3.
rewrite Z_div_mult_full.
generalize (Zgcd_is_pos a b).
intros.
rewrite H3 in H0.
assert (0 < Zgcd a b) by omega.
eauto using Zmult_lt_0_reg_r.
assumption.
Qed.

Theorem lcm_prop : forall a, 0 < a -> forall b, 0 < b -> forall q,
(a | q) -> (b | q) -> (lcm a b | q).
Proof.
destruct 3; subst.
destruct 1; subst.
unfold lcm.
generalize (Zgcd_is_gcd a b).
inversion 1.
clear H5.
destruct H3.
destruct H4.
generalize (Zgcd_is_pos a b).
intros.
assert (0 < Zgcd a b).
cut (Zgcd a b = 0 -> False).
intros.
omega.
intros.
generalize (Zgcd_inv_0_l _ _ H6).
omega.
assert (b > 0) by omega.
assert (Zgcd a b >= 0) by omega.
generalize (Zis_gcd_rel_prime _ _ _ H7 H8 H2).
revert H6 H4 H3.
clear H2 H5 H7 H8.
generalize (Zgcd a b).
intros.
subst.
assert (z <> 0) by omega.
revert H2.
replace (q2 * z / z) with q2.
replace (q1 * z / z) with q1.
intros.
revert H1.
rewrite Zmult_assoc.
rewrite Zmult_assoc.
intros.
generalize (Zmult_reg_r _ _ _ H3 H1).
intros.
assert (q2 | q0).
apply Gauss with q1.
exists q.
rewrite Zmult_comm.
congruence.
apply rel_prime_sym.
assumption.
destruct H5.
subst.
exists q3.
ring.
rewrite Z_div_mult_full; trivial.
rewrite Z_div_mult_full; trivial.
Qed.

Lemma lcm_divides_left : forall a b, (a | lcm a b).
Proof.
unfold lcm.
intros.
exists (b / Zgcd a b).
rewrite Zmult_comm.
trivial.
Qed.

Lemma lcm_divides_right : forall a b, 0 < b -> (b | lcm a b).
Proof.
unfold lcm.
intros.
assert (Zgcd a b = 0 -> False).
intro.
generalize (Zgcd_inv_0_r _ _ H0).
omega.
generalize (Zgcd_is_pos a b).
intros.
assert (0 < Zgcd a b) by omega.
rewrite <- (Zgcd_div_swap0 _ _ H2 H).
exists (a / Zgcd a b).
trivial.
Qed.

Lemma incr_align : forall a, (0 < a) -> forall p, {q | p <= q /\ (a | q)}.
Proof.
intros.
assert (J : a > 0) by omega.
generalize (Z_div_mod p _ J).
destruct (Zdiv_eucl p a).
destruct 1.
destruct (Z_eq_dec z0 0).
exists p.
subst.
split.
omega.
exists z.
rewrite Zmult_comm.
omega.
exists (p + a - z0).
split.
omega.
exists (z + 1).
subst.
rewrite Zmult_plus_distr_l.
rewrite Zmult_comm.
replace (1 * a) with a by omega.
omega.
Qed.

Section Bounded.

Variable align : Z.
Hypothesis align_pos : 0 < align.

Variable low_bound high_bound : Z.

Variable f : Z -> bool.

Definition bounded_offset : {z | low_bound <= z /\ (align | z) /\ (high_bound <= z \/ f z = true)}.
Proof.
cut (forall j, 0 <= j -> forall z, (align | z) -> high_bound - z = j -> {z' | z <= z' /\ (align | z') /\ (high_bound <= z' \/ f z' = true)}).
intros.
destruct (incr_align align_pos low_bound).
destruct a.
destruct (Z_le_dec 0 (high_bound - x)).
destruct (H _ z _ H1 (refl_equal _)).
destruct a.
exists x0.
split.
omega.
assumption.
exists x.
split.
assumption.
split.
assumption.
left.
omega.
intros until 1.
pattern j.
eapply Z_lt_rec; try eassumption.
intros.
clear j H.
subst.
case_eq (f z).
intros.
exists z.
split.
omega.
split.
assumption.
auto.
intros _.
assert (align | z + align) by eauto using Zdivide_plus_r, Zdivide_refl.
destruct (Z_le_dec (high_bound) (z + align)).
exists (z + align).
split.
omega.
split.
assumption.
auto.
assert (0 <= high_bound - (z + align) < high_bound - z) by omega.
destruct (H0 _ H2 _ H (refl_equal _)).
destruct a.
exists x.
split.
omega.
assumption.
Qed.

End Bounded.