ElementwiseWalkProof.walk_left_same: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as ElementwiseWalkProof
Lines 81-102 of bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&start_line=81&end_line=102

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/elementwise.bend as Elementwise

# Rows whose left stride is the output's on every axis, the last one 1:
# the left walk of every position is the position.
def walk_left_same(+rows: List<&2, Shape.Row>, +same: {Elementwise.same_left(rows) == True{} : Bool}, +i: Nat) ->
  {Shape.walk_left(rows, i) == i : Nat}:
  match rows:
    case Shape.Row{+stride, +left, +right} <> Nil{}:
      +unit = Arith.eq_true(stride, 1n, Arith.and_left(Nat.is_eq(stride, 1n), Nat.is_eq(left, 1n), same))
      +step = Arith.eq_true(left, 1n, Arith.and_right(Nat.is_eq(stride, 1n), Nat.is_eq(left, 1n), same))
      %Equal.sym(Nat, left, stride, Equal.trans(Nat, left, 1n, stride, step, Equal.sym(Nat, stride, 1n, unit))) :
        {Nat.add(Nat.mul(_, Nat.div(i, stride)), 0n) == i : Nat}
      %Equal.sym(Nat, stride, 1n, unit) : {Nat.add(Nat.mul(_, Nat.div(i, _)), 0n) == i : Nat}
      %mod_one(i) : {Nat.add(Nat.mul(1n, Nat.div(i, 1n)), _) == i : Nat}
      div_mod(i, 1n)
    case Shape.Row{+stride, +left, +right} <> +next <> +rest:
      +equal = Arith.eq_true(left, stride, Arith.and_left(Nat.is_eq(left, stride), Elementwise.same_left(next <> rest), same))
      %Equal.sym(Nat, left, stride, equal) : {Nat.add(Nat.mul(_, Nat.div(i, stride)), Shape.walk_left(next <> rest, Nat.mod(i, stride))) == i : Nat}
      %Equal.sym(Nat, Shape.walk_left(next <> rest, Nat.mod(i, stride)), Nat.mod(i, stride),
        walk_left_same(next <> rest, Arith.and_right(Nat.is_eq(left, stride), Elementwise.same_left(next <> rest), same), Nat.mod(i, stride))) :
        {Nat.add(Nat.mul(stride, Nat.div(i, stride)), _) == i : Nat}
      div_mod(i, stride)
    case Nil{}:
      Empty.absurd({Shape.walk_left(Nil{}, i) == i : Nat}, Arith.clash(same))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=eq_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=same_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=div_mod
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=mod_one