英文:
Isabelle: [simp] leading to an infinite loop
问题
I am trying to solve the simple lemma "add m (Suc n) = add n (Suc m)" by induction over m.
I tried solving the last remaining subgoal after applying auto by another lemma, howerver if i use the simplification rule on that auxiliary lemma it leads to an infinite loop at apply(auto) in the original lemma.
Do you know why that happens? And if my way doesn't work, how would i solve the original lemma?
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)";
lemma aux:"Suc n = add n (Suc 0)"
apply(induction n)
apply(auto)
done;
lemma original:"add m (Suc n) = add n (Suc m)"
apply(induction m arbitrary: n)
apply(auto)
oops;
These are the lemmas in question, i also proved commutatvity of add in a seperate lemma.
The subgoal of "original" after apply(auto) is
- ⋀n. Suc n = add n (Suc 0)
When adding [simp] to the lemma aux, the apply(auto) in the lemma original gets into an infinite loop.
Sorry if this is trivial, i am just getting into Isabelle.
英文:
I am trying to solve the simple lemma "add m (Suc n) = add n (Suc m)" by induction over m.
I tried solving the last remaining subgoal after applying auto by another lemma, howerver if i use the simplification rule on that auxiliary lemma it leads to an infinite loop at apply(auto) in the original lemma.
Do you know why that happens? And if my way doesn't work, how would i solve the original lemma?
fun add :: "nat ⇒ nat ⇒ nat" where
"add 0 n = n" |
"add (Suc m) n = Suc(add m n)"
lemma aux:"Suc n = add n (Suc 0)"
apply(induction n)
apply(auto)
done
lemma original:"add m (Suc n) = add n (Suc m)"
apply(induction m arbitrary: n)
apply(auto)
oops
These are the lemmas in question, i also proved commutatvity of add in a seperate lemma.
The subgoal of "original" after apply(auto) is
- ⋀n. Suc n = add n (Suc 0)
When adding [simp] to the lemma aux, the apply(auto) in the lemma original gets into an infinite loop.
Sorry if this is trivial, i am just getting into Isabelle.
答案1
得分: 1
设计良好的 simp 规则本身就是一门艺术。在你的情况下，aux 的方向完全相反。左边有 Suc n，右边有 Suc n 匹配的内容，即 Suc 0。这本身会导致无限循环。
如果你颠倒 aux 的两边，它就可以正常工作。
一般规则是，在 simp 规则中，右边的内容应比左边的内容“简单”。在这种情况下很清楚，但还有其他情况更复杂，例如，如果你有类似 f (x + y) = f x + f y 的情况。
在这些情况下，典型的方法是全局决定你的目标是将 f 尽可能深入到项内部 或者 尽可能拉出来，然后相应地设计涉及 f 的所有 simp 规则。
英文:
Designing good simp rules is an art in and of itself. In your case, aux is exactly oriented the wrong way round. You have Suc n on the left-hand side and you have something that Suc n matches on on the right-hand side, namely Suc 0. So that alone gives you an infinite loop.
If you flip the two sides of aux it works fine.
A general rule is that in a simp rule, the right-hand side should be ‘simpler’ than the left-hand one. In this case it's very clear what that means, but there are other cases where it is trickier, e.g. if you have something like f (x + y) = f x + f y.
In those cases the typical approach is to either globally decide that your goal is to push f as far inside the term as possible or to pull it out as far as possible, and then design all simp rules involving f accordingly.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论