LAWS_div.bend

bend-osdev-u32@0.1.0.0 · 28 lines · 4 definitions

1# Base's Nat division by a divisor 1 + bp (every positive divisor), as the
2# packages' proofs use it: quotient and remainder recompose the dividend,
3# the remainder is below the divisor, a dividend g (1 + bp) + i with i below
4# the divisor has quotient g and remainder i, and rounding a up to a
5# multiple of the divisor adds the slack (1 + bp - 1) - (a + bp) mod (1 + bp).
6import Base
7
8law nat_div_mod:
9  for +a: Nat
10  for +bp: Nat
11  {Nat.add(Nat.mul(Nat.div(a, 1n+bp), 1n+bp), Nat.mod(a, 1n+bp)) == a : Nat}
12
13law nat_mod_lt:
14  for +a: Nat
15  for +bp: Nat
16  {Nat.is_lt(Nat.mod(a, 1n+bp), 1n+bp) == True{} : Bool}
17
18law nat_divmod_exact:
19  for +g: Nat
20  for +i: Nat
21  for +bp: Nat
22  for h: {Nat.is_lt(i, 1n+bp) == True{} : Bool}
23  {Nat.divmod(Nat.add(Nat.mul(g, 1n+bp), i), 1n+bp) == (g, i) : Nat & Nat}
24
25law nat_round_up:
26  for +bp: Nat
27  for +a: Nat
28  {Nat.mul(Nat.div(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp), 1n+bp) == Nat.add(a, Nat.sub(Nat.sub(1n+bp, 1n), Nat.mod(Nat.add(a, Nat.sub(1n+bp, 1n)), 1n+bp))) : Nat}