## Stream: Beginner Questions

### Topic: Feeding knowledge about functions

#### Gergely Buday (Jan 26 2021 at 10:42):

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.

#### Manuel Eberl (Jan 26 2021 at 10:46):

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

#### Gergely Buday (Jan 26 2021 at 10:58):

Here is a minimal version of the file:

AvalPlus.thy

#### Jakub Kądziołka (Jan 26 2021 at 11:15):

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)

#### Jakub Kądziołka (Jan 26 2021 at 11:16):

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

#### Jakub Kądziołka (Jan 26 2021 at 11:16):

could you post what you actually want to prove?

#### Mathias Fleury (Jan 26 2021 at 11:20):

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

#### Jakub Kądziołka (Jan 26 2021 at 11:21):

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

#### Jakub Kądziołka (Jan 26 2021 at 11:22):

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

#### Gergely Buday (Jan 26 2021 at 11:24):

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

AvalPlus.thy

#### Mathias Fleury (Jan 26 2021 at 11:25):

Jakub Kądziołka said:

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

Good point, reading the theory files helps :grinning:

#### Gergely Buday (Jan 26 2021 at 11:27):

Now with the final theorem and its definitions included:

AvalPlus.thy

#### Gergely Buday (Jan 26 2021 at 11:28):

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

#### Mathias Fleury (Jan 26 2021 at 11:28):

@Gergely Buday I opened the file, called `auto` and was like: "why on earth is `aval (plus ... ....)` not simplified to `aval ... + aval ...`?"

#### Jakub Kądziołka (Jan 26 2021 at 11:30):

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

#### Mathias Fleury (Jan 26 2021 at 11:30):

You should really add the lemma on aval plus.

#### Jakub Kądziołka (Jan 26 2021 at 11:30):

it would compose with aval_sepN wonderfully

#### Mathias Fleury (Jan 26 2021 at 11:32):

Jakub Kądziołka said:

it would compose with aval_sepN wonderfully

both lemmas even deserve to be [simp] rules!

#### Gergely Buday (Jan 26 2021 at 11:32):

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

#### Gergely Buday (Jan 26 2021 at 12:05):

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.

AvalPlus.thy

#### Gergely Buday (Jan 26 2021 at 12:52):

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?

#### Jakub Kądziołka (Jan 26 2021 at 14:48):

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.

#### Jakub Kądziołka (Jan 26 2021 at 14:50):

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

#### Jakub Kądziołka (Jan 26 2021 at 14:51):

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]: "..."`

#### Jakub Kądziołka (Jan 26 2021 at 14:52):

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

#### Jakub Kądziołka (Jan 26 2021 at 14:54):

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

#### Jakub Kądziołka (Jan 26 2021 at 14:55):

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)

#### Jakub Kądziołka (Jan 26 2021 at 14:56):

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

Last updated: Dec 07 2023 at 20:16 UTC