Stream: Beginner Questions

Topic: Feeding knowledge about functions


view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Gergely Buday (Jan 26 2021 at 10:58):

Here is a minimal version of the file:

AvalPlus.thy

view this post on Zulip 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)

view this post on Zulip 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...

view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 11:16):

could you post what you actually want to prove?

view this post on Zulip 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)) = t1theorem

view this post on Zulip 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

view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 11:22):

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

view this post on Zulip Gergely Buday (Jan 26 2021 at 11:24):

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

AvalPlus.thy

view this post on Zulip 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:

view this post on Zulip Gergely Buday (Jan 26 2021 at 11:27):

Now with the final theorem and its definitions included:

AvalPlus.thy

view this post on Zulip 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.

view this post on Zulip 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 ...?"

view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 11:30):

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

view this post on Zulip Mathias Fleury (Jan 26 2021 at 11:30):

You should really add the lemma on aval plus.

view this post on Zulip Jakub Kądziołka (Jan 26 2021 at 11:30):

it would compose with aval_sepN wonderfully

view this post on Zulip 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!

view this post on Zulip Gergely Buday (Jan 26 2021 at 11:32):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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]: "..."

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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: Aug 13 2022 at 06:26 UTC