Zulip Chat Archive

Stream: general

Topic: contrapositive


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

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:01):

What if you assume Q is decidable and try again?

view this post on Zulip Johan Commelin (Oct 03 2019 at 20:02):

by contrapose!, ...?

view this post on Zulip Kevin Buzzard (Oct 03 2019 at 20:03):

I'm assuming everything's decidable!

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

view this post on Zulip Kevin Buzzard (Oct 03 2019 at 20:05):

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

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:07):

by tauto!

view this post on Zulip Johan Commelin (Oct 03 2019 at 20:08):

It is a tautology after all :grinning_face_with_smiling_eyes:

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:08):

And contrapose!, library_search works too

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:08):

Even by tauto works

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:09):

and apply not_imp_not works too

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:10):

Looks like almost any random sequence of characters works then.

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:10):

That sounds like the right conclusion to draw

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

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:12):

Oh, have you tried apply'?

view this post on Zulip Rob Lewis (Oct 03 2019 at 20:12):

apply' leaves you with a mess.

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

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:13):

simp [not_imp_not] works

view this post on Zulip Reid Barton (Oct 03 2019 at 20:14):

Why are you all still writing random sequences of characters

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:14):

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

view this post on Zulip Rob Lewis (Oct 03 2019 at 20:14):

Heh. cc works.

view this post on Zulip Reid Barton (Oct 03 2019 at 20:14):

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

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:14):

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

view this post on Zulip Rob Lewis (Oct 03 2019 at 20:15):

I think the problem is with apply, not library_search.

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:15):

by finish

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:15):

by clarify

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:15):

by safe

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

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:16):

Did I win?

view this post on Zulip Rob Lewis (Oct 03 2019 at 20:16):

by cc is the shortest!

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:17):

Can we write a shorter proof still?

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

view this post on Zulip Rob Lewis (Oct 03 2019 at 20:18):

Nah, the auxiliary def counts.

view this post on Zulip Simon Hudon (Oct 03 2019 at 20:18):

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

view this post on Zulip Patrick Massot (Oct 03 2019 at 20:18):

Let me open some PR.

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

view this post on Zulip Johan Commelin (Oct 03 2019 at 20:20):

I think that library_search doesn't break iffs into implications

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

view this post on Zulip Reid Barton (Oct 03 2019 at 20:21):

It doesn't use apply'

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

view this post on Zulip Reid Barton (Oct 03 2019 at 20:23):

There was a time when it didn't, though

view this post on Zulip Johan Commelin (Oct 03 2019 at 20:24):

It tries iffs in the reverse direction

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

view this post on Zulip Johan Commelin (Oct 03 2019 at 20:25):

Ok, I give up

view this post on Zulip Mario Carneiro (Oct 03 2019 at 21:02):

the problem is the decidable instances probably

view this post on Zulip Mario Carneiro (Oct 03 2019 at 21:02):

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

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

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

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

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