def indexed_fold_change_context

stelliferous@0.0.2.0 · proofs/traversal_array_refinement.bend:254

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal

254# One bounded induction carries capacity, preserved sources and completed
255# output values together. A strategy proves its local update obligation;
256# it does not reimplement the whole output traversal proof.
257def indexed_fold_change_context(~State: Data,~Outer: Data,~Inner: Data,
258  ~project: Outer -> Inner,~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
259  ~same_step: @+index: U32 -> @+context: Outer -> @+state: State ->
260    {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
261  +count: Nat,+first: U32,+context: Outer,+state: State) ->
262  {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
263    Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
264  match count:
265    case 0n: {==}
266    case 1n+ +rest:
267      %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state)) :
268        {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
269          Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
270      indexed_fold_change_context(~State,~Outer,~Inner,~project,~outer_step,~inner_step,~same_step,
271        rest,(first + 1 : U32),context,inner_step(first,project(context),state))