Guarded fixpoints

[markusdemedeiros]

Can we metaprogram away the functor/fixpoint construction everyone copy-pastes for defining partial weakest preconditions? I'm picturing something that behaves like partial_fixpoint but for guarded recursion:

def wp (s : Stuckness) (E : CoPset) (e₁ : Expr) (Φ : Val -> IProp GF) : IProp GF :=
  match toVal e₁ with
  | some v => iprop(|={E}=> Φ v)
  | none => iprop(∀ (σ₁ : State) (ns : Nat) (obs obs' : List Obs) (nt : Nat),
    stateInterp σ₁ ns (obs ++ obs') nt ={E,∅}=∗
    ⌜s.MaybeReducible (e₁, σ₁)⌝ ∗
    ∀ e₂ σ₂ eₜ, ⌜(e₁, σ₁) -<obs>-> (e₂, σ₂, eₜ)⌝ -∗
      £ (ι.numLatersPerStep ns + 1) ={∅}▷=∗^[ι.numLatersPerStep ns + 1] |={∅,E}=>
      stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
      wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
guarded_fixpoint

Like partial_fixpoint and coinductive_fixpoint etc, I'd imagine that guarded_fixpoint first tries to solve the contractivity goal by something like aesop_contractive, but also gives an escape hatch for doing it manually

guarded_fixpoint contractive by  
    ...

[MackieLoeffel]

This would indeed be quite nice to have. For greatest and least fixpoints, we should be able to reuse the partial_fixpoint infrastructure of lean by implementing a suitable CCPO instance. This would be enough for WP since WP is monotone.

For guarded_fixpoints, I don't think we can use the partial fixpoint infrastructure since guarded fixpoints are Banach fixpoints, but partial_fixpoint constructs a Kanster Tarski fixpoint.

[oliversoeser]

Claiming this!

[Kaptch]

Just a small follow up on that (and probably you already know that): it is possible to construct CCPO from a COFE by defining it (for X : COFE) as X' := \Sigma (n : Nat with infinity point) (X quotiented by dist n) with order defined as (for a, b : X') a <= b := a.1 <= b.1 \and dist a.1 a.2 b.2. IIRC, that allows to compute Banach's fixpoints by Kleene's fixpoints in this CCPO. Perhaps, it can be used here somehow.