library for fintype and boolean

Stream: general

[Thorsten Altenkirch]

Is there a library that does quantifiers for finite types and booleans and shows that they are equivalent to the usual quantifiers?

[Eric Wieser]

I guess you can just use finset.univ.sup f (as exists) and finset.univ.inf f (as forall) where f is a function from your finite type to bool?

[Eric Wieser]

import data.finset.lattice
import data.fintype.basic

lemma sup_bool_eq_bexists {α : Type*} (s : finset α) (f : α → bool) :
  (s.sup f : _) ↔ ∃ a ∈ s, f a :=
begin
  induction s using finset.cons_induction with a ha s ih,
  { simp },
  { simp only [ih, finset.sup_cons, bool.sup_eq_bor, bor_coe_iff, exists_prop, finset.mem_cons],
    simp_rw [or_and_distrib_right, exists_or_distrib, exists_eq_left] },
end

lemma univ_sup_bool_eq_exists {α : Type*} [fintype α] (f : α → bool) :
  (finset.univ.sup f : _) ↔ ∃ a, f a :=
by simpa using sup_bool_eq_bexists finset.univ f

[Kyle Miller]

@Thorsten Altenkirch You might also be interested to know that there are decidable instances that support doing these sorts of coercions to bool automatically.

import data.fintype.basic

def bool.forall (α : Type*) [fintype α] (f : α → bool) : bool := ∀ x, f x
def bool.exists (α : Type*) [fintype α] (f : α → bool) : bool := ∃ x, f x

The relevant lemma then for equivalence is docs#to_bool_iff

[Yaël Dillies]

Maybe you're looking for docs#list.all, docs#list.any?