simp attribute

Stream: new members

[Damiano Testa]

Dear All,

this question is mostly for my own education about simp.

With my very limited understanding of how simp works, I would have thought that the lemma below would not fire with simp, due to the hypothesis h.

@[simp]
lemma to_nat_pred_coe_of_pos {i : ℤ} (h : 0 < i) : ((i.to_nat - 1 : ℕ) : ℤ) = i - 1 :=

I tried proving this lemma using by simp [h] and I could not get it to work.
Proving this lemma using by simp [h] works, but by simp does not.

However, the simp attribute is in data.int.basic.

What is the simp attribute doing in this case?

Thanks!

[Johan Commelin]

It means that simp will try to use the lemma to_nat_pred_coe_of_pos. But it can only use if after it knows how to prove h. So you either pass it h directly, like you did. Or you hope that other simp lemmas can provide a proof of h, recursively. The latter will be unlikely for a generic 0 < i proof. But if i = 1, then it will probably work.

[Damiano Testa]

Ah, thanks for the explanation! I had not realized about the specific number case!