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.

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: Nov 11 2024 at 01:24 UTC