def last_inside

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:76

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

76# Last{k} in range is limit - 1 - k: the two subtractions borrow nothing.
77def last_inside(+limit: U32, +k: U32, +inside: {U32.is_lt(k, limit) == True{} : Bool}) ->
78  {Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}:
79  +below = Equal.trans(Bool, Nat.is_lt(U32.to_nat(k), U32.to_nat(limit)), U32.is_lt(k, limit), True{}, Arith.u32_lt(k, limit), inside)
80  +first = Arith.sub_u32(limit, 1, lt_positive(U32.to_nat(k), U32.to_nat(limit), below))
81  shifted = Equal.trans(Bool, Nat.is_lt(U32.to_nat(k), 1n+U32.to_nat(U32.sub(limit, 1))), Nat.is_lt(U32.to_nat(k), U32.to_nat(limit)), True{},
82    Equal.cong(Nat, Bool, x => Nat.is_lt(U32.to_nat(k), x), 1n+U32.to_nat(U32.sub(limit, 1)), U32.to_nat(limit),
83      Equal.sym(Nat, U32.to_nat(limit), 1n+U32.to_nat(U32.sub(limit, 1)), first)),
84    below)
85  second = Arith.sub_u32(U32.sub(limit, 1), k, le_from_lt(U32.to_nat(k), U32.to_nat(U32.sub(limit, 1)), shifted))
86  Equal.trans(Nat, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), 1n+U32.to_nat(k)),
87    1n+Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)), U32.to_nat(limit),
88    add_succ_right(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
89    Equal.trans(Nat, 1n+Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
90      1n+Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))), U32.to_nat(limit),
91      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k)),
92        Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
93        add_comm(U32.to_nat(U32.sub(U32.sub(limit, 1), k)), U32.to_nat(k))),
94      Equal.trans(Nat, 1n+Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
95        1n+U32.to_nat(U32.sub(limit, 1)), U32.to_nat(limit),
96        Equal.cong(Nat, Nat, x => 1n+x, Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))),
97          U32.to_nat(U32.sub(limit, 1)),
98          Equal.sym(Nat, U32.to_nat(U32.sub(limit, 1)), Nat.add(U32.to_nat(k), U32.to_nat(U32.sub(U32.sub(limit, 1), k))), second)),
99        Equal.sym(Nat, U32.to_nat(limit), 1n+U32.to_nat(U32.sub(limit, 1)), first))))