## Stream: new members

### Topic: How do you replace a goal by its contrapositive?

#### Quantum Horizon (Oct 30 2019 at 15:02):

For eg: Your goal is to show a=b => c=d. How do you replace this goal to c!=d => a!=b?
Thank You!

#### Kevin Buzzard (Oct 30 2019 at 15:07):

import tactic.library_search

example (P Q : Prop) [decidable P] [decidable Q]: (¬ Q → ¬ P) → (P → Q) := by library_search -- fails
example (P Q : Prop) [decidable P] [decidable Q]: (¬ Q → ¬ P) ↔ (P → Q) := by library_search -- not_imp_not


@Scott Morrison I am learning to tame library_search slowly but surely.

#### Bryan Gin-ge Chen (Oct 30 2019 at 15:07):

You can also try the contrapose tactic in mathlib.

#### Kevin Buzzard (Oct 30 2019 at 15:08):

Does this tactic only do the other way to the OP though?

#### Kevin Buzzard (Oct 30 2019 at 15:08):

Oh no it's exactly the right way

#### Kevin Buzzard (Oct 30 2019 at 15:12):

import tactic.push_neg

example (X : Type) (a b c d : X) (h : c ≠ d → a ≠ b) : a = b → c = d :=
begin
classical,
contrapose!,
assumption,
end


#### Quantum Horizon (Oct 30 2019 at 15:20):

You can also try the contrapose tactic in mathlib.

Thank you for your reply. I am afraid, I am not having success using it. I have tried 'contrapose,' 'rw contrapose' and 'apply contrapose'.
I am trying to solve level 13, World 2 on the number theory game: http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

#### Kevin Buzzard (Oct 30 2019 at 15:39):

Those levels are not properly documented. Some of the lemmas are stated in an inconvenient manner, and I have not properly explained the key point that computer scientists think that $\implies$ is a function and they think that ≠  is a function as well.

#### Kevin Buzzard (Oct 30 2019 at 15:39):

I am in the process of working on proper documentation right now. I would be interested to know if you had had any difficulty with levels 3-1 to 3-8 and 4-1 to 4-7.

#### Giovanni Mascellani (Oct 30 2019 at 15:48):

I am in the process of working on proper documentation right now. I would be interested to know if you had had any difficulty with levels 3-1 to 3-8 and 4-1 to 4-7.

I just finished the game and found it mostly easy (but I already have a little experience with formal provers). In particular, the commutativity theorems, which are referred as "bosses", are not more difficult than the other levels, in my opinion. The only level that took me a bit more of time was 3.12: my main mistake was to try to do induction on a, while it is more appropriate to do it on b and c (the fact that you need two inductions is itself an element of difficulty).

Other than that, for a few levels I used tactics that had not been introduced already. For example, I don't think the instruction ever say how to destruct inequality (I don't remember the level number). I could carry on only because I already suspected that inequality is "equality implies false". In the same and possibly other levels you also need to that you can use exfalso or directly destruct false.

#### Kevin Buzzard (Oct 30 2019 at 15:59):

Documenting destructing inequality is what I will be working on within an hour. I had not realised until today that you can solve all of world 4 including all prerequisites without ever using the intro tactic. Everyone is complaining that this is what they don't know how to do and I'm trying to fix it ASAP.

#### Quantum Horizon (Oct 30 2019 at 16:14):

Those levels are not properly documented. Some of the lemmas are stated in an inconvenient manner, and I have not properly explained the key point that computer scientists think that $\implies$ is a function and they think that ≠  is a function as well.

Just did world 3, level 1-8. It was quite easy apart from Level 7 which was more challenging than others and was not required to do level 8. I will let you know, how I do with world 4.

#### Quantum Horizon (Oct 30 2019 at 16:18):

I am in the process of working on proper documentation right now. I would be interested to know if you had had any difficulty with levels 3-1 to 3-8 and 4-1 to 4-7.

There is a problem with level 9, world 3. It says a!=0 implies b!=0 implies ab!=0. It should be a!=0 'and' b!=0.

#### Anne Baanen (Oct 30 2019 at 16:26):

It says a!=0 implies b!=0 implies ab!=0. It should be a!=0 'and' b!=0.

Note that a ≠ 0 → b ≠ 0 → a * b ≠ 0 should be read as a ≠ 0 → (b ≠ 0 → a * b ≠ 0) and x → (y → z)) is equivalent to ((x ∧ y) → z). So there are two assumptions to the theorem, and you can apply intro twice to get at them.

#### Anne Baanen (Oct 30 2019 at 16:27):

Computer scientists think that the form with two implications is the correct way to state theorems with two assumptions, and I'm inclined to agree with them :)

#### Anne Baanen (Oct 30 2019 at 16:36):

AFAICT, it's the first level with two assumptions, so I would suggest to explain what's going on there

#### Kevin Buzzard (Oct 30 2019 at 17:32):

There is a problem with level 9, world 3. It says a!=0 implies b!=0 implies ab!=0. It should be a!=0 'and' b!=0.

Mathematicians do not know Curry-Howard! This is exactly the point! It's so interesting! It's really easy to train them all to use rw and induction but their way of thinking about implicitions is so different to Lean's that it can be really confusing. The first tactic taught in TPIL is apply.

#### Chris B (Nov 06 2019 at 12:00):

@Kevin Buzzard You may be way ahead of me, but having an example that focuses on doing something fun with or exploits currying/partial application might be helpful for readers.

#### Kevin Buzzard (Nov 06 2019 at 12:20):

I am writing some levels now which might be very appropriate for this sort of thing. Thanks!

Last updated: May 14 2021 at 23:14 UTC