Robert Peterson (Aug 26 2022 at 01:47): 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?
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.
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.
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!
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)).
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.
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)
Manuel Eberl (Aug 26 2022 at 08:01):(not that your particular case here actually changes efficiency, but just for the future)
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:
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.
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: Dec 21 2024 at 16:20 UTC