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' α ff
: Atoms as ZFA prelists. Basically a copy ofα
.lists' α tt
: 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.
TODO #
The next step is to define ZFA sets as lists quotiented by lists.equiv
.
(
- atom : Π {α : Type u}, α → lists' α bool.ff
- nil : Π {α : Type u}, lists' α bool.tt
- cons' : Π {α : Type u} {b : bool}, lists' α b → lists' α bool.tt → lists' α bool.tt
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'
- lists'.has_sizeof_inst
- lists'.inhabited
- lists'.has_subset
- lists'.has_mem
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.
Instances for lists
Equations
Converts a list
of ZFA lists to a proper ZFA prelist.
Equations
- lists'.of_list (a :: l) = lists'.cons a (lists'.of_list l)
- lists'.of_list list.nil = lists'.nil
Equations
- lists'.has_subset = {subset := lists'.subset α}
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.
Sends a : α
to the corresponding atom in lists α
.
Equations
- lists.atom a = ⟨bool.ff, lists'.atom a⟩
Converts a ZFA list to a list
of ZFA lists. Atoms are sent to []
.
Equations
- lists.to_list ⟨b, l⟩ = l.to_list
Converts a list
of ZFA lists to a ZFA list.
Equations
Equations
Equations
- lists.decidable_eq = lists.decidable_eq._proof_1.mpr (λ (a b : Σ (b : bool), lists' α b), sigma.decidable_eq a b)
Equations
- lists.has_sizeof = lists.has_sizeof._proof_1.mpr (sigma.has_sizeof bool (λ (b : bool), lists' α b))
A recursion principle for pairs of ZFA lists and proper ZFA prelists.
Equations
- lists.induction_mut C D C0 C1 D0 D1 = ⟨λ (_x : lists α), lists.induction_mut._match_2 C D (λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α bool.tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨bool.tt, l⟩) (lists.induction_mut._match_1 D bool.tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) _x, λ (l : lists' α bool.tt), ((λ (b : bool) (l : lists' α b), lists'.rec (λ (a : α), ⟨C0 a, punit.star⟩) ⟨C1 lists'.nil D0, D0⟩ (λ {b : bool} (a : lists' α b) (l : lists' α bool.tt) (IH₁ : pprod (C ⟨b, a⟩) (lists.induction_mut._match_1 D b a)) (IH₂ : pprod (C ⟨bool.tt, l⟩) (lists.induction_mut._match_1 D bool.tt l)), ⟨C1 (a.cons' l) (D1 ⟨b, a⟩ l IH₁.fst IH₂.snd), D1 ⟨b, a⟩ l IH₁.fst IH₂.snd⟩) l) bool.tt l).snd⟩
- lists.induction_mut._match_2 C D this ⟨b, l⟩ = (this l).fst
- lists.induction_mut._match_1 D bool.tt l = D l
- lists.induction_mut._match_1 D bool.ff l = punit
Equations
- lists.has_mem = {mem := lists.mem α}
Equations
- lists.setoid = {r := lists.equiv α, iseqv := _}
Equations
- lists.mem.decidable a (b.cons' l₂) = decidable_of_iff' (a.equiv ⟨a_20, b⟩ ∨ a ∈ l₂) _
- lists.mem.decidable a lists'.nil = decidable.is_false _
Equations
- lists.subset.decidable (a.cons' l₁) l₂ = decidable_of_iff' (⟨b, a⟩ ∈ l₂ ∧ l₁ ⊆ l₂) _
- lists.subset.decidable lists'.nil l₂ = decidable.is_true lists'.subset.nil
Equations
Instances for finsets
Equations
Equations
- finsets.inhabited = {default := ∅}
Equations
- finsets.decidable_eq = finsets.decidable_eq._proof_1.mpr (λ (a b : quotient lists.setoid), quotient.decidable_eq a b)