Zulip Chat Archive

Stream: new members

Topic: Solving a problem about set membership


view this post on Zulip Dillon Huff (Feb 20 2021 at 20:13):

Is there a tactic in mathlib for solving set membership problems? I'm interested in proving some theorems about whether or not a set includes members from a superset. For example:

theorem set_trivia [α : Type] (S Γ : set α) (φ : α) (φ  S) (S  Γ  {φ}) :
  S  Γ :=
begin
  sorry,
end

Thanks in advance!

view this post on Zulip Ruben Van de Velde (Feb 20 2021 at 21:12):

I don't think there's a tactic; your example can be solved with

view this post on Zulip Kevin Buzzard (Feb 20 2021 at 21:19):

I think we've had this conversation before. What happens if you turn everything into propositions and then use cc?

view this post on Zulip Dillon Huff (Feb 20 2021 at 21:31):

Unfortunately I'm a newb so I don't know enough about lean to say.

I had thought there might be tactic for this because in this video on formalizing matroids in lean: https://www.youtube.com/watch?v=FzJuoXy5cG0 they seem to have a related tactic they call timed_simplify_sets, though at 37:14 the presenter says something about how its not efficient, and that the correspondence between some of the problems they wanted to solve and propositional logic was more complicated than they thought. Maybe that comment is relevant here?

view this post on Zulip Bryan Gin-ge Chen (Feb 20 2021 at 21:35):

Once you put in the have from Ruben's proof, finish can do the rest of the job:

import tactic

theorem set_trivia [α : Type] (S Γ : set α) (φ : α) (H : φ  S) (H' : S  Γ  {φ}) :
  S  Γ :=
begin
  intros x hs,
  have := H' hs,
  finish,
end

Last updated: May 16 2021 at 05:21 UTC