# Zulip Chat Archive

## Stream: new members

### Topic: if_neg

#### Damiano Testa (Oct 23 2020 at 13:13):

Dear All,

in the example below (and fairly often when I use `if_neg`

and sometimes with `if_pos`

), I would like the two term mode proofs to be `if_pos rfl`

and `if_neg h`

.

The first one is almost there, `show_term`

says `exact if_pos rfl`

, but then Lean complains.

The second one is even more frustrating. `show_term`

again believes `exact if_neg h`

, but Lean complains.

My vague understanding of the errors from Lean is that this has to do with some decidability. However, how can I overcome this?

Thank you!

```
import data.polynomial.basic
open polynomial finsupp
variables {R : Type*} [semiring R] {f : polynomial R}
@[simp] lemma coeff_single_same (n : ℕ) (r : R) : coeff (single n r) n = r :=
by apply if_pos rfl -- show_term: exact if_pos rfl
@[simp] lemma coeff_single_ne (a n : ℕ) (r : R) (h : a ≠ n) : coeff (single a r) n = 0 :=
begin
apply if_neg,
exact h, -- show_term: exact if_neg h
end
```

#### Eric Wieser (Oct 23 2020 at 13:19):

I think the difficulty is that some places in `finsupp`

/ `polynomial`

use classical `decidable`

instances, while other places use non-classical ones. I think it might be possible to change them all to explicit typeclass arguments, and leave `classical`

for the point of use?

#### Mario Carneiro (Oct 23 2020 at 13:20):

```
@[simp] lemma coeff_single_same (n : ℕ) (r : R) : coeff (single n r) n = r :=
@if_pos _ (id _) rfl _ _ _
@[simp] lemma coeff_single_ne (a n : ℕ) (r : R) (h : a ≠ n) : coeff (single a r) n = 0 :=
@if_neg _ (id _) h _ _ _
```

#### Mario Carneiro (Oct 23 2020 at 13:20):

@Eric Wieser No, we used to do this and the typeclass arguments caused everyone a lot of problems

#### Mario Carneiro (Oct 23 2020 at 13:22):

The correct answer is to use the lemmas that were given in the API instead of unfolding way too far

```
@[simp] lemma coeff_single_same (n : ℕ) (r : R) : coeff (single n r) n = r :=
single_eq_same
@[simp] lemma coeff_single_ne (a n : ℕ) (r : R) (h : a ≠ n) : coeff (single a r) n = 0 :=
single_eq_of_ne h
```

#### Mario Carneiro (Oct 23 2020 at 13:23):

Actually this theorem is already a bit problematic because `single`

is not a polynomial

#### Mario Carneiro (Oct 23 2020 at 13:24):

you should be using `monomial`

instead

#### Damiano Testa (Oct 23 2020 at 13:25):

@Mario Carneiro Thank you very much for the solution! To be honest, I am not sure whether I prefer to see so many underscores of the short tactic mode proofs. In any case, I am very happy and grateful!

Also, thank you for pointing me to the exact lemmas! Whenever I find the appropriate lemmas, I use them, but I had not found them in this case. I will also convert to `monomial`

!

#### Mario Carneiro (Oct 23 2020 at 13:25):

If you look at the proof of `single_eq_same`

you will note that underscores were not necessary

#### Damiano Testa (Oct 23 2020 at 13:25):

(for the record, even with `monomial`

, Lean complains)

#### Mario Carneiro (Oct 23 2020 at 13:26):

yes because you shouldn't use `if_pos`

#### Mario Carneiro (Oct 23 2020 at 13:27):

it might be good for

```
lemma coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 :=
```

to have an explicit decidable instance, so that if you rewrite with it you don't end up with the wrong instance

#### Damiano Testa (Oct 23 2020 at 13:27):

I am not sure whether now I am more or less confused: I used `single`

and it did not work, but in `single_eq_same`

it does?

#### Mario Carneiro (Oct 23 2020 at 13:28):

The reason is that your theorem is about `nat ->0 R`

while the one in finsupp is about `A ->0 B`

#### Mario Carneiro (Oct 23 2020 at 13:29):

the typeclass instance that is inferred for `nat`

is not the generic one

#### Mario Carneiro (Oct 23 2020 at 13:29):

generally, inside the same file that defines these things you will not have such problems because the context is the same so you get the same instances

#### Mario Carneiro (Oct 23 2020 at 13:30):

which is one more reason to make and use an API

#### Damiano Testa (Oct 23 2020 at 13:30):

Ok, this is starting to clear up some doubts that I have and was unable to express!

#### Mario Carneiro (Oct 23 2020 at 13:31):

In this case, I would just do

```
@[simp] lemma coeff_monomial_same (n : ℕ) (r : R) : coeff (monomial n r) n = r :=
by simp [coeff_monomial]
@[simp] lemma coeff_monomial_ne (a n : ℕ) (r : R) (h : a ≠ n) : coeff (monomial a r) n = 0 :=
by simp [coeff_monomial, h]
```

#### Mario Carneiro (Oct 23 2020 at 13:31):

or if you prefer

```
@[simp] lemma coeff_monomial_same (n : ℕ) (r : R) : coeff (monomial n r) n = r :=
by rw coeff_monomial; exact if_pos rfl
@[simp] lemma coeff_monomial_ne (a n : ℕ) (r : R) (h : a ≠ n) : coeff (monomial a r) n = 0 :=
by rw coeff_monomial; exact if_neg h
```

#### Mario Carneiro (Oct 23 2020 at 13:32):

because this doesn't involve unfolding past an API barrier

#### Damiano Testa (Oct 23 2020 at 13:32):

Maybe one more (vague and with a very long `mwe`

): sometimes, I am left to prove that two expressions that look the same, coincide and `refl`

does not work. If I ask Lean to tell me more, I realize that one has several extra layers of `eq.rec`

composed with one another. Likely, this is again a consequence of my extra unfolding: is there an "after the fact solution" for this?

#### Mario Carneiro (Oct 23 2020 at 13:33):

extra layers of eq.rec aren't necessarily a problem

#### Mario Carneiro (Oct 23 2020 at 13:33):

you have to see past that to find the actual place where they aren't defeq

#### Mario Carneiro (Oct 23 2020 at 13:34):

the `convert`

tactic sometimes helps

#### Damiano Testa (Oct 23 2020 at 13:35):

Ok, should I run into some other similar instance, I may ask a question here.

Thank you very much for your help: I always come out of these Q&A with a much better understanding!

#### Kevin Buzzard (Oct 23 2020 at 14:13):

Usually when I'm faced with a non-reflable `X = X`

goal I try `congr'`

. This zooms straight to the problematic part of the equality. If it's some typeclass issue then this might indicate I did something wrong earlier. But `congr'`

is ideal for this.

#### Damiano Testa (Oct 23 2020 at 14:22):

Kevin Buzzard said:

Usually when I'm faced with a non-reflable

`X = X`

goal I try`congr'`

. This zooms straight to the problematic part of the equality. If it's some typeclass issue then this might indicate I did something wrong earlier. But`congr'`

is ideal for this.

I will try `congr'`

, thanks for the suggestion, Kevin!

Last updated: Dec 20 2023 at 11:08 UTC