def counter_progress

stelliferous@0.0.2.0 · proofs/loop_projection.bend:101

import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

101def counter_progress(~State: Data,~step: State -> State,~position: State -> U32,~stride: Nat,
102  ~advances: @+state: State -> {position(step(state)) == (position(state) + U32.from_nat(stride) : U32) : U32},
103  +count: Nat,+state: State) ->
104  {position(iterate(~State,~step,count,state)) == (position(state) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32}:
105  match count:
106    case 0n: Equal.sym(U32,(position(state) + 0 : U32),position(state),Arithmetic.add_zero(position(state)))
107    case 1n+ +rest:
108      %add_counted_stride(position(state),stride,rest) : {position(iterate(~State,~step,rest,step(state))) == _ : U32}
109      %advances(state) : {position(iterate(~State,~step,rest,step(state))) == (_ + U32.from_nat(Nat.mul(rest,stride)) : U32) : U32}
110      counter_progress(~State,~step,~position,~stride,~advances,rest,step(state))