Email Gateway (Aug 18 2022 at 16:40): Email Gateway (Aug 18 2022 at 16:40):From: Jason Dagit <dagitj@gmail.com>
Hello,
I'm still very new to isabelle and I've been following the standard tutorial
from the isabelle website.
I was practicing proofs using my own definitions of rev and length.
Here is my theory:
\begin{code}
theory RevLength
imports Datatype
begin
datatype 'a list = Nil ("[]")
| Cons 'a "'a list" (infixr "#" 65)
primrec app :: "'a list => 'a list => 'a list" (infixr "++" 65)
where
"[] ++ ys = ys" |
"(x # xs) ++ ys = x # (xs ++ ys)"
primrec rev :: "'a list => 'a list" where
"rev [] = []" |
"rev (x # xs) = (rev xs) ++ (x # [])"
primrec length :: "'a list => nat" where
"length [] = 0" |
"length (x # xs) = 1 + length xs"
lemma length_suc: "Suc (length list) = length (list ++ a # [])"
apply(induct_tac list)
apply(auto)
done
lemma "length xs = length (rev xs)"
apply(induct_tac xs)
apply(simp, simp)
apply(rule length_suc)
done
lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply(simp, simp)
oops
(* apply(simp add: length_suc)
done *)
\end{code}
What I noticed was that between the last two lemmas, the direction of the
equality makes a huge difference when proving the lemma. The lemma "length
xs = length (rev xs)" is easy to prove but lemma "length (rev xs) = length
xs" is much harder to prove (for me at least).
I thought that maybe it was because the induction variable was inside a
function call on the LHS, but one of the first examples of induction in the
tutorial is theorem rev_rev[simp]: "(rev (rev xs)) = xs", which is easily
proven by induction on xs followed by auto.
I would expect "=" to be symmetric. Is that not the case? Is there
something else going on here?
On a side note, I tried to define Cons as ":" instead of "#", but I kept
getting ambiguous parses. Why is that? ":" doesn't seem to be used in the
grammar that I've seen thus far in the tutorial, but it's also a hard thing
to search for.
Thanks,
Jason
Email Gateway (Aug 18 2022 at 16:40):From: Lars Noschinski <noschinl@in.tum.de>
On 13.12.2010 05:58, Jason Dagit wrote:
lemma length_suc: "Suc (length list) = length (list ++ a # [])"
apply(induct_tac list)
apply(auto)
done
[...]
lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply(simp, simp)
oops
(* apply(simp add: length_suc)
done *)
\end{code}What I noticed was that between the last two lemmas, the direction of the
equality makes a huge difference when proving the lemma. The lemma"length
xs = length (rev xs)" is easy to prove but lemma "length (rev xs) =length
xs" is much harder to prove (for me at least).
You don't need to prove this for yourself. If you name the second lemma
e.g. rev_length, then the third lemma is just rev_length[symmetric].
I would expect "=" to be symmetric. Is that not the case? Is there
something else going on here?
The simplifier applies equalities only from left to right. In your case
the problem is the formulation of length_suc: The right hand side
contains a variable which does not occur on the left hand side, so the
simplifier does not apply this rule, as it does not know how to
instantiate this variable.
A proof easily succeeds by
apply(simp add: length_suc[symmetric])
but I suggest you change the definition of length suc. As a rule of
thumb, rules to be used by the simplifier should be "simpler" on the
right hand side than on the left hand side.
-- Lars
Email Gateway (Aug 18 2022 at 16:40):From: Brian Huffman <brianh@cs.pdx.edu>
On Sun, Dec 12, 2010 at 11:10 PM, Lars Noschinski <noschinl@in.tum.de> wrote:
On 13.12.2010 05:58, Jason Dagit wrote:
What I noticed was that between the last two lemmas, the direction of the
equality makes a huge difference when proving the lemma. The lemma"length
xs = length (rev xs)" is easy to prove but lemma "length (rev xs) =length
xs" is much harder to prove (for me at least).
[...]
I would expect "=" to be symmetric. Is that not the case? Is there
something else going on here?The simplifier applies equalities only from left to right. In your case the
problem is the formulation of length_suc: The right hand side contains a
variable which does not occur on the left hand side, so the simplifier does
not apply this rule, as it does not know how to instantiate this variable.
Another thing to remember about the simplifier: It uses the
assumptions of the current subgoal as rewrite rules. And as always, it
only uses equalities left-to-right.
So in your proof script:
lemma "length (rev xs) = length xs"
apply(induct_tac xs)
apply (simp, simp)
you now have the following subgoal:
goal (1 subgoal):
Here the simplifier would replace any occurrences of "length (rev
list)" in the conclusion with "length list", except that "length (rev
list)" does not appear in the conclusion, so the inductive hypothesis
does not get used by the simplifier.
Last updated: Apr 25 2024 at 08:20 UTC