A computable model of ZFA without infinity

In this file we define finite hereditary lists. This is useful for calculations in naive set theory.

We distinguish two kinds of ZFA lists:

• Atoms. Directly correspond to an element of the original type.
• Proper ZFA lists. Can be thought of (but aren't implemented) as a list of ZFA lists (not necessarily proper).

For example, Lists ℕ contains stuff like 23, [], [37], [1, [[2], 3], 4].

Implementation note

As we want to be able to append both atoms and proper ZFA lists to proper ZFA lists, it's handy that atoms and proper ZFA lists belong to the same type, even though atoms of α could be modelled as α directly. But we don't want to be able to append anything to atoms.

This calls for a two-steps definition of ZFA lists:

• First, define ZFA prelists as atoms and proper ZFA prelists. Those proper ZFA prelists are defined by inductive appending of (not necessarily proper) ZFA lists.
• Second, define ZFA lists by rubbing out the distinction between atoms and proper lists.

Main declarations

• Lists' α false: Atoms as ZFA prelists. Basically a copy of α.
• Lists' α true: Proper ZFA prelists. Defined inductively from the empty ZFA prelist (Lists'.nil) and from appending a ZFA prelist to a proper ZFA prelist (Lists'.cons a l).
• Lists α: ZFA lists. Sum of the atoms and proper ZFA prelists.
• Finsets α: ZFA sets. Defined as Lists quotiented by Lists.Equiv, the extensional equivalence.

inductive Lists' (α : Type u) : Bool → Type u

Prelists, helper type to define Lists. Lists' α false are the "atoms", a copy of α. Lists' α true are the "proper" ZFA prelists, inductively defined from the empty ZFA prelist and from appending a ZFA prelist to a proper ZFA prelist. It is made so that you can't append anything to an atom while having only one appending function for appending both atoms and proper ZFC prelists to a proper ZFA prelist.

• atom {α : Type u} : α → Lists' α false
• nil {α : Type u} : Lists' α true
• cons' {α : Type u} {b : Bool} : Lists' α b → Lists' α true → Lists' α true

instance instDecidableEqLists' {α✝ : Type u_2} {a✝ : Bool} [DecidableEq α✝] : DecidableEq (Lists' α✝ a✝)

Equations

• instDecidableEqLists' = decEqLists'✝

def Lists (α : Type u_2) : Type u_2

Hereditarily finite list, aka ZFA list. A ZFA list is either an "atom" (b = false), corresponding to an element of α, or a "proper" ZFA list, inductively defined from the empty ZFA list and from appending a ZFA list to a proper ZFA list.

Equations

• Lists α = ((b : Bool) × Lists' α b)

instance Lists'.instInhabited {α : Type u_1} [Inhabited α] (b : Bool) : Inhabited (Lists' α b)

Equations

• Lists'.instInhabited true = { default := Lists'.nil }
• Lists'.instInhabited false = { default := Lists'.atom default }

def Lists'.cons {α : Type u_1} : Lists α → Lists' α true → Lists' α true

Appending a ZFA list to a proper ZFA prelist.

Equations

• Lists'.cons ⟨fst, a⟩ x✝ = a.cons' x✝

def Lists'.toList {α : Type u_1} {b : Bool} : Lists' α b → List (Lists α)

Converts a ZFA prelist to a List of ZFA lists. Atoms are sent to [].

Equations

• (Lists'.atom a).toList = []
• Lists'.nil.toList = []
• (a.cons' l).toList = ⟨b, a⟩ :: l.toList

@[simp]

theorem Lists'.toList_cons {α : Type u_1} (a : Lists α) (l : Lists' α true) : (cons a l).toList = a :: l.toList

def Lists'.ofList {α : Type u_1} : List (Lists α) → Lists' α true

Converts a List of ZFA lists to a proper ZFA prelist.

Equations

• Lists'.ofList [] = Lists'.nil
• Lists'.ofList (a :: l) = Lists'.cons a (Lists'.ofList l)

@[simp]

theorem Lists'.to_ofList {α : Type u_1} (l : List (Lists α)) : (ofList l).toList = l

@[simp]

theorem Lists'.of_toList {α : Type u_1} (l : Lists' α true) : ofList l.toList = l

def Lists'.recOfList {α : Type u_1} {motive : Lists' α true → Sort u_2} (ofList : (l : List (Lists α)) → motive (ofList l)) (l : Lists' α true) : motive l

Recursion/induction principle for Lists'.ofList.

Equations

• Lists'.recOfList ofList l = cast ⋯ (ofList l.toList)

inductive Lists.Equiv {α : Type u_1} : Lists α → Lists α → Prop

Equivalence of ZFA lists. Defined inductively.

• refl {α : Type u_1} (l : Lists α) : l.Equiv l
• antisymm {α : Type u_1} {l₁ l₂ : Lists' α true} : l₁.Subset l₂ → l₂.Subset l₁ → Equiv ⟨true, l₁⟩ ⟨true, l₂⟩

inductive Lists'.Subset {α : Type u_1} : Lists' α true → Lists' α true → Prop

Subset relation for ZFA lists. Defined inductively.

• nil {α : Type u_1} {l : Lists' α true} : Lists'.nil.Subset l
• cons {α : Type u_1} {a a' : Lists α} {l l' : Lists' α true} : a.Equiv a' → a' ∈ l'.toList → l.Subset l' → (Lists'.cons a l).Subset l'

instance Lists'.instHasSubsetTrue {α : Type u_1} : HasSubset (Lists' α true)

Equations

• Lists'.instHasSubsetTrue = { Subset := Lists'.Subset }

instance Lists'.instMembershipLists {α : Type u_1} {b : Bool} : Membership (Lists α) (Lists' α b)

