vericert.common.ZExtra

Module ZLib.

Lemma mod2_cases: forall (n: Z), n mod 2 = 0 \/ n mod 2 = 1.

Lemma div_mul_undo: forall a b,
    b <> 0 ->
    a mod b = 0 ->
    a / b * b = a.

Lemma mod_0_r: forall (m: Z),
    m mod 0 = 0.

Lemma sub_mod_0: forall (a b m: Z),
    a mod m = 0 ->
    b mod m = 0 ->
    (a - b) mod m = 0.

Lemma add_mod_0: forall a b m : Z,
    a mod m = 0 ->
    b mod m = 0 ->
    (a + b) mod m = 0.

Lemma Z_mod_mult': forall a b : Z,
    (a * b) mod a = 0.

Lemma mod_add_r: forall a b,
    b <> 0 ->
    (a + b) mod b = a mod b.

Lemma mod_pow2_same_cases: forall a n,
    a mod 2 ^ n = a ->
    2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n.

Lemma mod_pow2_same_bounds: forall a n,
    a mod 2 ^ n = a ->
    0 <= n ->
    0 <= a < 2 ^ n.

Lemma pow2_nonneg: forall n,
    0 <= 2 ^ n.

Lemma pow2_pos: forall n,
    0 <= n ->
    0 < 2 ^ n.

Lemma pow2_times2: forall i,
    0 < i ->
    2 ^ i = 2 * 2 ^ (i - 1).

Lemma pow2_div2: forall i,
    0 <= i ->
    2 ^ (i - 1) = 2 ^ i / 2.

Lemma div_mul_undo_le: forall a b,
    0 <= a ->
    0 < b ->
    a / b * b <= a.

Lemma testbit_true_nonneg: forall a i,
    0 <= a ->
    0 <= i ->
    Z.testbit a i = true ->
    2 ^ i <= a.

Lemma range_div_pos: forall a b c d,
    0 < d ->
    a <= b <= c ->
    a / d <= b / d <= c / d.

Lemma testbit_true_nonneg': forall a i,
    0 <= i ->
    2 ^ i <= a < 2 ^ (i + 1) ->
    Z.testbit a i = true.

Lemma testbit_false_nonneg: forall a i,
    0 <= a < 2 ^ i ->
    0 < i ->
    Z.testbit a (i - 1) = false ->
    a < 2 ^ (i - 1).

Lemma signed_bounds_to_sz_pos: forall sz n,
    - 2 ^ (sz - 1) <= n < 2 ^ (sz - 1) ->
    0 < sz.

Lemma two_digits_encoding_inj_lo: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  b = d.

Lemma two_digits_encoding_inj_hi: forall base a b c d: Z,
  0 <= b < base ->
  0 <= d < base ->
  base * a + b = base * c + d ->
  a = c.

Lemma Z_to_nat_neg: forall (n: Z),
    n < 0 ->
    Z.to_nat n = 0%nat.

End ZLib.

Module ZExtra.

  Lemma mod_0_bounds :
    forall x y m,
      0 < m ->
      x mod m = 0 ->
      y mod m = 0 ->
      x <> y ->
      x + m > y ->
      y + m <= x.

  Lemma Ple_not_eq :
    forall x y,
    (x < y)%positive -> x <> y.

  Lemma Pge_not_eq :
    forall x y,
    (y < x)%positive -> x <> y.

  Lemma Ple_Plt_Succ :
    forall x y n,
    (x <= y)%positive -> (x < y + n)%positive.

End ZExtra.