Documentation

Init.Data.Sum.Basic

Disjoint union of types #

This file defines basic operations on the the sum type α ⊕ β.

α ⊕ β is the type made of a copy of α and a copy of β. It is also called disjoint union.

Main declarations #

Further material #

See Init.Data.Sum.Lemmas for theorems about these definitions.

Notes #

The definition of Sum takes values in Type _. This effectively forbids Prop- valued sum types. To this effect, we have PSum, which takes value in Sort _ and carries a more complicated universe signature in consequence. The Prop version is Or.

instance Sum.instBEq {α✝ : Type u_1} {β✝ : Type u_2} [BEq α✝] [BEq β✝] :
BEq (α✝ β✝)
Equations
    def Sum.isLeft {α : Type u_1} {β : Type u_2} :
    α βBool

    Checks whether a sum is the left injection inl.

    Equations
      Instances For
        def Sum.isRight {α : Type u_1} {β : Type u_2} :
        α βBool

        Checks whether a sum is the right injection inr.

        Equations
          Instances For
            def Sum.getLeft {α : Type u_1} {β : Type u_2} (ab : α β) :
            ab.isLeft = trueα

            Retrieves the contents from a sum known to be inl.

            Equations
              Instances For
                def Sum.getRight {α : Type u_1} {β : Type u_2} (ab : α β) :
                ab.isRight = trueβ

                Retrieves the contents from a sum known to be inr.

                Equations
                  Instances For
                    def Sum.getLeft? {α : Type u_1} {β : Type u_2} :
                    α βOption α

                    Checks whether a sum is the left injection inl and, if so, retrieves its contents.

                    Equations
                      Instances For
                        def Sum.getRight? {α : Type u_1} {β : Type u_2} :
                        α βOption β

                        Checks whether a sum is the right injection inr and, if so, retrieves its contents.

                        Equations
                          Instances For
                            @[simp]
                            theorem Sum.isLeft_inl {α : Type u_1} {β : Type u_2} {x : α} :
                            @[simp]
                            theorem Sum.isLeft_inr {α : Type u_1} {β : Type u_2} {x : β} :
                            @[simp]
                            theorem Sum.isRight_inl {α : Type u_1} {β : Type u_2} {x : α} :
                            @[simp]
                            theorem Sum.isRight_inr {α : Type u_1} {β : Type u_2} {x : β} :
                            @[simp]
                            theorem Sum.getLeft_inl {α : Type u_1} {β : Type u_2} {x : α} (h : (inl x).isLeft = true) :
                            (inl x).getLeft h = x
                            @[simp]
                            theorem Sum.getRight_inr {α : Type u_1} {β : Type u_2} {x : β} (h : (inr x).isRight = true) :
                            (inr x).getRight h = x
                            @[simp]
                            theorem Sum.getLeft?_inl {α : Type u_1} {β : Type u_2} {x : α} :
                            @[simp]
                            theorem Sum.getLeft?_inr {α : Type u_1} {β : Type u_2} {x : β} :
                            @[simp]
                            theorem Sum.getRight?_inl {α : Type u_1} {β : Type u_2} {x : α} :
                            @[simp]
                            theorem Sum.getRight?_inr {α : Type u_1} {β : Type u_2} {x : β} :
                            def Sum.elim {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : αγ) (g : βγ) :
                            α βγ

                            Case analysis for sums that applies the appropriate function f or g after checking which constructor is present.

                            Equations
                              Instances For
                                @[simp]
                                theorem Sum.elim_inl {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) (x : α) :
                                Sum.elim f g (inl x) = f x
                                @[simp]
                                theorem Sum.elim_inr {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) (x : β) :
                                Sum.elim f g (inr x) = g x
                                def Sum.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') :
                                α βα' β'

                                Transforms a sum according to functions on each type.

                                This function maps α ⊕ β to α' ⊕ β', sending α to α' and β to β'.

                                Equations
                                  Instances For
                                    @[simp]
                                    theorem Sum.map_inl {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') (x : α) :
                                    Sum.map f g (inl x) = inl (f x)
                                    @[simp]
                                    theorem Sum.map_inr {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') (x : β) :
                                    Sum.map f g (inr x) = inr (g x)
                                    def Sum.swap {α : Type u_1} {β : Type u_2} :
                                    α ββ α

                                    Swaps the factors of a sum type.

                                    The constructor Sum.inl is replaced with Sum.inr, and vice versa.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem Sum.swap_inl {α : Type u_1} {β : Type u_2} {x : α} :
                                        (inl x).swap = inr x
                                        @[simp]
                                        theorem Sum.swap_inr {α : Type u_1} {β : Type u_2} {x : β} :
                                        (inr x).swap = inl x
                                        inductive Sum.LiftRel {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} (r : αγProp) (s : βδProp) :
                                        α βγ δProp

                                        Lifts pointwise two relations between α and γ and between β and δ to a relation between α ⊕ β and γ ⊕ δ.

                                        Instances For
                                          @[simp]
                                          theorem Sum.liftRel_inl_inl {α✝ : Type u_1} {γ✝ : Type u_2} {r : α✝γ✝Prop} {β✝ : Type u_3} {δ✝ : Type u_4} {s : β✝δ✝Prop} {a : α✝} {c : γ✝} :
                                          LiftRel r s (inl a) (inl c) r a c
                                          @[simp]
                                          theorem Sum.not_liftRel_inl_inr {α✝ : Type u_1} {γ✝ : Type u_2} {r : α✝γ✝Prop} {β✝ : Type u_3} {δ✝ : Type u_4} {s : β✝δ✝Prop} {a : α✝} {d : δ✝} :
                                          ¬LiftRel r s (inl a) (inr d)
                                          @[simp]
                                          theorem Sum.not_liftRel_inr_inl {α✝ : Type u_1} {γ✝ : Type u_2} {r : α✝γ✝Prop} {β✝ : Type u_3} {δ✝ : Type u_4} {s : β✝δ✝Prop} {b : β✝} {c : γ✝} :
                                          ¬LiftRel r s (inr b) (inl c)
                                          @[simp]
                                          theorem Sum.liftRel_inr_inr {α✝ : Type u_1} {γ✝ : Type u_2} {r : α✝γ✝Prop} {β✝ : Type u_3} {δ✝ : Type u_4} {s : β✝δ✝Prop} {b : β✝} {d : δ✝} :
                                          LiftRel r s (inr b) (inr d) s b d
                                          instance Sum.instDecidableLiftRel {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : αγProp} {s : βδProp} [(a : α) → (c : γ) → Decidable (r a c)] [(b : β) → (d : δ) → Decidable (s b d)] (ab : α β) (cd : γ δ) :
                                          Decidable (LiftRel r s ab cd)
                                          Equations
                                            inductive Sum.Lex {α : Type u_1} {β : Type u_2} (r : ααProp) (s : ββProp) :
                                            α βα βProp

                                            Lexicographic order for sum. Sort all the inl a before the inr b, otherwise use the respective order on α or β.

                                            • inl {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {a₁ a₂ : α} (h : r a₁ a₂) : Lex r s (inl a₁) (inl a₂)

                                              inl a₁ and inl a₂ are related via Lex r s if a₁ and a₂ are related via r.

                                            • inr {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} {b₁ b₂ : β} (h : s b₁ b₂) : Lex r s (inr b₁) (inr b₂)

                                              inr b₁ and inr b₂ are related via Lex r s if b₁ and b₂ are related via s.

                                            • sep {α : Type u_1} {β : Type u_2} {r : ααProp} {s : ββProp} (a : α) (b : β) : Lex r s (inl a) (inr b)

                                              inl a and inr b are always related via Lex r s.

                                            Instances For
                                              @[simp]
                                              theorem Sum.lex_inl_inl {α✝ : Type u_1} {r : α✝α✝Prop} {β✝ : Type u_2} {s : β✝β✝Prop} {a₁ a₂ : α✝} :
                                              Lex r s (inl a₁) (inl a₂) r a₁ a₂
                                              @[simp]
                                              theorem Sum.lex_inr_inr {α✝ : Type u_1} {r : α✝α✝Prop} {β✝ : Type u_2} {s : β✝β✝Prop} {b₁ b₂ : β✝} :
                                              Lex r s (inr b₁) (inr b₂) s b₁ b₂
                                              @[simp]
                                              theorem Sum.lex_inr_inl {α✝ : Type u_1} {r : α✝α✝Prop} {β✝ : Type u_2} {s : β✝β✝Prop} {b : β✝} {a : α✝} :
                                              ¬Lex r s (inr b) (inl a)
                                              instance Sum.instDecidableRelSumLex {α✝ : Type u_1} {r : α✝α✝Prop} {α✝¹ : Type u_2} {s : α✝¹α✝¹Prop} [DecidableRel r] [DecidableRel s] :
                                              Equations