def iteration_matches_denotation

stelliferous@0.0.2.0 · proofs/loop_projection.bend:38

import Base

38def iteration_matches_denotation(
39  ~Observation: Data,~State: Data,
40  ~Index: Data,
41  ~step: State -> State,
42  ~project: Index -> State -> Observation,
43  ~denote: Index -> Nat -> State -> Observation,
44  ~at_zero: @+index: Index -> @+state: State -> {project(index,state) == denote(index,0n,state) : Observation},
45  ~after_step: @+index: Index -> @+count: Nat -> @+state: State -> {denote(index,count,step(state)) == denote(index,1n+count,state) : Observation},
46  +count: Nat,+index: Index,+state: State
47) -> {project(index,iterate(~State,~step,count,state)) == denote(index,count,state) : Observation}:
48  match count:
49    case 0n: at_zero(index,state)
50    case 1n+ +rest:
51      %after_step(index,rest,state) : {project(index,iterate(~State,~step,rest,step(state))) == _ : Observation}
52      iteration_matches_denotation(~Observation,~State,~Index,~step,~project,~denote,~at_zero,~after_step,rest,index,step(state))