## 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: May 06 2021 at 22:13 UTC