Stream: general

Topic: unique existence with Prop

Peter Nelson (Feb 16 2021 at 17:56):

This is probably an easy one... how do I replace the 'finish' (which works) with a less opaque proof here? When attempting a proof by cases, I seem to be getting snared up in dependent types - proof-irrelevance should somehow be used, but I don't immediately see how.

import data.setoid.partition

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
have := @setoid.classes_eqv_classes _ r a,
--  this: ∃! (b : set α) (H : b ∈ r.classes), a ∈ b
finish,
end


Yakov Pechersky (Feb 16 2021 at 18:01):

import data.setoid.partition

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
obtain ⟨b, ⟨h, hb, -⟩, hu⟩ := @setoid.classes_eqv_classes _ r a,
refine ⟨b, ⟨h, hb⟩, _⟩,
convert hu,
simp
end


Alex J. Best (Feb 16 2021 at 18:01):

You can do

example {α : Type} {r : setoid α} (a : α): ∃! (b : set α), b ∈ r.classes ∧ a ∈ b :=
begin
convert @setoid.classes_eqv_classes _ r a,
simp,
end


Peter Nelson (Feb 16 2021 at 18:05):

Thank you! simp is a little less opaque - however, in both your solutions, using simp? gives a suggestion which fails. The 'hard part' of the proof is still hiding. Can anyone shed some light on it?

Bryan Gin-ge Chen (Feb 16 2021 at 18:07):

simp? is still not quite ready for general use, I think. squeeze_simp returns: simp only [exists_prop, exists_unique_iff_exists],, which works.

Peter Nelson (Feb 16 2021 at 18:09):

Aha, thank you! I didn't realize simp? wasn't the same as squeeze_simp. Those two lemmas give exactly the missing pieces I was curious about.

Kevin Buzzard (Feb 16 2021 at 18:13):

One day it will be, but simp? is a work in progress right now.

Last updated: May 11 2021 at 00:31 UTC