def hlf_lt

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32half.bend:124

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

124# s < 2m gives s/2 < m: one narrowing step of a search range that started
125# below 2^f lands below 2^(f-1).
126def hlf_lt(+s: Nat, +m: Nat, +h: {Nat.is_lt(s, Nat.double(m)) == True{} : Bool}) -> {Nat.is_lt(hlf(s), m) == True{} : Bool}:
127  match s m:
128    case s0 0n:
129      Empty.absurd({Nat.is_lt(hlf(s0), 0n) == True{} : Bool}, N.lt_zero_absurd(s0, h))
130    case 0n 1n+q:
131      {==}
132    case 1n+0n 1n+q:
133      {==}
134    case 1n+1n+r 1n+q:
135      hlf_lt(r, q, h)