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

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.

We prove that if x lies in an interval [kT, (k+1)T), then x %/ T is equal to k.

Lemma divn_leq :
  ∀ k T x,
    k × T ≤ x < k .+1 × T →
    x %/ T = k.

Floors and Ceilings of Fractions

We define notions of div_floor and div_ceil and prove a few basic lemmas.

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 observe that when dividing a value exceeding T × n, then the ceiling exceeds n.

Lemma div_ceil_multiple :
  ∀ Δ T n,
    T > 0 →
    (T × n ) < Δ →
    n < 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 ).