Trying to prove

```
lemma aval_plus: " aval (Ex_3_1.plus (N (sumN t1)) (asimp (zeroN t1))) s = aval t1 s ⟹
aval (Ex_3_1.plus (N (sumN t2)) (asimp (zeroN t2))) s = aval t2 s ⟹
aval (Ex_3_1.plus (N (sumN t1 + sumN t2)) (Ex_3_1.plus (asimp (zeroN t1)) (asimp (zeroN t2)))) s = aval t1 s + aval t2 s
```

I have a vague feeling that the knowledge to prove this is within the knowledge of aval's, plus' and asimp's definition (induction rule?).

What is a good strategy when you find such a lemma? How to feed the necessary facts into the automated proof search procedures?

I tried (induction t1 arbitrary: t2) to no avail.

Please also provide context, i.e. the definitions of all these constants (you can attach a .thy file).

Here is a minimal version of the file:

your theory file doesn't define `asimp`

, so Isabelle wants you to prove this for all possible functions `asimp`

(as can be seen by the name being blue)

I assume the lemma you actually want to prove left you with this monstrosity after `simp`

...

could you post what you actually want to prove?

My teaching intuition says that after simp, you are left with something that is calling for a `aval (asimp (zeronN t1)) = t1`

theorem

also, I don't think it's necessary to remove lemmas you've already proven about these definitions

more like `aval (asimp (zeroN t1)) + sumN t1 = aval t1`

@Jakub Kądziołka here is a theory file with asimp's definition:

Jakub Kądziołka said:

more like

`aval (asimp (zeroN t1)) + sumN t1 = aval t1`

Good point, reading the theory files helps :grinning:

Now with the final theorem and its definitions included:

@Mathias Fleury yes reading helps but I am lost now and don't know what to look for.

@Gergely Buday I opened the file, called `auto`

and was like: "why on earth is `aval (plus ... ....)`

not simplified to `aval ... + aval ...`

?"

do you have a lemma that says `aval (asimp a) s = aval a s`

?

You should really add the lemma on aval plus.

it would compose with aval_sepN wonderfully

Jakub Kądziołka said:

it would compose with aval_sepN wonderfully

both lemmas even deserve to be [simp] rules!

@Jakub Kądziołka not yet but I go for it

Sorry for being so uncomprehending. Digging through the Concrete Semantics sketch files I have found a lemma that was essential:

```
lemma aval_plus: "aval (plus a1 a2) s = aval a1 s + aval a2 s"
```

This is a more basic lemma, and this was the real lesson: I should find the most basic "trivial" but unproven statement. With this missing element proof automation completes the puzzle.

Also, an answer to my original question on how to feed knowledge about functions into a proof: for "fun" functions this knowledge is automatically transferred into simplification, for "definition" functions they should be named as _defs, and the real question is the combination of functions for which the rules should be proven explicitly. Am I right?

Yes, some_function.simps is automatically included in the simplifier rule set and is thus used automatically by `simp`

, `auto`

, `force`

, and `fastforce`

; for definitions you need to use `unfolding some_definition_def`

or `apply (auto simp: some_definition_def)`

(the former will inline the definition within your goal, the latter will tell the simplifier to unfold it even if it arises after some simplification was already done).

There's nothing special about "combinations of functions", it's just that the auxiliary properties required an induction in their proof.

like, if you have `aval (asimp a) s`

, there aren't any rules in the definition of asimp that apply to an arbitrary term `a`

, so the simplifier can't do anything with that until you prove some lemma that has `asimp a`

or `aval (asimp a) s`

on the left-hand side of an equality

that lemma would then have to be named explicitly in the general case (`apply (simp add: some_fact)`

), but you can also tag your theorems as simplification rules with `lemma foo[simp]: "..."`

when you do that, the right-hand side of the equality should be 'simpler' in some way than the left-hand side

when a lemma is already in the simpset, you can remove it for a one-off proof with `simp del: some_fact`

(or `auto simp del: ...`

). However, if you find yourself doing that too often, then that fact probably shouldn't be `[simp]`

in the first place

also, if you aren't careful, the simplifier may not terminate on some terms. `using [[simp_trace]] apply simp`

is a useful way to debug that (there's also `using [[simp_trace_new]]`

, which I find easier to read, but it doesn't tell you the names of the facts it uses to rewrite)

FWIW, this is also useful to get an intuition for how the simplifier works

Last updated: Oct 13 2024 at 01:36 UTC