Abu (Sep 17 2023 at 02:17): Abu (Sep 17 2023 at 02:17):(Disclaimer: I'm using my own list definition instead of the built-in one for learning purposes)
Hello. I'm having trouble proving this simple lemma below. I've reduced it to: "reverse (reverse (exercises.list.Cons x1 xs)) = exercises.list.Cons x1 xs" but isabelle still can't solve it. What am I missing here?
datatype 'a list = Nil | Cons 'a " 'a list"
fun snoc :: "'a list ⇒ 'a ⇒ 'a list" where
"snoc Nil x = Cons x Nil" |
"snoc (Cons y ys) x = Cons y (snoc ys x)"
fun reverse :: "'a list ⇒ 'a list" where
"reverse Nil = Nil" |
"reverse (Cons x xs) = (snoc (reverse xs) x)"
lemma snoc_simp [simp] : "snoc (reverse xs) x = reverse (Cons x xs)"
apply(induction xs)
apply(auto)
done
lemma rev_1: "reverse (reverse xs) = xs"
apply (induction xs)
apply(auto)
done
Wolfgang Jeltsch (Sep 17 2023 at 14:10):For snoc_simp you can get away with a much simpler proof, as it is just the second defining equation of reverse with sides swapped. For example, this works:
lemma snoc_simp [simp]: "snoc (reverse xs) x = reverse (Cons x xs)"
apply (fact reverse.simps(2) [symmetric])
done
You can also let Isabelle automatically pick said defining equation as a rewrite rule, as in the following version:
lemma snoc_simp [simp]: "snoc (reverse xs) x = reverse (Cons x xs)"
apply simp
done
I guess the fact that snoc_simp is the second defining equation reversed is the root of auto in the last proof getting stuck: both snoc_simp and the second defining equation are part of the simpset, which means that simplifying proof methods like auto can just get stuck with rewriting back and forth.
Wolfgang Jeltsch (Sep 17 2023 at 14:17):When proving reverse (reverse xs) = xs and applying induction on xs, you get as the second case reverse (reverse (Cons y ys)). The inner reverse application can then get rewritten using the second defining equation of reverse, which turns the whole subgoal into reverse (snoc (reverse ys) y). I guess you now need a lemma for rewriting the outer reverse application such that the reverse is pushed inside and you get reverse (reverse ys) as a subterm, which can then be rewritten using the induction hypothesis. So you don’t need your snoc_simp, which is for rewriting snoc applied to a reverse application, but you need a lemma for rewriting reverse applied to a snoc application.
Abu (Sep 17 2023 at 23:30):Thank you so much!
Last updated: Dec 21 2024 at 16:20 UTC