def walk_left_same

bendtorch-core@0.1.0.0 · src/tensor/elementwise_walk_proof.bend:81

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

81# Rows whose left stride is the output's on every axis, the last one 1:
82# the left walk of every position is the position.
83def walk_left_same(+rows: List<&2, Shape.Row>, +same: {Elementwise.same_left(rows) == True{} : Bool}, +i: Nat) ->
84  {Shape.walk_left(rows, i) == i : Nat}:
85  match rows:
86    case Shape.Row{+stride, +left, +right} <> Nil{}:
87      +unit = Arith.eq_true(stride, 1n, Arith.and_left(Nat.is_eq(stride, 1n), Nat.is_eq(left, 1n), same))
88      +step = Arith.eq_true(left, 1n, Arith.and_right(Nat.is_eq(stride, 1n), Nat.is_eq(left, 1n), same))
89      %Equal.sym(Nat, left, stride, Equal.trans(Nat, left, 1n, stride, step, Equal.sym(Nat, stride, 1n, unit))) :
90        {Nat.add(Nat.mul(_, Nat.div(i, stride)), 0n) == i : Nat}
91      %Equal.sym(Nat, stride, 1n, unit) : {Nat.add(Nat.mul(_, Nat.div(i, _)), 0n) == i : Nat}
92      %mod_one(i) : {Nat.add(Nat.mul(1n, Nat.div(i, 1n)), _) == i : Nat}
93      div_mod(i, 1n)
94    case Shape.Row{+stride, +left, +right} <> +next <> +rest:
95      +equal = Arith.eq_true(left, stride, Arith.and_left(Nat.is_eq(left, stride), Elementwise.same_left(next <> rest), same))
96      %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}
97      %Equal.sym(Nat, Shape.walk_left(next <> rest, Nat.mod(i, stride)), Nat.mod(i, stride),
98        walk_left_same(next <> rest, Arith.and_right(Nat.is_eq(left, stride), Elementwise.same_left(next <> rest), same), Nat.mod(i, stride))) :
99        {Nat.add(Nat.mul(stride, Nat.div(i, stride)), _) == i : Nat}
100      div_mod(i, stride)
101    case Nil{}:
102      Empty.absurd({Shape.walk_left(Nil{}, i) == i : Nat}, Arith.clash(same))