Stream: Beginner Questions

Topic: Why doesn't this proof work without rule_format?

o7 (Dec 11 2024 at 13:45):

I'm trying to understand the proof structure of one of the lemmas in this file, namely

lemma [simp]: "ListSumT (x#xs) = x + ListSumT xs"
  by (auto simp add: ListSumT_def ListSumTAux_add[THEN sym])

The lemma ListSumTAux_add is used to help prove the goal

ListSumTAux xs x = x + ListSumTAux xs 0

for reference it looks like:

lemma ListSumTAux_add [rule_format]: "∀a b. ListSumTAux xs (a+b) = a + ListSumTAux xs b"
  by (induct xs) auto

Why doesn't the proof work if I remove the [rule_format] tag from the lemma and the [THEN sym] tag from the apply command? Is it because the structure of the goal does not exactly match that of ListSumTAux_add - that is, isabelle cannot deduce on its own that ListSumTAux xs x = ListSumTAux xs (x + 0) and proceed from there?

Furthermore, what is [THEN sym] and what does it do?

Mathias Fleury (Dec 11 2024 at 14:23):

Like every theorem, print it:

thm ListSumTAux_add[THEN sym]

and Control-click on sym to see what it is

Mathias Fleury (Dec 11 2024 at 14:24):

thm ListSumTAux_add[rule_format] ListSumTAux_add

Mathias Fleury (Dec 11 2024 at 14:26):

ListSumTAux xs x = ListSumTAux xs (x + 0)

The simplifier only rewrites to make terms easier and this is in the wrong direction

o7 (Dec 11 2024 at 14:29):

So in that case, was the proof trying to modify the RHS of the goal, not the LHS?

Mathias Fleury (Dec 11 2024 at 14:30):

It is modifying both

Mathias Fleury (Dec 11 2024 at 14:31):

And ListSumTAux xs (x + 0) -> ListSumTAux xs x due to x+0=x

o7 (Dec 11 2024 at 14:31):

very interesting. If it was modifying both sides I would have thought that the ordering of the sides in ListSumTAux_add shouldn't matter

o7 (Dec 11 2024 at 14:32):

so I would expect that [THEN sym] doesn't need to be there, yet it is

o7 (Dec 11 2024 at 14:34):

Mathias Fleury said:

ListSumTAux xs x = ListSumTAux xs (x + 0)

The simplifier only rewrites to make terms easier and this is in the wrong direction

just to make sure I fully understand, why is this in the wrong direction?

Mathias Fleury (Dec 11 2024 at 14:34):

 thm ListSumTAux_add
  lemma [simp]: "ListSumT (x#xs) = x + ListSumT xs"
    apply (auto simp add: ListSumT_def ListSumTAux_add)
(*
proof (prove)
goal (1 subgoal):
 1. ListSumTAux xs x = x + ListSumTAux xs 0
*)

Mathias Fleury (Dec 11 2024 at 14:34):

It is clear why ListSumTAux_add[THEN sym] applies here

Mathias Fleury (Dec 11 2024 at 14:35):

o7 said:

ListSumTAux xs x = ListSumTAux xs (x + 0)

ListSumTAux xs x ~> ListSumTAux xs (x + 0)

Which term is more complicated? Rewriting simplifies the term

o7 (Dec 11 2024 at 14:36):

RHS looks more obvious to simplify

o7 (Dec 11 2024 at 14:40):

oh, so lemmas involving equality are like left to right applications.
When applying one to prove a goal, you want to make sure that the LHS of the lemma matches with either of the sides of the goal, which will then be transformed into the RHS of the applied lemma.

Is my understanding correct?

Last updated: Dec 21 2024 at 16:20 UTC