## Stream: new members

### Topic: simp attribute

#### Damiano Testa (Mar 02 2022 at 07:56):

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 (Mar 02 2022 at 08:04):

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 (Mar 02 2022 at 08:07):

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

Last updated: Dec 20 2023 at 11:08 UTC