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
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