def walk_left_rows

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

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

36def walk_left_rows(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +index: Nat, same: {List.length(&2, Nat, right) == List.length(&2, Nat, output) : Nat}) -> {Shape.walk_left(Shape.index_rows(left, right, output), index) == dot(strides_of(left), Shape.digits(output, index)) : Nat}:
37  match left right output:
38    case +lh <> +lt +rh <> +rt +oh <> +ot:
39      +stride = Shape.numel(ot)
40      Equal.cong(Nat, Nat, rest => Nat.add(Nat.mul(Shape.broadcast_index(lh, Shape.numel(lt)), Nat.div(index, stride)), rest), Shape.walk_left(Shape.index_rows(lt, rt, ot), Nat.mod(index, stride)), dot(strides_of(lt), Shape.digits(ot, Nat.mod(index, stride))), walk_left_rows(lt, rt, ot, Nat.mod(index, stride), Unique.succ_injective(List.length(&2, Nat, rt), List.length(&2, Nat, ot), same)))
41    case Nil{} right output:
42      {==}
43    case lh <> lt Nil{} Nil{}:
44      {==}
45    case lh <> lt Nil{} oh <> ot:
46      Empty.absurd({Shape.walk_left(Shape.index_rows(lh <> lt, Nil{}, oh <> ot), index) == dot(strides_of(lh <> lt), 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)))
47    case lh <> lt rh <> rt Nil{}:
48      {==}