def length_decided
bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:587
import bendtorch-core@0.1.0.0/src/autograd/reduce_PROOF.bend as ReducePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as Conversion
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as Laws
587def length_decided(+shape: Shape.Shape, tensor: Core.Tensor<shape>, +values: List<&2, F32>,
588 -listed: Laws.Listed(Core.Packed{shape, tensor}, values), +below: Bool,
589 -decision: {below == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}) -> Holds<{List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}>:
590 match below:
591 case True{}:
592 Holds{Empty.absurd({List.length(&2, F32, values) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}, Arith.clash(
593 Equal.trans(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), True{},
594 Equal.sym(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), False{}, below_self(List.length(&2, F32, values))),
595 Equal.trans(Bool, Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)), Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), True{},
596 {\{Holds: proof => proof} : Holds<{Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(List.length(&2, F32, values), List.length(&2, F32, values)) == Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
597 natural_presence(shape, tensor, values, listed, List.length(&2, F32, values),
598 Shape.LE.from(List.length(&2, F32, values), 1048576n, Equal.sym(Bool, Nat.is_le(List.length(&2, F32, values), 1048576n), True{},
599 Conversion.le_trans(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), 1048576n,
600 Conversion.lt_le(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)),
601 Equal.sym(Bool, True{}, Nat.is_le(Shape.logical_numel(Shape.dimensions(shape)), 1048576n), Nats.le_true(Shape.logical_numel(Shape.dimensions(shape)), 1048576n, capacity_of(shape)))))))),
602 Equal.sym(Bool, True{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision)))))}
603 case False{}:
604 Holds{neither_below(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape)), Equal.sym(Bool, False{}, Nat.is_lt(List.length(&2, F32, values), Shape.logical_numel(Shape.dimensions(shape))), decision),
605 Equal.trans(Bool, Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)), Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))), False{},
606 {\{Holds: proof => proof} : Holds<{Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}> -> {Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), List.length(&2, F32, values)) == Nat.is_lt(Shape.logical_numel(Shape.dimensions(shape)), Shape.logical_numel(Shape.dimensions(shape))) : Bool}}(
607 natural_presence(shape, tensor, values, listed, Shape.logical_numel(Shape.dimensions(shape)), capacity_of(shape))),
608 below_self(Shape.logical_numel(Shape.dimensions(shape)))))}