Gergely Buday (Jan 26 2021 at 10:42): 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:
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)) = t1theorem
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:
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:
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.
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: Apr 20 2024 at 12:26 UTC