Zulip Chat Archive

Stream: general

Topic: option golf puzzle


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

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

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

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

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

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

view this post on Zulip Mario Carneiro (Nov 22 2019 at 17:20):

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

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

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