Stream: General

Topic: ✔ Broken fact computation in connection with Eisbach

Wolfgang Jeltsch (Nov 08 2021 at 01:55):

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 simp.

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.

Kevin Kappelmann (Nov 11 2021 at 11:12):

Since nobody seems to know an answer here: I think this is something technical that someone on the mailing list could answer.

Wolfgang Jeltsch (Nov 21 2021 at 16:29):

I’ll report this as a bug to the developers.

Notification Bot (Nov 21 2021 at 16:30):

Wolfgang Jeltsch has marked this topic as resolved.

Last updated: Dec 21 2024 at 12:33 UTC