Zulip Chat Archive
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.
Patrick Massot (Oct 03 2019 at 20:16):
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_notworks 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_searchdoesn'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.
Johan Commelin (Oct 03 2019 at 20:25):
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_searchboth 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: Dec 20 2023 at 11:08 UTC