Module LibPos

Require Export Coqlib.
Require Export ZArith.
Require Import Tactics.
Load Param.

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.