I am using the AFP entry Kildall to obtain a fixpoint by iteration. Now I have proved `fixpoint = step fixpoint`

. I also proved completeness for the obtained algorithm but am struggling with showing soundness, due to missing an induction rule.

The fixpoint is over `replicate N False`

, ie. I want to prove something like `i < N ⟹ fixpoint ! i ⟹ P i`

- however I am struggling a lot. Is there a good way, or do I need to redifine my function?

I can expand `fixpoint`

to `next fixpoint`

and then from this I can obtain some variables `?a0. P' a0`

with `!x : set a0. fixpoint ! x`

but I cannot tie the loop, the proof would recurse indefinitely (but due to using Kildall I know it shouldn't).

Is there some neat trick to make my life easier and exploit that the function is well-founded and the inter-dependencies/ordering of my `i`

don't matter as it is a fixpoint?

I want to keep this as general as possible, because in the end I will be using Kildall multiple times for different functions (always bit-vectors/`bool list`

) and it seems that generalizing this from the biginning should save me a bunch of proof.

cai has marked this topic as resolved.

Last updated: Dec 07 2023 at 08:19 UTC