def walk_right_same

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

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

104def walk_right_same(+rows: List<&2, Shape.Row>, +same: {Elementwise.same_right(rows) == True{} : Bool}, +i: Nat) ->
105  {Shape.walk_right(rows, i) == i : Nat}:
106  match rows:
107    case Shape.Row{+stride, +left, +right} <> Nil{}:
108      +unit = Arith.eq_true(stride, 1n, Arith.and_left(Nat.is_eq(stride, 1n), Nat.is_eq(right, 1n), same))
109      +step = Arith.eq_true(right, 1n, Arith.and_right(Nat.is_eq(stride, 1n), Nat.is_eq(right, 1n), same))
110      %Equal.sym(Nat, right, stride, Equal.trans(Nat, right, 1n, stride, step, Equal.sym(Nat, stride, 1n, unit))) :
111        {Nat.add(Nat.mul(_, Nat.div(i, stride)), 0n) == i : Nat}
112      %Equal.sym(Nat, stride, 1n, unit) : {Nat.add(Nat.mul(_, Nat.div(i, _)), 0n) == i : Nat}
113      %mod_one(i) : {Nat.add(Nat.mul(1n, Nat.div(i, 1n)), _) == i : Nat}
114      div_mod(i, 1n)
115    case Shape.Row{+stride, +left, +right} <> +next <> +rest:
116      +equal = Arith.eq_true(right, stride, Arith.and_left(Nat.is_eq(right, stride), Elementwise.same_right(next <> rest), same))
117      %Equal.sym(Nat, right, stride, equal) : {Nat.add(Nat.mul(_, Nat.div(i, stride)), Shape.walk_right(next <> rest, Nat.mod(i, stride))) == i : Nat}
118      %Equal.sym(Nat, Shape.walk_right(next <> rest, Nat.mod(i, stride)), Nat.mod(i, stride),
119        walk_right_same(next <> rest, Arith.and_right(Nat.is_eq(right, stride), Elementwise.same_right(next <> rest), same), Nat.mod(i, stride))) :
120        {Nat.add(Nat.mul(stride, Nat.div(i, stride)), _) == i : Nat}
121      div_mod(i, stride)
122    case Nil{}:
123      Empty.absurd({Shape.walk_right(Nil{}, i) == i : Nat}, Arith.clash(same))