mathlib3 documentation

set_theory.lists

A computable model of ZFA without infinity #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

We distinguish two kinds of ZFA lists:

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:

Main declarations #

@[protected, instance]
def lists'.decidable_eq (α : Type u) [a : decidable_eq α] (ᾰ : bool) :
inductive lists' (α : Type u) :

Prelists, helper type to define lists. lists' α ff are the "atoms", a copy of α. lists' α tt 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.

Instances for lists'
def lists (α : Type u_1) :
Type u_1

Hereditarily finite list, aka ZFA list. A ZFA list is either an "atom" (b = ff), 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
Instances for lists
def lists'.cons {α : Type u_1} :

Appending a ZFA list to a proper ZFA prelist.

Equations
@[simp]
def lists'.to_list {α : Type u_1} {b : bool} :
lists' α b list (lists α)

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

Equations
@[simp]
theorem lists'.to_list_cons {α : Type u_1} (a : lists α) (l : lists' α bool.tt) :
@[simp]
def lists'.of_list {α : Type u_1} :

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

Equations
@[simp]
theorem lists'.to_of_list {α : Type u_1} (l : list (lists α)) :
@[simp]
theorem lists'.of_to_list {α : Type u_1} (l : lists' α bool.tt) :
@[protected, instance]
Equations
@[protected, instance]
def lists'.has_mem {α : Type u_1} {b : bool} :
has_mem (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
theorem lists'.mem_def {α : Type u_1} {b : bool} {a : lists α} {l : lists' α b} :
a l (a' : lists α) (H : a' l.to_list), a.equiv a'
@[simp]
theorem lists'.mem_cons {α : Type u_1} {a y : lists α} {l : lists' α bool.tt} :
a lists'.cons y l a.equiv y a l
theorem lists'.cons_subset {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α bool.tt} :
lists'.cons a l₁ l₂ a l₂ l₁ l₂
theorem lists'.of_list_subset {α : Type u_1} {l₁ l₂ : list (lists α)} (h : l₁ l₂) :
theorem lists'.subset_nil {α : Type u_1} {l : lists' α bool.tt} :
theorem lists'.mem_of_subset' {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α bool.tt} (s : l₁ l₂) (h : a l₁.to_list) :
a l₂
theorem lists'.subset_def {α : Type u_1} {l₁ l₂ : lists' α bool.tt} :
l₁ l₂ (a : lists α), a l₁.to_list a l₂
def lists.atom {α : Type u_1} (a : α) :

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

Equations
def lists.of' {α : Type u_1} (l : lists' α bool.tt) :

Converts a proper ZFA prelist to a ZFA list.

Equations
@[simp]
def lists.to_list {α : Type u_1} :

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

Equations
def lists.is_list {α : Type u_1} (l : lists α) :
Prop

Predicate stating that a ZFA list is proper.

Equations
def lists.of_list {α : Type u_1} (l : list (lists α)) :

Converts a list of ZFA lists to a ZFA list.

Equations
theorem lists.is_list_to_list {α : Type u_1} (l : list (lists α)) :
theorem lists.to_of_list {α : Type u_1} (l : list (lists α)) :
theorem lists.of_to_list {α : Type u_1} {l : lists α} :
@[protected, instance]
def lists.inhabited {α : Type u_1} :
Equations
@[protected, instance]
def lists.decidable_eq {α : Type u_1} [decidable_eq α] :
Equations
@[protected, instance]
def lists.has_sizeof {α : Type u_1} [has_sizeof α] :
Equations
def lists.induction_mut {α : Type u_1} (C : lists α Sort u_2) (D : lists' α bool.tt Sort u_3) (C0 : Π (a : α), C (lists.atom a)) (C1 : Π (l : lists' α bool.tt), D l C (lists.of' l)) (D0 : D lists'.nil) (D1 : Π (a : lists α) (l : lists' α bool.tt), C a D l D (lists'.cons a l)) :
pprod (Π (l : lists α), C l) (Π (l : lists' α bool.tt), D l)

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

Equations
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
@[protected, instance]
def lists.has_mem {α : Type u_1} :
has_mem (lists α) (lists α)
Equations
theorem lists.is_list_of_mem {α : Type u_1} {a l : lists α} :
theorem lists.equiv_atom {α : Type u_1} {a : α} {l : lists α} :
(lists.atom a).equiv l lists.atom a = l
@[protected, instance]
def lists.setoid {α : Type u_1} :
Equations
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' α bool.tt) :
sizeof b, a⟩ < sizeof (a.cons' l)
@[instance]
def lists.mem.decidable {α : Type u_1} [decidable_eq α] (a : lists α) (l : lists' α bool.tt) :
Equations
@[instance]
def lists.subset.decidable {α : Type u_1} [decidable_eq α] (l₁ l₂ : lists' α bool.tt) :
decidable (l₁ l₂)
Equations
theorem lists'.mem_equiv_left {α : Type u_1} {l : lists' α bool.tt} {a a' : lists α} :
a.equiv a' (a l a' l)
theorem lists'.mem_of_subset {α : Type u_1} {a : lists α} {l₁ l₂ : lists' α bool.tt} (s : l₁ l₂) :
a l₁ a l₂
def finsets (α : Type u_1) :
Type u_1
Equations
Instances for finsets
@[protected, instance]
def finsets.has_emptyc {α : Type u_1} :
Equations
@[protected, instance]
def finsets.inhabited {α : Type u_1} :
Equations
@[protected, instance]
Equations