Zulip Chat Archive

Stream: new members

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


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

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

view this post on Zulip Bryan Gin-ge Chen (Oct 30 2019 at 15:07):

You can also try the contrapose tactic in mathlib.

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 15:08):

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

view this post on Zulip Kevin Buzzard (Oct 30 2019 at 15:08):

Oh no it's exactly the right way

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

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

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

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

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

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

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

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

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

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

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

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

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

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