Stream: new members

Topic: contrapose

Damiano Testa (Sep 07 2020 at 08:14):

Dear All,

I want to go from an A ↔ B to ¬A ↔ ¬B. I know that I can prove the equivalence of these two by tauto, but it seems a little silly. Is there a "contrapositive iff" automatically generated by Lean? Is there a better way? Below is the actual statement that I was trying to prove. Note that this is part of a larger proof: I would rather not include this step in my argument!

Thanks!

lemma zero_coeff_iff {R : Type*} [semiring R] {f : polynomial R} {a : ℕ} : f.coeff a = 0 ↔ a ∉ f.support :=
begin
split,
{ contrapose,
push_neg,
exact (f.3 a).mp, },
{ contrapose,
push_neg,
exact (f.3 a).mpr, },
end


Johan Commelin (Sep 07 2020 at 08:15):

not_mem_support_iff

Johan Commelin (Sep 07 2020 at 08:15):

And unfold coeff

Damiano Testa (Sep 07 2020 at 08:15):

Thank! I will try it!

Johan Commelin (Sep 07 2020 at 08:15):

I agree that this lemma should be added to mathlib, because you shouldn't need to unfold coeff

Johan Commelin (Sep 07 2020 at 08:16):

Concerning your actual question, I think there is something like not_iff_not and not_iff_not_of_iff

Damiano Testa (Sep 07 2020 at 08:17):

But, as a general rule, proving an iff does not automatically also prove the iff between the \nots. right?

Damiano Testa (Sep 07 2020 at 08:17):

Johan Commelin said:

Concerning your actual question, I think there is something like not_iff_not and not_iff_not_of_iff

Ah, ok!!

Shing Tak Lam (Sep 07 2020 at 08:17):

docs#not_congr I think

Damiano Testa (Sep 07 2020 at 08:23):

Johan Commelin said:

I agree that this lemma should be added to mathlib, because you shouldn't need to unfold coeff

I think so too: when Lean "interprets" f.coeff n, it often writes it as ⇑f n and unfold coeff does not work...

Mario Carneiro (Sep 07 2020 at 09:11):

Johan Commelin said:

I agree that this lemma should be added to mathlib, because you shouldn't need to unfold coeff

Every logic lemma under the sun is already there, but no one wants to refer to them by name

Mario Carneiro (Sep 07 2020 at 09:14):

lemma zero_coeff_iff {R : Type*} [semiring R] {f : polynomial R} {a : ℕ} : f.coeff a = 0 ↔ a ∉ f.support :=
iff_not_comm.1 (f.3 _)


Johan Commelin (Sep 07 2020 at 09:21):

But (f.not_mem_support_iff _).symm should hopefully also work, and be a slightly more readable proof...

Scott Morrison (Sep 07 2020 at 10:08):

:-( I did a bunch of work earlier trying to stamp out the coercion to a function for polynomials, but the problem is everytime you forget that it is a polynomial and treat it as a finsupp the coercion starts to sneak in again.

Scott Morrison (Sep 07 2020 at 10:09):

My attitude if that if you ever see ⇑f, and f : polynomial R, then you have encountered a bug, for which the correct fix is make the definition of polynomial irreducible as early as possible (if not earlier).

Johan Commelin (Sep 07 2020 at 10:09):

I very much agree

Johan Commelin (Sep 07 2020 at 10:10):

(Although I admit to having written a lot of evil code)

Scott Morrison (Sep 07 2020 at 10:10):

we did a bunch of cleanup of the polynomials files a few months ago, but I guess there's still a ways to go

Anne Baanen (Sep 07 2020 at 10:11):

Thinking out loud: would it be possible/useful to write a linter that checks for coe_fn being applied to a term of type polynomial _? It won't catch any occurrence in the goal, but it should catch some evil usages.

Mario Carneiro (Sep 07 2020 at 10:23):

One thing that is interesting here is that f.3 itself is abstraction-breaking

Mario Carneiro (Sep 07 2020 at 10:24):

even if you write that after it is made irreducible, lean will make it work

Mario Carneiro (Sep 07 2020 at 10:27):

Oh wait, lean is doing the right thing here. If you write f.3, it resolves to finsupp.mem_support_to_fun f, which will fail to typecheck if polynomial is irreducible.

Mario Carneiro (Sep 07 2020 at 10:28):

So the question is, why isn't attribute [irreducible] polynomial at the bottom of data.polynomial?

Mario Carneiro (Sep 07 2020 at 10:30):

Of course the statement of this theorem itself doesn't typecheck, since f.support is referring to finsupp.support f. If we need this then it should be redeclared as polynomial.support

Kevin Buzzard (Sep 07 2020 at 11:32):

I made has_zero irreducible, added very little API, and if people really want it reducible so they can abuse defeq for some reason then they can just locally tag it as reducible

Kevin Buzzard (Sep 07 2020 at 11:34):

I did this when I was making has_zero irreducible: some proofs broke, but surprisingly few. The proofs which broke were of two kinds: those which broke because of missing API, and those that broke because they abuse the API; in those cases I fixed the proofs by removing the option lemma and replacing it with the corresponding has_zero lemma

Kevin Buzzard (Sep 07 2020 at 11:34):

Actually there was also a funny third kind

Kevin Buzzard (Sep 07 2020 at 11:35):

There were two theorems about option for which some stupid trivial lemma was missing from the option API and so the proof used the corresponding result from has_zero :-)

Kevin Buzzard (Sep 07 2020 at 11:36):

I added the result to the option API

Mario Carneiro (Sep 07 2020 at 11:42):

You made has_zero irreducible? That would break quite a lot. I assume you mean with_zero

Reid Barton (Sep 07 2020 at 11:58):

Rather than making polynomial irreducible, why not just make it a structure?

Scott Morrison (Sep 07 2020 at 12:14):

One argument against that (making it a structure) is that it commits you a single big refactor. You can make gradual progress by making polynomial irreducible, fixing the API a bit in response to a subset of the errors, then removing the irreducible again. But yeah.

Mario Carneiro (Sep 07 2020 at 12:20):

I was going to propose that, but then I looked up the definition and it's equal to add_monoid_algebra and I'm not sure where to assert the structure

Mario Carneiro (Sep 07 2020 at 12:20):

should add_monoid_algebra be a structure with a G-indexed coeff field?

Reid Barton (Sep 07 2020 at 13:04):

oh yeah, that does make things a bit more complicated. I think at least add_monoid_algebra should be a structure, because finsupp is not the only sensible representation (constructively it's perhaps not even the correct representation). Not sure whether polynomial should also be a structure.

Reid Barton (Sep 07 2020 at 13:09):

Scott Morrison said:

One argument against that (making it a structure) is that it commits you a single big refactor.

Right--so the broader lesson is that we should be more eager to use structure in the first place

Kevin Buzzard (Sep 07 2020 at 18:04):

Do you think it would have been a good idea to define with_zero as an inductive type instead of making it an alias for option?

Kevin Buzzard (Sep 07 2020 at 18:04):

This would enforce good behaviour but now you'd have to prove some things twice

Kevin Buzzard (Sep 07 2020 at 18:05):

Although can this be automated because of the non-refl equiv between option and with_zero?

Last updated: May 11 2021 at 12:15 UTC