Lean.MetaEval (Set ℕ)

Stream: new members

[Enrico Borba]

Why can't I #eval a Set Nat? Specifically:

#eval {1, 2, 3}

results in

typeclass instance problem is stuck, it is often due to metavariables
  Insert ℕ ?m.55319

And if I try

#eval ({1, 2, 3} : Set ℕ)

I get

expression
  {1, 2, 3}
has type
  Set ℕ
but instance
  Lean.MetaEval (Set ℕ)
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

Is there any way to "print" the items in this (or any finite set)? Finset.toList is noncomputable, and I can't seem to find a way around this.

[Ruben Van de Velde]

Certainly not with Set, since it could be infinite

[Ruben Van de Velde]

Really the question is "what are you trying to do"

[Enrico Borba]

I'm trying to constructively enumerate the preimage of a boolean function:

#eval {b : Bool × Bool | Bool.xor b.1 b.2}

[Enrico Borba]

Specifically, I'm trying to formalize some basic theorems about boolean functions and propositional logic. I'm trying to prove that the symbols {¬, ∧, ∨} are enough to represent a boolean function. I've defined my own structures for a signature (set of symbols) and formulas, and now I'm trying to construct a disjunctive normal form of a boolean function, which requires me to constructively enumerate the inputs for which the boolean function evaluates to true.

[Ruben Van de Velde]

#eval (Finset.univ : Finset (Bool × Bool)).filter fun b => Bool.xor b.1 b.2

example : ((Finset.univ : Finset (Bool × Bool)).filter fun b => Bool.xor b.1 b.2) = {(true, false), (false, true)} := by
  decide

[Enrico Borba]

Am I missing some Finset import or something?
This still fails for me

#eval (Finset.univ : Finset (Bool × Bool)).filter fun b => Bool.xor b.1 b.2

with:

expression
  Finset.filter (fun b => Bool.xor b.1 b.2 = true) Finset.univ
has type
  Finset (Bool × Bool)
but instance
  Lean.MetaEval (Finset (Bool × Bool))
failed to be synthesized, this instance instructs Lean on how to display the resulting value, recall that any type implementing the `Repr` class also implements the `Lean.MetaEval` class

[Enrico Borba]

Also thank you for the example proof of the contents of the set, that will be useful.

[Enrico Borba]

It seems I was. Mathlib/Data/Finset/Sort.lean contains

unsafe instance [Repr α] : Repr (Finset α) where
  reprPrec s _ :=
    -- multiset uses `0` not `∅` for empty sets
    if s.card = 0 then "∅" else repr s.1

[Enrico Borba]

Not sure what the consequences of using an unsafe instance is... But I'll take it for now. Thank you for the help :)

[Enrico Borba]

I also guess unsafe doesn't matter much for a Repr instance, since it won't be used in the theorems.

[Eric Wieser]

unsafe means that if you try to prove things about the repr you'll derive a contradiction, since {1, 2} = {2, 1} but they have different reprs

[Enrico Borba]

Ah got it, thanks!

[Enrico Borba]

also interesting that Finset.toList is noncomputable but Finset.sort is not. Surprised a relation is necessary for this.

[Ruben Van de Velde]

By sorting, the output is well-defined

[Enrico Borba]

Ah that makes sense.

[Enrico Borba]

FinEnum is what actually solved the root of my problem.