Documentation

Batteries.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 Batteries.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.instDecidableEq_batteries :
{α : Type u_1} → {β : Type u_2} → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (α β)
Equations
  • Sum.instDecidableEq_batteries = Sum.decEqSum✝
instance Sum.instBEq_batteries :
{α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst : BEq β] → BEq (α β)
Equations
  • Sum.instBEq_batteries = { beq := Sum.beqSum✝ }
def Sum.isLeft {α : Type u_1} {β : Type u_2} :
α βBool

Check if a sum is inl.

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

    Check if a sum is inr.

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

      Retrieve 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β

        Retrieve the contents from a sum known to be inr.

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

          Define a function on α ⊕ β by giving separate definitions on α and β.

          Equations
          Instances For
            @[simp]
            theorem Sum.elim_inl {α : Type u_1} {γ : Sort u_2} {β : Type u_3} (f : αγ) (g : βγ) (x : α) :
            Sum.elim f g (Sum.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 (Sum.inr x) = g x
            def Sum.map {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : αα') (g : ββ') :
            α βα' β'

            Map α ⊕ β 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 (Sum.inl x) = Sum.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 (Sum.inr x) = Sum.inr (g x)
              def Sum.swap {α : Type u_1} {β : Type u_2} :
              α ββ α

              Swap the factors of a sum type

              Equations
              Instances For
                @[simp]
                theorem Sum.swap_inl {α : Type u_1} {β : Type u_2} {x : α} :
                (Sum.inl x).swap = Sum.inr x
                @[simp]
                theorem Sum.swap_inr {α : Type u_1} {β : Type u_2} {x : β} :
                (Sum.inr x).swap = Sum.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 : γ}, Sum.LiftRel r s (Sum.inl a) (Sum.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 : δ}, ¬Sum.LiftRel r s (Sum.inl a) (Sum.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 : γ}, ¬Sum.LiftRel r s (Sum.inr b) (Sum.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 : δ}, Sum.LiftRel r s (Sum.inr b) (Sum.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 : γ δ) :
                  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 β.

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