Max Nowak (Jun 06 2021 at 19:30): Max Nowak (Jun 06 2021 at 19:30):I'm stuck in a proof and thoroughly confused about what I am even doing. I have defined myself a loop composition operator which just starts a helper initalized with a neutral accumulator: loop m p = loop_helper dummy m p, and then I have (excessively simplified):
function loop_helper where
(my_term_cond (acc p)) ==> loop_helper acc m p = acc
not (my_term_cond (acc p)) ==> loop_helper acc m p = loop_helper (steppy acc m) m p
And now I want to prove something about loop, akin to loop m p = loop m (f p), but I can't figure out the approach. I know of loop_helper.induct, but I don't think I can use it, or at least, I can't figure it out. Is there some canonical approach on how I can induct over the steps of loop?
Manuel Eberl (Jun 06 2021 at 20:09):If you define a recursive function and want to prove anything about it, you're indeed going to have to use induction. Before you can use the induction rule, you will however also have to prove termination (not sure if you have – you did not really mention it). Before that, there is only a partial induction (pinduct) rule that has termination as an additional assumption. In most cases, you should aim to prove termination.
Once that is done, you can use the induct rule to prove some property about loop_helper that is a generalisation of the thing you want to prove for loop.
However, I should point out that you might fare better using one of the while combinators from HOL-Library.While_Combinator. You give them an initial state, a step function, and a breaking condition. There's one where you have to prove termination and one that does not require proving termination but only returns an option type (with None signifying non-termination). You can then prove whatever result you need about the result by providing a suitable loop invariant using e.g. while_rule.
Max Nowak (Jun 06 2021 at 20:16):I have termination, yes. While While-Combinators look promising, sadly I am only adding new code to an existing framework which contains loop. Maybe if I had more time to delve into restructuring the existing code I'd give it a shot, but I don't :/.
Manuel Eberl (Jun 06 2021 at 20:22):In that case, you have to figure out the loop invariant and prove that
The rest is then a simple induction.
Max Nowak (Jun 06 2021 at 21:04):The thing I can't figure out is the accumulator though. I need to prove my property just for loop_helper dummy m p, with dummy being the starting point, and then loop_helper expands it until it terminates. But loop_helper.induct gives me goals such as (base case:) !!acc m p. my_term_cond (acc p) ==> ?P acc m p, so, do I have to prove it for all possible acc in the base case? Maybe you know of some (hopefully very) simple sample proofs so I can have a look at how to do it, since I'm just hopelessly confused.
Mohammad Abdulaziz (Jun 07 2021 at 09:41):I would like to note that the approach of using the function package gives you better flexibility if you want to prove partial termination. E.g. you will not need to learn any of the automation behind the while-combinator and you have greater flexibility in structuring your proofs. A good reference on how to use the induction principle that comes out of the function package is in section 8 in the `functions' tutorial in the Isabelle documentation. The following paper uses the function package for an interesting small example:
https://files.sketis.net/Isabelle_Workshop_2020/Isabelle_2020_paper_1.pdf
Max Nowak (Jun 07 2021 at 09:58):....I now noticed there is a small inductive proof example in the isabelle docs on functions, which I skipped when first learning Isabelle, and then forgot forever that it existed.
Max Nowak (Jun 07 2021 at 11:32):Hmm, using proof (induct p rule: loop_helper.induct) just highlights the proof (induct...) line purple and Isabelle becomes unberably laggy forever, to the point I need to terminate the process.
Jakub Kądziołka (Jun 07 2021 at 11:33):Hmm, this means that the induct proof method does not terminate. Perhaps induction instead will work better?
Max Nowak (Jun 07 2021 at 11:34):I wasn't aware there is a difference between the two. And nope, same issue sadly.
Max Nowak (Jun 07 2021 at 11:38):Adding the remaining free variables as arbitraries worked somehow though. I have no clue why.
Max Nowak (Jun 07 2021 at 11:40):But now (after clicking on the proof outline in jEdit ouput window), the then show statements have a squiggly underline. It fails to refine any pending goal.
Max Nowak (Jun 07 2021 at 11:41):(Now I remember, this was the point where I gave up a month or two ago :D)
Jakub Kądziołka (Jun 07 2021 at 11:42):IIRC this sometimes happens when one of the goals was automatically solved because the assumptions were trivially contradictory
Jakub Kądziołka (Jun 07 2021 at 11:42):are there as many goals as there are shows?
Jakub Kądziołka (Jun 07 2021 at 11:42):anyway, you can always use show manually to show the expected thing
Max Nowak (Jun 07 2021 at 11:43):I just have lemma " ... = ..." proof (induct...)
Max Nowak (Jun 07 2021 at 11:43):And yes two goals are generated
Jakub Kądziołka (Jun 07 2021 at 11:44):assumptions as in the goal is ?P 0 and you're inducting over Suc n
Jakub Kądziołka (Jun 07 2021 at 11:44):is there a chance you could create a minimal example that reproduces the problem?
Max Nowak (Jun 07 2021 at 12:49):Here you go. I didn't manage to recreate how adding arbitraries fixes it though, I'd have to copy over even more code then.
I had initially created an MWE without Mutators, but adding those introduced the hanging again.
theory LoopyLand imports Main
begin
type_synonym 'a Result = "('a set)"
type_synonym 'a Module = "'a list ⇒ 'a Result"
type_synonym 'a Mutator = "'a Result ⇒ 'a list ⇒ 'a list" (* Modifies `as` given a Result. *)
type_synonym 'a TermCond = "'a Result ⇒ bool"
(* Run m1, then mutate p, and pipe that into m2. Unify results. Probably irrelevant for MWE though. *)
fun steppy :: "'a Module ⇒ 'a Mutator ⇒ 'a Module ⇒ 'a Module" where
"steppy m1 M m2 p = (m1 p) ∪ (m2 (M (m1 p) p))"
(* loop_helper stops when user-provided termination condition tell us to, or
when we reached a fixed point (result remains the same when we add more `m`). *)
fun whendoesitstop where
"whendoesitstop acc m M t p = (t (acc p) ∨ (steppy acc M m) p = acc p)"
(* Build a chain of steppy. Which slowly grows our result set. *)
function loop_helper :: "'a Module ⇒ 'a Module ⇒ 'a Mutator ⇒ 'a TermCond ⇒ 'a Module" where
"whendoesitstop acc m M t p ⟹ loop_helper acc m M t p = acc p" |
"¬(whendoesitstop acc m M t p) ⟹ loop_helper acc m M t p = loop_helper (steppy acc M m) m M t p"
apply fast apply simp apply simp by simp termination sorry
fun dummy :: "'a Module" where "dummy p = {}"
fun never_stop :: "'a TermCond" where "never_stop result = False"
fun fake_mutator :: "'a Mutator" where "fake_mutator result p = p"
(* The module we want to prove stuff for. In reality, does more exciting stuff. *)
fun find_nemo :: "'a Module" where "find_nemo p = {}"
lemma "loop_helper dummy find_nemo fake_mutator never_stop p = loop_helper dummy find_nemo fake_mutator never_stop (f p)"
proof (induct p rule: loop_helper.induct (* <---- complete the brace *)
qed
end
Actually, if you just completely get rid of TermCond (you want me to copy paste the code again?), it does manage to come up with some goals. Some very.... questionable goals :D
proof (state)
goal (2 subgoals):
1. ⋀acc m M p.
whendoesitstop acc m M p ⟹
m p =
m (M (?Pa3 acc m M p)
(M (?Pa4 acc m M p)
(M (?Pa5 acc m M p)
(M (?Pa6 acc m M p)
...
(M (?Pa57 acc m M p) (f p))
Last updated: Apr 25 2024 at 08:20 UTC