if_neg

Stream: new members

[Damiano Testa]

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]

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]

@[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]

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

[Mario Carneiro]

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]

Actually this theorem is already a bit problematic because single is not a polynomial

[Mario Carneiro]

you should be using monomial instead

[Damiano Testa]

@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]

If you look at the proof of single_eq_same you will note that underscores were not necessary

[Damiano Testa]

(for the record, even with monomial, Lean complains)

[Mario Carneiro]

yes because you shouldn't use if_pos

[Mario Carneiro]

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]

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]

The reason is that your theorem is about nat ->0 R while the one in finsupp is about A ->0 B

[Mario Carneiro]

the typeclass instance that is inferred for nat is not the generic one

[Mario Carneiro]

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]

which is one more reason to make and use an API

[Damiano Testa]

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

[Mario Carneiro]

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]

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]

because this doesn't involve unfolding past an API barrier

[Damiano Testa]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

the convert tactic sometimes helps

[Damiano Testa]

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]

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]

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!