Zulip Chat Archive

Stream: general

Topic: unique existence with Prop


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

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

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

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

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

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

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