(¬ Q → ¬ P) → (P → Q)

Stream: general

[Kevin Buzzard]

gaargh I can't find

example (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := sorry

I understand it will be classical.something. I know mt (the other direction). I've looked in logic.basic but I couldn't find it (maybe I missed it). I want to find this with #find and not bother people here. But #find (¬ _ → ¬ _) → (_ → _) doesn't work for me. I want this to be easier. Help!

[petercommand]

how do you use #find? #find doesn't work for me at all..

[Mario Carneiro]

you have to import tactic.find

[Mario Carneiro]

of course this is going to be in logic.basic

[Mario Carneiro]

looks like it is not_imp_not

[Mario Carneiro]

it's a biconditional, which is why find didn't find it the way you stated it

[Mario Carneiro]

it's not classical.something because it has a decidability assumption

[Kevin Buzzard]

I didn't know whether to look in logic.basic or core. I've run into several issues like this recently. I am doing my undergraduate example sheets again, with an extra year of hindsight. Now I understand what "should be somewhere", so instead of proving things like this myself I try to find them. If I can guess the name then I'm in business, but my guesses failed me this time. Not knowing whether I should search for -> or <->, and not knowing where to look, doesn't help (I am slow at learning where things are because I can't pick stuff up as quickly as when I was younger -- I need machine assistance here ideally).

None of

#find (¬ _ → ¬ _) → (_ → _)
#find (¬ _ → ¬ _) ↔ (_ → _)
#find (_ → _) ↔ (¬ _ → ¬ _)

give me anything. Why does the middle one fail? I have logic.basic imported.

not_imp_not : ∀ {a b : Prop} [_inst_1 : decidable a], ¬a → ¬b ↔ b → a

What is the philosophy behind calling this not_imp_not?

I really did try before I asked. It was the decidable v classical which caught me out.