Finset-typed refinement of the IE substrate

@cite{fox-2007} @cite{spector-2016}

Finset-typed computable refinement of the canonical Set-side definitions in Operators/Basic.lean. There is no parallel theory: Innocent.IsCompatible / IsMCSet are abbrevs over their Set-side counterparts under the Finset → Set coercion, with bridge iffs that recover the explicit Finset characterizations + provide the Decidable instances downstream Excluder.exh needs.

Worlds are an arbitrary [Fintype W] [DecidableEq W]. A proposition is a Finset W. An alternative collection is a Finset (Finset W).

Architecture

The Set-side Exhaustification.IsCompatible / IsMCSet / IE (defined in Operators/Basic.lean) are the canonical specifications. Here:

1. asSetOfSets : Finset (Finset W) → Set (Set W) — the obvious coercion (lift each inner Finset to a Set, take the image).
2. Innocent.IsCompatible E := Exhaustification.IsCompatible (asSetOfSets ALT) ↑φ (asSetOfSets E) and similarly for IsMCSet. These are abbrevs, so any Set-side theorem about IsCompatible / IsMCSet automatically applies.
3. Bridge iffs to the explicit Finset characterizations: IsCompatible ↔ E ⊆ excludables ∧ φ ∈ E ∧ (E.inf id).Nonempty, etc.
4. Decidable instances via the bridges (the Finset characterization is decidable by construction).
5. IE / innocentlyExcludable as Finset filters using the derived Decidable instances.

Standard mathlib pattern for "abstract spec + computable refinement" (cf. Set.Finite + Set.Finite.toFinset, Set.image + Finset.image, etc.).

Key definitions

• excludables ALT φ — bound on every IsCompatible witness
• IsCompatible ALT φ E — Spector Definition 3.2 (Finset-typed, defined as a Set-side abbrev)
• IsMCSet ALT φ E — Spector Definition 3.3 (similarly)
• IE ALT φ — Spector Definition 3.4: alternatives in every MC-set
• innocentlyExcludable ALT φ — alternatives whose complement is in IE

The Fox 2007 Excluder packaging lives in InnocentExclusion.lean (sibling Excluder file, parallel to Tolerant.lean / Relevance.lean).

Coercion

def Exhaustification.Innocent.asSetOfSets {W : Type u_1} (E : Finset (Finset W)) : Set (Set W)

Lift a Finset (Finset W) to Set (Set W) by coercing each inner Finset to a Set.

Equations

• Exhaustification.Innocent.asSetOfSets E = (fun (s : Finset W) => ↑s) '' ↑E

@[simp]

theorem Exhaustification.Innocent.mem_asSetOfSets {W : Type u_1} [Fintype W] [DecidableEq W] {E : Finset (Finset W)} {s : Set W} : s ∈ asSetOfSets E ↔ ∃ a ∈ E, ↑a = s

theorem Exhaustification.Innocent.coe_univ_sdiff {W : Type u_1} [Fintype W] [DecidableEq W] (a : Finset W) : ↑(Finset.univ \ a) = (↑a)ᶜ

↑(univ \ a) = (↑a)ᶜ: Finset complement coerces to Set complement.

theorem Exhaustification.Innocent.finset_ext_of_coe_eq {W : Type u_1} [Fintype W] [DecidableEq W] {a b : Finset W} (h : ↑a = ↑b) : a = b

Two Finsets are equal iff their Set coercions are equal.

theorem Exhaustification.Innocent.mem_inf_id_iff {W : Type u_1} [Fintype W] [DecidableEq W] {s : Finset (Finset W)} {w : W} : w ∈ s.inf id ↔ ∀ a ∈ s, w ∈ a

Membership in the Finset inf id (intersection of a family of Finsets).

Excludables: the bound on compatible sets

