Fintype/finset

Stream: new members

[Logan Murphy]

I'm getting a bit lost navigating between the fintype/finset APIs - I'm not sure how to do what I want to do (if I even can).

First, I want to be able to take a fintype AP, an evalution from AP to bool, and construct a set of the elements of AP which evaluate to true. Simple enough.

Then, I want to take a set AP s and construct an evaluation from AP to bool which returns tt if a is in s and ff otherwise.

Of course, membership isn't decidable, but since AP is a fintype I thought I should assume that s is a finset instead. But then, I can't seem to adjust my first function to construct a computable finset AP rather than a set AP.

import data.set

def to_finset {AP : Type}
(μ : AP → bool)  [fintype AP]  : finset AP :=
{a ∈ finset.univ | μ a = tt}  -- noncomputable

def to_eval
{AP : Type}
(s : finset AP) [fintype AP] [decidable_eq AP] : AP → bool :=
λ a, if a ∈ s then tt else ff

is there a way to do this so that both functions are decidable/computable?

[Mario Carneiro]

def to_finset {AP : Type} (μ : AP → bool) [fintype AP] : finset AP :=
finset.univ.filter (λ a, μ a)

def to_eval {AP : Type} (s : finset AP) [fintype AP] [decidable_eq AP]
  (a : AP) : bool := a ∈ s