Kleenes Fixpoint Theorem

Stream: mathlib4

[Ira Fesefeldt]

I am interested in formalizing fixpoint theorems and have previous so formalized cousot-cousots fixed point theorem in Mathlib. But I struggle a bit to grasp what the state of the closely related kleenes fixed point theorem is in Mathlib4.

Kleenes Fixed Point theorem says: Given a cpo and a continuos function f, the least fixed point of f is $\sup \{ f^n(\bot) \mid n \in Nat \}$

It seems that this fixed point theorem was implemented for the Part domain in Mathlib.Control.LawfulFix, but no general theorem has been provided yet. Is that correct? Is it then worth it to do this myself?

[Yaël Dillies]

That sounds right, yes

[Ira Fesefeldt]

Assuming I would formalize the general kleene fixpoint theorem, how would I proceed to refactor Mathlib.Control.LawfulFix and Mathlib.Control.Fix? I guess, the proofs for many theorems can be changed. But can I also remove definitions and replace them with their generic counterpart in the theorems without worrying to much? Or should I not worry about refactoring at this point?

[Yaël Dillies]

Everything under Control is unused. Go wild

[Martin Dvořák]

If this version is useful for you
https://github.com/madvorak/fecssk/blob/d7fe3aaa462c7a5cb30a0e35ec6f2973dff0d57b/Fecssk/Class03.lean#L131
I can send you a proof (it was a homework so it is not in the public repo).