def indexed_fold_refines_model

stelliferous@0.0.2.0 · proofs/traversal_array_refinement.bend:237

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

237def indexed_fold_refines_model(~Runtime: Type,~Model: Data,~Context: Data,
238  ~update: U32 -> Context -> Runtime -> Runtime,~model_update: U32 -> Context -> Model -> Model,
239  ~represent: Model -> Runtime,
240  ~step_matches: @+index: U32 -> @+context: Context -> @+state: Model ->
241    {update(index,context,represent(state)) == represent(model_update(index,context,state)) : Runtime},
242  +count: Nat,+index: U32,+context: Context,+state: Model) ->
243  {Traversal.indexed_fold(~Runtime,~Context,~update,count,index,context,represent(state)) ==
244    represent(Traversal.indexed_fold(~Model,~Context,~model_update,count,index,context,state)) : Runtime}:
245  match count:
246    case 0n: {==}
247    case 1n+ +rest:
248      %Equal.sym(Runtime,update(index,context,represent(state)),represent(model_update(index,context,state)),step_matches(index,context,state)) :
249        {Traversal.indexed_fold(~Runtime,~Context,~update,rest,(index + 1 : U32),context,_) ==
250          represent(Traversal.indexed_fold(~Model,~Context,~model_update,rest,(index + 1 : U32),context,model_update(index,context,state))) : Runtime}
251      indexed_fold_refines_model(~Runtime,~Model,~Context,~update,~model_update,~represent,~step_matches,
252        rest,(index + 1 : U32),context,model_update(index,context,state))