cai (Feb 25 2022 at 15:23): cai (Feb 25 2022 at 15:23):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?
cai (Feb 25 2022 at 15:25):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.
Notification Bot (Mar 11 2022 at 22:50):cai has marked this topic as resolved.
Last updated: Dec 21 2024 at 12:33 UTC