Zulip Chat Archive

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.

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?


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