Library prosa.util.div_mod

From mathcomp Require Export ssreflect ssrbool eqtype ssrnat seq fintype bigop div ssrfun.
Require Export prosa.util.nat prosa.util.subadditivity.

Additional lemmas about divn and modn.

Section DivMod.

First, we show that if t1 / h is equal to t2 / h and t1 ≤ t2, then t1 mod h is bounded by t2 mod h.

  Lemma eqdivn_leqmodn :
    ∀ t1 t2 h,
      t1 ≤ t2 →
      t1 %/ h = t2 %/ h →
      t1 %% h ≤ t2 %% h.

Given two natural numbers x and y, the fact that x / y < (x + 1) / y implies that y divides x + 1.

  Lemma ltdivn_dvdn :
    ∀ x y,
      x %/ y < (x + 1) %/ y →
      y %| (x + 1).

We prove an auxiliary lemma allowing us to change the order of operations _ + 1 and _ %% h.

  Lemma addn1_modn_commute :
    ∀ x h,
      h > 0 →
      x %/ h = (x + 1) %/ h →
      (x + 1) %% h = x %% h + 1 .

We show that the fact that x / h = (x + y) / h implies that h is larder than x mod h + y mod h.

  Lemma addmod_le_mod :
    ∀ x y h,
      h > 0 →
      x %/ h = (x + y) %/ h →
      h > x %% h + y %% h.

End DivMod.

In this section, we define notions of div_floor and div_ceil and prove a few basic lemmas.

Section DivFloorCeil.

We define functions div_floor and div_ceil, which are divisions rounded down and up, respectively.

Definition div_floor (x y : nat) : nat := x %/ y.
Definition div_ceil (x y : nat) := if y %| x then x %/ y else (x %/ y).+1.

We start with an observation that div_ceil 0 b is equal to 0 for any b.

Lemma div_ceil0:
∀ b, div_ceil 0 b = 0.

Next, we show that, given two positive integers a and b, div_ceil a b is also positive.

  Lemma div_ceil_gt0:
    ∀ a b,
      a > 0 → b > 0 →
      div_ceil a b > 0.

We show that div_ceil is monotone with respect to the first argument.

  Lemma div_ceil_monotone1:
    ∀ d m n,
      m ≤ n → div_ceil m d ≤ div_ceil n d.

Given T and Δ such that Δ ≥ T > 0, we show that div_ceil Δ T is strictly greater than div_ceil (Δ - T) T.

  Lemma leq_div_ceil_add1:
    ∀ Δ T,
      T > 0 → Δ ≥ T →
      div_ceil (Δ - T) T < div_ceil Δ T.

We show that the division with ceiling by a constant T is a subadditive function.

Lemma div_ceil_subadditive:
∀ T, subadditive (div_ceil ^~T).

We show that for any two integers a and b, a is less than a %/ b × b + b given that b is positive.

  Lemma div_floor_add_g:
    ∀ a b,
      b > 0 →
      a < a %/ b × b + b.

We prove a technical lemma stating that for any three integers a, b, c such that c > b, mod can be swapped with subtraction in the expression (a + c - b) %% c.

  Lemma mod_elim:
    ∀ a b c,
      c > b →
      (a + c - b) %% c = if a %% c ≥ b then (a %% c - b ) else (a %% c + c - b ).

End DivFloorCeil.