Zulip Chat Archive

Stream: new members

Topic: contraposition

Henning Dieterichs (Nov 13 2020 at 18:17):

Sorry for this stupid question. My goal is to show A -> B. I would like to rewrite this goal to \neg B -> \neg A. How do I do that? I know I could prove (A -> B) -> (\neg B -> \neg A) and use rewrite, but I was hoping for something built in

Kevin Buzzard (Nov 13 2020 at 18:18):

This result will be in the library -- is it called something like neg_imp_neg or something?

Henning Dieterichs (Nov 13 2020 at 18:18):

What is the best way to search the library?

Kevin Buzzard (Nov 13 2020 at 18:19):

import tactic

example (A B : Prop) : (¬ B → ¬ A) ↔ (A → B) := by library_search

Kevin Buzzard (Nov 13 2020 at 18:19):

not_imp_not

Kevin Buzzard (Nov 13 2020 at 18:20):

That's one way. Another way is to guess what the result is called using #naming and start to type your guess and see what VS Code predicts. import tactic imports a bunch of stuff, making library_search more likely to succeed.

Kevin Buzzard (Nov 13 2020 at 18:21):

As you can see, you tripped me up by calling it neg, but #naming tells us it's called not

Henning Dieterichs (Nov 13 2020 at 18:23):

Thanks, I didn't know about these naming guidelines or library_search ;) not_imp_not works as expected

Kevin Buzzard (Nov 13 2020 at 18:23):

Yeah, there are a lot of secrets :-) Useful tactics get written much faster than useful documentation of the tactics. https://leanprover-community.github.io/mathlib_docs/tactics.html

Henning Dieterichs (Nov 13 2020 at 18:24):

Can I somehow list all tactics that are applicable at the current position?

Henning Dieterichs (Nov 13 2020 at 18:25):

Or all lemmas l so that rw l succeeds?

Bryan Gin-ge Chen (Nov 13 2020 at 18:25):

tactic#hint for the former, rw_hint is supposed to do the latter, but the PR #2030 was closed without being merged.

Bryan Gin-ge Chen (Nov 13 2020 at 18:26):

hint won't give anything like a complete list

Bryan Gin-ge Chen (Nov 13 2020 at 18:26):

but maybe it's still useful

Henning Dieterichs (Nov 13 2020 at 18:27):

wow, hint is useful, thanks

Kevin Buzzard (Nov 13 2020 at 18:27):

PS "stupid" questions are welcome in #new members , you're doing exactly the right thing

Patrick Massot (Nov 13 2020 at 19:34):

@Henning Dieterichs see also the contrapose tactic.

Henning Dieterichs (Nov 13 2020 at 19:36):

thanks! I tried contrapose/contraposition before, but I couldn't find it in the standard documentation. I didn't import tactic though, but now, after I did, it works

Last updated: Dec 20 2023 at 11:08 UTC