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 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 : {α : Type u_1} → {β : Type u_2} → [inst : DecidableEq α] → [inst : DecidableEq β] → DecidableEq (α ⊕ β)

Equations

• Sum.instDecidableEq = Sum.decEqSum✝

instance Sum.instBEq : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst : BEq β] → BEq (α ⊕ β)

Equations

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

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

Check if a sum is inl.

Equations

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

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

Check if a sum is 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 → α

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

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

Check if a sum is inl and if so, retrieve its contents.

Equations

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

def Sum.getRight? {α : Type u_1} {β : Type u_2} : α ⊕ β → Option β

Check if a sum is inr and if so, retrieve 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 : α} : (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

• 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 (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

• 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 (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

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

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

• inl: ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ}, r a c → Sum.LiftRel r s (Sum.inl a) (Sum.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 → Sum.LiftRel r s (Sum.inr b) (Sum.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 : γ}, 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 : γ ⊕ δ) : Decidable (Sum.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₂ : α}, r a₁ a₂ → Sum.Lex r s (Sum.inl a₁) (Sum.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₂ : β}, s b₁ b₂ → Sum.Lex r s (Sum.inr b₁) (Sum.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 : β), Sum.Lex r s (Sum.inl a) (Sum.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₂ : α}, 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 → α_1 → Prop} → [inst : DecidableRel r] → [inst : DecidableRel s] → DecidableRel (Sum.Lex r s)

Equations

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