## Stream: general

### Topic: contrapositive

#### Kevin Buzzard (Oct 03 2019 at 20:00):

A student has asked me how to prove example (P Q : Prop) : (¬ Q → ¬ P) → (P → Q)  and library_search is failing me :-) What's this function called?

#### Simon Hudon (Oct 03 2019 at 20:01):

What if you assume Q is decidable and try again?

#### Johan Commelin (Oct 03 2019 at 20:02):

by contrapose!, ...?

#### Kevin Buzzard (Oct 03 2019 at 20:03):

I'm assuming everything's decidable!

#### Kevin Buzzard (Oct 03 2019 at 20:04):

example (P Q : Prop) [decidable P] [decidable Q] : (¬ Q → ¬ P) → (P → Q) :=
begin
library_search,


still fails!

#### Kevin Buzzard (Oct 03 2019 at 20:05):

 contrapose!, exact (and_comm _ _).1, works :-/

#### Patrick Massot (Oct 03 2019 at 20:07):

by tauto!

#### Johan Commelin (Oct 03 2019 at 20:08):

It is a tautology after all :grinning_face_with_smiling_eyes:

#### Patrick Massot (Oct 03 2019 at 20:08):

And contrapose!, library_search works too

#### Patrick Massot (Oct 03 2019 at 20:08):

Even by tauto works

#### Simon Hudon (Oct 03 2019 at 20:09):

and apply not_imp_not works too

#### Patrick Massot (Oct 03 2019 at 20:10):

Looks like almost any random sequence of characters works then.

#### Simon Hudon (Oct 03 2019 at 20:10):

That sounds like the right conclusion to draw

#### Rob Lewis (Oct 03 2019 at 20:11):

apply not_imp_not doesn't work, it's an iff, and I think you hit the apply bug if you use .1. exact not_imp_not.1 works.

#### Simon Hudon (Oct 03 2019 at 20:12):

Oh, have you tried apply'?

#### Rob Lewis (Oct 03 2019 at 20:12):

apply' leaves you with a mess.

#### Rob Lewis (Oct 03 2019 at 20:12):

4 goals
P Q : Prop,
_inst_1 : decidable P,
_inst_2 : decidable Q
⊢ ¬((¬Q → ¬P) → P → Q) → ¬?m_1

P Q : Prop,
_inst_1 : decidable P,
_inst_2 : decidable Q
⊢ ?m_1

P Q : Prop,
_inst_1 : decidable P,
_inst_2 : decidable Q
⊢ Prop

P Q : Prop,
_inst_1 : decidable P,
_inst_2 : decidable Q
⊢ decidable ((¬Q → ¬P) → P → Q)


#### Patrick Massot (Oct 03 2019 at 20:13):

simp [not_imp_not] works

#### Reid Barton (Oct 03 2019 at 20:14):

Why are you all still writing random sequences of characters

#### Patrick Massot (Oct 03 2019 at 20:14):

I sort of lost track of what we are trying to do.

#### Rob Lewis (Oct 03 2019 at 20:14):

Heh. cc works.

#### Reid Barton (Oct 03 2019 at 20:14):

Also, isn't library_search supposed to be able to apply iff lemmas?

#### Patrick Massot (Oct 03 2019 at 20:14):

Isn't it a contest about finding as many proofs are possible?

#### Rob Lewis (Oct 03 2019 at 20:15):

I think the problem is with apply, not library_search.

#### Patrick Massot (Oct 03 2019 at 20:15):

by finish

#### Patrick Massot (Oct 03 2019 at 20:15):

by clarify

#### Patrick Massot (Oct 03 2019 at 20:15):

by safe

#### Rob Lewis (Oct 03 2019 at 20:16):

tidy takes a long time and reduces the goal to proving Q, that's not so good.

Did I win?

#### Rob Lewis (Oct 03 2019 at 20:16):

by cc is the shortest!

#### Simon Hudon (Oct 03 2019 at 20:17):

Can we write a shorter proof still?

#### Patrick Massot (Oct 03 2019 at 20:17):

meta def i : tactic unit := [cc]

example (P Q : Prop) [decidable P] [decidable Q] : (¬ Q → ¬ P) → (P → Q) :=
by i


#### Rob Lewis (Oct 03 2019 at 20:18):

Nah, the auxiliary def counts.

#### Simon Hudon (Oct 03 2019 at 20:18):

Does that count as shorter? You have to write a definition first

#### Patrick Massot (Oct 03 2019 at 20:18):

Let me open some PR.

#### Kevin Buzzard (Oct 03 2019 at 20:18):

and apply not_imp_not works too

Chris is here and he swore blind that something with not_imp_not should work -- I don't know why it didn't show up. What I don't understand is why library_search doesn't help

#### Johan Commelin (Oct 03 2019 at 20:20):

I think that library_search doesn't break iffs into implications

#### Rob Lewis (Oct 03 2019 at 20:20):

library_search doesn't work because of the apply bug. I'm not sure if it uses apply' instead, but it doesn't matter, because apply' is broken here too.

#### Reid Barton (Oct 03 2019 at 20:21):

It doesn't use apply'

#### Rob Lewis (Oct 03 2019 at 20:23):

I think that library_search doesn't break iffs into implications

I think it does. The tactic is definitely doing something with iffs.

#### Reid Barton (Oct 03 2019 at 20:23):

There was a time when it didn't, though

#### Johan Commelin (Oct 03 2019 at 20:24):

It tries iffs in the reverse direction

#### Rob Lewis (Oct 03 2019 at 20:25):

constants A B : Prop
axiom ax : A ↔ B
example : A → B :=
by library_search
example : B → A :=
by library_search


both work.

Ok, I give up

#### Mario Carneiro (Oct 03 2019 at 21:02):

the problem is the decidable instances probably

#### Mario Carneiro (Oct 03 2019 at 21:02):

is classical.dec in the context / a local instance?

#### Kevin Buzzard (Oct 03 2019 at 21:34):

It was sometimes, and it wasn't sometimes. I think it wasn't when I made the props decidable. Before that I was just using the classical tactic before library_search and it still didn't work.

#### Scott Morrison (Oct 04 2019 at 02:21):

constants A B : Prop
axiom ax : A ↔ B
example : A → B :=
by library_search
example : B → A :=
by library_search


both work.

Currently example : B ↔ A := by library_search doesn't work, and I would like to fix this.

#### Chris B (Jan 12 2020 at 14:28):

@Scott Morrison
Not sure if this is related, but in mathlib rev c5d91, the following fails when I would have expected it to find not_not :

example (p : Prop) [decidable p] : (¬¬p) → p := by library_search

failed
state:
p : Prop,
_inst_1 : decidable p
|- ¬¬p → p


#### Chris B (Jan 12 2020 at 14:32):

Actually this also fails, but some how succeeds in finding MyAx if I change both to (¬¬p ↔ p).

axiom MyAx (p : Prop) [decidable p] : (¬¬p) → p

example (p : Prop) [decidable p] : (¬¬p) → p := by library_search
`

Last updated: May 14 2021 at 06:16 UTC