Zulip Chat Archive

Stream: new members

Topic: Set membership with explicit constructor


view this post on Zulip ROCKY KAMEN-RUBIO (Jun 22 2020 at 17:22):

I'm back with another noob finset question.

MWE:

import tactic
import data.finset
variable P : Type*
example {p1 p2 p3 p : P} {h : p  ({p1, p2} : finset P)} : p  ({p1, p2, p3} : finset P) :=
begin
  sorry,
end

More context:

I'm trying to simplify a more complex expression that a finset is a subset of the union/intersection of other finsets. All are defined explicitly, and I have equality/inequality expressions for every pair of elements. simp reduces the larger set into a series of insert expression, but that's it. Has anyone tried writing something like linarith but for sets?

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 17:24):

tidy solves it.

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 17:25):

simp * at *, tauto also works

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 22 2020 at 17:45):

Thank you! I always forget about tidy. That's fascinating that simp at h, simp, behaves differently than simp * at *.

view this post on Zulip Kevin Buzzard (Jun 22 2020 at 18:22):

For me, both simp at h, simp and simp * at * turn the local context into

P : Type u_1
_inst_1 : decidable_eq P
p1 : P
p2 : P
p3 : P
p : P
h : p = p1  p = p2
 p = p1  p = p2  p = p3

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 22 2020 at 18:29):

Kevin Buzzard said:

For me, both simp at h, simp and simp * at * turn the local context into

P : Type u_1
_inst_1 : decidable_eq P
p1 : P
p2 : P
p3 : P
p : P
h : p = p1  p = p2
 p = p1  p = p2  p = p3

Interesting. Trying it again I'm getting the same behavior as you. Maybe my file is just getting too big. I've been careful not to leave any errors though.


Last updated: May 15 2021 at 23:13 UTC