def step_lt

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/bits.bend as B

89def step_lt(+n: Nat, +gp: Nat, +m: Nat, +hm: {m == M.sqrt_next(n, 1n+gp) : Nat}) -> {Nat.is_lt(n, Nat.mul(1n+m, 1n+m)) == True{} : Bool}:
90  +g = {1n+gp : Nat}
91  +q = Nat.div(n, g)
92  +r = Nat.mod(n, g)
93  +s = Nat.add(g, q)
94  # n < g (q + 1)
95  +ha = Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)), True{},
96    Equal.trans(Bool, Nat.is_lt(n, Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.mul(g, 1n+q)), Nat.is_lt(Nat.add(Nat.mul(q, g), r), Nat.add(Nat.mul(q, g), g)),
97      Equal.cong(Nat, Bool, z => Nat.is_lt(z, Nat.mul(g, 1n+q)), n, Nat.add(Nat.mul(q, g), r), R.dm_eq(gp, n)),
98      Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(Nat.mul(q, g), r), z), Nat.mul(g, 1n+q), Nat.add(Nat.mul(q, g), g), Equal.trans(Nat, Nat.mul(g, 1n+q), Nat.mul(1n+q, g), Nat.add(Nat.mul(q, g), g), A.mul_comm(g, 1n+q), A.add_comm(g, Nat.mul(q, g))))),
99    N.lt_add_left(r, g, Nat.mul(q, g), R.dm_lt(gp, n)))
100  # g + (q + 1) <= 2 (m + 1): s == 2 m + (s mod 2)
101  +es = Equal.trans(Nat, s, Nat.add(Nat.double(m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), Nat.mod(s, 2n)),
102    Equal.trans(Nat, s, Nat.add(Nat.double(Nat.div(s, 2n)), Nat.mod(s, 2n)), Nat.add(Nat.double(m), Nat.mod(s, 2n)), B.half_eq(s), Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), Nat.mod(s, 2n)), Nat.div(s, 2n), m, Equal.sym(Nat, m, Nat.div(s, 2n), hm))),
103    Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(s, 2n)), Nat.double(m), Nat.add(m, m), A.double_self(m)))
104  +hs = Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)), True{},
105    Equal.trans(Bool, Nat.is_le(s, 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), 1n+Nat.add(m, m)), Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), Nat.add(Nat.add(m, m), 1n)),
106      Equal.cong(Nat, Bool, z => Nat.is_le(z, 1n+Nat.add(m, m)), s, Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), es),
107      Equal.cong(Nat, Bool, z => Nat.is_le(Nat.add(Nat.add(m, m), Nat.mod(s, 2n)), z), 1n+Nat.add(m, m), Nat.add(Nat.add(m, m), 1n), A.add_comm(1n, Nat.add(m, m)))),
108    N.le_add_left(Nat.mod(s, 2n), 1n, Nat.add(m, m), N.lt_succ_le(Nat.mod(s, 2n), 1n, B.half_rem(s))))
109  +hb = Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)), True{},
110    Equal.trans(Bool, Nat.is_le(Nat.add(g, 1n+q), Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, Nat.add(1n+m, 1n+m)), Nat.is_le(1n+s, 2n+Nat.add(m, m)),
111      Equal.cong(Nat, Bool, z => Nat.is_le(z, Nat.add(1n+m, 1n+m)), Nat.add(g, 1n+q), 1n+s, A.add_succ(g, q)),
112      Equal.cong(Nat, Bool, z => Nat.is_le(1n+s, z), Nat.add(1n+m, 1n+m), 2n+Nat.add(m, m), add_two(m, m))),
113    hs)
114  N.lt_le_trans(n, Nat.mul(g, 1n+q), Nat.mul(1n+m, 1n+m), ha, prod_le(g, 1n+q, 1n+m, hb))