def read_value

bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:59

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement

59def read_value(-d: Nat, -original: Array<F32>, -target: Array<F32>, -i: U32, -pair: Array<F32> & F32,
60  -exact: {pair == Array.get(F32, original, i) : Array<F32> & F32}, -same: {original == target : Array<F32>},
61  -valid: Model.Balanced(F32, d, target)) ->
62  Fact<{Some{Refinement.second(F32, pair)} == Model.observe(F32, d, target, Refinement.route(d, i)) : Maybe<&2, F32>}>:
63  Fact{Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, pair)}, Some{Refinement.second(F32, Array.get(F32, original, i))},
64    Model.observe(F32, d, target, Refinement.route(d, i)),
65    Equal.cong(Array<F32> & F32, Maybe<&2, F32>, p => Some{Refinement.second(F32, p)}, pair, Array.get(F32, original, i), exact),
66    Equal.trans(Maybe<&2, F32>, Some{Refinement.second(F32, Array.get(F32, original, i))},
67      Model.observe(F32, d, original, Refinement.route(d, i)), Model.observe(F32, d, target, Refinement.route(d, i)),
68      Refinement.law_get_refines(F32, d, original, i, {\{Fact: p => p} : Fact<(Model.Balanced(F32, d, original))> -> Model.Balanced(F32, d, original)}(transport_balanced(d, original, target, same, valid))),
69      Equal.cong(Array<F32>, Maybe<&2, F32>, a => Model.observe(F32, d, a, Refinement.route(d, i)), original, target, same)))}