def looked_keeps

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:254

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
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

254# A forward read hands both arrays back ...
255def looked_keeps(+plan: Gather.Plan, +at: Nat, +da: Nat, -A: Array<F32>, -I: Array<U32>, pair: Array<U32> & U32,
256  -kept: {Refinement.first(U32, pair) == I : Array<U32>}, -valid: Model.Balanced(F32, da, A)) ->
257  Generic.Fact<{Pair.snd(F32, Array<F32> & Array<U32>, Gather.looked(plan, at, A, pair)) == (A, I) : Array<F32> & Array<U32>}>:
258  (index, +j) = pair
259  Generic.Fact{Equal.trans(Array<F32> & Array<U32>, Pair.snd(F32, Array<F32> & Array<U32>, Gather.take(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j)))))),
260    (Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index), (A, I),
261    take_snd(index, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))),
262    both(Refinement.first(F32, Array.get(F32, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))))), index, A, I,
263      Refinement.law_get_retains(F32, da, A, U32.from_nat(Gather.source(plan, at, U32.to_nat(j))), valid), kept))}