def Exhaustification.Innocent.excludables {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : Finset (Finset W)

Bound on every IsCompatible set: the prejacent plus complements of every alternative. Every member of any compatible set is either φ or aᶜ for some a ∈ ALT, so the powerset of this set is the natural search space.

Equations

• Exhaustification.Innocent.excludables ALT φ = insert φ (Finset.image (fun (a : Finset W) => Finset.univ \ a) ALT)

IsCompatible: Spector Def 3.2

Defined as a thin specialization of the Set-side IsCompatible under coercion. The Finset shape is recovered via isCompatible_iff_finset, which also yields the Decidable instance.

@[reducible, inline]

abbrev Exhaustification.Innocent.IsCompatible {W : Type u_1} (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Prop

Spector Def 3.2 (Finset-typed). Defined as the Set-side IsCompatible applied to the coercions of ALT, φ, and E.

Equations

• Exhaustification.Innocent.IsCompatible ALT φ E = Exhaustification.IsCompatible (Exhaustification.Innocent.asSetOfSets ALT) (↑φ) (Exhaustification.Innocent.asSetOfSets E)

theorem Exhaustification.Innocent.isCompatible_iff_finset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : IsCompatible ALT φ E ↔ E ⊆ excludables ALT φ ∧ φ ∈ E ∧ (E.inf id).Nonempty

Bridge: the abbrev unfolds to the explicit Finset condition.

@[implicit_reducible]

instance Exhaustification.Innocent.decidableIsCompatible {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Decidable (IsCompatible ALT φ E)

Equations

• Exhaustification.Innocent.decidableIsCompatible ALT φ E = decidable_of_iff (E ⊆ Exhaustification.Innocent.excludables ALT φ ∧ φ ∈ E ∧ (E.inf id).Nonempty) ⋯

IsMCSet: Spector Def 3.3

@[reducible, inline]

abbrev Exhaustification.Innocent.IsMCSet {W : Type u_1} (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Prop

Spector Def 3.3 (Finset-typed). Defined as the Set-side IsMCSet on the coercions.

Equations

• Exhaustification.Innocent.IsMCSet ALT φ E = Exhaustification.IsMCSet (Exhaustification.Innocent.asSetOfSets ALT) (↑φ) (Exhaustification.Innocent.asSetOfSets E)

theorem Exhaustification.Innocent.isMCSet_iff_finset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : IsMCSet ALT φ E ↔ IsCompatible ALT φ E ∧ ∀ E' ∈ (excludables ALT φ).powerset, IsCompatible ALT φ E' → E ⊆ E' → E' ⊆ E

Bridge: equivalent to the explicit Finset MC-set condition (using excludables.powerset as the bounded search space, which suffices because every compatible set is bounded by excludables).

@[implicit_reducible]

instance Exhaustification.Innocent.decidableIsMCSet {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (E : Finset (Finset W)) : Decidable (IsMCSet ALT φ E)

Equations

• One or more equations did not get rendered due to their size.

IE: Spector Def 3.4

IE is the set of alternatives in every MC-set. On the Finset side it is a Finset (filter from excludables); membership corresponds to membership in the Set-side Exhaustification.IE.

def Exhaustification.Innocent.IE {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : Finset (Finset W)

Spector Def 3.4: IE = {ψ : ψ is in every MC-set}. Bounded by excludables, since every MC-set is a subset of excludables.

Equations

• One or more equations did not get rendered due to their size.

def Exhaustification.Innocent.innocentlyExcludable {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : Finset (Finset W)

The innocently-excludable alternatives: a ∈ ALT such that aᶜ ∈ IE. For each such a, exhaustification negates a (asserts aᶜ).

Equations

• Exhaustification.Innocent.innocentlyExcludable ALT φ = {a ∈ ALT | Finset.univ \ a ∈ Exhaustification.Innocent.IE ALT φ}

theorem Exhaustification.Innocent.innocentlyExcludable_subset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : innocentlyExcludable ALT φ ⊆ ALT

theorem Exhaustification.Innocent.phi_mem_IE {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : φ ∈ IE ALT φ

The prejacent is in every MC-set (it's in every compatible set), hence in IE. Specialization of Exhaustification.phi_mem_IE to the Finset side.

IsInnocentlyExcludable: bridge + decidability

The Set-typed Exhaustification.IsInnocentlyExcludable a requires a ∈ ALT AND aᶜ ∈ IE. The Finset side already has innocentlyExcludable ALT φ as a Finset (alternatives whose complements are in IE). Bridge theorem + Decidable instance below.

theorem Exhaustification.Innocent.isInnocentlyExcludable_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ a : Finset W) : IsInnocentlyExcludable (asSetOfSets ALT) ↑φ ↑a ↔ a ∈ innocentlyExcludable ALT φ

Bridge: Set-side IsInnocentlyExcludable on the coercion ↔ Finset-side membership in innocentlyExcludable.

@[implicit_reducible]

instance Exhaustification.Innocent.decidableIsInnocentlyExcludable {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ a : Finset W) : Decidable (IsInnocentlyExcludable (asSetOfSets ALT) ↑φ ↑a)

IsInnocentlyExcludable is decidable on the Finset side via the bridge to innocentlyExcludable membership.

Equations

• Exhaustification.Innocent.decidableIsInnocentlyExcludable ALT φ a = decidable_of_iff (a ∈ Exhaustification.Innocent.innocentlyExcludable ALT φ) ⋯

Cell: bridge + decidability

The Set-typed Exhaustification.cell predicate at world w requires: w ∈ φ ∧ (∀q IE, w ∉ q) ∧ (∀ r ∈ nonExcludable, w ∈ r). The Finset version cellFinset enumerates worlds satisfying this; bridge below recovers the Set predicate from Finset membership.

def Exhaustification.Innocent.cellFinset {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) : Finset W

Finset-side cell witness predicate at a world. Decidable by construction (all quantifications are over Finsets).

Equations

• One or more equations did not get rendered due to their size.

theorem Exhaustification.Innocent.mem_cellFinset_iff {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (w : W) : w ∈ cellFinset ALT φ ↔ cell (asSetOfSets ALT) (↑φ) w

Bridge: Finset-side cellFinset membership ↔ Set-side cell predicate. Lets decide proofs of cell-witness facts on the Finset side discharge Set-typed cell-witness hypotheses required by the general substrate theorems (Operators/InnocentInclusion.lean::mem_II_of_cell_witness, exhIEII_implies_cell_witnessed_alt, etc.).

@[implicit_reducible]

instance Exhaustification.Innocent.decidableCell {W : Type u_1} [Fintype W] [DecidableEq W] (ALT : Finset (Finset W)) (φ : Finset W) (w : W) : Decidable (cell (asSetOfSets ALT) (↑φ) w)

Exhaustification.cell on the Finset coercion is decidable via the bridge to cellFinset membership.

Equations

• Exhaustification.Innocent.decidableCell ALT φ w = decidable_of_iff (w ∈ Exhaustification.Innocent.cellFinset ALT φ) ⋯