A choice-free Finset prelude

One of the project's goals (Goal 3) is to certify that the information-system presentation of Scott domains can be developed in a purely constructive fragment of Lean: every result must have a #print axioms footprint contained in [propext, Quot.sound], with no Classical.choice and no use of the law of excluded middle.

This is harder than it looks, because several of mathlib's Finset operations and even a few basic lemmas transitively depend on Classical.choice (through the Multiset.dedup / quotient machinery), in version v4.30.0:

• tainted operations: (· ∪ ·), Finset.image, (· ×ˢ ·), Finset.biUnion, (· \ ·);
• tainted lemmas: e.g. Finset.insert_comm;
• tainted tactics: tauto, aesop (they close goals via classical reasoning).

By contrast the following are choice-free and form our working toolkit: insert, (· ∩ ·), Finset.filter, Finset.fold, Multiset.foldr, the membership/subset lemmas (Finset.mem_insert, Finset.mem_singleton, Finset.subset_iff, Finset.mem_coe, Finset.coe_subset, Finset.mem_inter, Finset.ext), set-level unions/intersections, and explicit term-mode/rintro/constructor proofs.

This file provides the one finite-set operation the development needs but mathlib only offers in choice-tainted form: a binary union of Finsets, built choice-free by folding insert. Every declaration here is audited to depend only on [propext, Quot.sound].

theorem Domain.Constructive.insert_comm' {α : Type u_1} [DecidableEq α] (a b : α) (s : Finset α) : insert a (insert b s) = insert b (insert a s)

Choice-free commutativity of insert (mathlib's Finset.insert_comm is choice-tainted). Needed to fold insert over a Multiset.

instance Domain.Constructive.instLeftCommutativeFinsetInsert_leanPool {α : Type u_1} [DecidableEq α] : LeftCommutative insert

def Domain.Constructive.funion {α : Type u_1} [DecidableEq α] (u v : Finset α) : Finset α

Choice-free binary union of finite sets, obtained by folding insert over the second argument's underlying multiset. Definitionally equal in content to u ∪ v, but — unlike mathlib's (· ∪ ·) — free of any Classical.choice dependency.

Equations

• u ∪' v = Multiset.foldr insert u v.val

def Domain.Constructive.«term_∪'_» : Lean.TrailingParserDescr

Choice-free binary union of finite sets, obtained by folding insert over the second argument's underlying multiset. Definitionally equal in content to u ∪ v, but — unlike mathlib's (· ∪ ·) — free of any Classical.choice dependency.

Equations

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

theorem Domain.Constructive.mem_foldr_insert {α : Type u_1} [DecidableEq α] (a : α) (u : Finset α) (s : Multiset α) : a ∈ Multiset.foldr insert u s ↔ a ∈ u ∨ a ∈ s

@[simp]

theorem Domain.Constructive.mem_funion {α : Type u_1} [DecidableEq α] {a : α} {u v : Finset α} : a ∈ u ∪' v ↔ a ∈ u ∨ a ∈ v

theorem Domain.Constructive.coe_funion {α : Type u_1} [DecidableEq α] (u v : Finset α) : ↑(u ∪' v) = ↑u ∪ ↑v

The coercion of u ∪' v to a Set is the (choice-free) set union of the coercions.

theorem Domain.Constructive.subset_funion_left {α : Type u_1} [DecidableEq α] (u v : Finset α) : u ⊆ u ∪' v

theorem Domain.Constructive.subset_funion_right {α : Type u_1} [DecidableEq α] (u v : Finset α) : v ⊆ u ∪' v

theorem Domain.Constructive.funion_subset_iff {α : Type u_1} [DecidableEq α] {u v w : Finset α} : u ∪' v ⊆ w ↔ u ⊆ w ∧ v ⊆ w

Universal property of the union: u ∪' v ⊆ w iff both u ⊆ w and v ⊆ w.