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
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