How do you replace a goal by its contrapositive?

Stream: new members

[Quantum Horizon]

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]

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]

You can also try the contrapose tactic in mathlib.

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh no it's exactly the right way

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

@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]

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