The Coq mailing list

[KIKUCHI Masashi <kikuchi AT lepidum.co.jp>]

Hi.

Current Coq.ZArith.Zdiv provides existence of division on Z but
doesn't uniqueness.
Because of this, some simple equations about division are hard to prove.
(i.e. forall x, x > 0 -> (x - 1) / x = 0 /\ (x - 1) mod x = x - 1)

Proof of uniqueness is easy.
I think this lemma should be added to Coq.ZArith.Zdiv.

Require Import ZArith.
Require Import Zdiv.
Require Import Omega.

Open Scope Z_scope.

Lemma Z_div_eucl_unique:
  forall a b q r, b > 0 -> a = b * q + r -> 0 <= r < b ->
     q = a / b /\ r = a mod b.
Proof.
  intros.
  assert (r = a - b * q) by ring [H0].
  rewrite (Z_div_mod_eq a b H) in H2.
  set (rd := r - a mod b).
  set (qd := a / b - q).
  assert (rd = qd * b).
  unfold rd, qd.
  ring [H2].

  assert (-b < qd * b < b).
  generalize (Z_mod_lt a b H).
  rewrite <- H3.
  unfold rd.
  omega.
  assert (-1 < qd < 1).
  generalize (Zmult_gt_0_lt_reg_r (-1) qd b H).
  generalize (Zmult_gt_0_lt_reg_r qd 1 b H).
  auto with zarith.
  assert (qd = 0).
  omega.
  assert (rd = 0).
  rewrite H3.
  rewrite H6.
  auto with zarith.
  unfold qd, rd in H6, H7.
  auto with zarith.
Qed.

(* And Z_mod_plus in Coq.ZArith.Zdiv can be proved in more
straightforward way. *)
Lemma Z_mod_plus : forall a b c:Z, c > 0 -> (a + b * c) mod c = a mod c.
Proof.
   intros.
   generalize (Z_div_mod_eq a c H).
   generalize (Z_mod_lt a c H).
   intros.
   assert (a + b * c = c * (a / c + b) + a mod c).
   ring [H1].
   generalize (Z_div_eucl_unique (a + b * c) c (a / c + b) (a mod c) H
H2 H0).
   symmetry.
   tauto.
Qed.

(* Example *)
Goal forall a, a > 0 -> 0 = (a-1) / a /\ a-1 = (a-1) mod a.
Proof.
  intros a H.
  apply (Z_div_eucl_unique (a-1) a 0 (a-1) H).
  ring.
  omega.
Qed.

Thank you.