def halve

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:98

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

98# Knuth: b < 2^k and 2k + 1 <= f reach the end (r is a mod b, given)
99def halve(+k: Nat, +f: Nat, +a: Nat, +b: Nat, +r: Nat, +hr: {Nat.mod(a, b) == r : Nat}, +hb: {Nat.is_lt(b, C.pow2(k)) == True{} : Bool}, +hf: {Nat.is_le(1n+Nat.double(k), f) == True{} : Bool}) -> {ends(f, a, b) == True{} : Bool}:
100  match k f b r:
101    case 0n _ 0n _:
102      ends_zero(f, a)
103    case 0n _ 1n+bp _:
104      Empty.absurd({ends(f, a, 1n+bp) == True{} : Bool}, N.lt_zero_absurd(bp, hb))
105    case 1n+j _ 0n _:
106      ends_zero(f, a)
107    case 1n+j 0n 1n+bp _:
108      Empty.absurd({ends(0n, a, 1n+bp) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
109    case 1n+j 1n 1n+bp _:
110      Empty.absurd({ends(1n, a, 1n+bp) == True{} : Bool}, true_ne_false(Equal.sym(Bool, False{}, True{}, hf)))
111    case 1n+j 2n+ +h 1n+ +bp 0n:
112      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 0n, hr) : {ends(1n+h, 1n+bp, _) == True{} : Bool}
113      ends_zero(1n+h, 1n+bp)
114    case 1n+ +j 2n+ +h 1n+ +bp 1n+ +rp:
115      %Equal.sym(Nat, Nat.mod(a, 1n+bp), 1n+rp, hr) : {ends(1n+h, 1n+bp, _) == True{} : Bool}
116      +r2 = Nat.mod(1n+bp, 1n+rp)
117      +h21 = NR.dm_lt(rp, 1n+bp)
118      +hlt = L.subst(Nat, z => {Nat.is_lt(z, 1n+bp) == True{} : Bool}, Nat.mod(a, 1n+bp), 1n+rp, hr, NR.dm_lt(bp, a))
119      +hs = mod_le_sub(1n+bp, rp, N.lt_le(1n+rp, 1n+bp, hlt))
120      +hb2 = halve2(1n+bp, 1n+rp, r2, C.pow2(j), hb, h21, hs)
121      halve(j, h, 1n+rp, r2, Nat.mod(1n+rp, r2), {==}, hb2, hf)