Zulip Chat Archive

Stream: new members

Topic: if_neg


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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 _ _ _

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:23):

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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:24):

you should be using monomial instead

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Damiano Testa (Oct 23 2020 at 13:25):

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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:26):

yes because you shouldn't use if_pos

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:29):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:30):

which is one more reason to make and use an API

view this post on Zulip 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!

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:32):

because this doesn't involve unfolding past an API barrier

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:33):

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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:33):

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

view this post on Zulip Mario Carneiro (Oct 23 2020 at 13:34):

the convert tactic sometimes helps

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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