Documentation

Mathlib.SetTheory.Lists

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:

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 #

inductive Lists' (α : Type u) :
BoolType 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.

Instances For
    instance instDecidableEqLists' :
    {α : Type u_2} → {a : Bool} → [inst : 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
    Instances For
      instance Lists'.instInhabited {α : Type u_1} [Inhabited α] (b : Bool) :
      Equations
      def Lists'.cons {α : Type u_1} :
      Lists αLists' α trueLists' α true

      Appending a ZFA list to a proper ZFA prelist.

      Equations
      • Lists'.cons x✝ x = match x✝, x with | fst, a, l => a.cons' l
      Instances For
        def Lists'.toList {α : Type u_1} {b : Bool} :
        Lists' α bList (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
        Instances For
          theorem Lists'.toList_cons {α : Type u_1} (a : Lists α) (l : Lists' α true) :
          (Lists'.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
          Instances For
            @[simp]
            theorem Lists'.to_ofList {α : Type u_1} (l : List (Lists α)) :
            (Lists'.ofList l).toList = l
            @[simp]
            theorem Lists'.of_toList {α : Type u_1} (l : Lists' α true) :
            Lists'.ofList l.toList = l
            inductive Lists.Equiv {α : Type u_1} :
            Lists αLists αProp

            Equivalence of ZFA lists. Defined inductively.

            Instances For
              inductive Lists'.Subset {α : Type u_1} :
              Lists' α trueLists' α trueProp

              Subset relation for ZFA lists. Defined inductively.

              Instances For
                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 (a : Lists α) (l : Lists' α b) => 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 : Lists α} {y : Lists α} {l : Lists' α true} :
                a Lists'.cons y l a.Equiv y a l
                theorem Lists'.cons_subset {α : Type u_1} {a : Lists α} {l₁ : Lists' α true} {l₂ : Lists' α true} :
                Lists'.cons a l₁ l₂ a l₂ l₁ l₂
                theorem Lists'.ofList_subset {α : Type u_1} {l₁ : List (Lists α)} {l₂ : List (Lists α)} (h : l₁ l₂) :
                theorem Lists'.Subset.refl {α : Type u_1} {l : Lists' α true} :
                l l
                theorem Lists'.subset_nil {α : Type u_1} {l : Lists' α true} :
                l Lists'.nill = Lists'.nil
                theorem Lists'.mem_of_subset' {α : Type u_1} {a : Lists α} {l₁ : Lists' α true} {l₂ : Lists' α true} :
                l₁ l₂a l₁.toLista l₂
                theorem Lists'.subset_def {α : Type u_1} {l₁ : Lists' α true} {l₂ : Lists' α true} :
                l₁ l₂ al₁.toList, a l₂
                @[match_pattern]
                def Lists.atom {α : Type u_1} (a : α) :

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

                Equations
                Instances For
                  @[match_pattern]
                  def Lists.of' {α : Type u_1} (l : Lists' α true) :

                  Converts a proper ZFA prelist to a ZFA list.

                  Equations
                  Instances For
                    def Lists.toList {α : Type u_1} :
                    Lists αList (Lists α)

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

                    Equations
                    • x.toList = match x with | fst, l => l.toList
                    Instances For
                      def Lists.IsList {α : Type u_1} (l : Lists α) :

                      Predicate stating that a ZFA list is proper.

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

                        Converts a List of ZFA lists to a ZFA list.

                        Equations
                        Instances For
                          theorem Lists.isList_toList {α : Type u_1} (l : List (Lists α)) :
                          (Lists.ofList l).IsList
                          theorem Lists.to_ofList {α : Type u_1} (l : List (Lists α)) :
                          (Lists.ofList l).toList = l
                          theorem Lists.of_toList {α : Type u_1} {l : Lists α} :
                          l.IsListLists.ofList l.toList = l
                          instance Lists.instInhabited {α : Type u_1} :
                          Equations
                          • Lists.instInhabited = { default := Lists.of' Lists'.nil }
                          instance Lists.instDecidableEq {α : Type u_1} [DecidableEq α] :
                          Equations
                          • Lists.instDecidableEq = id inferInstance
                          instance Lists.instSizeOf {α : Type u_1} [SizeOf α] :
                          Equations
                          • Lists.instSizeOf = id inferInstance
                          def Lists.inductionMut {α : Type u_1} (C : Lists αSort u_2) (D : Lists' α trueSort u_3) (C0 : (a : α) → C (Lists.atom a)) (C1 : (l : Lists' α true) → D lC (Lists.of' l)) (D0 : D Lists'.nil) (D1 : (a : Lists α) → (l : Lists' α true) → C aD lD (Lists'.cons a l)) :
                          PProd ((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.
                          Instances For
                            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 x = match x with | false, snd => False | fst, l => a l
                            Instances For
                              instance Lists.instMembership {α : Type u_1} :
                              Equations
                              • Lists.instMembership = { mem := Lists.mem }
                              theorem Lists.isList_of_mem {α : Type u_1} {a : Lists α} {l : Lists α} :
                              a ll.IsList
                              theorem Lists.Equiv.antisymm_iff {α : Type u_1} {l₁ : Lists' α true} {l₂ : Lists' α true} :
                              (Lists.of' l₁).Equiv (Lists.of' l₂) l₁ l₂ l₂ l₁
                              theorem Lists.equiv_atom {α : Type u_1} {a : α} {l : Lists α} :
                              (Lists.atom a).Equiv l Lists.atom a = l
                              theorem Lists.Equiv.symm {α : Type u_1} {l₁ : Lists α} {l₂ : Lists α} (h : l₁.Equiv l₂) :
                              l₂.Equiv l₁
                              theorem Lists.Equiv.trans {α : Type u_1} {l₁ : Lists α} {l₂ : Lists α} {l₃ : Lists α} :
                              l₁.Equiv l₂l₂.Equiv l₃l₁.Equiv l₃
                              instance Lists.instSetoidLists {α : Type u_1} :
                              Equations
                              • Lists.instSetoidLists = { r := fun (x x_1 : Lists α) => x.Equiv x_1, iseqv := }
                              @[deprecated]
                              def Lists.Equiv.decidableMeas {α : Type u_1} :
                              (_ : Lists α) ×' Lists α ⊕' (_ : Lists' α true) ×' Lists' α true ⊕' (_ : Lists α) ×' Lists' α true

                              Auxiliary function to prove termination of decidability checking

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                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)
                                instance Lists.Equiv.decidable {α : Type u_1} [DecidableEq α] (l₁ : Lists α) (l₂ : Lists α) :
                                Decidable (l₁.Equiv l₂)
                                Equations
                                instance Lists.Subset.decidable {α : Type u_1} [DecidableEq α] (l₁ : Lists' α true) (l₂ : Lists' α true) :
                                Decidable (l₁ l₂)
                                Equations
                                instance Lists.mem.decidable {α : Type u_1} [DecidableEq α] (a : Lists α) (l : Lists' α true) :
                                Equations
                                theorem Lists'.mem_equiv_left {α : Type u_1} {l : Lists' α true} {a : Lists α} {a' : Lists α} :
                                a.Equiv a'(a l a' l)
                                theorem Lists'.mem_of_subset {α : Type u_1} {a : Lists α} {l₁ : Lists' α true} {l₂ : Lists' α true} (s : l₁ l₂) :
                                a l₁a l₂
                                theorem Lists'.Subset.trans {α : Type u_1} {l₁ : Lists' α true} {l₂ : Lists' α true} {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
                                Instances For
                                  Equations
                                  • Finsets.instEmptyCollection = { emptyCollection := Lists.of' Lists'.nil }
                                  instance Finsets.instInhabited {α : Type u_1} :
                                  Equations
                                  • Finsets.instInhabited = { default := }
                                  Equations
                                  • Finsets.instDecidableEq = id Quotient.decidableEq