Ordinals and fixed points of monotone functions

Stream: mathlib4

[Simon Tobias Lund]

Hi everyone,

I am a PhD student who has previously worked quite a bit in Isabelle and is currently trying out Lean. I have some questions about whether something already exists or if it could be appropriate as a contribution. General thoughts would also be appreciated :)

In an Isabelle project on weakest preconditions and program verification I needed to create some new machinery for working with fixed points of monotone functions over complete lattices. The problem with the existing framework was that they define the least fixed point (lfp) of a monotone function f as infimum({x | f(x) <= x}) and then show that a transfinite induction principle is admissible: (forall x. P(x) ==> P(f(x))) && (forall X. (forall x in X. P(x)) ==> P (supremum(X))) ==> P(lfp(f)). This works for properties of a single function, but not for relations between the least fixed points of different monotone functions.

I found, for example, that showing that the weakest preconditions of a simple while-language is conjunctive (wp(s,Q) && wp(s,P) ==> wp(s,Q && P)) was quite hard with the existing framework. My solution was to define new machinery for finding the least fixed point of a monotone function as follows:

We define the transfinite iteration of a function f
f^0 (x) = x
f^(o+1) (x) = f (f^o (x))
f^o (x) = bound({ f^o' (x) | o' < o}) for limit ordinal o

We can show that if we use bound=supremum then there is an ordinal o such that for all o' >= o we have that f^o' (bot) is the least fixed point of f.

This means that we can show P(lfp f, lfp g) for monotone functions f and g by showing P(f^o (bot), g^o (bot)) (for all o) by transfinite induction on o.

What do you think? Does something like this already exists? Would it be relevant for mathlib?

Best,
Simon

[Mario Carneiro]

Do you have an example of an argument that would use this style of induction? In lean, it's pretty rare to directly perform transfinite induction on ordinals, because induction on carefully chosen inductive types usually more directly relates to the problem domain.

[Simon Tobias Lund]

Here is a thing I have used it for in Isabelle:

If we have a programming language with while-statements, if-statements, and a variable declarations/havoc-statement (non-deterministically assign an arbitrary value to a variable), then the weakest precondition (given a set of acceptable states at the end of a program, return the acceptable states at the start) of that language is not scott-continuous, but it is monotone. I will write wp(s,Q) for the weakest precondition of program s for postcondition Q

The weakest precondition of while(b){s} is lfp (λ X. (b ==> wp(s,X)) && (¬b ==> Q)). I will call λ X. (b ==> wp(s,X)) && (¬b ==> Q) for phi(Q) from now on.

To show that the weakest precondition is conjunctive (wp(s,P) && wp(s,Q) ==> wp(s,P && Q)) we then need to show:
lfp(phi(P)) && lfp (phi(Q)) ==> lfp (phi(P && Q))

It is easy enough to show that if X && Y ==> Z then phi(P)(X) && phi(Q)(Y) ==> phi(P && Q)(Z) and that if all the elements of three sets U, V, and W can be ordered into tuples (X,Y,Z) with X in U, Y in V, and Z in W such that X && Y ==> Z, then supremum(U) && supremum(V) ==> supremum(W). These are the two proofs required for showing that phi(P)^o (bot) && phi(Q)^o (bot) ==> phi(P && Q)^o (bot) by induction on o. I could, however, not find any way to use these proofs to show conjunctivity with the existing induction principles for fixed points in Isabelle.

Other ways of showing this property that I have considered all seem far more complicated.

Best,
Simon

[Mario Carneiro]

This sounds like something used to fill a gap in isabelle. It's not clear at all from this whether this is a gap in lean/mathlib; you would have to do something at least vaguely analogous in lean and find out if/when you get stuck

[Simon Tobias Lund]

Right, that is a good point. I'll try to do so.