Faster Way to prove all possible elements in a set

Stream: new members

[Colin Jones ⚛️]

Would there be a way to prove that mwe is a closed / finite set, such as:

def mwe := { s : String // s.length == 2 && s.dropWhile "AB".toList.contains == ""}

example (y : mwe) : y = ⟨"AA", by rfl⟩ ∨ y = ⟨"AB", by rfl⟩ ∨ y = ⟨"BA", by rfl⟩ ∨ y = ⟨"BB", by rfl⟩
  := by
  obtain ⟨val, property⟩ := y
  simp only [String.toList, ↓Char.isValue]
  sorry

[Kevin Buzzard]

What do you mean by a closed set? This is a term coming from topology, but there is no topological space in sight. For finiteness, there are several ways to state this: which one are you interested? In short, can you ask your question with a #mwe rather than in words?

[Eric Wieser]

I think what you're trying to show is Fintype mwe?

[Eric Wieser]

Or perhaps, (Set.univ : Set mwe) = {⟨"AA", by rfl⟩, ⟨"AB", by rfl⟩, ⟨"BA", by rfl⟩, ⟨"BB", by rfl⟩}, but that's a weaker result

[Colin Jones ⚛️]

Yes sorry I shouldn't use the word "closed set". Rather I want to show it is finite and only has those elements within it.

[Colin Jones ⚛️]

Exactly as the example says shown above. Would this be possible?

[Colin Jones ⚛️]

Eric Wieser said:

Or perhaps, (Set.univ : Set mwe) = {⟨"AA", by rfl⟩, ⟨"AB", by rfl⟩, ⟨"BA", by rfl⟩, ⟨"BB", by rfl⟩}, but that's a weaker result

Something like this, but to show that if y is an element of mwe it can only be those four items, nothing else

[Colin Jones ⚛️]

Is there a way to do this combinatorially?

[Colin Jones ⚛️]

Or to prove that the mwe type only has four possible members?

[Colin Jones ⚛️]

Is there a faster way to prove this?

def mwe' := {s : String // s ∈ ({"A", "B", "C"} : Set String)}

def A : mwe' := ⟨"A", by simp only [Set.mem_insert_iff, Set.mem_singleton_iff, String.reduceEq,
  or_false]⟩
def B : mwe' := ⟨"B", by simp only [Set.mem_insert_iff, String.reduceEq, Set.mem_singleton_iff,
  or_false, or_true]⟩
def C : mwe' := ⟨"C", by simp only [Set.mem_insert_iff, String.reduceEq, Set.mem_singleton_iff,
  or_true]⟩

example (x : mwe') : x = A ∨ x = B ∨ x = C := by
  obtain ⟨h, property⟩ := x
  rw [A, B, C]
  rcases property
  left
  simp_all
  rename_i property
  rcases property
  right
  left
  simp_all
  rename_i property
  right
  right
  simp only [Set.mem_singleton_iff] at property
  simp_all

[Kyle Miller]

def mwe' := {s : String // s ∈ ({"A", "B", "C"} : Set String)}

def A : mwe' := ⟨"A", by decide⟩
def B : mwe' := ⟨"B", by decide⟩
def C : mwe' := ⟨"C", by decide⟩

example (x : mwe') : x = A ∨ x = B ∨ x = C := by
  obtain ⟨s, h⟩ := x
  simpa [A, B, C, mwe'] using h

[Kevin Buzzard]

(I have no idea about the API for String.dropWhile or contains, so I can't answer)

[Notification Bot]

10 messages were moved here from #new members > Trouble with a String Matching Function by Eric Wieser.

[Eric Wieser]

(I've merged two threads since I think they're basicaly the same idea)