Re: [isabelle] Curious failure of simp when goal equation is reoriented

Dear Nick,

if you really prefer the resulting lemma in the orientation you gave you could also do

  lemma rev_app_2 [symmetric]:
    "rev (app xs ys) = app (rev ys) (rev xs)"
    by (induct xs) simp_all

to get the desired lemma in one step. (I.e., inside the proof the given orientation is used, but after the proof is finished the attribute [symmetric] swaps the two sides of the equation before the name "rev_app_2" is assigned to it.)



On 02/04/2014 01:05 PM, Manuel Eberl wrote:

first of all, the simplifier can sometimes work with “A = B”, but not
with “B = A”, if the rule it needs to apply is something like “(A = B) =
(C = D)”. However, this is not the case here. The problem in your case
is that you call induct before simp_all, and the case that does not go
through here is the induction step.

In the induction step, you have the induction hypothesis as a premise,
and it obviously depends on the goal of your original lemma statement.
Therefore, if you flip your original goal, the induction hypothesis will
also be flipped.

The induction step you get in your case is:
⋀a xs. app (rev ys) (rev xs) = rev (app xs ys) ⟹
           app (rev ys) (rev (Cons a xs)) = rev (app (Cons a xs) ys)

After simplification, it looks like this:

  ⋀a xs. app (rev ys) (rev xs) = rev (app xs ys) ⟹
            app (rev ys) (app (rev xs) (Cons a Nil)) = app (rev (app xs
ys)) (Cons a Nil)

As you can see, the left-hand side of your induction hypothesis does not
match anything in the goal, and because the simplifier uses equations
left-to-right, there is nothing else it can do here. One simple way to
fix this is by using

apply (drule sym)

which flips your induction hypothesis, then it matches and everything
goes through with the simplifier, so something like

lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
apply (induct xs)
apply simp
apply (drule sym)
apply simp

However, I would rather suggest this:

lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
by (rule sym) (fact rev_app_1)

sym is simply the rule “A = B ⟹ B = A”, so “rule sym” flips the equation
in your goal, after which it is identical to the statement of rev_app_1.


On 03/02/14 16:29, Nick Smallbone wrote:
Hi Isabellers,

I've been playing with the list theory from the Isabelle tutorial and
bumped into something odd. After defining rev and app, and giving a
couple of simplification rules, I can prove the following lemma with
induct and simp:
    lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
But not this one:
    lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"

This seems rather strange to me, because all I've done is flipped the
equation around. I can understand that reorienting a simplification
rule will affect the behaviour of simp, but why does reorienting the
goal make a difference?

Code follows at the end of this message. What have I missed?

Nick (with his confused newbie hat on)

theory Lists
imports Datatype

datatype 'a list = Nil | Cons 'a "'a list"

primrec app :: "'a list => 'a list => 'a list"
"app Nil xs = xs" |
"app (Cons x xs) ys = Cons x (app xs ys)"

primrec rev :: "'a list => 'a list"
"rev Nil = Nil" |
"rev (Cons x xs) = app (rev xs) (Cons x Nil)"

(* Two simplification rules *)
lemma app_nil[simp]: "app xs Nil = xs"
apply (induct xs)
apply simp_all

lemma app_assoc[simp]: "app (app xs ys) zs = app xs (app ys zs)"
apply (induct xs)
apply simp_all

(* This lemma goes through... *)
lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
apply (induct xs)
apply simp_all

(* ...but this one doesn't *)
lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
apply (induct xs)
apply simp_all

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.