Go backward to Reasoning about Least Fixed Points Go up to Top

Reasoning about Least Fixed Points

C[[repeat C until B]] = fix(lambda f. lambda s.
    let s' = C[[C]]s in B[[B]]s' -> s' [] (f s'))

C[[C; while ~B do C]] =^? C[[repeat C until B]]

Proof: P(f,g) = forall s. f(C[[C]]s) = (g s)

1. P(_|_, _|_) holds obviously.
2. Prove P(F(f), G(g))

   F=(lambda f. lambda s. B[[~ B]]s -> f(C[[C]]s) [] s)
   G=(lambda f. lambda s. let s' = C[[C]]s in B[[B]]s'
       -> s' [] (f s'))

   1. F(f)(C[[C]]_|_) = _|_ = G(g)(_|_).
   2. s != _|_:
      1. C[[C]]s=_|_: F(f)(_|_)=_|_=(let s' = _|_ in B[[B]]s' -> s' [] (g s')) = G(g)(_|_).
      2. C[[C]]s=s₀ != _|_: F(f)(s₀)=B[[~ B]]s₀ -> f(C[[C]]s₀)[]s₀ = B[[B]]s₀ -> s₀ [] f(C[[C]]s₀) = B[[B]]s₀ -> s₀ [] f(g s₀) = G(g)(s)