Zulip Chat Archive

Stream: new members

Topic: Sets


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

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

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

view this post on Zulip Brandon Brown (May 15 2020 at 03:59):

Thanks!

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

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 04:02):

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

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

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

view this post on Zulip Mario Carneiro (May 15 2020 at 04:18):

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

view this post on Zulip Johan Commelin (May 15 2020 at 04:18):

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 04:18):

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

view this post on Zulip Mario Carneiro (May 15 2020 at 04:18):

and rfl is a proof of 1 = 1

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

view this post on Zulip Mario Carneiro (May 15 2020 at 04:23):

rfl is short for eq.refl _

view this post on Zulip Johan Commelin (May 15 2020 at 04:23):

rfl is a smart kid (-;

view this post on Zulip Kevin Buzzard (May 15 2020 at 05:59):

refl is a powerful tactic!

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

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

view this post on Zulip Kenny Lau (May 15 2020 at 06:58):

(thanks, squeeze_simp)

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 07:01):

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

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

view this post on Zulip Kenny Lau (May 15 2020 at 07:03):

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

view this post on Zulip Bryan Gin-ge Chen (May 15 2020 at 07:07):

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

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