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



Hallo,

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
done

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.


Cheers,
Manuel


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
> begin
>
> datatype 'a list = Nil | Cons 'a "'a list"
>
> primrec app :: "'a list => 'a list => 'a list"
> where
> "app Nil xs = xs" |
> "app (Cons x xs) ys = Cons x (app xs ys)"
>
> primrec rev :: "'a list => 'a list"
> where
> "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
> done
>
> lemma app_assoc[simp]: "app (app xs ys) zs = app xs (app ys zs)"
> apply (induct xs)
> apply simp_all
> done
>
> (* This lemma goes through... *)
> lemma rev_app_1: "rev (app xs ys) = app (rev ys) (rev xs)"
> apply (induct xs)
> apply simp_all
> done
>
> (* ...but this one doesn't *)
> lemma rev_app_2: "app (rev ys) (rev xs) = rev (app xs ys)"
> apply (induct xs)
> apply simp_all
> done
>





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