contrapose

Stream: new members

[Damiano Testa]

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]

not_mem_support_iff

[Johan Commelin]

And unfold coeff

[Damiano Testa]

Thank! I will try it!

[Johan Commelin]

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

[Johan Commelin]

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

[Damiano Testa]

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

[Damiano Testa]

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]

docs#not_congr I think

[Damiano Testa]

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]

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]

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]

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

[Scott Morrison]

:-( 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]

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]

I very much agree

[Johan Commelin]

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

[Scott Morrison]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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]

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]

Actually there was also a funny third kind

[Kevin Buzzard]

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]

I added the result to the option API

[Mario Carneiro]

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

[Reid Barton]

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

[Scott Morrison]

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]

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]

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

[Reid Barton]

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]

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]

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]

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

[Kevin Buzzard]

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