def mod2_bit

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:187

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NA

187# r + 2h mod 2 is the bit r
188def mod2_bit(+r: Nat, +h: Nat, +hr: {Nat.is_lt(r, 2n) == True{} : Bool}) -> {r == Nat.mod(Nat.add(r, Nat.double(h)), 2n) : Nat}:
189  match r:
190    case 0n:
191      %dbl(h) : {0n == Nat.mod(_, 2n) : Nat}
192      %N.add_zero(Nat.mul(h, 2n)) : {0n == Nat.mod(_, 2n) : Nat}
193      Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 0n), 2n), 0n, NA.absorb(1n, h, 0n))
194    case 1n:
195      %dbl(h) : {1n == Nat.mod(1n+_, 2n) : Nat}
196      %N.add_zero(Nat.mul(h, 2n)) : {1n == Nat.mod(1n+_, 2n) : Nat}
197      %N.add_succ(Nat.mul(h, 2n), 0n) : {1n == Nat.mod(_, 2n) : Nat}
198      Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(h, 2n), 1n), 2n), 1n, NA.absorb(1n, h, 1n))
199    case 2n+ +q:
200      Empty.absurd({2n+q == Nat.mod(Nat.add(2n+q, Nat.double(h)), 2n) : Nat}, N.lt_zero_absurd(q, hr))