Zulip Chat Archive

Stream: new members

Topic: contrapose


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

view this post on Zulip Johan Commelin (Sep 07 2020 at 08:15):

not_mem_support_iff

view this post on Zulip Johan Commelin (Sep 07 2020 at 08:15):

And unfold coeff

view this post on Zulip Damiano Testa (Sep 07 2020 at 08:15):

Thank! I will try it!

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

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

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

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

view this post on Zulip Shing Tak Lam (Sep 07 2020 at 08:17):

docs#not_congr I think

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 07 2020 at 10:09):

I very much agree

view this post on Zulip Johan Commelin (Sep 07 2020 at 10:10):

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

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

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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 10:23):

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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 10:24):

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

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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 10:28):

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:34):

Actually there was also a funny third kind

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 11:36):

I added the result to the option API

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

view this post on Zulip Reid Barton (Sep 07 2020 at 11:58):

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

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

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

view this post on Zulip Mario Carneiro (Sep 07 2020 at 12:20):

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

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

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

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

view this post on Zulip Kevin Buzzard (Sep 07 2020 at 18:04):

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

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