def inside_split

bendtorch-core@0.1.0.0 · src/tensor/contracts/pointwise_proof.bend:110

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/contracts/pointwise.bend as Pointwise

110def inside_split(~P: Data, ~map: P -> Nat -> Nat, +plan: P, +previous: Nat, +bound: Nat,
111  all: {Pointwise.inside(~P, ~map, plan, 1n+previous, bound) == True{} : Bool}, +index: Nat,
112  below: {Nat.is_lt(index, 1n+previous) == True{} : Bool},
113  rec: {Pointwise.inside(~P, ~map, plan, previous, bound) == True{} : Bool} -> {Nat.is_lt(index, previous) == True{} : Bool} ->
114    {Nat.is_lt(map(plan, index), bound) == True{} : Bool},
115  decision: Shape.BoolCase<Nat.is_eq(index, previous)>) -> {Nat.is_lt(map(plan, index), bound) == True{} : Bool}:
116  match decision:
117    case Shape.BTrue{same}:
118      %Equal.sym(Nat, index, previous, Lifecycle.natural_equal(index, previous, same)) : {Nat.is_lt(map(plan, _), bound) == True{} : Bool}
119      Arith.and_right(Pointwise.inside(~P, ~map, plan, previous, bound), Nat.is_lt(map(plan, previous), bound), all)
120    case Shape.BFalse{other}:
121      rec(Arith.and_left(Pointwise.inside(~P, ~map, plan, previous, bound), Nat.is_lt(map(plan, previous), bound), all),
122        lt_succ_ne(index, previous, below, other))