def walk_right_rows

bendtorch-core@0.1.0.0 · src/shape/projection_proofs.bend:50

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/unique_proofs.bend as Unique

50def walk_right_rows(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +index: Nat, same: {List.length(&2, Nat, left) == List.length(&2, Nat, output) : Nat}) -> {Shape.walk_right(Shape.index_rows(left, right, output), index) == dot(strides_of(right), Shape.digits(output, index)) : Nat}:
51  match left right output:
52    case +lh <> +lt +rh <> +rt +oh <> +ot:
53      +stride = Shape.numel(ot)
54      Equal.cong(Nat, Nat, rest => Nat.add(Nat.mul(Shape.broadcast_index(rh, Shape.numel(rt)), Nat.div(index, stride)), rest), Shape.walk_right(Shape.index_rows(lt, rt, ot), Nat.mod(index, stride)), dot(strides_of(rt), Shape.digits(ot, Nat.mod(index, stride))), walk_right_rows(lt, rt, ot, Nat.mod(index, stride), Unique.succ_injective(List.length(&2, Nat, lt), List.length(&2, Nat, ot), same)))
55    case Nil{} Nil{} Nil{}:
56      {==}
57    case Nil{} rh <> rt Nil{}:
58      {==}
59    case Nil{} right oh <> ot:
60      Empty.absurd({Shape.walk_right(Shape.index_rows(Nil{}, right, oh <> ot), index) == dot(strides_of(right), Shape.digits(oh <> ot, index)) : Nat}, Unique.succ_zero(List.length(&2, Nat, ot), Equal.sym(Nat, 0n, 1n+List.length(&2, Nat, ot), same)))
61    case lh <> lt Nil{} output:
62      {==}
63    case lh <> lt rh <> rt Nil{}:
64      {==}