def filled_one

bendtorch-core@0.1.0.0 · src/tensor/signed_PROOF.bend:495

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed

495def filled_one(+extents: List<&2, Signed.Extent>, one: {Signed.inferred_count(extents) == 1n : Nat}, +size: U32) ->
496  {Shape.logical_numel(Signed.filled(extents, size)) == Nat.mul(U32.to_nat(size), Signed.exact_product(extents)) : Nat}:
497  match extents:
498    case Nil{}:
499      Empty.absurd({Shape.logical_numel(Signed.filled([], size)) == Nat.mul(U32.to_nat(size), Signed.exact_product([])) : Nat},
500        zero_not_one(one))
501    case Signed.Exact{+extent} <> +tail:
502      Equal.trans(Nat, Nat.mul(U32.to_nat(extent), Shape.logical_numel(Signed.filled(tail, size))),
503        Nat.mul(U32.to_nat(extent), Nat.mul(U32.to_nat(size), Signed.exact_product(tail))),
504        Nat.mul(U32.to_nat(size), Nat.mul(U32.to_nat(extent), Signed.exact_product(tail))),
505        Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(extent), x), Shape.logical_numel(Signed.filled(tail, size)),
506          Nat.mul(U32.to_nat(size), Signed.exact_product(tail)), filled_one(tail, one, size)),
507        mul_swap(U32.to_nat(extent), U32.to_nat(size), Signed.exact_product(tail)))
508    case Signed.Inferred{} <> +tail:
509      Equal.cong(Nat, Nat, x => Nat.mul(U32.to_nat(size), x), Shape.logical_numel(Signed.filled(tail, size)), Signed.exact_product(tail),
510        filled_none(tail, size, Equal.cong(Nat, Nat, pred, 1n+Signed.inferred_count(tail), 1n, one)))