Stream: General

Topic: ✔ Induction rule for Jinja.Kildall

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Notification Bot (Mar 11 2022 at 22:50):

cai has marked this topic as resolved.

Last updated: Dec 07 2023 at 08:19 UTC