## Stream: new members

### Topic: Sets

#### Brandon Brown (May 15 2020 at 03:53):

How do I do something as trivial as proving set membership?

import data.finset

def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1   --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := sorry


#### Bryan Gin-ge Chen (May 15 2020 at 03:57):

In this case you can use dec_trivial:

import data.finset

def x1 : finset ℕ := {1,2,3}
#reduce 1 ∈ x1   --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false
example : 1 ∈ x1 := dec_trivial


#### Johan Commelin (May 15 2020 at 03:58):

@Brandon Brown If you've got a very explicit set, like in your example, then it's dec_trivial, like Bryan said. If you have a set if the form finset.range n or finset.filter foo bar, then there will be lemmas finset.mem_range and finset.mem_filter etc... that help you proving this.

Thanks!

#### Johan Commelin (May 15 2020 at 04:00):

Brandon Brown said:

#reduce 1 ∈ x1   --1 = 3 ∨ 1 = 2 ∨ 1 = 1 ∨ false


Note that this is about to change to

#reduce 1 ∈ x1   --1 = 1 ∨ 1 = 2 ∨ 1 = 3


which I think is a big improvement (-;

#### Johan Commelin (May 15 2020 at 04:01):

Also, if you don't like dec_trivial, you could use a combination of or.inl, or.inr and rfl.

#### Bryan Gin-ge Chen (May 15 2020 at 04:02):

This reminds me a lot of one of my early threads here.

#### Brandon Brown (May 15 2020 at 04:17):

I have a more basic question. I understand constructions of the form

variables (p q : Prop)
example (h : p) : p ∨ q := or.inl h


Because I'm injecting h

#### Brandon Brown (May 15 2020 at 04:18):

But I don't really understand what's going on under the hood with

example : (1 = 1) ∨ false := or.inl (rfl)


#### Mario Carneiro (May 15 2020 at 04:18):

or.inl _ would expect a proof of 1 = 1 at the location of the _

#### Johan Commelin (May 15 2020 at 04:18):

Well, you need to inject a proof of 1 = 1

#### Bryan Gin-ge Chen (May 15 2020 at 04:18):

Let p := 1=1, q := false and h := rfl.

#### Mario Carneiro (May 15 2020 at 04:18):

and rfl is a proof of 1 = 1

#### Brandon Brown (May 15 2020 at 04:22):

Ahh right I see

variable p : (1 = 1)
example : (1 = 1) ∨ false := or.inl p


So using rfl is inferring this since what else could it be

#### Mario Carneiro (May 15 2020 at 04:23):

rfl is short for eq.refl _

#### Johan Commelin (May 15 2020 at 04:23):

rfl is a smart kid (-;

#### Kevin Buzzard (May 15 2020 at 05:59):

refl is a powerful tactic!

#### Kenny Lau (May 15 2020 at 06:54):

the correct way, much as I hate it, is by simp:

import data.finset

def x1 : finset ℕ := {1,2,3}
example : 1 ∈ x1 := by simp [x1]

variables {α : Type*} [has_one α] [has_add α] [decidable_eq α]
def x2 : finset α := {1,2,3}
example : (1 : α) ∈ (x2 : finset α) := dec_trivial -- fails
example : (1 : α) ∈ (x2 : finset α) := by simp [x2] -- works


#### Kenny Lau (May 15 2020 at 06:58):

the last line is equivalent to simp only [x2, eq_self_iff_true, or_true, finset.mem_insert, finset.mem_singleton, finset.singleton_eq_singleton]

#### Kenny Lau (May 15 2020 at 06:58):

(thanks, squeeze_simp)

#### Bryan Gin-ge Chen (May 15 2020 at 07:01):

That's surprising to me. Are there some missing decidability instances somewhere?

#### Kenny Lau (May 15 2020 at 07:03):

no, it's just that asserting \a has decidable_eq does not actually give an algorithm to decide whether two terms of \a are equal

#### Kenny Lau (May 15 2020 at 07:03):

if \a is anything concrete (like \N) then it will work

#### Bryan Gin-ge Chen (May 15 2020 at 07:07):

Oh, right. The type class is a variable so there's no actual definition.

#### Kenny Lau (May 15 2020 at 07:19):

yeah that also confused me for a while :P

Last updated: May 14 2021 at 00:42 UTC