def preserves_observation

stelliferous@0.0.2.0 · proofs/loop_projection.bend:26

import Base

26# A read-only observation is preserved for every number of iterations.
27def preserves_observation(
28  ~State: Data,~Observation: Data,~step: State -> State,~observe: State -> Observation,
29  ~preserved: @+state: State -> {observe(step(state)) == observe(state) : Observation},
30  +count: Nat,+state: State
31) -> {observe(iterate(~State,~step,count,state)) == observe(state) : Observation}:
32  match count:
33    case 0n: {==}
34    case 1n+ +rest:
35      %preserved(state) : {observe(iterate(~State,~step,rest,step(state))) == _ : Observation}
36      preserves_observation(~State,~Observation,~step,~observe,~preserved,rest,step(state))