Stream: Beginner Questions

Topic: max nat in list


view this post on Zulip Robert Peterson (Aug 26 2022 at 01:47):

hello! i have the following definitions:

fun snoc::"'a list ⇒ 'a ⇒ 'a list" where
"snoc [] x' = [x']" |
"snoc (x#xs) x' = x # (snoc xs x')"

fun reverse :: "'a list ⇒ 'a list" where
"reverse [] = []" |
"reverse (x#xs) = snoc (reverse xs) x"

fun lmax :: "nat list ⇒ nat" where
"lmax [] = 0" |
"lmax [x] = x" |
"lmax (x # xs) = (if x > lmax xs then x else lmax xs)"

and i'd like to prove the following lemma:

lemma "lmax (reverse xs) = lmax xs"
  apply(induction xs)
  apply(auto)
  sorry

the auto fails:

goal (1 subgoal):
 1. a xs. lmax (reverse xs) = lmax xs  lmax (snoc (reverse xs) a) = lmax (a # xs)

so i know i need to prove a lemma related to lmax and snoc. this leads me to think i need to prove:

lemma [simp]:"lmax (snoc xs a) = lmax (a # xs)"
  apply(induction xs)
  apply(auto)
  sorry

which leads me to the following subgoals:

goal (2 subgoals):
 1. aa xs. lmax (snoc xs a) = lmax (a # xs)  lmax (aa # xs) < a  lmax (aa # snoc xs a) = a
 2. aa xs. lmax (snoc xs a) = lmax (a # xs)  ¬ lmax (aa # xs) < a  lmax (aa # snoc xs a) = lmax (aa # xs)

and now i'm stuck :) however, if i check the original lemma with all these sorrys added, i still have a subgoal of:

 1. a xs. lmax (reverse xs) = lmax xs  lmax (a # reverse xs) = lmax (a # xs)

so perhaps i'm not going down the right rabbit hole at all! needless to say, i'm very stuck. does anyone have any pointers?

view this post on Zulip Manuel Eberl (Aug 26 2022 at 07:49):

First of all, it is good practice to give all lemmas (especially those that you declare as simp lemmas) a name, e.g. lmax_snoc.

Second, your problem with the last one is that you reduced lmax (snoc xs a) to lmax (a # xs), but then you're stuck with lmax (a # xs), or to write it in a perhaps clearer form, lmax (Cons a xs). This is also where you get stuck in the proof of your lemma. The solution is therefore to prove a lemma of the form lmax (Cons a xs) = …. This can be done by induction as well, but considering the fact that you define lmax by recursion on the first two elements, a case distinction on xs (i.e. cases xs) also suffices and is a bit easier.

view this post on Zulip Manuel Eberl (Aug 26 2022 at 07:57):

Oh and by the way, you made your life more difficult than necessary: the case lmax [x] = x is unnecessary. If you omit it you get the exact same function. Adding it only makes your induction rule more complicated.

view this post on Zulip Manuel Eberl (Aug 26 2022 at 07:57):

In fact, if you leave it out, you don't even have to prove a lmax (a # xs) rule at all!

view this post on Zulip Manuel Eberl (Aug 26 2022 at 07:59):

If you're confused as to why you don't get a lmax (a # xs) = … simp rule from your definition of lmax, the reason is that the function package will split the pattern matches up to be non-overlapping, i.e. you get lmax [x] = x and then something like lmax (a # b # xs) = (if a > lmax (b # xs) then x else lmax (b # xs)).

view this post on Zulip Manuel Eberl (Aug 26 2022 at 07:59):

You can see this e.g. by doing thm lmax.simps. This shows you the simp rules generated by the function package.

view this post on Zulip Manuel Eberl (Aug 26 2022 at 08:00):

Take-away message: For proofs, keep your definitions as simple as possible! (even if they are ‘inefficient’ – they're mathematical definitions, not code)

view this post on Zulip Manuel Eberl (Aug 26 2022 at 08:01):

(not that your particular case here actually changes efficiency, but just for the future)

view this post on Zulip Robert Peterson (Aug 26 2022 at 15:57):

Manuel Eberl brilliant. that was very helpful. i'm no longer stuck :+1:

the take-away message is great. i need to focus on remembering they're mathematical definitions, not code. thanks :smile:

view this post on Zulip Manuel Eberl (Aug 26 2022 at 16:56):

Absolutely! That is often very confusing for beginners. In particular, Isabelle definitions don't even have to be ‘computable’. You can e.g. define some predicate to hold if and only if (some unknown mathematical conjecture holds). That's perfectly admissible.

view this post on Zulip Manuel Eberl (Aug 26 2022 at 16:57):

And if there is a more efficient way to compute something, or perhaps an alternative definition of the same concept, you can always prove those as theorems later on.


Last updated: Mar 29 2024 at 04:18 UTC