Consider the following contrived example of a lemma:
lemma assumes "Suc n < Suc m" shows "n < m" by (simp only: Suc_less_SucD [OF assms])
The proof is accepted, which is to be expected, as the fact
Suc_less_SucD [OF assms] is precisely what is to be proved.
Now let’s make this a bit more complicated, using some Eisbach:
lemma assumes "Suc n < Suc m" shows "n < m" by (match assms in assumption: _ ⇒ ‹simp only: Suc_less_SucD [OF assumption]›)
The proof in this example fails. When debugging with
simp_trace, I can see that the rewrite rule added to the simplifier is not
n < m ≡ True but
Suc n < Suc m ≡ True. Apparently, the computation of the fact
Suc_less_SucD [OF assumption] goes completely wrong, and
assumption itself is returned as the result.
If I replace
simp only: Suc_less_SucD [OF assumption] by
insert Suc_less_SucD [OF assumption], the proof is accepted again. So it seems the above-mentioned behavior has to do with particularities of
Is this behavior due to a bug? It quite looks to me as if it is, but I can actually not even image what kind of bug should cause picking a fact behind
OF as the result of a fact computation and furthermore doing so only in certain situations.
Since nobody seems to know an answer here: I think this is something technical that someone on the mailing list could answer.
I’ll report this as a bug to the developers.
Wolfgang Jeltsch has marked this topic as resolved.
Last updated: Dec 07 2023 at 08:19 UTC