[isabelle] Beginner question: Symmetry of equality in proofs?
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:
datatype 'a list = Nil ("")
| Cons 'a "'a list" (infixr "#" 65)
primrec app :: "'a list => 'a list => 'a list" (infixr "++" 65)
" ++ 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 # )"
lemma "length xs = length (rev xs)"
lemma "length (rev xs) = length xs"
(* apply(simp add: length_suc)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and