ZFA prelist membership. A ZFA list is in a ZFA prelist if some element of this ZFA prelist is equivalent as a ZFA list to this ZFA list.

Equations

• Lists'.instMembershipLists = { mem := fun (l : Lists' α b) (a : Lists α) => ∃ a' ∈ l.toList, a.Equiv a' }

theorem Lists'.mem_def {α : Type u_1} {b : Bool} {a : Lists α} {l : Lists' α b} : a ∈ l ↔ ∃ a' ∈ l.toList, a.Equiv a'

@[simp]

theorem Lists'.mem_cons {α : Type u_1} {a y : Lists α} {l : Lists' α true} : a ∈ cons y l ↔ a.Equiv y ∨ a ∈ l

theorem Lists'.cons_subset {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true} : cons a l₁ ⊆ l₂ ↔ a ∈ l₂ ∧ l₁ ⊆ l₂

theorem Lists'.ofList_subset {α : Type u_1} {l₁ l₂ : List (Lists α)} (h : l₁ ⊆ l₂) : ofList l₁ ⊆ ofList l₂

theorem Lists'.Subset.refl {α : Type u_1} {l : Lists' α true} : l ⊆ l

theorem Lists'.subset_nil {α : Type u_1} {l : Lists' α true} : l ⊆ nil → l = nil

@[irreducible]

theorem Lists'.mem_of_subset' {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true} : l₁ ⊆ l₂ → a ∈ l₁.toList → a ∈ l₂

theorem Lists'.subset_def {α : Type u_1} {l₁ l₂ : Lists' α true} : l₁ ⊆ l₂ ↔ ∀ a ∈ l₁.toList, a ∈ l₂

@[match_pattern]

def Lists.atom {α : Type u_1} (a : α) : Lists α

Sends a : α to the corresponding atom in Lists α.

Equations

• Lists.atom a = ⟨false, Lists'.atom a⟩

@[match_pattern]

def Lists.of' {α : Type u_1} (l : Lists' α true) : Lists α

Converts a proper ZFA prelist to a ZFA list.

Equations

• Lists.of' l = ⟨true, l⟩

def Lists.toList {α : Type u_1} : Lists α → List (Lists α)

Converts a ZFA list to a List of ZFA lists. Atoms are sent to [].

Equations

• Lists.toList ⟨fst, l⟩ = l.toList

def Lists.IsList {α : Type u_1} (l : Lists α) : Prop

Predicate stating that a ZFA list is proper.

Equations

• l.IsList = (l.fst = true)

def Lists.ofList {α : Type u_1} (l : List (Lists α)) : Lists α

Converts a List of ZFA lists to a ZFA list.

Equations

• Lists.ofList l = Lists.of' (Lists'.ofList l)

theorem Lists.isList_toList {α : Type u_1} (l : List (Lists α)) : (ofList l).IsList

theorem Lists.to_ofList {α : Type u_1} (l : List (Lists α)) : (ofList l).toList = l

theorem Lists.of_toList {α : Type u_1} {l : Lists α} : l.IsList → ofList l.toList = l

instance Lists.instInhabited {α : Type u_1} : Inhabited (Lists α)

Equations

• Lists.instInhabited = { default := Lists.of' Lists'.nil }

instance Lists.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Lists α)

Equations

• Lists.instDecidableEq = id inferInstance

instance Lists.instSizeOf {α : Type u_1} [SizeOf α] : SizeOf (Lists α)

Equations

• Lists.instSizeOf = id inferInstance

def Lists.inductionMut {α : Type u_1} (C : Lists α → Sort u_2) (D : Lists' α true → Sort u_3) (C0 : (a : α) → C (atom a)) (C1 : (l : Lists' α true) → D l → C (of' l)) (D0 : D Lists'.nil) (D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)) : ((l : Lists α) → C l) ×' ((l : Lists' α true) → D l)

A recursion principle for pairs of ZFA lists and proper ZFA prelists.

Equations

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

def Lists.mem {α : Type u_1} (a : Lists α) : Lists α → Prop

