def written_true

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:247

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/autograd/gradient_LAWS.bend as Laws

247def written_true(+shape: Shape.Shape, -original: Core.Tensor<shape>, -contribution: Core.Dynamic, +cursor: Nat,
248  -before: Core.Tensor<shape>, -written: Core.Tensor<shape>, +index: U32, +accumulated: F32, +value: F32,
249  +other: U32, -equal: {True{} == Nat.is_eq(U32.to_nat(index), U32.to_nat(other)) : Bool},
250  -inside: {Nat.is_lt(U32.to_nat(other), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool},
251  -exact: {U32.to_nat(index) == cursor : Nat},
252  -inv: Inv(shape, original, contribution, cursor, before),
253  -read: {Core.checked_observe(shape, before, index) == Some{accumulated} : Maybe<&2, F32>},
254  -stored: {Core.checked_observe(shape, written, index) == Some{F32.add(accumulated, value)} : Maybe<&2, F32>},
255  -word: {Core.checked_observe_dynamic(contribution, index) == Some{value} : Maybe<&2, F32>}) ->
256  Holds<{Core.checked_observe(shape, written, other) ==
257    partial(Nat.is_lt(U32.to_nat(other), 1n+cursor), Core.checked_observe(shape, original, other), Core.checked_observe_dynamic(contribution, other)) : Maybe<&2, F32>}>:
258  Holds{
259    %{\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal)) :
260      {Core.checked_observe(shape, written, _) ==
261        partial(Nat.is_lt(U32.to_nat(_), 1n+cursor), Core.checked_observe(shape, original, _), Core.checked_observe_dynamic(contribution, _)) : Maybe<&2, F32>}
262    Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, written, index), Some{F32.add(accumulated, value)},
263      partial(Nat.is_lt(U32.to_nat(index), 1n+cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
264      stored,
265      %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), 1n+cursor), True{},
266        %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, 1n+cursor) == True{} : Bool}
267        lt_succ_self(cursor)) :
268        {Some{F32.add(accumulated, value)} == partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
269      %Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, original, index), Some{accumulated},
270        Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, original, index),
271          partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
272          Some{accumulated},
273          %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), cursor), False{},
274            %Equal.sym(Nat, U32.to_nat(index), cursor, exact) : {Nat.is_lt(_, cursor) == False{} : Bool}
275            lt_self(cursor)) :
276            {Core.checked_observe(shape, original, index) ==
277              partial(_, Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
278          {==},
279          Equal.trans(Maybe<&2, F32>,
280            partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
281            Core.checked_observe(shape, before, index), Some{accumulated},
282            Equal.sym(Maybe<&2, F32>, Core.checked_observe(shape, before, index),
283              partial(Nat.is_lt(U32.to_nat(index), cursor), Core.checked_observe(shape, original, index), Core.checked_observe_dynamic(contribution, index)),
284              inv(index)(
285                %Equal.sym(U32, index, other, {\{Holds: proof => proof} : Holds<{index == other : U32}> -> {index == other : U32}}(word_exact(index, other, equal))) :
286                  {Nat.is_lt(U32.to_nat(_), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool}
287                inside)),
288            read))) :
289        {Some{F32.add(accumulated, value)} == Laws.add_word(_, Core.checked_observe_dynamic(contribution, index)) : Maybe<&2, F32>}
290      %Equal.sym(Maybe<&2, F32>, Core.checked_observe_dynamic(contribution, index), Some{value}, word) :
291        {Some{F32.add(accumulated, value)} == Laws.add_word(Some{accumulated}, _) : Maybe<&2, F32>}
292      {==})}