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?

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`

.

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 :/.

In that case, you have to figure out the loop invariant and prove that

- the initial state fulfils it
- the step function preserves it
- the invariant plus the termination condition imply what you want to show

The rest is then a simple induction.

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.

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

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

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.

Hmm, this means that the `induct`

proof method does not terminate. Perhaps `induction`

instead will work better?

I wasn't aware there is a difference between the two. And nope, same issue sadly.

Adding the remaining free variables as arbitraries worked somehow though. I have no clue why.

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.

(Now I remember, this was the point where I gave up a month or two ago :D)

IIRC this sometimes happens when one of the goals was automatically solved because the assumptions were trivially contradictory

are there as many goals as there are `show`

s?

anyway, you can always use `show`

manually to show the expected thing

I just have `lemma " ... = ..." proof (induct...)`

And yes two goals are generated

assumptions as in the goal is `?P 0`

and you're inducting over `Suc n`

is there a chance you could create a minimal example that reproduces the problem?

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

s, 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: Sep 25 2021 at 08:21 UTC