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

• Sum.isLeft: Returns whether x : α ⊕ β comes from the left component or not.
• Sum.isRight: Returns whether x : α ⊕ β comes from the right component or not.
• Sum.getLeft: Retrieves the left content of a x : α ⊕ β that is known to come from the left.
• Sum.getRight: Retrieves the right content of x : α ⊕ β that is known to come from the right.
• Sum.getLeft?: Retrieves the left content of x : α ⊕ β as an option type or returns none if it's coming from the right.
• Sum.getRight?: Retrieves the right content of x : α ⊕ β as an option type or returns none if it's coming from the left.
• Sum.map: Maps α ⊕ β to γ ⊕ δ component-wise.
• Sum.elim: Nondependent eliminator/induction principle for α ⊕ β.
• Sum.swap: Maps α ⊕ β to β ⊕ α by swapping components.
• Sum.LiftRel: The disjoint union of two relations.
• Sum.Lex: Lexicographic order on α ⊕ β induced by a relation on α and a relation on β.

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

• Sum.instBEq = { beq := Sum.beqSum✝ }

def Sum.isLeft {α : Type u_1} {β : Type u_2} : α ⊕ β → Bool

Checks whether a sum is the left injection inl.

Equations

• (Sum.inl val).isLeft = true
• (Sum.inr val).isLeft = false

def Sum.isRight {α : Type u_1} {β : Type u_2} : α ⊕ β → Bool

Checks whether a sum is the right injection inr.

Equations

• (Sum.inl val).isRight = false
• (Sum.inr val).isRight = true

def Sum.getLeft {α : Type u_1} {β : Type u_2} (ab : α ⊕ β) : ab.isLeft = true → α

Retrieves the contents from a sum known to be inl.

Equations

• (Sum.inl a).getLeft x_2 = a

def Sum.getRight {α : Type u_1} {β : Type u_2} (ab : α ⊕ β) : ab.isRight = true → β

Retrieves the contents from a sum known to be inr.

Equations

• (Sum.inr b).getRight x_2 = b

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

• (Sum.inl val).getLeft? = some val
• (Sum.inr val).getLeft? = none

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

• (Sum.inr b).getRight? = some b
• (Sum.inl val).getRight? = none

@[simp]

theorem Sum.isLeft_inl {α : Type u_1} {β : Type u_2} {x : α} : (inl x).isLeft = true

@[simp]

theorem Sum.isLeft_inr {α : Type u_1} {β : Type u_2} {x : β} : (inr x).isLeft = false

@[simp]

theorem Sum.isRight_inl {α : Type u_1} {β : Type u_2} {x : α} : (inl x).isRight = false

@[simp]

theorem Sum.isRight_inr {α : Type u_1} {β : Type u_2} {x : β} : (inr x).isRight = true

@[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 : α} : (inl x).getLeft? = some x

@[simp]

theorem Sum.getLeft?_inr {α : Type u_1} {β : Type u_2} {x : β} : (inr x).getLeft? = none

@[simp]

theorem Sum.getRight?_inl {α : Type u_1} {β : Type u_2} {x : α} : (inl x).getRight? = none

@[simp]

theorem Sum.getRight?_inr {α : Type u_1} {β : Type u_2} {x : β} : (inr x).getRight? = some 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

• Sum.elim f g x = Sum.casesOn x f g

@[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

• Sum.map f g = Sum.elim (Sum.inl ∘ f) (Sum.inr ∘ g)

@[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

• Sum.swap = Sum.elim Sum.inr Sum.inl

@[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 γ ⊕ δ.

• inl {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ} : r a c → LiftRel r s (inl a) (inl c)

  inl a and inl c are related via LiftRel r s if a and c are related via r.

• inr {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {b : β} {d : δ} : s b d → LiftRel r s (inr b) (inr d)

  inr b and inr d are related via LiftRel r s if b and d are related via s.

@[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

• (Sum.inl val).instDecidableLiftRel (Sum.inl val_1) = decidable_of_iff' (r val val_1) ⋯
• (Sum.inl val).instDecidableLiftRel (Sum.inr val_1) = isFalse ⋯
• (Sum.inr val).instDecidableLiftRel (Sum.inl val_1) = isFalse ⋯
• (Sum.inr val).instDecidableLiftRel (Sum.inr val_1) = decidable_of_iff' (s val val_1) ⋯

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.

@[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] : DecidableRel (Lex r s)

Equations

• (Sum.inl val).instDecidableRelSumLex (Sum.inl val_1) = decidable_of_iff' (r val val_1) ⋯
• (Sum.inl val).instDecidableRelSumLex (Sum.inr val_1) = isTrue ⋯
• (Sum.inr val).instDecidableRelSumLex (Sum.inl val_1) = isFalse ⋯
• (Sum.inr val).instDecidableRelSumLex (Sum.inr val_1) = decidable_of_iff' (s val val_1) ⋯