def below_span

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:179

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/contracts/build_facts.bend as Facts

179def below_span(+start: Nat, +stop: Nat, +step: Nat, +k: Nat, +span: Nat, e: {Nat.sub(stop, start) == span : Nat},
180  below: {Nat.is_lt(k, Slice.counted(span, step)) == True{} : Bool}) ->
181  {Nat.is_lt(Nat.add(start, Nat.mul(k, step)), stop) == True{} : Bool}:
182  match span:
183    case 0n:
184      Empty.absurd({Nat.is_lt(Nat.add(start, Nat.mul(k, step)), stop) == True{} : Bool}, Arith.lt_zero(k, below))
185    case 1n+rest:
186      %sub_back(stop, start, rest, e) : {Nat.is_lt(Nat.add(start, Nat.mul(k, step)), _) == True{} : Bool}
187      %Equal.sym(Nat, Nat.add(start, 1n+rest), 1n+Nat.add(start, rest), Arith.add_succ(start, rest)) :
188        {Nat.is_lt(Nat.add(start, Nat.mul(k, step)), _) == True{} : Bool}
189      Arith.lt_succ(Nat.add(start, Nat.mul(k, step)), Nat.add(start, rest),
190        Facts.le_add_cong(start, Nat.mul(k, step), rest, scaled_le(k, rest, step, below)))