Decidability helpers for Sym2 and Set

Small, graph-independent deciders that Mathlib does not provide in the form needed by a library whose objects are Set-valued rather than type-valued. Everything here is stated in the root namespace, since nothing in it mentions graphs; these are natural candidates for upstreaming.

Main results

• Sym2.decidableForallMem — ∀ v ∈ e, p v is decidable for e : Sym2 α.
• Set.decidableSubsetOfFintype — s ⊆ t is decidable when s is finite (as data) and t has decidable membership.
• Set.decidableSubsingletonOfFintype — s.Subsingleton is decidable for a finite s.

Design choices

• [Fintype ↥s], not [Fintype α]. Mathlib's deciders for ⊆ and Subsingleton (Fintype.decidableSubsingleton) quantify over a finite type. A library in which a graph is a vertexSet : Set α for an arbitrary α never has that, but it does have finiteness of the individual sets involved, which is all these proofs need.
• Decidability, not Classical. Each result is stated so that its Decidable instance actually evaluates: Set.toFinset needs only [Fintype ↥s] and computes.

Sym2

@[implicit_reducible]

instance Sym2.decidableForallMem {α : Type u_1} {p : α → Prop} [DecidablePred p] (e : Sym2 α) : Decidable (∀ v ∈ e, p v)

A bounded universal quantifier over the two endpoints of an unordered pair is decidable. Mathlib provides Sym2.Mem.decidable but no decider for ∀ v ∈ e, p v.

The elimination has to go through Sym2.recOnSubsingleton: the goal is Decidable-, hence Sort-valued, so the Prop-valued recursor Sym2.ind does not apply.

Equations

• e.decidableForallMem = Sym2.recOnSubsingleton e fun (x y : α) => decidable_of_iff (p x ∧ p y) ⋯

Set

theorem Set.subset_iff_forall_mem_toFinset {α : Type u_1} (s t : Set α) [Fintype ↑s] : s ⊆ t ↔ ∀ x ∈ s.toFinset, x ∈ t

Inclusion of a finite Set into another, as a bounded quantifier over a Finset.

@[implicit_reducible]

instance Set.decidableSubsetOfFintype {α : Type u_1} (s t : Set α) [Fintype ↑s] [DecidablePred fun (x : α) => x ∈ t] : Decidable (s ⊆ t)

Inclusion is decidable when the smaller set is finite and the larger one has decidable membership.

Equations

• s.decidableSubsetOfFintype t = decidable_of_iff (∀ x ∈ s.toFinset, x ∈ t) ⋯

theorem Set.subsingleton_iff_toFinset_card_le_one {α : Type u_1} (s : Set α) [Fintype ↑s] : s.Subsingleton ↔ s.toFinset.card ≤ 1

Being a subsingleton, as a cardinality bound on the Finset view.

@[implicit_reducible]

instance Set.decidableSubsingletonOfFintype {α : Type u_1} (s : Set α) [Fintype ↑s] [DecidableEq α] : Decidable s.Subsingleton

Set.Subsingleton is decidable for a set with finite coercion.

Equations

• s.decidableSubsingletonOfFintype = decidable_of_iff (s.toFinset.card ≤ 1) ⋯

@[implicit_reducible]

instance Finset.decidablePredMemCoe {α : Type u_1} [DecidableEq α] (s : Finset α) : DecidablePred fun (x : α) => x ∈ ↑s

Membership in the coercion of a Finset is decidable. Stated as an instance because (↑s : Set α) and s have different head symbols, so instance search does not reach Finset.decidableMem on its own in every position.

Equations

• s.decidablePredMemCoe a = decidable_of_iff (a ∈ s) ⋯