## Stream: general

### Topic: option golf puzzle

#### Kevin Buzzard (Nov 22 2019 at 09:06):

I ran into this in the middle of a tactic mode proof and it took me an annoying number of lines:

import data.set.basic

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
intro h1,
apply hS,
ext x,
cases x, simpa using h,
show x ∈ (coe ⁻¹' S : set α) ↔ _,
rw h1,
refl
end


Can I use some automation here? (or any other way of reducing the line-count) [hmm: set.ne_empty_iff_exists_mem looks helpful. ] [update: I'm about to do this myself now]

#### Kevin Buzzard (Nov 22 2019 at 09:18):

import data.set.basic

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
rcases (set.exists_mem_of_ne_empty hS) with ⟨⟨⟩|a, ha⟩, contradiction,
rw set.ne_empty_iff_exists_mem,
exact ⟨a, ha⟩,
end


This is probably preferable. I was barking up the wrong tree thinking about automation perhaps (unless there's some one line automation proof)

#### Patrick Massot (Nov 22 2019 at 09:56):

example (α : Type) (S : set (option α)) (hS : S ≠ ∅) (h : none ∉ S) :
(coe ⁻¹' S : set α) ≠ ∅ :=
begin
rw set.ne_empty_iff_exists_mem at *,
rcases hS with ⟨_| _, _⟩ ; tauto
end


#### Kevin Buzzard (Nov 22 2019 at 13:02):

Thanks for this Patrick. I am doing some abstract nonsense with lattices and I suspect I am underusing tauto.

#### Kevin Buzzard (Nov 22 2019 at 13:03):

Hmm...I am suddenly not sure if I'm allowed to import tauto in order/complete_lattice.lean...

#### Patrick Massot (Nov 22 2019 at 16:41):

In any case, we don't want to read the proof of that lemma, so you could as well use an unreadable proof term (preferably hand-crafted rather that copy-pasted from tauto).

#### Mario Carneiro (Nov 22 2019 at 17:20):

I like kevin's second proof best. Short and no advanced dependencies

#### Patrick Massot (Nov 22 2019 at 22:53):

My message was in the context of Kevin's question: "can we automate this?". I still think a proof term is probably the most relevant proof here.

#### Kevin Buzzard (Nov 22 2019 at 23:43):

You're probably right for this example but in the PR I'm in tactic mode because I've just done split_ifs and it's somehow hard to exit -- or at least I feel it is. I'm always happy to hear about ways I can improve my code-writing, for me the goal has always been to prove the theorem and who cares if it's pretty, but I am slowly beginning to care more about the code I'm writing.

Last updated: May 06 2021 at 21:09 UTC