set to list

Stream: Is there code for X?

[Patrick Thomas]

Is there a function in mathlib to take a set to a list?

[Yaël Dillies]

How would it do that? What if the set is infinite?

[Patrick Thomas]

an infinite list?

[Yakov Pechersky]

Patrick, what do you want to do with the list you get?

[Yaël Dillies]

So not docs#list but rather a function ℕ → α?

[Patrick Thomas]

I have a function to extract the set of atoms from a prop formula, now I want to write one that determines if the formula is a tautology by iterating over its atoms.

[Patrick Thomas]

I'm not sure if this is enough context, I can add the other definitions if it helps:

def update {A U : Type} [decidable_eq A]
  (f : A → U) (v : A) (a : U) : A → U := fun i, if i = v then a else f i


def all_val : list string -> formula -> (string -> bool) -> bool
| [] fm f := eval fm f
| (a :: as) fm f := (all_val as fm (update f a tt)) && (all_val as fm (update f a ff))


def is_tauto (fm : formula) : bool := all_val (atoms fm) fm (fun a, ff)

[Yakov Pechersky]

If you have a proof that your set is finite, you can use docs#set.finite.induction_on

[Patrick Thomas]

Oh. Ok. That might work.

[Yakov Pechersky]

Your update is docs#function.update

[Patrick Thomas]

Oh. Cool.

[Patrick Thomas]

Can I inductively prove the set is finite by saying that the empty list and singleton is finite, and if two sets are finite then their union is finite?

[Patrick Thomas]

I have this:

inductive formula : Type
| bottom : formula
| top : formula
| atom : string → formula
| not : formula → formula
| and : formula → formula → formula
| or : formula → formula → formula
| imp : formula → formula → formula
| iff : formula → formula → formula

open formula

def atoms : formula → (set string)
| bottom := {}
| top := {}
| (atom v) := {v}
| (not p) := atoms p
| (and p q) := (atoms p) ∪ (atoms q)
| (or p q) := (atoms p) ∪ (atoms q)
| (imp p q) := (atoms p) ∪ (atoms q)
| (iff p q) := (atoms p) ∪ (atoms q)

[Yakov Pechersky]

You can. You can also use docs#finset too, you'll just need to add @[derive decidable_eq] above inductive formula : Type

[Yakov Pechersky]

For your specific question, check out docs#set.finite.union, docs#set.finite_empty, docs#set.finite_singleton

[Patrick Thomas]

Thank you!