evaluation finite sets

Stream: mathlib4

[Mark Aagaard]

I'm new to Lean and am considering using it in an undergraduate course on logic and discrete math. Does Lean support evaluation of finite sets? I tried the following example:

import MIL.Common
import Mathlib.Data.Finset.Basic

def xs : Finset ℕ := {1,2,3}

#eval xs
-- this works and gives the expected answer of {1,2,3}

def x := 3 ∈ xs

#eval x

The last command causes the error message:
failed to synthesize
Decidable x
use set_option diagnostics true to get diagnostic information

-mark

[David Renshaw]

Does it work if you define x like this?

def x : Bool := 3 ∈ xs

[Yaël Dillies]

You should make x and xs `reducible as in

import Mathlib.Data.Finset.Basic

abbrev xs : Finset ℕ := {1,2,3}
abbrev x := 3 ∈ xs

#eval x

[Mark Aagaard]

Thanks for the quick replies. Both suggestions work. I'll read more about abbrev.

-mark

[Kim Morrison]

@Mark Aagaard, you possibly don't want to be relying on #eval for things like this in the first place, and if you tell us more about what you want the user to see/do we might suggest an alternative.

[Mark Aagaard]

@Kim Morrison Thanks for the offer of help.

In short, I'm looking for a statically typed functional language that supports all of the usual features, plus set comprehension for finite sets. Symbolic evaluation would be nice, but is not a requirement. I don't need theorem proving at this point, but might in the future. The course is for computer engineers, so the emphasis is on practical techniques that they will choose of their own accord to use in the future.

I played around with macros yesterdays and was able to define syntax that I'm happy with for set comprehension with a single variable. I'll dig into macros further to understand how to extend this to multiple variables. Here's what I have so far:

import MIL.Common
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Image

abbrev s0 : Finset ℕ := { 0,1,2,3,4,5,6 }

macro (priority := high) "{" res:term "|" id:ident "∈" S:term "," p:term "}" : term =>
  `( Finset.image (fun $id => ($res)) (Finset.filter (fun $id => $p) ($S)))

abbrev y4 := { x+2 | x ∈ s0 , x > 3}

#eval y4
{2, 3, 4, 5, 6, 7, 8}