def pow_bin

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/float.bend:134

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N

134def pow_bin(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +fuel: Nat, +k: Nat, +b: T, +a: T) -> {G.pow_go(~T, ~op, ~test, fuel, k, b, True{}, (a, True{})) == Some{SG.binpow(~T, ~op, fuel, k, b, a)} : Maybe<&2, T>}:
135  match fuel k:
136    case 0n _:
137      {==}
138    case 1n+ +f 0n:
139      %Equal.sym(T, SG.binpow(~T, ~op, f, 0n, b, a), a, binpow_zero(~T, ~op, f, b, a)) : {Some{a} == Some{_} : Maybe<&2, T>}
140      {==}
141    case 1n+ +f 1n+ +j:
142      %Equal.sym(T & Bool, G.mul_st(~T, ~op, ~test, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, True{}, (a, True{})), (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{}), mul_st_eq(~T, ~op, ~test, ~mo, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), b, a)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), _) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
143      %Equal.sym(Bool, G.sq_ok(~T, ~test, Nat.is_lt(1n, 1n+j), b, True{}), True{}, sq_ok_eq(~T, ~test, ~mo, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), _, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
144      %Equal.sym(T, G.sq_val(~T, ~op, Nat.is_lt(1n, 1n+j), b), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), sq_val_eq(~T, ~op, Nat.is_lt(1n, 1n+j), b)) : {G.pow_go(~T, ~op, ~test, f, Nat.div(1n+j, 2n), _, True{}, (SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a), True{})) == Some{SG.binpow(~T, ~op, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))} : Maybe<&2, T>}
145      pow_bin(~T, ~op, ~test, ~mo, f, Nat.div(1n+j, 2n), SG.pick(T, Nat.is_lt(1n, 1n+j), op(N.Mul{b, b}), b), SG.pick(T, Nat.is_eq(Nat.mod(1n+j, 2n), 1n), op(N.Mul{a, b}), a))