def iter_sq

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/sqrtn.bend:74

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as RT

74def iter_sq(fuel: Nat, +n: Nat, +g: Nat, +m: Nat, +down: Bool, +hm: {m == M.sqrt_next(n, g) : Nat}, +hd: {down == Nat.is_lt(m, g) : Bool}, +hf: {Nat.is_le(g, fuel) == True{} : Bool}) -> {Nat.is_le(Nat.mul(M.sqrt_iter(fuel, n, g, m, down), M.sqrt_iter(fuel, n, g, m, down)), n) == True{} : Bool}:
75  match fuel down:
76    case 0n False{}:
77      %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
78      N.zero_le(n)
79    case 0n True{}:
80      %Equal.sym(Nat, g, 0n, le_zero(g, hf)) : {Nat.is_le(Nat.mul(_, _), n) == True{} : Bool}
81      N.zero_le(n)
82    case 1n+f False{}:
83      stop_sq(n, g, Equal.trans(Bool, Nat.is_lt(M.sqrt_next(n, g), g), Nat.is_lt(m, g), False{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, g), M.sqrt_next(n, g), m, Equal.sym(Nat, m, M.sqrt_next(n, g), hm)), Equal.sym(Bool, False{}, Nat.is_lt(m, g), hd)))
84    case 1n+ +f True{}:
85      iter_sq(f, n, m, M.sqrt_next(n, m), Nat.is_lt(M.sqrt_next(n, m), m), {==}, {==}, RT.shrink(m, g, f, Equal.sym(Bool, True{}, Nat.is_lt(m, g), hd), hf))