proofs/math/pow2/pow2.bend

bend-collections-laws-containers@1.0.0.0 · 20 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/src/math/pow2.bend as P
5
6# The tail-recursive 2^d (src/pow2.bend) is the structural spec pow2.
7
8def go_double(+d: Nat, +acc: Nat) -> {P.go(d, Nat.double(acc)) == Nat.double(P.go(d, acc)) : Nat}:
9  match d:
10    case 0n:
11      {==}
12    case 1n+ +p:
13      go_double(p, Nat.double(acc))
14
15def same(+d: Nat) -> {P.pow2t(d) == SC.pow2(d) : Nat}:
16  match d:
17    case 0n:
18      {==}
19    case 1n+ +p:
20      Equal.trans(Nat, P.go(p, 2n), Nat.double(P.go(p, 1n)), SC.pow2(1n+p), go_double(p, 1n), Equal.cong(Nat, Nat, Nat.double, P.go(p, 1n), SC.pow2(p), same(p)))