def halves_equal

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

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

181# A split hands each half both input arrays.
182def halves_equal(+dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, lp: Array<F32> & Array<F32>, rp: Array<F32> & Array<F32>,
183  -le: {lp == Array.clone(F32, A) : Array<F32> & Array<F32>}, -re: {rp == Array.clone(F32, B) : Array<F32> & Array<F32>},
184  -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
185  Fact<({Pair.fst(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.halves(lp, rp)) == (A, B) : Array<F32> & Array<F32>} &
186    {Pair.snd(Array<F32> & Array<F32>, Array<F32> & Array<F32>, Elementwise.halves(lp, rp)) == (A, B) : Array<F32> & Array<F32>})>:
187  (l1, l2) = lp
188  (r1, r2) = rp
189  Fact{(pair_equal(l1, r1, A, B,
190      {\{Fact: q => q} : Fact<({Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>})> -> {Pair.fst(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>}}(
191        clone_first(dl, A, A, (l1, l2), le, {==}, left_valid)),
192      {\{Fact: q => q} : Fact<({Pair.fst(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>})> -> {Pair.fst(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>}}(
193        clone_first(dr, B, B, (r1, r2), re, {==}, right_valid))),
194    pair_equal(l2, r2, A, B,
195      {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>})> -> {Pair.snd(Array<F32>, Array<F32>, (l1, l2)) == A : Array<F32>}}(
196        clone_second(dl, A, A, (l1, l2), le, {==}, left_valid)),
197      {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>})> -> {Pair.snd(Array<F32>, Array<F32>, (r1, r2)) == B : Array<F32>}}(
198        clone_second(dr, B, B, (r1, r2), re, {==}, right_valid))))}