Membership of ZFA list. A ZFA list belongs to a proper ZFA list if it belongs to the latter as a proper ZFA prelist. An atom has no members.

Equations

• a.mem ⟨false, snd⟩ = False
• a.mem ⟨fst, l⟩ = (a ∈ l)

instance Lists.instMembership {α : Type u_1} : Membership (Lists α) (Lists α)

Equations

• Lists.instMembership = { mem := fun (ls l : Lists α) => l.mem ls }

theorem Lists.isList_of_mem {α : Type u_1} {a l : Lists α} : a ∈ l → l.IsList

theorem Lists.Equiv.antisymm_iff {α : Type u_1} {l₁ l₂ : Lists' α true} : (of' l₁).Equiv (of' l₂) ↔ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

theorem Lists.equiv_atom {α : Type u_1} {a : α} {l : Lists α} : (atom a).Equiv l ↔ atom a = l

theorem Lists.Equiv.symm {α : Type u_1} {l₁ l₂ : Lists α} (h : l₁.Equiv l₂) : l₂.Equiv l₁

theorem Lists.Equiv.trans {α : Type u_1} {l₁ l₂ l₃ : Lists α} : l₁.Equiv l₂ → l₂.Equiv l₃ → l₁.Equiv l₃

instance Lists.instSetoidLists {α : Type u_1} : Setoid (Lists α)

Equations

• Lists.instSetoidLists = { r := fun (x1 x2 : Lists α) => x1.Equiv x2, iseqv := ⋯ }

theorem Lists.sizeof_pos {α : Type u_1} {b : Bool} (l : Lists' α b) : 0 < sizeOf l

theorem Lists.lt_sizeof_cons' {α : Type u_1} {b : Bool} (a : Lists' α b) (l : Lists' α true) : sizeOf ⟨b, a⟩ < sizeOf (a.cons' l)

@[irreducible]

instance Lists.Equiv.decidable {α : Type u_1} [DecidableEq α] (l₁ l₂ : Lists α) : Decidable (l₁.Equiv l₂)

Equations

• Lists.Equiv.decidable ⟨false, l₁⟩ ⟨false, l₂⟩ = decidable_of_iff' (l₁ = l₂) ⋯
• Lists.Equiv.decidable ⟨false, l₁⟩ ⟨true, l₂⟩ = isFalse ⋯
• Lists.Equiv.decidable ⟨true, l₁⟩ ⟨false, l₂⟩ = isFalse ⋯
• Lists.Equiv.decidable ⟨true, l₁⟩ ⟨true, l₂⟩ = decidable_of_iff' (l₁ ⊆ l₂ ∧ l₂ ⊆ l₁) ⋯

@[irreducible]

instance Lists.Subset.decidable {α : Type u_1} [DecidableEq α] (l₁ l₂ : Lists' α true) : Decidable (l₁ ⊆ l₂)

Equations

• Lists.Subset.decidable Lists'.nil x✝ = isTrue ⋯
• Lists.Subset.decidable (a.cons' l₁) x✝ = decidable_of_iff' (⟨b, a⟩ ∈ x✝ ∧ l₁ ⊆ x✝) ⋯

@[irreducible]

instance Lists.mem.decidable {α : Type u_1} [DecidableEq α] (a : Lists α) (l : Lists' α true) : Decidable (a ∈ l)

Equations

• Lists.mem.decidable x✝ Lists'.nil = isFalse ⋯
• Lists.mem.decidable x✝ (b_1.cons' l₂) = decidable_of_iff' (x✝.Equiv ⟨b, b_1⟩ ∨ x✝ ∈ l₂) ⋯

theorem Lists'.mem_equiv_left {α : Type u_1} {l : Lists' α true} {a a' : Lists α} : a.Equiv a' → (a ∈ l ↔ a' ∈ l)

theorem Lists'.mem_of_subset {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true} (s : l₁ ⊆ l₂) : a ∈ l₁ → a ∈ l₂

theorem Lists'.Subset.trans {α : Type u_1} {l₁ l₂ l₃ : Lists' α true} (h₁ : l₁ ⊆ l₂) (h₂ : l₂ ⊆ l₃) : l₁ ⊆ l₃

def Finsets (α : Type u_2) : Type u_2

Finsets are defined via equivalence classes of Lists

Equations

• Finsets α = Quotient Lists.instSetoidLists

instance Finsets.instEmptyCollection {α : Type u_1} : EmptyCollection (Finsets α)

Equations

• Finsets.instEmptyCollection = { emptyCollection := ⟦Lists.of' Lists'.nil⟧ }

instance Finsets.instInhabited {α : Type u_1} : Inhabited (Finsets α)

Equations

• Finsets.instInhabited = { default := ∅ }

instance Finsets.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (Finsets α)

Equations

• Finsets.instDecidableEq = id Quotient.decidableEq