ReduceParallelProof.obs_gather: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 753-776 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=753&end_line=776

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/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend as ReduceLaws

def obs_gather(+d: Nat, -A: Array<F32>, +values: List<&2, F32>, +bound: Nat, +positions: List<&2, Nat>, +words: List<&2, F32>,
  +accumulator: F32, -seen: Obs(d, A, positions, words), +below: {all_below(positions, bound) == True{} : Bool},
  -reads: Reads(d, A, values, bound)) ->
  Parallel.Fact<{Some{fsum(words, accumulator)} == gather(values, positions, Some{accumulator}) : Maybe<&2, F32>}>:
  match positions words:
    case Nil{} Nil{}:
      Parallel.Fact{{==}}
    case +p <> +ps +w <> +ws:
      +inside = Arith.and_left(Nat.is_lt(p, bound), all_below(ps, bound), below)
      +others = Arith.and_right(Nat.is_lt(p, bound), all_below(ps, bound), below)
      Parallel.Fact{{\{ObsStep: observed => more =>
        %Equal.sym(Maybe<&2, F32>, ReduceLaws.word_at(values, p), Some{w},
          Equal.trans(Maybe<&2, F32>, ReduceLaws.word_at(values, p), Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(p))), Some{w},
            Equal.sym(Maybe<&2, F32>, Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(p))), ReduceLaws.word_at(values, p), reads(p, inside)),
            observed)) :
          {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, ReduceLaws.add_word(Some{accumulator}, _)) : Maybe<&2, F32>}
        {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, Some{F32.add(accumulator, w)}) : Maybe<&2, F32>}> ->
          {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, ps, Some{F32.add(accumulator, w)}) : Maybe<&2, F32>}}(
          obs_gather(d, A, values, bound, ps, ws, F32.add(accumulator, w), more, others, reads))} :
        ObsStep<d, A, p, w, ps, ws> -> {Some{fsum(ws, F32.add(accumulator, w))} == gather(values, p <> ps, Some{accumulator}) : Maybe<&2, F32>}}(seen)}
    case Nil{} +w <> +ws:
      Parallel.Fact{Empty.absurd({Some{fsum(w <> ws, accumulator)} == gather(values, Nil{}, Some{accumulator}) : Maybe<&2, F32>}, seen)}
    case +p <> +ps Nil{}:
      Parallel.Fact{Empty.absurd({Some{accumulator} == gather(values, p <> ps, Some{accumulator}) : Maybe<&2, F32>}, seen)}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=add_word
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_LAWS.bend&name=word_at
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=Obs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=ObsStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=Reads
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=all_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=fsum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact