# Zulip Chat Archive

## 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 ~~`\not`

s. 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