set iteration

Stream: new members

[Prince Varshney]

I have set of type Expr. Members of this set can belong to one of three categories alpha,beta or literal(I have a function which can take Expr and tell it's category). I need to find any element with category alpha.
I wanted to know how to iterate through sets to get the required result.

[Kevin Buzzard]

Can you post an #mwe ? (Read the link to see what I'm asking)

[Prince Varshney]

@Kevin Buzzard

structure var :=
mk :: (idx : ℕ)

inductive Expr
| atom (v : var) : Expr
| not  : Expr -> Expr
| and  : Expr -> Expr -> Expr
| or   : Expr -> Expr -> Expr
| impl : Expr -> Expr -> Expr
| err  : Expr

prefix `atom` : 49 := Expr.atom
prefix `-`    : 50 := Expr.not
infix `Λ`     : 51 := Expr.and
infix `V`     : 52 := Expr.or
infix `⇒`     : 53 := Expr.impl

def p1 := var.mk 1
def p2 := var.mk 2

def e1 : Expr := (atom p1)
def e2 : Expr := (atom p2)
def e3 : Expr := (e1 V e2)
def e4 : Expr := (e1 Λ  e2)
def e5 : Expr := e1 ⇒ e2

inductive formula : Type
| alpha : formula
| beta : formula
| literal : formula
| err : formula

open formula

def getFormulaType : Expr -> formula
| (atom p) := formula.literal
| - (atom p) := formula.literal
| -(- e) := formula.alpha
| (e1 Λ e2) := formula.alpha
| -(e1 V e2) := formula.alpha
| -(e1 ⇒ e2) := formula.alpha
| (e1 V e2) := formula.beta
| -(e1 Λ e2) := formula.beta
| (e1 ⇒ e2) := formula.beta
| Expr.err := formula.err
| -(Expr.err) := formula.err

def pickAlpha : list Expr -> Expr
| [] := Expr.err
| (x :: xs) := match (getFormulaType x) with
                | alpha := x
                | _ := pickAlpha xs
               end

def formulas : list Expr := [e1,e2,e3,e4,e5]
#eval pickAlpha formulas

constant pickAlphaType : set Expr -> Expr

I wanted to write pickAlpha function with sets instead of list

[Prince Varshney]

i.e pick any alpha formula given a set of Expr

[Yury G. Kudryashov]

set α is just α → Prop, so you have no way to iterate over all elements. If you want to deal with finite test, then have a look at docs#finset.

[Cameron Torrance]

If you are just looking example of an alpha in your set, don't care which one and are willing to use classical logic you could write such a function. Using excluded middle you can consider the case where your set doesn't have alphas (return err) and when it does use choice to pick out a alpha.

[Yury G. Kudryashov]

But this function won't be computable