Manipulating finsets

Stream: new members

[Cayden Codel]

I'm attempting to write what amounts to the same recursive functions on a variety of set-like types. The one I wrote for lists was pretty straightfoward:

def transform_func : list Prop -> Prop
 | []  := ff
 | (x :: xs) := or x (transform_func xs)

However, I want to write a similar function but on finsets instead, i.e. transform_func : finset Prop -> Prop. The trouble I have is in casing on whether the set is inhabited or not (or, if I claim the set is inhabited, that the set has one versus many elements). I've tried writing cases h with hp, hnp where h is an exlcuded middle hypothesis that states that

or (\exists a, a \in s ) (\neg \exists a, a \in s)

but every time I try to uses cases, the compiler complains about breaking down h into component parts. Is there an easier or more canonical way of casing on the cardinality of sets? Or am I going about this the wrong way? Thanks!

[Yakov Pechersky]

What's your #mwe? Have you tried using list.foldr? You should use if h : ... then ... else ... if you're defining a function that cases on things; cases is a tactic.

[Kyle Miller]

@Mario Carneiro once pointed out that for this you can make use of the has_mem instance. He might write it a different way, but this would be equivalent to your definition:

def transform_func' (l : list Prop) : Prop := ∃ p ∈ l, p
def transform_func'' (l : finset Prop) : Prop := ∃ p ∈ l, p

[Kyle Miller]

It's probably more useful in this form:

def finset.any {α : Sort*} (s : finset α) (f : α → Prop) := ∃ x ∈ s, f x

You can write stuff like s.any (λ x, x > 2)

[Kyle Miller]

(but at this point you might just write the existential directly without making a new definition)

[Kyle Miller]

I can't find the previous thread about this, but they too were working on formalizing SAT, which I'm assuming is what you're up to :smile: