Mathlib.Data.Part

Part structure

(α : Type u)

Full source

/-- `Part α` is the type of "partial values" of type `α`. It
  is similar to `Option α` except the domain condition can be an
  arbitrary proposition, not necessarily decidable. -/
structure Part.{u} (α : Type u) : Type u where
  /-- The domain of a partial value -/
  Dom : Prop
  /-- Extract a value from a partial value given a proof of `Dom` -/
  get : Dom → α

Partial Values of a Type

Informal description

The structure `Part α` represents partial values of type `α`, where each partial value consists of a proposition `Dom` (the domain) and a function `get : Dom → α` (the value). Unlike `Option α`, the domain does not need to be decidable. A partial value can be thought of as a value that exists conditionally on its domain being true.

Part.toOption definition

(o : Part α) [Decidable o.Dom] : Option α

Full source

/-- Convert a `Part α` with a decidable domain to an option -/
def toOption (o : Part α) [Decidable o.Dom] : Option α :=
  if h : Dom o then some (o.get h) else none

Conversion from partial value to option

Informal description

Given a partial value `o : Part α` with a decidable domain, the function converts `o` to an `Option α` by returning `some (o.get h)` if the domain is true (with proof `h`), and `none` otherwise.

Part.toOption_isSome theorem

(o : Part α) [Decidable o.Dom] : o.toOption.isSome ↔ o.Dom

Full source

@[simp] lemma toOption_isSome (o : Part α) [Decidable o.Dom] : o.toOption.isSome ↔ o.Dom := by
  by_cases h : o.Dom <;> simp [h, toOption]

Non-emptiness of Partial-to-Option Conversion ↔ Domain Condition

Informal description

For any partial value $o : \text{Part}\,\alpha$ with a decidable domain, the option obtained by converting $o$ is non-empty (i.e., $\text{toOption}\,o$ is $\text{some}\,a$ for some $a$) if and only if the domain of $o$ holds.

Part.toOption_eq_none theorem

(o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom

Full source

@[simp] lemma toOption_eq_none (o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom := by
  by_cases h : o.Dom <;> simp [h, toOption]

Partial-to-Option Conversion Yields None if and only if Domain is False

Informal description

For a partial value $o : \text{Part}\,\alpha$ with a decidable domain, the conversion of $o$ to an option yields `none` if and only if the domain of $o$ does not hold, i.e., $o.\text{toOption} = \text{none} \leftrightarrow \neg o.\text{Dom}$.

Part.ext' theorem

: ∀ {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ h₁ h₂, o.get h₁ = p.get h₂) → o = p

Full source

/-- `Part` extensionality -/
theorem ext' : ∀ {o p : Part α}, (o.Dom ↔ p.Dom) → (∀ h₁ h₂, o.get h₁ = p.get h₂) → o = p
  | ⟨od, o⟩, ⟨pd, p⟩, H1, H2 => by
    have t : od = pd := propext H1
    cases t; rw [show o = p from funext fun p => H2 p p]

Extensionality of Partial Values

Informal description

For any two partial values $o$ and $p$ of type $\alpha$, if their domains are equivalent (i.e., $o.\text{Dom} \leftrightarrow p.\text{Dom}$) and for any proofs $h_1$ of $o.\text{Dom}$ and $h_2$ of $p.\text{Dom}$ their values are equal ($o.\text{get}(h_1) = p.\text{get}(h_2)$), then $o = p$.

Part.eta theorem

: ∀ o : Part α, (⟨o.Dom, fun h => o.get h⟩ : Part α) = o

Full source

/-- `Part` eta expansion -/
@[simp]
theorem eta : ∀ o : Part α, (⟨o.Dom, fun h => o.get h⟩ : Part α) = o
  | ⟨_, _⟩ => rfl

Eta Expansion for Partial Values

Informal description

For any partial value $o$ of type $\alpha$, the partial value constructed with domain $o.\text{Dom}$ and value function $\lambda h, o.\text{get}(h)$ is equal to $o$ itself.

Part.Mem definition

(o : Part α) (a : α) : Prop

Full source

/-- `a ∈ o` means that `o` is defined and equal to `a` -/
protected def Mem (o : Part α) (a : α) : Prop :=
  ∃ h, o.get h = a

Membership in partial values

Informal description

For a partial value $o$ of type $\alpha$ and an element $a$ of $\alpha$, the relation $a \in o$ holds if and only if $o$ is defined (i.e., $o.\text{Dom}$ is true) and the value of $o$ equals $a$. Formally, this means there exists a proof $h$ of $o.\text{Dom}$ such that $o.\text{get}(h) = a$.

Part.instMembership instance

: Membership α (Part α)

Full source

instance : Membership α (Part α) :=
  ⟨Part.Mem⟩

Membership Relation for Partial Values

Informal description

For any type $\alpha$, the partial values $\mathrm{Part}\,\alpha$ can be equipped with a membership relation where $a \in o$ holds if and only if the partial value $o$ is defined (i.e., its domain is true) and its value equals $a$.

Part.mem_eq theorem

(a : α) (o : Part α) : (a ∈ o) = ∃ h, o.get h = a

Full source

theorem mem_eq (a : α) (o : Part α) : (a ∈ o) = ∃ h, o.get h = a :=
  rfl

Membership in Partial Values is Equivalent to Existence of Proof and Value

Informal description

For any element $a$ of type $\alpha$ and any partial value $o$ of type $\mathrm{Part}\,\alpha$, the statement $a \in o$ is equivalent to the existence of a proof $h$ of $o.\text{Dom}$ such that the value of $o$ at $h$ equals $a$. Formally, this is expressed as: $$ (a \in o) \iff (\exists h : o.\text{Dom}, o.\text{get}(h) = a). $$

Part.dom_iff_mem theorem

: ∀ {o : Part α}, o.Dom ↔ ∃ y, y ∈ o

Full source

theorem dom_iff_mem : ∀ {o : Part α}, o.Dom ↔ ∃ y, y ∈ o
  | ⟨_, f⟩ => ⟨fun h => ⟨f h, h, rfl⟩, fun ⟨_, h, rfl⟩ => h⟩

Domain of Partial Value is Equivalent to Existence of Member

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$, the domain of $o$ is true if and only if there exists an element $y \in \alpha$ such that $y \in o$ (i.e., $o$ is defined and its value equals $y$).

Part.get_mem theorem

{o : Part α} (h) : get o h ∈ o

Full source

theorem get_mem {o : Part α} (h) : getget o h ∈ o :=
  ⟨_, rfl⟩

Value of Partial Element Belongs to Itself

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$ and any proof $h$ of its domain $o.\mathrm{Dom}$, the value $o.\mathrm{get}\,h$ belongs to $o$ (i.e., $o.\mathrm{get}\,h \in o$ holds).

Part.mem_mk_iff theorem

{p : Prop} {o : p → α} {a : α} : a ∈ Part.mk p o ↔ ∃ h, o h = a

Full source

@[simp]
theorem mem_mk_iff {p : Prop} {o : p → α} {a : α} : a ∈ Part.mk p oa ∈ Part.mk p o ↔ ∃ h, o h = a :=
  Iff.rfl

Membership Condition for Constructed Partial Value

Informal description

For any proposition $p$, function $o : p \to \alpha$, and element $a \in \alpha$, the statement $a \in \mathrm{Part.mk}\,p\,o$ holds if and only if there exists a proof $h$ of $p$ such that $o\,h = a$.

Part.ext theorem

{o p : Part α} (H : ∀ a, a ∈ o ↔ a ∈ p) : o = p

Full source

/-- `Part` extensionality -/
@[ext]
theorem ext {o p : Part α} (H : ∀ a, a ∈ oa ∈ o ↔ a ∈ p) : o = p :=
  (ext' ⟨fun h => ((H _).1 ⟨h, rfl⟩).fst, fun h => ((H _).2 ⟨h, rfl⟩).fst⟩) fun _ _ =>
    ((H _).2 ⟨_, rfl⟩).snd

Extensionality of Partial Values via Membership

Informal description

For any two partial values $o$ and $p$ of type $\alpha$, if for every element $a \in \alpha$ we have $a \in o$ if and only if $a \in p$, then $o = p$. Here, $a \in o$ means that $o$ is defined (i.e., $o.\text{Dom}$ holds) and its value equals $a$.

Part.none definition

: Part α

Full source

/-- The `none` value in `Part` has a `False` domain and an empty function. -/
def none : Part α :=
  ⟨False, False.rec⟩

Undefined partial value (`none`)

Informal description

The partial value `none` of type `Part α` has a domain that is always false (i.e., it is never defined) and an empty function (since the domain is false, no value can be extracted).

Part.instInhabited instance

: Inhabited (Part α)

Full source

instance : Inhabited (Part α) :=
  ⟨none⟩

Inhabitedness of Partial Values

Informal description

For any type $\alpha$, the type $\mathrm{Part}\,\alpha$ of partial values of $\alpha$ is inhabited.

Part.not_mem_none theorem

(a : α) : a ∉ @none α

Full source

@[simp]
theorem not_mem_none (a : α) : a ∉ @none α := fun h => h.fst

No Element Belongs to Undefined Partial Value

Informal description

For any element $a$ of type $\alpha$, $a$ is not a member of the undefined partial value `none` (i.e., $a \notin \text{none}$).

Part.some definition

(a : α) : Part α

Full source

/-- The `some a` value in `Part` has a `True` domain and the
  function returns `a`. -/
def some (a : α) : Part α :=
  ⟨True, fun _ => a⟩

Partial value with true domain

Informal description

The partial value `some a` of type `Part α` has a domain that is always true (i.e., `Dom` is `True`), and its value function returns the element `a` for any proof of the domain.

Part.some_dom theorem

(a : α) : (some a).Dom

Full source

@[simp]
theorem some_dom (a : α) : (some a).Dom :=
  trivial

Domain of Partial Value $\text{some } a$ is Defined

Informal description

For any element $a$ of type $\alpha$, the partial value $\text{some } a$ has a defined domain (i.e., $(\text{some } a).\text{Dom}$ holds).

Part.mem_unique theorem

: ∀ {a b : α} {o : Part α}, a ∈ o → b ∈ o → a = b

Full source

theorem mem_unique : ∀ {a b : α} {o : Part α}, a ∈ o → b ∈ o → a = b
  | _, _, ⟨_, _⟩, ⟨_, rfl⟩, ⟨_, rfl⟩ => rfl

Uniqueness of Membership in Partial Values

Informal description

For any elements $a$ and $b$ of type $\alpha$ and any partial value $o$ of type $\mathrm{Part}\,\alpha$, if both $a \in o$ and $b \in o$ hold, then $a = b$.

Part.mem_right_unique theorem

: ∀ {a : α} {o p : Part α}, a ∈ o → a ∈ p → o = p

Full source

theorem mem_right_unique : ∀ {a : α} {o p : Part α}, a ∈ o → a ∈ p → o = p
  | _, _, _, ⟨ho, _⟩, ⟨hp, _⟩ => ext' (iff_of_true ho hp) (by simp [*])

Uniqueness of Partial Values with Common Member

Informal description

For any element $a$ of type $\alpha$ and any partial values $o, p : \mathrm{Part}\,\alpha$, if $a$ is a member of both $o$ and $p$ (i.e., $a \in o$ and $a \in p$), then $o = p$.

Part.Mem.left_unique theorem

: Relator.LeftUnique ((· ∈ ·) : α → Part α → Prop)

Full source

theorem Mem.left_unique : Relator.LeftUnique ((· ∈ ·) : α → Part α → Prop) := fun _ _ _ =>
  mem_unique

Left Uniqueness of Membership in Partial Values

Informal description

The membership relation $\in$ between elements of type $\alpha$ and partial values of type $\mathrm{Part}\,\alpha$ is left unique. That is, for any elements $a, b \in \alpha$ and any partial value $o \in \mathrm{Part}\,\alpha$, if both $a \in o$ and $b \in o$ hold, then $a = b$.

Part.Mem.right_unique theorem

: Relator.RightUnique ((· ∈ ·) : α → Part α → Prop)

Full source

theorem Mem.right_unique : Relator.RightUnique ((· ∈ ·) : α → Part α → Prop) := fun _ _ _ =>
  mem_right_unique

Right-Uniqueness of Membership in Partial Values

Informal description

The membership relation $\in$ on partial values $\mathrm{Part}\,\alpha$ is right-unique, meaning that for any element $a \in \alpha$ and any partial values $o, p \in \mathrm{Part}\,\alpha$, if $a \in o$ and $a \in p$, then $o = p$.

Part.get_eq_of_mem theorem

{o : Part α} {a} (h : a ∈ o) (h') : get o h' = a

Full source

theorem get_eq_of_mem {o : Part α} {a} (h : a ∈ o) (h') : get o h' = a :=
  mem_unique ⟨_, rfl⟩ h

Uniqueness of Value in Partial Membership

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$ and any element $a \in \alpha$, if $a$ is a member of $o$ (i.e., $a \in o$), then for any proof $h'$ that the domain of $o$ is true, the value obtained from $o$ via the `get` function satisfies $\mathrm{get}\,o\,h' = a$.

Part.subsingleton theorem

(o : Part α) : Set.Subsingleton {a | a ∈ o}

Full source

protected theorem subsingleton (o : Part α) : Set.Subsingleton { a | a ∈ o } := fun _ ha _ hb =>
  mem_unique ha hb

Uniqueness of Membership in Partial Values

Informal description

For any partial value $o$ of type $\mathrm{Part}\,\alpha$, the set $\{a \mid a \in o\}$ is a subsingleton, meaning it contains at most one element. In other words, if $a \in o$ and $b \in o$ for some $a, b \in \alpha$, then $a = b$.

Part.get_some theorem

{a : α} (ha : (some a).Dom) : get (some a) ha = a

Full source

@[simp]
theorem get_some {a : α} (ha : (some a).Dom) : get (some a) ha = a :=
  rfl

Value Extraction from Partial Some

Informal description

For any element $a$ of type $\alpha$ and any proof $ha$ that the domain of the partial value $\text{some } a$ is true, the value obtained by applying the `get` function to $\text{some } a$ and $ha$ is equal to $a$. In other words, $\text{get } (\text{some } a) \ ha = a$.

Part.mem_some theorem

(a : α) : a ∈ some a

Full source

theorem mem_some (a : α) : a ∈ some a :=
  ⟨trivial, rfl⟩

Membership in Partial Some: $a \in \text{some } a$

Informal description

For any element $a$ of type $\alpha$, the element $a$ belongs to the partial value $\text{some } a$ (i.e., $a \in \text{some } a$ holds).

Part.mem_some_iff theorem

{a b} : b ∈ (some a : Part α) ↔ b = a

Full source

@[simp]
theorem mem_some_iff {a b} : b ∈ (some a : Part α)b ∈ (some a : Part α) ↔ b = a :=
  ⟨fun ⟨_, e⟩ => e.symm, fun e => ⟨trivial, e.symm⟩⟩

Membership in Partial Some Equals Equality: $b \in \text{some } a \leftrightarrow b = a$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the statement $b \in \text{some } a$ holds if and only if $b = a$, where $\text{some } a$ denotes the partial value with a domain that is always true and value $a$.

Part.not_none_dom theorem

: ¬(none : Part α).Dom

Full source

@[simp]
theorem not_none_dom : ¬(none : Part α).Dom :=
  id

Undefined Partial Value Has Empty Domain

Informal description

The domain of the partial value `none : Part α` is false, i.e., `¬(none : Part α).Dom`.

Part.some_ne_none theorem

(x : α) : some x ≠ none

Full source

@[simp]
theorem some_ne_none (x : α) : somesome x ≠ none := by
  intro h
  exact true_ne_false (congr_arg Dom h)

Partial Value $\text{some } x$ is Not Undefined

Informal description

For any element $x$ of type $\alpha$, the partial value $\text{some } x$ is not equal to the undefined partial value $\text{none}$.

Part.none_ne_some theorem

(x : α) : none ≠ some x

Full source

@[simp]
theorem none_ne_some (x : α) : nonenone ≠ some x :=
  (some_ne_none x).symm

Undefined Partial Value is Not Equal to Defined Partial Value

Informal description

For any element $x$ of type $\alpha$, the undefined partial value $\text{none}$ is not equal to the defined partial value $\text{some } x$.

Part.ne_none_iff theorem

{o : Part α} : o ≠ none ↔ ∃ x, o = some x

Full source

theorem ne_none_iff {o : Part α} : o ≠ noneo ≠ none ↔ ∃ x, o = some x := by
  constructor
  · rw [Ne, eq_none_iff', not_not]
    exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩
  · rintro ⟨x, rfl⟩
    apply some_ne_none

Characterization of Non-Undefined Partial Values

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$, $o$ is not equal to the undefined partial value $\mathrm{none}$ if and only if there exists an element $x \in \alpha$ such that $o = \mathrm{some}\,x$.

Part.some_injective theorem

: Injective (@Part.some α)

Full source

theorem some_injective : Injective (@Part.some α) := fun _ _ h =>
  congr_fun (eq_of_heq (Part.mk.inj h).2) trivial

Injectivity of Partial Value Construction

Informal description

The function $\mathrm{some} : \alpha \to \mathrm{Part}\,\alpha$ is injective. That is, for any $a, b \in \alpha$, if $\mathrm{some}\,a = \mathrm{some}\,b$, then $a = b$.

Part.some_inj theorem

{a b : α} : Part.some a = some b ↔ a = b

Full source

@[simp]
theorem some_inj {a b : α} : Part.somePart.some a = some b ↔ a = b :=
  some_injective.eq_iff

Injectivity of Partial Value Construction: $\mathrm{some}\,a = \mathrm{some}\,b \leftrightarrow a = b$

Informal description

For any elements $a$ and $b$ of type $\alpha$, the partial values $\mathrm{some}\,a$ and $\mathrm{some}\,b$ are equal if and only if $a = b$.

Part.some_get theorem

{a : Part α} (ha : a.Dom) : Part.some (Part.get a ha) = a

Full source

@[simp]
theorem some_get {a : Part α} (ha : a.Dom) : Part.some (Part.get a ha) = a :=
  Eq.symm (eq_some_iff.2 ⟨ha, rfl⟩)

Partial Value Decomposition: $\mathrm{some}(a.\mathrm{get}) = a$ for Defined $a$

Informal description

For any partial value $a \in \mathrm{Part}\,\alpha$ with a defined domain (i.e., $a.\mathrm{Dom}$ holds), the partial value $\mathrm{some}(a.\mathrm{get}\,ha)$ is equal to $a$, where $ha$ is a proof that $a.\mathrm{Dom}$ holds.

Part.get_eq_iff_eq_some theorem

{a : Part α} {ha : a.Dom} {b : α} : a.get ha = b ↔ a = some b

Full source

theorem get_eq_iff_eq_some {a : Part α} {ha : a.Dom} {b : α} : a.get ha = b ↔ a = some b :=
  ⟨fun h => by simp [h.symm], fun h => by simp [h]⟩

Equivalence of Get and Some for Partial Values

Informal description

For a partial value $a \in \mathrm{Part}\,\alpha$ with a defined domain (i.e., $a.\mathrm{Dom}$ holds, witnessed by $ha$), the value $a.\mathrm{get}\,ha$ equals $b$ if and only if $a$ is equal to the partial value $\mathrm{some}\,b$.

Part.get_eq_get_of_eq theorem

(a : Part α) (ha : a.Dom) {b : Part α} (h : a = b) : a.get ha = b.get (h ▸ ha)

Full source

theorem get_eq_get_of_eq (a : Part α) (ha : a.Dom) {b : Part α} (h : a = b) :
    a.get ha = b.get (h ▸ ha) := by
  congr

Equality of Partial Values Implies Equality of Their Extracted Values

Informal description

For any partial values $a$ and $b$ of type $\alpha$, if $a$ is defined (i.e., $a.Dom$ holds) and $a = b$, then the value of $a$ obtained via $a.get$ is equal to the value of $b$ obtained via $b.get$ (where the proof that $b$ is defined is derived from $a = b$).

Part.get_eq_iff_mem theorem

{o : Part α} {a : α} (h : o.Dom) : o.get h = a ↔ a ∈ o

Full source

theorem get_eq_iff_mem {o : Part α} {a : α} (h : o.Dom) : o.get h = a ↔ a ∈ o :=
  ⟨fun H => ⟨h, H⟩, fun ⟨_, H⟩ => H⟩

Equivalence of Get and Membership for Partial Values

Informal description

For a partial value $o : \mathrm{Part}\,\alpha$ with a defined domain (i.e., $o.\mathrm{Dom}$ holds), the value obtained via $o.\mathrm{get}$ equals $a$ if and only if $a$ is a member of $o$ (i.e., $a \in o$).

Part.none_toOption theorem

[Decidable (@none α).Dom] : (none : Part α).toOption = Option.none

Full source

@[simp]
theorem none_toOption [Decidable (@none α).Dom] : (none : Part α).toOption = Option.none :=
  dif_neg id

Conversion of Undefined Partial Value to Option Yields None

Informal description

For any type $\alpha$, the conversion of the undefined partial value `none : Part α` to an `Option α` results in `Option.none`, provided that the domain of `none` is decidable.

Part.some_toOption theorem

(a : α) [Decidable (some a).Dom] : (some a).toOption = Option.some a

Full source

@[simp]
theorem some_toOption (a : α) [Decidable (some a).Dom] : (some a).toOption = Option.some a :=
  dif_pos trivial

Conversion of Defined Partial Value to Option Yields Some

Informal description

For any element $a$ of type $\alpha$, the conversion of the partial value $\text{some } a$ to an $\text{Option } \alpha$ yields $\text{some } a$, provided that the domain of $\text{some } a$ is decidable.

Part.noneDecidable instance

: Decidable (@none α).Dom

Full source

instance noneDecidable : Decidable (@none α).Dom :=
  instDecidableFalse

Decidability of the Undefined Partial Value's Domain

Informal description

The domain of the undefined partial value `none : Part α` is decidable.

Part.someDecidable instance

(a : α) : Decidable (some a).Dom

Full source

instance someDecidable (a : α) : Decidable (some a).Dom :=
  instDecidableTrue

Decidability of the Domain for Defined Partial Values

Informal description

For any element $a$ of type $\alpha$, the domain of the partial value $\text{some } a$ is decidable.

Part.getOrElse definition

(a : Part α) [Decidable a.Dom] (d : α)

Full source

/-- Retrieves the value of `a : Part α` if it exists, and return the provided default value
otherwise. -/
def getOrElse (a : Part α) [Decidable a.Dom] (d : α) :=
  if ha : a.Dom then a.get ha else d

Default value for partial value

Informal description

The function retrieves the value of a partial value `a : Part α` if its domain is true (i.e., `a.Dom` holds), and returns the default value `d : α` otherwise. More formally, given a partial value `a` with a decidable domain and a default value `d`, `getOrElse a d` evaluates to `a.get h` if there exists a proof `h` that `a.Dom` is true, and to `d` otherwise.

Part.getOrElse_of_dom theorem

(a : Part α) (h : a.Dom) [Decidable a.Dom] (d : α) : getOrElse a d = a.get h

Full source

theorem getOrElse_of_dom (a : Part α) (h : a.Dom) [Decidable a.Dom] (d : α) :
    getOrElse a d = a.get h :=
  dif_pos h

Value Retrieval for Defined Partial Values

Informal description

For a partial value $a : \text{Part } \alpha$ with a decidable domain, if $h$ is a proof that $a.\text{Dom}$ holds, then for any default value $d : \alpha$, the function $\text{getOrElse}$ returns $a.\text{get}(h)$, i.e., $\text{getOrElse } a d = a.\text{get}(h)$.

Part.getOrElse_of_not_dom theorem

(a : Part α) (h : ¬a.Dom) [Decidable a.Dom] (d : α) : getOrElse a d = d

Full source

theorem getOrElse_of_not_dom (a : Part α) (h : ¬a.Dom) [Decidable a.Dom] (d : α) :
    getOrElse a d = d :=
  dif_neg h

Default Value for Partial Value with False Domain

Informal description

For a partial value $a : \text{Part } \alpha$ with a decidable domain, if the domain of $a$ is false (i.e., $\neg a.\text{Dom}$ holds), then for any default value $d : \alpha$, the function $\text{getOrElse}$ returns $d$, i.e., $\text{getOrElse } a d = d$.

Part.getOrElse_none theorem

(d : α) [Decidable (none : Part α).Dom] : getOrElse none d = d

Full source

@[simp]
theorem getOrElse_none (d : α) [Decidable (none : Part α).Dom] : getOrElse none d = d :=
  none.getOrElse_of_not_dom not_none_dom d

Default Value for Undefined Partial Value (`none`)

Informal description

For any default value $d : \alpha$ and a decidable domain of the partial value `none : \text{Part } \alpha`, the function `getOrElse` returns $d$, i.e., $\text{getOrElse none } d = d$.

Part.getOrElse_some theorem

(a : α) (d : α) [Decidable (some a).Dom] : getOrElse (some a) d = a

Full source

@[simp]
theorem getOrElse_some (a : α) (d : α) [Decidable (some a).Dom] : getOrElse (some a) d = a :=
  (some a).getOrElse_of_dom (some_dom a) d

$\text{getOrElse } (\text{some } a) d = a$ for Partial Values

Informal description

For any element $a$ of type $\alpha$ and any default value $d : \alpha$, the function `getOrElse` applied to the partial value `some a` (which has a decidable domain) returns $a$, i.e., $\text{getOrElse } (\text{some } a) d = a$.

Part.mem_toOption theorem

{o : Part α} [Decidable o.Dom] {a : α} : a ∈ toOption o ↔ a ∈ o

Full source

theorem mem_toOption {o : Part α} [Decidable o.Dom] {a : α} : a ∈ toOption oa ∈ toOption o ↔ a ∈ o := by
  unfold toOption
  by_cases h : o.Dom <;> simp [h]
  · exact ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩
  · exact mt Exists.fst h

Equivalence of Membership in Partial Value and Its Option Conversion

Informal description

For a partial value $o : \mathrm{Part}\,\alpha$ with a decidable domain and an element $a \in \alpha$, the element $a$ is in the option obtained by converting $o$ to an $\mathrm{Option}\,\alpha$ if and only if $a$ is in the partial value $o$. In other words, $a \in \mathrm{toOption}\,o \leftrightarrow a \in o$.

Part.toOption_eq_some_iff theorem

{o : Part α} [Decidable o.Dom] {a : α} : toOption o = Option.some a ↔ a ∈ o

Full source

@[simp]
theorem toOption_eq_some_iff {o : Part α} [Decidable o.Dom] {a : α} :
    toOptiontoOption o = Option.some a ↔ a ∈ o := by
  rw [← Option.mem_def, mem_toOption]

Equivalence between Option Conversion and Membership in Partial Values

Informal description

For a partial value $o : \mathrm{Part}\,\alpha$ with a decidable domain and an element $a \in \alpha$, the conversion of $o$ to an $\mathrm{Option}\,\alpha$ equals $\mathrm{some}\,a$ if and only if $a$ is in the partial value $o$. That is, $\mathrm{toOption}\,o = \mathrm{some}\,a \leftrightarrow a \in o$.

Part.Dom.toOption theorem

{o : Part α} [Decidable o.Dom] (h : o.Dom) : o.toOption = o.get h

Full source

protected theorem Dom.toOption {o : Part α} [Decidable o.Dom] (h : o.Dom) : o.toOption = o.get h :=
  dif_pos h

Partial Value to Option Conversion with Valid Domain

Informal description

For a partial value `o : Part α` with a decidable domain, if `h` is a proof that `o.Dom` holds, then the conversion of `o` to an `Option α` via `toOption` yields `some (o.get h)`.

Part.toOption_eq_none_iff theorem

{a : Part α} [Decidable a.Dom] : a.toOption = Option.none ↔ ¬a.Dom

Full source

theorem toOption_eq_none_iff {a : Part α} [Decidable a.Dom] : a.toOption = Option.none ↔ ¬a.Dom :=
  Ne.dite_eq_right_iff fun _ => Option.some_ne_none _

Partial Value to Option Conversion Yields None iff Domain is False

Informal description

For a partial value `a : Part α` with a decidable domain, the conversion to an `Option α` results in `none` if and only if the domain of `a` is false, i.e., `a.toOption = none ↔ ¬a.Dom`.

Part.elim_toOption theorem

 {α β : Type*} (a : Part α) [Decidable a.Dom] (b : β) (f : α → β) :
  a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Full source

@[simp]
theorem elim_toOption {α β : Type*} (a : Part α) [Decidable a.Dom] (b : β) (f : α → β) :
    a.toOption.elim b f = if h : a.Dom then f (a.get h) else b := by
  split_ifs with h
  · rw [h.toOption]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    rfl

Elimination of Partial Value to Option Conversion

Informal description

For any partial value `a : Part α` with a decidable domain, a default value `b : β`, and a function `f : α → β`, the elimination of `a.toOption` with `b` and `f` is equal to `f (a.get h)` if `a.Dom` holds (with proof `h`), and `b` otherwise. In other words: \[ \text{Option.elim } a.\text{toOption } b f = \begin{cases} f (a.\text{get } h) & \text{if } a.\text{Dom} \text{ holds} \\ b & \text{otherwise} \end{cases} \]

Part.ofOption definition

: Option α → Part α

Full source

/-- Converts an `Option α` into a `Part α`. -/
@[coe]
def ofOption : Option α → Part α
  | Option.none => none
  | Option.some a => some a

Conversion from Option to Partial Value

Informal description

The function converts an `Option α` into a `Part α` by mapping `Option.none` to `Part.none` (an undefined partial value) and `Option.some a` to `Part.some a` (a defined partial value with value `a`).

Part.mem_ofOption theorem

{a : α} : ∀ {o : Option α}, a ∈ ofOption o ↔ a ∈ o

Full source

@[simp]
theorem mem_ofOption {a : α} : ∀ {o : Option α}, a ∈ ofOption oa ∈ ofOption o ↔ a ∈ o
  | Option.none => ⟨fun h => h.fst.elim, fun h => Option.noConfusion h⟩
  | Option.some _ => ⟨fun h => congr_arg Option.some h.snd, fun h => ⟨trivial, Option.some.inj h⟩⟩

Membership Preservation in Option-to-Partial Conversion

Informal description

For any element $a$ of type $\alpha$ and any option $o : \mathrm{Option}\,\alpha$, the element $a$ belongs to the partial value $\mathrm{ofOption}\,o$ if and only if $a$ belongs to the option $o$. Here, $a \in \mathrm{ofOption}\,o$ means that the partial value $\mathrm{ofOption}\,o$ is defined (i.e., its domain is true) and its value equals $a$, while $a \in o$ means that $o$ is of the form $\mathrm{some}\,a$.

Part.ofOption_dom theorem

{α} : ∀ o : Option α, (ofOption o).Dom ↔ o.isSome

Full source

@[simp]
theorem ofOption_dom {α} : ∀ o : Option α, (ofOption o).Dom ↔ o.isSome
  | Option.none => by simp [ofOption, none]
  | Option.some a => by simp [ofOption]

Domain of Option-to-Partial Conversion Reflects Option's Definedness

Informal description

For any option `o : Option α`, the domain of the partial value `ofOption o` is true if and only if `o` is of the form `some a` for some `a : α`.

Part.ofOption_eq_get theorem

{α} (o : Option α) : ofOption o = ⟨_, @Option.get _ o⟩

Full source

theorem ofOption_eq_get {α} (o : Option α) : ofOption o = ⟨_, @Option.get _ o⟩ :=
  Part.ext' (ofOption_dom o) fun h₁ h₂ => by
    cases o
    · simp at h₂
    · rfl

Equality of Option-to-Partial Conversion with Partial Value Construction

Informal description

For any option `o : Option α`, the partial value `ofOption o` is equal to the partial value constructed with domain `o.isSome` and value function `Option.get o`.

Part.instCoeOption instance

: Coe (Option α) (Part α)

Full source

instance : Coe (Option α) (Part α) :=
  ⟨ofOption⟩

Canonical Coercion from Option to Partial Values

Informal description

There is a canonical coercion from `Option α` to `Part α`, where `Option.none` is mapped to `Part.none` and `Option.some a` is mapped to `Part.some a`.

Part.mem_coe theorem

{a : α} {o : Option α} : a ∈ (o : Part α) ↔ a ∈ o

Full source

theorem mem_coe {a : α} {o : Option α} : a ∈ (o : Part α)a ∈ (o : Part α) ↔ a ∈ o :=
  mem_ofOption

Membership Preservation under Option-to-Partial Coercion

Informal description

For any element $a$ of type $\alpha$ and any option $o : \mathrm{Option}\,\alpha$, the element $a$ belongs to the partial value obtained by coercing $o$ to $\mathrm{Part}\,\alpha$ if and only if $a$ belongs to $o$. Here, $a \in o$ means that $o$ is of the form $\mathrm{some}\,a$, and $a \in (o : \mathrm{Part}\,\alpha)$ means that the partial value $(o : \mathrm{Part}\,\alpha)$ is defined and its value equals $a$.

Part.coe_none theorem

: (@Option.none α : Part α) = none

Full source

@[simp]
theorem coe_none : (@Option.none α : Part α) = none :=
  rfl

Coercion of `Option.none` to `Part.none`

Informal description

The coercion of `Option.none` to a partial value `Part α` is equal to `Part.none`.

Part.coe_some theorem

(a : α) : (Option.some a : Part α) = some a

Full source

@[simp]
theorem coe_some (a : α) : (Option.some a : Part α) = some a :=
  rfl

Coercion of `Option.some` to `Part.some`

Informal description

For any element $a$ of type $\alpha$, the coercion of `Option.some a` to a partial value `Part α` is equal to `Part.some a`.

Part.induction_on theorem

{P : Part α → Prop} (a : Part α) (hnone : P none) (hsome : ∀ a : α, P (some a)) : P a

Full source

@[elab_as_elim]
protected theorem induction_on {P : Part α → Prop} (a : Part α) (hnone : P none)
    (hsome : ∀ a : α, P (some a)) : P a :=
  (Classical.em a.Dom).elim (fun h => Part.some_get h ▸ hsome _) fun h =>
    (eq_none_iff'.2 h).symm ▸ hnone

Induction Principle for Partial Values

Informal description

For any predicate $P$ on partial values of type $\mathrm{Part}\,\alpha$, a partial value $a \in \mathrm{Part}\,\alpha$, and proofs that $P$ holds for $\mathrm{none}$ and for all $\mathrm{some}\,a$ with $a \in \alpha$, it follows that $P$ holds for $a$.

Part.ofOptionDecidable instance

: ∀ o : Option α, Decidable (ofOption o).Dom

Full source

instance ofOptionDecidable : ∀ o : Option α, Decidable (ofOption o).Dom
  | Option.none => Part.noneDecidable
  | Option.some a => Part.someDecidable a

Decidability of Domain for Partial Values from Options

Informal description

For any option `o : Option α`, the domain of the partial value `ofOption o` is decidable.

Part.to_ofOption theorem

(o : Option α) : toOption (ofOption o) = o

Full source

@[simp]
theorem to_ofOption (o : Option α) : toOption (ofOption o) = o := by cases o <;> rfl

Conversion Round-Trip: `toOption (ofOption o) = o`

Informal description

For any option `o : Option α`, converting `o` to a partial value using `ofOption` and then back to an option using `toOption` yields the original option `o`. In other words, the composition `toOption ∘ ofOption` is the identity function on `Option α`.

Part.of_toOption theorem

(o : Part α) [Decidable o.Dom] : ofOption (toOption o) = o

Full source

@[simp]
theorem of_toOption (o : Part α) [Decidable o.Dom] : ofOption (toOption o) = o :=
  ext fun _ => mem_ofOption.trans mem_toOption

Round-Trip Identity for Partial-to-Option Conversion

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$ with a decidable domain, converting $o$ to an option using $\mathrm{toOption}$ and then back to a partial value using $\mathrm{ofOption}$ yields the original partial value $o$. In other words, $\mathrm{ofOption} \circ \mathrm{toOption}$ is the identity function on $\mathrm{Part}\,\alpha$ with decidable domains.

Part.equivOption definition

: Part α ≃ Option α

Full source

/-- `Part α` is (classically) equivalent to `Option α`. -/
noncomputable def equivOption : PartPart α ≃ Option α :=
  haveI := Classical.dec
  ⟨fun o => toOption o, ofOption, fun o => of_toOption o, fun o =>
    Eq.trans (by dsimp; congr) (to_ofOption o)⟩

Equivalence between partial values and options

Informal description

The equivalence `Part.equivOption` establishes a classical bijection between `Part α` and `Option α`. It consists of two functions: `toOption`, which converts a partial value with a decidable domain to an option, and `ofOption`, which converts an option back to a partial value. These functions satisfy `ofOption ∘ toOption = id` and `toOption ∘ ofOption = id`.

Part.instPartialOrder instance

: PartialOrder (Part α)

Full source

/-- We give `Part α` the order where everything is greater than `none`. -/
instance : PartialOrder (Part
        α) where
  le x y := ∀ i, i ∈ x → i ∈ y
  le_refl _ _ := id
  le_trans _ _ _ f g _ := g _ ∘ f _
  le_antisymm _ _ f g := Part.ext fun _ => ⟨f _, g _⟩

Partial Order on Partial Values

Informal description

The partial values `Part α` of a type `α` form a partial order where `none` is the least element and the ordering is defined by domain inclusion and value equality. Specifically, for `x, y : Part α`, we have `x ≤ y` if whenever `x` is defined (i.e., `x.Dom` holds), then `y` is also defined and their values coincide (`x.get _ = y.get _`).

Part.instOrderBot instance

: OrderBot (Part α)

Full source

instance : OrderBot (Part α) where
  bot := none
  bot_le := by rintro x _ ⟨⟨_⟩, _⟩

Partial Values as an Order with Bottom Element

Informal description

The partial values `Part α` of a type `α` form an order with a bottom element, where the bottom element is the undefined partial value `none`.

Part.le_total_of_le_of_le theorem

{x y : Part α} (z : Part α) (hx : x ≤ z) (hy : y ≤ z) : x ≤ y ∨ y ≤ x

Full source

theorem le_total_of_le_of_le {x y : Part α} (z : Part α) (hx : x ≤ z) (hy : y ≤ z) :
    x ≤ y ∨ y ≤ x := by
  rcases Part.eq_none_or_eq_some x with (h | ⟨b, h₀⟩)
  · rw [h]
    left
    apply OrderBot.bot_le _
  right; intro b' h₁
  rw [Part.eq_some_iff] at h₀
  have hx := hx _ h₀; have hy := hy _ h₁
  have hx := Part.mem_unique hx hy; subst hx
  exact h₀

Total Order Condition for Partial Values Under Common Upper Bound

Informal description

For any partial values $x, y, z$ of type $\mathrm{Part}\,\alpha$, if both $x \leq z$ and $y \leq z$ hold, then either $x \leq y$ or $y \leq x$. Here, the relation $\leq$ on partial values is defined as: $a \leq b$ if whenever $a$ is defined (i.e., its domain is true), then $b$ is also defined and their values coincide.

Part.assert definition

(p : Prop) (f : p → Part α) : Part α

Full source

/-- `assert p f` is a bind-like operation which appends an additional condition
  `p` to the domain and uses `f` to produce the value. -/
def assert (p : Prop) (f : p → Part α) : Part α :=
  ⟨∃ h : p, (f h).Dom, fun ha => (f ha.fst).get ha.snd⟩

Partial value with asserted condition

Informal description

Given a proposition $p$ and a function $f : p \to \text{Part } \alpha$, the partial value $\text{Part.assert } p f$ is defined to have domain $\exists h : p, (f h).\text{Dom}$ and value $(f h).\text{get } \_$ for any proof $h$ of $p$ and $(f h).\text{Dom}$. This operation appends the condition $p$ to the domain of the partial value produced by $f$.

Part.bind definition

(f : Part α) (g : α → Part β) : Part β

Full source

/-- The bind operation has value `g (f.get)`, and is defined when all the
  parts are defined. -/
protected def bind (f : Part α) (g : α → Part β) : Part β :=
  assert (Dom f) fun b => g (f.get b)

Partial value binding operation

Informal description

Given a partial value `f : Part α` and a function `g : α → Part β`, the partial value `Part.bind f g` is defined to have domain `Dom f ∧ ∀ (h : Dom f), Dom (g (f.get h))` and value `(g (f.get h)).get _` for any proof `h` of `Dom f` and `Dom (g (f.get h))`. This operation composes the partial values `f` and `g` in a way that the resulting partial value is defined only when both `f` and the application of `g` to `f`'s value are defined.

Part.map definition

(f : α → β) (o : Part α) : Part β

Full source

/-- The map operation for `Part` just maps the value and maintains the same domain. -/
@[simps]
def map (f : α → β) (o : Part α) : Part β :=
  ⟨o.Dom, f ∘ o.get⟩

Mapping of Partial Values

Informal description

The function `Part.map` applies a function $f : \alpha \to \beta$ to the value of a partial value $o : \text{Part } \alpha$, while preserving the domain of $o$. Specifically, if $o$ has domain $\text{Dom}$ and value $\text{get} : \text{Dom} \to \alpha$, then $\text{Part.map } f o$ has the same domain $\text{Dom}$ and value $f \circ \text{get} : \text{Dom} \to \beta$.

Part.mem_map theorem

(f : α → β) {o : Part α} : ∀ {a}, a ∈ o → f a ∈ map f o

Full source

theorem mem_map (f : α → β) {o : Part α} : ∀ {a}, a ∈ o → f a ∈ map f o
  | _, ⟨_, rfl⟩ => ⟨_, rfl⟩

Membership Preservation under Mapping of Partial Values

Informal description

For any function $f : \alpha \to \beta$ and partial value $o : \text{Part } \alpha$, if $a \in o$ (i.e., $o$ is defined and its value is $a$), then $f(a) \in \text{map } f o$ (i.e., the mapped partial value is defined and its value is $f(a)$).

Part.mem_map_iff theorem

(f : α → β) {o : Part α} {b} : b ∈ map f o ↔ ∃ a ∈ o, f a = b

Full source

@[simp]
theorem mem_map_iff (f : α → β) {o : Part α} {b} : b ∈ map f ob ∈ map f o ↔ ∃ a ∈ o, f a = b :=
  ⟨fun hb => match b, hb with
    | _, ⟨_, rfl⟩ => ⟨_, ⟨_, rfl⟩, rfl⟩,
    fun ⟨_, h₁, h₂⟩ => h₂ ▸ mem_map f h₁⟩

Membership Characterization in Mapped Partial Values: $b \in \text{map } f o \leftrightarrow \exists a \in o, f(a) = b$

Informal description

For any function $f : \alpha \to \beta$ and partial value $o : \text{Part } \alpha$, an element $b \in \beta$ belongs to the mapped partial value $\text{map } f o$ if and only if there exists an element $a \in \alpha$ such that $a \in o$ and $f(a) = b$.

Part.map_none theorem

(f : α → β) : map f none = none

Full source

@[simp]
theorem map_none (f : α → β) : map f none = none :=
  eq_none_iff.2 fun a => by simp

Mapping Preserves Undefined Partial Value: $\text{map}\,f\,\text{none} = \text{none}$

Informal description

For any function $f : \alpha \to \beta$, the mapping of the undefined partial value `none` under $f$ is again `none`, i.e., $\text{map}\,f\,\text{none} = \text{none}$.

Part.map_some theorem

(f : α → β) (a : α) : map f (some a) = some (f a)

Full source

@[simp]
theorem map_some (f : α → β) (a : α) : map f (some a) = some (f a) :=
  eq_some_iff.2 <| mem_map f <| mem_some _

Mapping of Partial Some: $\text{map}\,f\,(\text{some } a) = \text{some } (f a)$

Informal description

For any function $f : \alpha \to \beta$ and element $a \in \alpha$, the mapping of the partial value $\text{some } a$ under $f$ is equal to $\text{some } (f a)$. In other words, $\text{map}\,f\,(\text{some } a) = \text{some } (f a)$.

Part.mem_assert theorem

{p : Prop} {f : p → Part α} : ∀ {a} (h : p), a ∈ f h → a ∈ assert p f

Full source

theorem mem_assert {p : Prop} {f : p → Part α} : ∀ {a} (h : p), a ∈ f h → a ∈ assert p f
  | _, x, ⟨h, rfl⟩ => ⟨⟨x, h⟩, rfl⟩

Membership Preservation under Assertion in Partial Values

Informal description

For any proposition $p$, function $f : p \to \text{Part } \alpha$, element $a \in \alpha$, and proof $h$ of $p$, if $a$ is in the partial value $f(h)$, then $a$ is also in the asserted partial value $\text{assert } p f$.

Part.mem_assert_iff theorem

{p : Prop} {f : p → Part α} {a} : a ∈ assert p f ↔ ∃ h : p, a ∈ f h

Full source

@[simp]
theorem mem_assert_iff {p : Prop} {f : p → Part α} {a} : a ∈ assert p fa ∈ assert p f ↔ ∃ h : p, a ∈ f h :=
  ⟨fun ha => match a, ha with
    | _, ⟨_, rfl⟩ => ⟨_, ⟨_, rfl⟩⟩,
    fun ⟨_, h⟩ => mem_assert _ h⟩

Membership in Asserted Partial Value Characterization

Informal description

For any proposition $p$, function $f : p \to \text{Part } \alpha$, and element $a \in \alpha$, the element $a$ belongs to the asserted partial value $\text{assert } p f$ if and only if there exists a proof $h$ of $p$ such that $a$ belongs to $f(h)$.

Part.assert_pos theorem

{p : Prop} {f : p → Part α} (h : p) : assert p f = f h

Full source

theorem assert_pos {p : Prop} {f : p → Part α} (h : p) : assert p f = f h := by
  dsimp [assert]
  cases h' : f h
  simp only [h', mk.injEq, h, exists_prop_of_true, true_and]
  apply Function.hfunext
  · simp only [h, h', exists_prop_of_true]
  · simp

Assertion of True Condition Yields Original Partial Value

Informal description

For any proposition $p$ and function $f : p \to \text{Part } \alpha$, if $p$ holds (with proof $h$), then the asserted partial value $\text{assert } p f$ is equal to $f(h)$.

Part.assert_neg theorem

{p : Prop} {f : p → Part α} (h : ¬p) : assert p f = none

Full source

theorem assert_neg {p : Prop} {f : p → Part α} (h : ¬p) : assert p f = none := by
  dsimp [assert, none]; congr
  · simp only [h, not_false_iff, exists_prop_of_false]
  · apply Function.hfunext
    · simp only [h, not_false_iff, exists_prop_of_false]
    simp at *

Assertion with False Condition Yields Undefined Partial Value

Informal description

For any proposition $p$ and function $f : p \to \text{Part } \alpha$, if $\neg p$ holds, then the partial value $\text{assert } p f$ is equal to $\text{none}$.

Part.mem_bind theorem

{f : Part α} {g : α → Part β} : ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g

Full source

theorem mem_bind {f : Part α} {g : α → Part β} : ∀ {a b}, a ∈ f → b ∈ g a → b ∈ f.bind g
  | _, _, ⟨h, rfl⟩, ⟨h₂, rfl⟩ => ⟨⟨h, h₂⟩, rfl⟩

Membership Preservation under Partial Value Binding

Informal description

For any partial values $f : \mathrm{Part}\,\alpha$ and $g : \alpha \to \mathrm{Part}\,\beta$, and any elements $a \in \alpha$, $b \in \beta$, if $a$ is in the domain of $f$ with value $a$, and $b$ is in the domain of $g(a)$ with value $b$, then $b$ is in the domain of the partial value $f \mathbin{\mathrm{bind}} g$ with value $b$.

Part.mem_bind_iff theorem

{f : Part α} {g : α → Part β} {b} : b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a

Full source

@[simp]
theorem mem_bind_iff {f : Part α} {g : α → Part β} {b} : b ∈ f.bind gb ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a :=
  ⟨fun hb => match b, hb with
    | _, ⟨⟨_, _⟩, rfl⟩ => ⟨_, ⟨_, rfl⟩, ⟨_, rfl⟩⟩,
    fun ⟨_, h₁, h₂⟩ => mem_bind h₁ h₂⟩

Characterization of Membership in Partial Value Binding: $b \in f \mathbin{\mathrm{bind}} g \leftrightarrow \exists a \in f, b \in g(a)$

Informal description

For any partial values $f : \mathrm{Part}\,\alpha$ and $g : \alpha \to \mathrm{Part}\,\beta$, and any element $b \in \beta$, we have $b \in f \mathbin{\mathrm{bind}} g$ if and only if there exists an element $a \in \alpha$ such that $a \in f$ and $b \in g(a)$.

Part.Dom.bind theorem

{o : Part α} (h : o.Dom) (f : α → Part β) : o.bind f = f (o.get h)

Full source

protected theorem Dom.bind {o : Part α} (h : o.Dom) (f : α → Part β) : o.bind f = f (o.get h) := by
  ext b
  simp only [Part.mem_bind_iff, exists_prop]
  refine ⟨?_, fun hb => ⟨o.get h, Part.get_mem _, hb⟩⟩
  rintro ⟨a, ha, hb⟩
  rwa [Part.get_eq_of_mem ha]

Binding Defined Partial Value Yields Function Application

Informal description

For any partial value $o : \mathrm{Part}\,\alpha$ with a proof $h$ that its domain is true, and any function $f : \alpha \to \mathrm{Part}\,\beta$, the binding $o \mathbin{\mathrm{bind}} f$ is equal to $f(o.\mathrm{get}\,h)$.

Part.Dom.of_bind theorem

{f : α → Part β} {a : Part α} (h : (a.bind f).Dom) : a.Dom

Full source

theorem Dom.of_bind {f : α → Part β} {a : Part α} (h : (a.bind f).Dom) : a.Dom :=
  h.1

Domain Preservation under Partial Binding

Informal description

For any partial value $a : \text{Part } \alpha$ and function $f : \alpha \to \text{Part } \beta$, if the partial value $a.\text{bind } f$ is defined (i.e., has a non-empty domain), then $a$ itself must be defined.

Part.bind_none theorem

(f : α → Part β) : none.bind f = none

Full source

@[simp]
theorem bind_none (f : α → Part β) : none.bind f = none :=
  eq_none_iff.2 fun a => by simp

Binding with `none` yields `none`

Informal description

For any function $f : \alpha \to \text{Part } \beta$, the binding of the undefined partial value `none` with $f$ results in `none`, i.e., $\text{none.bind } f = \text{none}$.

Part.bind_some theorem

(a : α) (f : α → Part β) : (some a).bind f = f a

Full source

@[simp]
theorem bind_some (a : α) (f : α → Part β) : (some a).bind f = f a :=
  ext <| by simp

Binding of Defined Partial Value Equals Function Application

Informal description

For any element $a$ of type $\alpha$ and any function $f : \alpha \to \text{Part } \beta$, the binding of the partial value $\text{some } a$ with $f$ is equal to $f(a)$. That is, $(\text{some } a).\text{bind } f = f(a)$.

Part.bind_of_mem theorem

{o : Part α} {a : α} (h : a ∈ o) (f : α → Part β) : o.bind f = f a

Full source

theorem bind_of_mem {o : Part α} {a : α} (h : a ∈ o) (f : α → Part β) : o.bind f = f a := by
  rw [eq_some_iff.2 h, bind_some]

Binding of Partial Value with Known Element Equals Function Application

Informal description

For any partial value $o : \text{Part } \alpha$ and any element $a \in \alpha$ such that $a \in o$ (i.e., $o$ is defined and its value is $a$), and for any function $f : \alpha \to \text{Part } \beta$, the binding of $o$ with $f$ is equal to $f(a)$. That is, $o.\text{bind } f = f(a)$.

Part.bind_some_eq_map theorem

(f : α → β) (x : Part α) : x.bind (fun y => some (f y)) = map f x

Full source

theorem bind_some_eq_map (f : α → β) (x : Part α) : x.bind (fun y => some (f y)) = map f x :=
  ext <| by simp [eq_comm]

Equivalence of Binding with Some and Mapping for Partial Values

Informal description

For any function $f : \alpha \to \beta$ and any partial value $x : \mathrm{Part}\,\alpha$, the binding of $x$ with the function $\lambda y, \mathrm{some}\,(f y)$ is equal to mapping $f$ over $x$. That is, $$ x.\mathrm{bind}\,(\lambda y, \mathrm{some}\,(f y)) = x.\mathrm{map}\,f. $$

Part.bind_toOption theorem

 (f : α → Part β) (o : Part α) [Decidable o.Dom] [∀ a, Decidable (f a).Dom] [Decidable (o.bind f).Dom] :
  (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption

Full source

theorem bind_toOption (f : α → Part β) (o : Part α) [Decidable o.Dom] [∀ a, Decidable (f a).Dom]
    [Decidable (o.bind f).Dom] :
    (o.bind f).toOption = o.toOption.elim Option.none fun a => (f a).toOption := by
  by_cases h : o.Dom
  · simp_rw [h.toOption, h.bind]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    exact Part.toOption_eq_none_iff.2 fun ho => h ho.of_bind

Option Conversion of Partial Binding Equals Elimination of Option

Informal description

For any function $f \colon \alpha \to \mathrm{Part}\,\beta$ and partial value $o \in \mathrm{Part}\,\alpha$ with decidable domains, the conversion of the binding $o \mathbin{\mathrm{bind}} f$ to an option is equal to eliminating the option obtained from $o$: if $o$ is undefined (i.e., $o.\mathrm{toOption} = \mathrm{none}$), the result is $\mathrm{none}$; otherwise, it is the conversion of $f(a)$ to an option for the value $a$ obtained from $o$.

Part.bind_assoc theorem

{γ} (f : Part α) (g : α → Part β) (k : β → Part γ) : (f.bind g).bind k = f.bind fun x => (g x).bind k

Full source

theorem bind_assoc {γ} (f : Part α) (g : α → Part β) (k : β → Part γ) :
    (f.bind g).bind k = f.bind fun x => (g x).bind k :=
  ext fun a => by
    simp only [mem_bind_iff]
    exact ⟨fun ⟨_, ⟨_, h₁, h₂⟩, h₃⟩ => ⟨_, h₁, _, h₂, h₃⟩,
           fun ⟨_, h₁, _, h₂, h₃⟩ => ⟨_, ⟨_, h₁, h₂⟩, h₃⟩⟩

Associativity of Partial Value Binding

Informal description

For any partial value $f \in \mathrm{Part}\,\alpha$ and functions $g \colon \alpha \to \mathrm{Part}\,\beta$ and $k \colon \beta \to \mathrm{Part}\,\gamma$, the following associativity law holds: $$ (f \mathbin{\mathrm{bind}} g) \mathbin{\mathrm{bind}} k = f \mathbin{\mathrm{bind}} \big( \lambda x \mapsto (g\,x) \mathbin{\mathrm{bind}} k \big). $$ Here, $\mathrm{bind}$ denotes the partial value binding operation, and the equality means that both sides have the same domain and yield the same value when defined.

Part.bind_map theorem

{γ} (f : α → β) (x) (g : β → Part γ) : (map f x).bind g = x.bind fun y => g (f y)

Full source

@[simp]
theorem bind_map {γ} (f : α → β) (x) (g : β → Part γ) :
    (map f x).bind g = x.bind fun y => g (f y) := by rw [← bind_some_eq_map, bind_assoc]; simp

Binding-Map Interchange for Partial Values

Informal description

For any function $f \colon \alpha \to \beta$, partial value $x \in \mathrm{Part}\,\alpha$, and function $g \colon \beta \to \mathrm{Part}\,\gamma$, the following equality holds: $$ (\mathrm{map}\,f\,x) \mathbin{\mathrm{bind}} g = x \mathbin{\mathrm{bind}} \big( \lambda y \mapsto g(f y) \big). $$ Here, $\mathrm{map}$ denotes the partial mapping operation and $\mathrm{bind}$ denotes the partial value binding operation. The equality means both sides have the same domain and yield the same value when defined.

Part.map_bind theorem

{γ} (f : α → Part β) (x : Part α) (g : β → γ) : map g (x.bind f) = x.bind fun y => map g (f y)

Full source

@[simp]
theorem map_bind {γ} (f : α → Part β) (x : Part α) (g : β → γ) :
    map g (x.bind f) = x.bind fun y => map g (f y) := by
  rw [← bind_some_eq_map, bind_assoc]; simp [bind_some_eq_map]

Commutativity of Mapping and Binding for Partial Values

Informal description

For any functions $f \colon \alpha \to \mathrm{Part}\,\beta$ and $g \colon \beta \to \gamma$, and any partial value $x \in \mathrm{Part}\,\alpha$, the following equality holds: $$ \mathrm{map}\,g\,(x \mathbin{\mathrm{bind}} f) = x \mathbin{\mathrm{bind}} \big( \lambda y \mapsto \mathrm{map}\,g\,(f y) \big). $$ Here, $\mathrm{map}$ denotes the mapping operation on partial values, and $\mathrm{bind}$ denotes the partial value binding operation. The equality means that both sides have the same domain and yield the same value when defined.

Part.map_map theorem

(g : β → γ) (f : α → β) (o : Part α) : map g (map f o) = map (g ∘ f) o

Full source

theorem map_map (g : β → γ) (f : α → β) (o : Part α) : map g (map f o) = map (g ∘ f) o := by
  simp [map, Function.comp_assoc]

Composition of Partial Mappings

Informal description

For any functions $g : \beta \to \gamma$ and $f : \alpha \to \beta$, and any partial value $o : \text{Part } \alpha$, the composition of the partial mappings satisfies $\text{map } g (\text{map } f o) = \text{map } (g \circ f) o$.

Part.instMonad instance

: Monad Part

Full source

instance : Monad Part where
  pure := @some
  map := @map
  bind := @Part.bind

Monad Structure on Partial Values

Informal description

The type `Part α` of partial values of a type `α` forms a monad, where: - The `pure` operation is given by `Part.some`, which creates a partial value with a true domain and the given value. - The `bind` operation `Part.bind` composes partial values as described in its definition.

Part.instLawfulMonad instance

: LawfulMonad Part

Full source

instance : LawfulMonad
      Part where
  bind_pure_comp := @bind_some_eq_map
  id_map f := by cases f; rfl
  pure_bind := @bind_some
  bind_assoc := @bind_assoc
  map_const := by simp [Functor.mapConst, Functor.map]
  --Porting TODO : In Lean3 these were automatic by a tactic
  seqLeft_eq x y := ext'
    (by simp [SeqLeft.seqLeft, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm])
    (fun _ _ => rfl)
  seqRight_eq x y := ext'
    (by simp [SeqRight.seqRight, Part.bind, assert, Seq.seq, const, (· <$> ·), and_comm])
    (fun _ _ => rfl)
  pure_seq x y := ext'
    (by simp [Seq.seq, Part.bind, assert, (· <$> ·), pure])
    (fun _ _ => rfl)
  bind_map x y := ext'
    (by simp [(· >>= ·), Part.bind, assert, Seq.seq, get, (· <$> ·)] )
    (fun _ _ => rfl)

Partial Values Form a Lawful Monad

Informal description

The type `Part α` of partial values forms a lawful monad, where: - The `pure` operation is given by `Part.some`, which creates a partial value with a true domain and the given value. - The `bind` operation `Part.bind` composes partial values as described in its definition, satisfying the monad laws (left identity, right identity, and associativity).

Part.map_id' theorem

{f : α → α} (H : ∀ x : α, f x = x) (o) : map f o = o

Full source

theorem map_id' {f : α → α} (H : ∀ x : α, f x = x) (o) : map f o = o := by
  rw [show f = id from funext H]; exact id_map o

Identity Mapping Preserves Partial Values

Informal description

For any function $f : \alpha \to \alpha$ satisfying $f(x) = x$ for all $x \in \alpha$, and for any partial value $o : \text{Part } \alpha$, the mapped partial value $\text{map } f o$ is equal to $o$.

Part.bind_some_right theorem

(x : Part α) : x.bind some = x

Full source

@[simp]
theorem bind_some_right (x : Part α) : x.bind some = x := by
  rw [bind_some_eq_map]
  simp [map_id']

Right Identity Law for Partial Value Binding: $x.\mathrm{bind}\,\mathrm{some} = x$

Informal description

For any partial value $x : \mathrm{Part}\,\alpha$, the binding of $x$ with the identity function `some` equals $x$ itself. That is, $$ x.\mathrm{bind}\,\mathrm{some} = x. $$

Part.pure_eq_some theorem

(a : α) : pure a = some a

Full source

@[simp]
theorem pure_eq_some (a : α) : pure a = some a :=
  rfl

Equality of Pure and Some in Partial Values

Informal description

For any element $a$ of type $\alpha$, the monadic `pure` operation on partial values is equal to the `some` constructor, i.e., $\text{pure}(a) = \text{some}(a)$.

Part.ret_eq_some theorem

(a : α) : (return a : Part α) = some a

Full source

@[simp]
theorem ret_eq_some (a : α) : (return a : Part α) = some a :=
  rfl

Monadic Return Equals Partial Some: $\text{return } a = \text{some } a$

Informal description

For any element $a$ of type $\alpha$, the monadic return operation applied to $a$ in the `Part` monad is equal to the partial value `some a`, i.e., $\text{return } a = \text{some } a$.

Part.map_eq_map theorem

{α β} (f : α → β) (o : Part α) : f <$> o = map f o

Full source

@[simp]
theorem map_eq_map {α β} (f : α → β) (o : Part α) : f <$> o = map f o :=
  rfl

Equivalence of Monadic Map and Partial Map Operations

Informal description

For any types $\alpha$ and $\beta$, any function $f : \alpha \to \beta$, and any partial value $o : \text{Part } \alpha$, the monadic map operation $f <$> $o$ is equal to $\text{map } f o$.

Part.bind_eq_bind theorem

{α β} (f : Part α) (g : α → Part β) : f >>= g = f.bind g

Full source

@[simp]
theorem bind_eq_bind {α β} (f : Part α) (g : α → Part β) : f >>= g = f.bind g :=
  rfl

Monadic Bind Equals Partial Value Binding

Informal description

For any types $\alpha$ and $\beta$, given a partial value $f : \text{Part } \alpha$ and a function $g : \alpha \to \text{Part } \beta$, the monadic bind operation `>>=` is equal to the partial value binding operation `bind`, i.e., $f \gg\!\!= g = f.\text{bind } g$.

Part.bind_le theorem

{α} (x : Part α) (f : α → Part β) (y : Part β) : x >>= f ≤ y ↔ ∀ a, a ∈ x → f a ≤ y

Full source

theorem bind_le {α} (x : Part α) (f : α → Part β) (y : Part β) :
    x >>= fx >>= f ≤ y ↔ ∀ a, a ∈ x → f a ≤ y := by
  constructor <;> intro h
  · intro a h' b
    have h := h b
    simp only [and_imp, exists_prop, bind_eq_bind, mem_bind_iff, exists_imp] at h
    apply h _ h'
  · intro b h'
    simp only [exists_prop, bind_eq_bind, mem_bind_iff] at h'
    rcases h' with ⟨a, h₀, h₁⟩
    apply h _ h₀ _ h₁

Characterization of Partial Order for Monadic Binding on Partial Values

Informal description

For any partial value $x \in \mathrm{Part}\,\alpha$, function $f \colon \alpha \to \mathrm{Part}\,\beta$, and partial value $y \in \mathrm{Part}\,\beta$, the following are equivalent: 1. The partial value obtained by binding $x$ with $f$ is less than or equal to $y$ in the partial order on $\mathrm{Part}\,\beta$. 2. For every element $a \in \alpha$ such that $a \in x$, the partial value $f(a)$ is less than or equal to $y$. Here, $a \in x$ means that $x$ is defined (i.e., $x.\mathrm{Dom}$ holds) and $x.\mathrm{get} = a$.

Part.restrict definition

(p : Prop) (o : Part α) (H : p → o.Dom) : Part α

Full source

/-- `restrict p o h` replaces the domain of `o` with `p`, and is well defined when
  `p` implies `o` is defined. -/
def restrict (p : Prop) (o : Part α) (H : p → o.Dom) : Part α :=
  ⟨p, fun h => o.get (H h)⟩

Restriction of a partial value

Informal description

Given a proposition `p` and a partial value `o : Part α` with a proof `H` that `p` implies `o.Dom`, the function `Part.restrict` constructs a new partial value with domain `p` and value `o.get (H h)` for any proof `h : p`. This effectively restricts the domain of `o` to `p`.

Part.mem_restrict theorem

(p : Prop) (o : Part α) (h : p → o.Dom) (a : α) : a ∈ restrict p o h ↔ p ∧ a ∈ o

Full source

@[simp]
theorem mem_restrict (p : Prop) (o : Part α) (h : p → o.Dom) (a : α) :
    a ∈ restrict p o ha ∈ restrict p o h ↔ p ∧ a ∈ o := by
  dsimp [restrict, mem_eq]; constructor
  · rintro ⟨h₀, h₁⟩
    exact ⟨h₀, ⟨_, h₁⟩⟩
  rintro ⟨h₀, _, h₂⟩; exact ⟨h₀, h₂⟩

Membership in Restricted Partial Value

Informal description

For any proposition $p$, partial value $o \in \mathrm{Part}\,\alpha$, proof $h$ that $p$ implies $o.\mathrm{Dom}$, and element $a \in \alpha$, we have $a \in \mathrm{restrict}\,p\,o\,h$ if and only if $p$ holds and $a \in o$.

Part.unwrap definition

(o : Part α) : α

Full source

/-- `unwrap o` gets the value at `o`, ignoring the condition. This function is unsound. -/
unsafe def unwrap (o : Part α) : α :=
  o.get lcProof

Unsound extraction of partial value

Informal description

The function `Part.unwrap` takes a partial value `o : Part α` and returns its value `o.get _`, ignoring the domain condition. This function is unsound because it does not require a proof that the domain is true, and thus may lead to inconsistencies if used improperly.

Part.assert_defined theorem

{p : Prop} {f : p → Part α} : ∀ h : p, (f h).Dom → (assert p f).Dom

Full source

theorem assert_defined {p : Prop} {f : p → Part α} : ∀ h : p, (f h).Dom → (assert p f).Dom :=
  Exists.intro

Domain Condition for Asserted Partial Value

Informal description

For any proposition $p$ and function $f : p \to \text{Part } \alpha$, if there exists a proof $h$ of $p$ such that $(f h).\text{Dom}$ holds, then the domain of $\text{Part.assert } p f$ is satisfied.

Part.bind_defined theorem

{f : Part α} {g : α → Part β} : ∀ h : f.Dom, (g (f.get h)).Dom → (f.bind g).Dom

Full source

theorem bind_defined {f : Part α} {g : α → Part β} :
    ∀ h : f.Dom, (g (f.get h)).Dom → (f.bind g).Dom :=
  assert_defined

Domain Condition for Partial Value Binding

Informal description

For any partial value $f : \text{Part } \alpha$ and function $g : \alpha \to \text{Part } \beta$, if $f$ is defined at $h$ (i.e., $f.\text{Dom}$ holds) and $g$ applied to $f.\text{get}(h)$ is defined, then the partial value $f.\text{bind } g$ is defined.

Part.bind_dom theorem

{f : Part α} {g : α → Part β} : (f.bind g).Dom ↔ ∃ h : f.Dom, (g (f.get h)).Dom

Full source

@[simp]
theorem bind_dom {f : Part α} {g : α → Part β} : (f.bind g).Dom ↔ ∃ h : f.Dom, (g (f.get h)).Dom :=
  Iff.rfl

Domain Condition for Partial Value Binding: $(f \mathbin{\text{bind}} g).\text{Dom} \leftrightarrow \exists h : f.\text{Dom}, (g(f.\text{get } h)).\text{Dom}$

Informal description

For a partial value $f : \text{Part } \alpha$ and a function $g : \alpha \to \text{Part } \beta$, the domain of the partial value $f \mathbin{\text{bind}} g$ holds if and only if there exists a proof $h$ that $f$ is defined (i.e., $f.\text{Dom}$ holds) and the partial value $g(f.\text{get } h)$ is also defined.

Part.instOne instance

[One α] : One (Part α)

Full source

@[to_additive]
instance [One α] : One (Part α) where one := pure 1

Distinguished Element in Partial Values

Informal description

For any type $\alpha$ with a distinguished element $1$, the type $\text{Part }\alpha$ of partial values of $\alpha$ inherits a distinguished element. Specifically, the partial value $\text{Part.some } 1$ has domain $\text{True}$ and value $1$.

Part.instMul instance

[Mul α] : Mul (Part α)

Full source

@[to_additive]
instance [Mul α] : Mul (Part α) where mul a b := (· * ·) <$> a(· * ·) <$> a <*> b

Multiplication Operation on Partial Values

Informal description

For any type $\alpha$ equipped with a multiplication operation, the type $\text{Part }\alpha$ of partial values of $\alpha$ inherits a multiplication operation. Specifically, if $o_1, o_2 : \text{Part }\alpha$ have domains $\text{Dom}_1$ and $\text{Dom}_2$ respectively, and values $\text{get}_1 : \text{Dom}_1 \to \alpha$ and $\text{get}_2 : \text{Dom}_2 \to \alpha$, then the product $o_1 \cdot o_2$ has domain $\text{Dom}_1 \land \text{Dom}_2$ and value $\text{get}_1 \cdot \text{get}_2 : \text{Dom}_1 \land \text{Dom}_2 \to \alpha$.

Part.instInv instance

[Inv α] : Inv (Part α)

Full source

@[to_additive]
instance [Inv α] : Inv (Part α) where inv := map Inv.inv

Inversion Operation on Partial Values

Informal description

For any type $\alpha$ with an inversion operation, the type $\text{Part }\alpha$ of partial values of $\alpha$ inherits an inversion operation. Specifically, if $o : \text{Part }\alpha$ has domain $\text{Dom}$ and value $\text{get} : \text{Dom} \to \alpha$, then the inverse $o^{-1}$ has the same domain $\text{Dom}$ and value $\text{get}^{-1} : \text{Dom} \to \alpha$.

Part.instDiv instance

[Div α] : Div (Part α)

Full source

@[to_additive]
instance [Div α] : Div (Part α) where div a b := (· / ·) <$> a(· / ·) <$> a <*> b

Division Operation on Partial Values

Informal description

For any type $\alpha$ equipped with a division operation, the type $\text{Part }\alpha$ of partial values of $\alpha$ inherits a division operation. Specifically, if $o_1, o_2 : \text{Part }\alpha$ have domains $\text{Dom}_1$ and $\text{Dom}_2$ respectively, and values $\text{get}_1 : \text{Dom}_1 \to \alpha$ and $\text{get}_2 : \text{Dom}_2 \to \alpha$, then the division $o_1 / o_2$ has domain $\text{Dom}_1 \land \text{Dom}_2$ and value $\text{get}_1 / \text{get}_2 : \text{Dom}_1 \land \text{Dom}_2 \to \alpha$.

Part.instMod instance

[Mod α] : Mod (Part α)

Full source

instance [Mod α] : Mod (Part α) where mod a b := (· % ·) <$> a(· % ·) <$> a <*> b

Modulus Operation on Partial Values

Informal description

For any type $\alpha$ with a modulus operation, the type $\text{Part }\alpha$ of partial values of $\alpha$ inherits a modulus operation. Specifically, if $o : \text{Part }\alpha$ has domain $\text{Dom}$ and value $\text{get} : \text{Dom} \to \alpha$, then the modulus operation $o \ \% \ o'$ has domain $\text{Dom} \land \text{Dom}'$ and value $\text{get} \ \% \ \text{get}' : \text{Dom} \land \text{Dom}' \to \alpha$.

Part.instAppend instance

[Append α] : Append (Part α)

Full source

instance [Append α] : Append (Part α) where append a b := (· ++ ·) <$> a(· ++ ·) <$> a <*> b

Append Operation on Partial Values

Informal description

For any type $\alpha$ with an append operation, the partial values $\mathrm{Part}\,\alpha$ inherit an append operation where the domain of the result is the conjunction of the domains of the operands, and the value is the append of their values when defined.

Part.instInter instance

[Inter α] : Inter (Part α)

Full source

instance [Inter α] : Inter (Part α) where inter a b := (· ∩ ·) <$> a(· ∩ ·) <$> a <*> b

Intersection Operation on Partial Values

Informal description

For any type $\alpha$ with an intersection operation $\cap$, the partial values $\mathrm{Part}\,\alpha$ inherit an intersection operation where the domain of the intersection is the conjunction of the domains of the operands, and the value is the intersection of their values when both domains are satisfied.

Part.instUnion instance

[Union α] : Union (Part α)

Full source

instance [Union α] : Union (Part α) where union a b := (· ∪ ·) <$> a(· ∪ ·) <$> a <*> b

Union Operation on Partial Values

Informal description

For any type $\alpha$ equipped with a union operation $\cup$, the partial values `Part α` inherit a union operation where the union of two partial values is defined when both are defined, and its value is the union of their values.

Part.instSDiff instance

[SDiff α] : SDiff (Part α)

Full source

instance [SDiff α] : SDiff (Part α) where sdiff a b := (· \ ·) <$> a(· \ ·) <$> a <*> b

Set Difference Operation on Partial Values

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$, the type $\mathrm{Part}\,\alpha$ of partial values of $\alpha$ inherits a set difference operation, defined pointwise on the domains.

Part.mul_def theorem

[Mul α] (a b : Part α) : a * b = bind a fun y ↦ map (y * ·) b

Full source

@[to_additive]
theorem mul_def [Mul α] (a b : Part α) : a * b = bind a fun y ↦ map (y * ·) b := rfl

Definition of Multiplication for Partial Values: $a * b = \text{bind } a (\lambda y, \text{map } (y * \cdot) b)$

Informal description

For any type $\alpha$ with a multiplication operation and any partial values $a, b \in \text{Part }\alpha$, the product $a * b$ is equal to the partial value obtained by binding $a$ with the function $\lambda y, \text{map } (y * \cdot) b$.

Part.one_def theorem

[One α] : (1 : Part α) = some 1

Full source

@[to_additive]
theorem one_def [One α] : (1 : Part α) = some 1 := rfl

Definition of One in Partial Values: $1 = \mathrm{some}\,1$

Informal description

For any type $\alpha$ with a distinguished element $1$, the partial value $1$ in $\mathrm{Part}\,\alpha$ is equal to $\mathrm{some}\,1$, where $\mathrm{some}$ constructs a partial value with a true domain and value $1$.

Part.inv_def theorem

[Inv α] (a : Part α) : a⁻¹ = Part.map (·⁻¹) a

Full source

@[to_additive]
theorem inv_def [Inv α] (a : Part α) : a⁻¹ = Part.map (· ⁻¹) a := rfl

Definition of Inversion for Partial Values: $a^{-1} = \text{map } (\cdot^{-1}) a$

Informal description

For any type $\alpha$ with an inversion operation and any partial value $a : \text{Part }\alpha$, the inverse $a^{-1}$ is equal to the partial value obtained by mapping the inversion operation over $a$. That is, $a^{-1} = \text{Part.map } (\cdot^{-1}) a$.

Part.div_def theorem

[Div α] (a b : Part α) : a / b = bind a fun y => map (y / ·) b

Full source

@[to_additive]
theorem div_def [Div α] (a b : Part α) : a / b = bind a fun y => map (y / ·) b := rfl

Definition of Division for Partial Values: $a / b = \text{bind } a (\lambda y, \text{map } (y / \cdot) b)$

Informal description

For any type $\alpha$ equipped with a division operation and any partial values $a, b : \text{Part }\alpha$, the division $a / b$ is defined as the partial value obtained by first binding $a$ to a function that maps division by elements of $b$. Specifically, $a / b = \text{bind } a (\lambda y, \text{map } (y / \cdot) b)$.

Part.mod_def theorem

[Mod α] (a b : Part α) : a % b = bind a fun y => map (y % ·) b

Full source

theorem mod_def [Mod α] (a b : Part α) : a % b = bind a fun y => map (y % ·) b := rfl

Modulus Operation Definition for Partial Values: $a \% b = \text{bind } a (\lambda y, \text{map } (y \% \cdot) b)$

Informal description

For any type $\alpha$ with a modulus operation and any partial values $a, b : \text{Part }\alpha$, the modulus operation $a \% b$ is defined as the partial value obtained by first binding $a$ to a function that maps the modulus operation over $b$. Specifically, $a \% b = \text{bind } a (\lambda y, \text{map } (y \% \cdot) b)$.

Part.append_def theorem

[Append α] (a b : Part α) : a ++ b = bind a fun y => map (y ++ ·) b

Full source

theorem append_def [Append α] (a b : Part α) : a ++ b = bind a fun y => map (y ++ ·) b := rfl

Definition of Append Operation on Partial Values

Informal description

For any type $\alpha$ with an append operation `++`, and for any partial values $a, b : \mathrm{Part}\,\alpha$, the append operation on partial values is defined as: \[ a \mathbin{++} b = \mathrm{bind}\, a \, \bigl( \lambda y \mapsto \mathrm{map}\, (y \mathbin{++} \cdot)\, b \bigr) \] Here, $\mathrm{bind}$ and $\mathrm{map}$ are the monadic operations for partial values, where $\mathrm{bind}$ composes partial values and $\mathrm{map}$ applies a function to the value of a partial value while preserving its domain.

Part.inter_def theorem

[Inter α] (a b : Part α) : a ∩ b = bind a fun y => map (y ∩ ·) b

Full source

theorem inter_def [Inter α] (a b : Part α) : a ∩ b = bind a fun y => map (y ∩ ·) b := rfl

Definition of Intersection for Partial Values

Informal description

For any type $\alpha$ with an intersection operation $\cap$, the intersection of two partial values $a, b : \mathrm{Part}\,\alpha$ is defined as the partial value obtained by first binding $a$ to a value $y$ and then mapping the intersection operation $y \cap \cdot$ over $b$. Formally, $a \cap b = \mathrm{bind}\, a\, (\lambda y, \mathrm{map}\, (y \cap \cdot)\, b)$.

Part.union_def theorem

[Union α] (a b : Part α) : a ∪ b = bind a fun y => map (y ∪ ·) b

Full source

theorem union_def [Union α] (a b : Part α) : a ∪ b = bind a fun y => map (y ∪ ·) b := rfl

Definition of Union for Partial Values via Binding and Mapping

Informal description

For any type $\alpha$ with a union operation $\cup$, and for any partial values $a, b : \text{Part } \alpha$, the union $a \cup b$ is defined as the partial value obtained by first binding $a$ to a function that maps each value $y$ of $a$ to the union of $y$ with the value of $b$ (via `map`).

Part.sdiff_def theorem

[SDiff α] (a b : Part α) : a \ b = bind a fun y => map (y \ ·) b

Full source

theorem sdiff_def [SDiff α] (a b : Part α) : a \ b = bind a fun y => map (y \ ·) b := rfl

Definition of Set Difference for Partial Values

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$, and for any partial values $a, b : \mathrm{Part}\,\alpha$, the set difference $a \setminus b$ is defined as the partial value obtained by binding $a$ with a function that maps each element $y$ of $a$ to the set difference $y \setminus x$ for each element $x$ of $b$.

Part.one_mem_one theorem

[One α] : (1 : α) ∈ (1 : Part α)

Full source

@[to_additive]
theorem one_mem_one [One α] : (1 : α) ∈ (1 : Part α) :=
  ⟨trivial, rfl⟩

Membership of One in Partial One

Informal description

For any type $\alpha$ with a distinguished element $1$, the element $1$ is a member of the partial value $1$ in $\mathrm{Part}\,\alpha$. That is, $1 \in (1 : \mathrm{Part}\,\alpha)$ holds, meaning the partial value is defined and its value equals $1$.

Part.mul_mem_mul theorem

[Mul α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma * mb ∈ a * b

Full source

@[to_additive]
theorem mul_mem_mul [Mul α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma * mb ∈ a * b := ⟨⟨ha.1, hb.1⟩, by simp only [← ha.2, ← hb.2]; rfl⟩

Membership Preservation under Multiplication of Partial Values

Informal description

For any type $\alpha$ with a multiplication operation, and for any partial values $a, b : \mathrm{Part}\,\alpha$ and elements $m_a, m_b : \alpha$, if $m_a$ is in $a$ (i.e., $a$ is defined and equals $m_a$) and $m_b$ is in $b$ (i.e., $b$ is defined and equals $m_b$), then the product $m_a \cdot m_b$ is in the product $a \cdot b$ (i.e., $a \cdot b$ is defined and equals $m_a \cdot m_b$).

Part.left_dom_of_mul_dom theorem

[Mul α] {a b : Part α} (hab : Dom (a * b)) : a.Dom

Full source

@[to_additive]
theorem left_dom_of_mul_dom [Mul α] {a b : Part α} (hab : Dom (a * b)) : a.Dom := hab.1

Left Factor Definedness in Partial Multiplication

Informal description

For any type $\alpha$ with a multiplication operation, and for any partial values $a, b : \text{Part }\alpha$, if the product $a \cdot b$ is defined (i.e., $\text{Dom}(a \cdot b)$ holds), then $a$ is defined (i.e., $a.\text{Dom}$ holds).

Part.right_dom_of_mul_dom theorem

[Mul α] {a b : Part α} (hab : Dom (a * b)) : b.Dom

Full source

@[to_additive]
theorem right_dom_of_mul_dom [Mul α] {a b : Part α} (hab : Dom (a * b)) : b.Dom := hab.2

Right Multiplicand is Defined When Product is Defined in Partial Values

Informal description

For any type $\alpha$ with a multiplication operation and partial values $a, b : \text{Part }\alpha$, if the product $a \cdot b$ is defined (i.e., $\text{Dom}(a \cdot b)$ holds), then the partial value $b$ is also defined (i.e., $\text{Dom}(b)$ holds).

Part.mul_get_eq theorem

 [Mul α] (a b : Part α) (hab : Dom (a * b)) :
  (a * b).get hab = a.get (left_dom_of_mul_dom hab) * b.get (right_dom_of_mul_dom hab)

Full source

@[to_additive (attr := simp)]
theorem mul_get_eq [Mul α] (a b : Part α) (hab : Dom (a * b)) :
    (a * b).get hab = a.get (left_dom_of_mul_dom hab) * b.get (right_dom_of_mul_dom hab) := rfl

Value of Product of Partial Values Equals Product of Values

Informal description

For any type $\alpha$ with a multiplication operation and any partial values $a, b : \text{Part }\alpha$, if the product $a \cdot b$ is defined (i.e., $\text{Dom}(a \cdot b)$ holds), then the value of $a \cdot b$ is equal to the product of the values of $a$ and $b$ under their respective domains. That is, $$(a \cdot b).\text{get}(hab) = a.\text{get}(h_a) \cdot b.\text{get}(h_b)$$ where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined (which exist since $a \cdot b$ is defined).

Part.some_mul_some theorem

[Mul α] (a b : α) : some a * some b = some (a * b)

Full source

@[to_additive]
theorem some_mul_some [Mul α] (a b : α) : some a * some b = some (a * b) := by simp [mul_def]

Multiplication of Partial Some Values: $\text{some } a \cdot \text{some } b = \text{some } (a \cdot b)$

Informal description

For any type $\alpha$ with a multiplication operation and any elements $a, b \in \alpha$, the product of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \cdot b)$.

Part.inv_mem_inv theorem

[Inv α] (a : Part α) (ma : α) (ha : ma ∈ a) : ma⁻¹ ∈ a⁻¹

Full source

@[to_additive]
theorem inv_mem_inv [Inv α] (a : Part α) (ma : α) (ha : ma ∈ a) : ma⁻¹ma⁻¹ ∈ a⁻¹ := by
  simp [inv_def]; aesop

Inverse Membership in Partial Values: $m_a \in a \implies m_a^{-1} \in a^{-1}$

Informal description

For any type $\alpha$ with an inversion operation and any partial value $a : \text{Part }\alpha$, if an element $m_a \in \alpha$ is a member of $a$ (i.e., $a$ is defined and its value equals $m_a$), then the inverse $m_a^{-1}$ is a member of the inverse partial value $a^{-1}$.

Part.inv_some theorem

[Inv α] (a : α) : (some a)⁻¹ = some a⁻¹

Full source

@[to_additive]
theorem inv_some [Inv α] (a : α) : (some a)⁻¹ = some a⁻¹ :=
  rfl

Inverse of Partial Some: $(\text{some } a)^{-1} = \text{some } a^{-1}$

Informal description

For any type $\alpha$ with an inversion operation and any element $a \in \alpha$, the inverse of the partial value $\text{some } a$ is equal to $\text{some } a^{-1}$.

Part.div_mem_div theorem

[Div α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma / mb ∈ a / b

Full source

@[to_additive]
theorem div_mem_div [Div α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma / mb ∈ a / b := by simp [div_def]; aesop

Membership Preservation under Division of Partial Values: $m_a \in a \land m_b \in b \implies m_a / m_b \in a / b$

Informal description

For any type $\alpha$ with a division operation, and for any partial values $a, b : \mathrm{Part}\,\alpha$, if $m_a \in \alpha$ is a member of $a$ (i.e., $a$ is defined and its value equals $m_a$) and $m_b \in \alpha$ is a member of $b$, then the division $m_a / m_b$ is a member of the partial value $a / b$.

Part.left_dom_of_div_dom theorem

[Div α] {a b : Part α} (hab : Dom (a / b)) : a.Dom

Full source

@[to_additive]
theorem left_dom_of_div_dom [Div α] {a b : Part α} (hab : Dom (a / b)) : a.Dom := hab.1

Left Operand Defined in Partial Division

Informal description

For any type $\alpha$ with a division operation and any partial values $a, b : \text{Part }\alpha$, if the division $a / b$ is defined (i.e., $\text{Dom}(a / b)$ holds), then the partial value $a$ must also be defined (i.e., $\text{Dom}(a)$ holds).

Part.right_dom_of_div_dom theorem

[Div α] {a b : Part α} (hab : Dom (a / b)) : b.Dom

Full source

@[to_additive]
theorem right_dom_of_div_dom [Div α] {a b : Part α} (hab : Dom (a / b)) : b.Dom := hab.2

Right Operand's Domain in Division of Partial Values

Informal description

For any type $\alpha$ with a division operation and any partial values $a, b : \text{Part }\alpha$, if the division $a / b$ is defined (i.e., $\text{Dom}(a / b)$ holds), then the domain of $b$ must hold (i.e., $\text{Dom}(b)$ holds).

Part.div_get_eq theorem

 [Div α] (a b : Part α) (hab : Dom (a / b)) :
  (a / b).get hab = a.get (left_dom_of_div_dom hab) / b.get (right_dom_of_div_dom hab)

Full source

@[to_additive (attr := simp)]
theorem div_get_eq [Div α] (a b : Part α) (hab : Dom (a / b)) :
    (a / b).get hab = a.get (left_dom_of_div_dom hab) / b.get (right_dom_of_div_dom hab) := by
  simp [div_def]; aesop

Value of Partial Division Equals Division of Values

Informal description

For any type $\alpha$ with a division operation and any partial values $a, b : \text{Part }\alpha$, if the division $a / b$ is defined (i.e., $\text{Dom}(a / b)$ holds), then the value of $a / b$ is equal to the division of the values of $a$ and $b$ under their respective domains. Specifically, $(a / b).\text{get}(h_{ab}) = a.\text{get}(h_a) / b.\text{get}(h_b)$, where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined, derived from $h_{ab}$.

Part.some_div_some theorem

[Div α] (a b : α) : some a / some b = some (a / b)

Full source

@[to_additive]
theorem some_div_some [Div α] (a b : α) : some a / some b = some (a / b) := by simp [div_def]

Division of Defined Partial Values: $\text{some } a / \text{some } b = \text{some } (a / b)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a division operation, the division of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a / b)$. That is, $\text{some } a / \text{some } b = \text{some } (a / b)$.

Part.mod_mem_mod theorem

[Mod α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma % mb ∈ a % b

Full source

theorem mod_mem_mod [Mod α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma % mb ∈ a % b := by simp [mod_def]; aesop

Membership Preservation under Modulus Operation on Partial Values

Informal description

For any type $\alpha$ with a modulus operation, given partial values $a, b : \text{Part }\alpha$ and elements $m_a, m_b \in \alpha$ such that $m_a \in a$ and $m_b \in b$, it holds that $m_a \% m_b \in a \% b$.

Part.left_dom_of_mod_dom theorem

[Mod α] {a b : Part α} (hab : Dom (a % b)) : a.Dom

Full source

theorem left_dom_of_mod_dom [Mod α] {a b : Part α} (hab : Dom (a % b)) : a.Dom := hab.1

Domain of Left Operand in Partial Modulus Operation

Informal description

For any type $\alpha$ with a modulus operation, and for any partial values $a, b : \text{Part }\alpha$, if the modulus operation $a \% b$ is defined (i.e., $\text{Dom}(a \% b)$ holds), then the partial value $a$ is also defined (i.e., $a.\text{Dom}$ holds).

Part.right_dom_of_mod_dom theorem

[Mod α] {a b : Part α} (hab : Dom (a % b)) : b.Dom

Full source

theorem right_dom_of_mod_dom [Mod α] {a b : Part α} (hab : Dom (a % b)) : b.Dom := hab.2

Right Operand Defined in Modulus of Partial Values

Informal description

For any type $\alpha$ with a modulus operation, and for any partial values $a, b : \text{Part }\alpha$, if the modulus operation $a \% b$ is defined (i.e., $\text{Dom}(a \% b)$ holds), then the domain of $b$ must also hold (i.e., $\text{Dom}(b)$ holds).

Part.mod_get_eq theorem

 [Mod α] (a b : Part α) (hab : Dom (a % b)) :
  (a % b).get hab = a.get (left_dom_of_mod_dom hab) % b.get (right_dom_of_mod_dom hab)

Full source

@[simp]
theorem mod_get_eq [Mod α] (a b : Part α) (hab : Dom (a % b)) :
    (a % b).get hab = a.get (left_dom_of_mod_dom hab) % b.get (right_dom_of_mod_dom hab) := by
  simp [mod_def]; aesop

Value of Modulus Operation on Partial Values

Informal description

For any type $\alpha$ with a modulus operation, and for any partial values $a, b : \text{Part }\alpha$, if the modulus operation $a \% b$ is defined (i.e., $\text{Dom}(a \% b)$ holds), then the value of $a \% b$ is equal to the modulus of the values of $a$ and $b$ under their respective domains. Specifically, $(a \% b).\text{get}(h_{ab}) = a.\text{get}(h_a) \% b.\text{get}(h_b)$, where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined, derived from $h_{ab}$.

Part.some_mod_some theorem

[Mod α] (a b : α) : some a % some b = some (a % b)

Full source

theorem some_mod_some [Mod α] (a b : α) : some a % some b = some (a % b) := by simp [mod_def]

Modulus of Partial Some Values: $\text{some } a \% \text{some } b = \text{some } (a \% b)$

Informal description

For any elements $a$ and $b$ of a type $\alpha$ equipped with a modulus operation, the modulus of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \% b)$. That is, $\text{some } a \% \text{some } b = \text{some } (a \% b)$.

Part.append_mem_append theorem

[Append α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ++ mb ∈ a ++ b

Full source

theorem append_mem_append [Append α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ++ mb ∈ a ++ b := by simp [append_def]; aesop

Membership Preservation under Append for Partial Values

Informal description

Let $\alpha$ be a type with an append operation `++`. For any partial values $a, b : \text{Part}\,\alpha$ and elements $m_a, m_b : \alpha$, if $m_a$ is in $a$ (i.e., $a$ is defined and equals $m_a$) and $m_b$ is in $b$ (i.e., $b$ is defined and equals $m_b$), then the append $m_a \mathbin{++} m_b$ is in the append $a \mathbin{++} b$ (i.e., $a \mathbin{++} b$ is defined and equals $m_a \mathbin{++} m_b$).

Part.left_dom_of_append_dom theorem

[Append α] {a b : Part α} (hab : Dom (a ++ b)) : a.Dom

Full source

theorem left_dom_of_append_dom [Append α] {a b : Part α} (hab : Dom (a ++ b)) : a.Dom := hab.1

Domain of Left Operand in Partial Append Operation

Informal description

For any type $\alpha$ with an append operation and any partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \mathbin{+\!\!+} b$ holds, then the domain of $a$ must also hold.

Part.right_dom_of_append_dom theorem

[Append α] {a b : Part α} (hab : Dom (a ++ b)) : b.Dom

Full source

theorem right_dom_of_append_dom [Append α] {a b : Part α} (hab : Dom (a ++ b)) : b.Dom := hab.2

Right Domain Condition for Append Operation on Partial Values

Informal description

For any type $\alpha$ with an append operation and any partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \mathbin{+\!\!+} b$ holds (i.e., $(a \mathbin{+\!\!+} b).\mathrm{Dom}$), then the domain of $b$ holds (i.e., $b.\mathrm{Dom}$).

Part.append_get_eq theorem

 [Append α] (a b : Part α) (hab : Dom (a ++ b)) :
  (a ++ b).get hab = a.get (left_dom_of_append_dom hab) ++ b.get (right_dom_of_append_dom hab)

Full source

@[simp]
theorem append_get_eq [Append α] (a b : Part α) (hab : Dom (a ++ b)) : (a ++ b).get hab =
    a.get (left_dom_of_append_dom hab) ++ b.get (right_dom_of_append_dom hab) := by
  simp [append_def]; aesop

Value of Partial Append Operation: $(a \mathbin{+\!\!+} b).\mathrm{get} = a.\mathrm{get} \mathbin{+\!\!+} b.\mathrm{get}$

Informal description

For any type $\alpha$ with an append operation `++`, and for any partial values $a, b : \mathrm{Part}\,\alpha$ such that the domain of $a \mathbin{+\!\!+} b$ holds, the value of $a \mathbin{+\!\!+} b$ is equal to the append of the values of $a$ and $b$ under their respective domain proofs. That is, $$(a \mathbin{+\!\!+} b).\mathrm{get}(h_{ab}) = a.\mathrm{get}(h_a) \mathbin{+\!\!+} b.\mathrm{get}(h_b),$$ where $h_a$ is a proof that $a$ is defined (obtained from $h_{ab}$ via `left_dom_of_append_dom`) and $h_b$ is a proof that $b$ is defined (obtained via `right_dom_of_append_dom`).

Part.some_append_some theorem

[Append α] (a b : α) : some a ++ some b = some (a ++ b)

Full source

theorem some_append_some [Append α] (a b : α) : some a ++ some b = some (a ++ b) := by
  simp [append_def]

Append of Partial Some Values: $\text{some } a \mathbin{+\!\!+} \text{some } b = \text{some } (a \mathbin{+\!\!+} b)$

Informal description

For any type $\alpha$ with an append operation `++`, and for any elements $a, b \in \alpha$, the append of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \mathbin{+\!\!+} b)$. That is, $\text{some } a \mathbin{+\!\!+} \text{some } b = \text{some } (a \mathbin{+\!\!+} b)$.

Part.inter_mem_inter theorem

[Inter α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ∩ mb ∈ a ∩ b

Full source

theorem inter_mem_inter [Inter α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ∩ mbma ∩ mb ∈ a ∩ b := by simp [inter_def]; aesop

Intersection of Elements in Partial Values

Informal description

For any type $\alpha$ with an intersection operation $\cap$, and for any partial values $a, b : \mathrm{Part}\,\alpha$ with elements $m_a \in a$ and $m_b \in b$, the intersection $m_a \cap m_b$ is an element of the intersection $a \cap b$. Here, $m_a \in a$ means that the partial value $a$ is defined (i.e., $a.\mathrm{Dom}$ holds) and its value equals $m_a$, and similarly for $m_b \in b$.

Part.left_dom_of_inter_dom theorem

[Inter α] {a b : Part α} (hab : Dom (a ∩ b)) : a.Dom

Full source

theorem left_dom_of_inter_dom [Inter α] {a b : Part α} (hab : Dom (a ∩ b)) : a.Dom := hab.1

Domain of Left Operand in Partial Intersection

Informal description

For any type $\alpha$ with an intersection operation $\cap$ and partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \cap b$ holds, then the domain of $a$ must also hold.

Part.right_dom_of_inter_dom theorem

[Inter α] {a b : Part α} (hab : Dom (a ∩ b)) : b.Dom

Full source

theorem right_dom_of_inter_dom [Inter α] {a b : Part α} (hab : Dom (a ∩ b)) : b.Dom := hab.2

Right Domain Condition for Intersection of Partial Values

Informal description

For any type $\alpha$ with an intersection operation $\cap$, and for any partial values $a, b : \mathrm{Part}\,\alpha$, if the intersection $a \cap b$ is defined (i.e., $\mathrm{Dom}(a \cap b)$ holds), then the partial value $b$ is also defined (i.e., $b.\mathrm{Dom}$ holds).

Part.inter_get_eq theorem

 [Inter α] (a b : Part α) (hab : Dom (a ∩ b)) :
  (a ∩ b).get hab = a.get (left_dom_of_inter_dom hab) ∩ b.get (right_dom_of_inter_dom hab)

Full source

@[simp]
theorem inter_get_eq [Inter α] (a b : Part α) (hab : Dom (a ∩ b)) :
    (a ∩ b).get hab = a.get (left_dom_of_inter_dom hab) ∩ b.get (right_dom_of_inter_dom hab) := by
  simp [inter_def]; aesop

Value of Intersection of Partial Values Equals Intersection of Values

Informal description

For any type $\alpha$ with an intersection operation $\cap$ and any partial values $a, b : \mathrm{Part}\,\alpha$, if the intersection $a \cap b$ is defined (i.e., $\mathrm{Dom}(a \cap b)$ holds), then the value of $a \cap b$ is equal to the intersection of the values of $a$ and $b$ under their respective domain proofs. That is, $(a \cap b).\mathrm{get}(hab) = a.\mathrm{get}(h_a) \cap b.\mathrm{get}(h_b)$, where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined.

Part.some_inter_some theorem

[Inter α] (a b : α) : some a ∩ some b = some (a ∩ b)

Full source

theorem some_inter_some [Inter α] (a b : α) : somesome a ∩ some b = some (a ∩ b) := by
  simp [inter_def]

Intersection of Defined Partial Values: $\text{some } a \cap \text{some } b = \text{some } (a \cap b)$

Informal description

For any type $\alpha$ with an intersection operation $\cap$ and any elements $a, b \in \alpha$, the intersection of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \cap b)$. That is, $\text{some } a \cap \text{some } b = \text{some } (a \cap b)$.

Part.union_mem_union theorem

[Union α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ∪ mb ∈ a ∪ b

Full source

theorem union_mem_union [Union α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ∪ mbma ∪ mb ∈ a ∪ b := by simp [union_def]; aesop

Union of Elements in Partial Values

Informal description

Let $\alpha$ be a type equipped with a union operation $\cup$. For any partial values $a, b : \mathrm{Part}\,\alpha$ and elements $m_a, m_b \in \alpha$, if $m_a \in a$ and $m_b \in b$, then $m_a \cup m_b \in a \cup b$.

Part.left_dom_of_union_dom theorem

[Union α] {a b : Part α} (hab : Dom (a ∪ b)) : a.Dom

Full source

theorem left_dom_of_union_dom [Union α] {a b : Part α} (hab : Dom (a ∪ b)) : a.Dom := hab.1

Left Operand Defined in Union of Partial Values

Informal description

For any type $\alpha$ with a union operation $\cup$ and partial values $a, b : \text{Part } \alpha$, if the union $a \cup b$ is defined (i.e., $\text{Dom}(a \cup b)$ holds), then $a$ is defined (i.e., $a.\text{Dom}$ holds).

Part.right_dom_of_union_dom theorem

[Union α] {a b : Part α} (hab : Dom (a ∪ b)) : b.Dom

Full source

theorem right_dom_of_union_dom [Union α] {a b : Part α} (hab : Dom (a ∪ b)) : b.Dom := hab.2

Right Operand Defined in Union of Partial Values

Informal description

For any type $\alpha$ with a union operation $\cup$, and for any partial values $a, b : \text{Part } \alpha$, if the union $a \cup b$ is defined (i.e., $\text{Dom}(a \cup b)$ holds), then $b$ is also defined (i.e., $\text{Dom}(b)$ holds).

Part.union_get_eq theorem

 [Union α] (a b : Part α) (hab : Dom (a ∪ b)) :
  (a ∪ b).get hab = a.get (left_dom_of_union_dom hab) ∪ b.get (right_dom_of_union_dom hab)

Full source

@[simp]
theorem union_get_eq [Union α] (a b : Part α) (hab : Dom (a ∪ b)) :
    (a ∪ b).get hab = a.get (left_dom_of_union_dom hab) ∪ b.get (right_dom_of_union_dom hab) := by
  simp [union_def]; aesop

Value of Union of Partial Values Equals Union of Their Values

Informal description

For any type $\alpha$ with a union operation $\cup$ and any partial values $a, b : \text{Part } \alpha$, if the union $a \cup b$ is defined (i.e., $\text{Dom}(a \cup b)$ holds), then the value of $a \cup b$ is equal to the union of the values of $a$ and $b$ under their respective domains. Formally, $(a \cup b).\text{get}(hab) = a.\text{get}(h_a) \cup b.\text{get}(h_b)$, where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined (which exist because $a \cup b$ is defined).

Part.some_union_some theorem

[Union α] (a b : α) : some a ∪ some b = some (a ∪ b)

Full source

theorem some_union_some [Union α] (a b : α) : somesome a ∪ some b = some (a ∪ b) := by simp [union_def]

Union of Defined Partial Values: $\text{some } a \cup \text{some } b = \text{some } (a \cup b)$

Informal description

For any type $\alpha$ with a union operation $\cup$ and any elements $a, b \in \alpha$, the union of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \cup b)$. In other words, $\text{some } a \cup \text{some } b = \text{some } (a \cup b)$.

Part.sdiff_mem_sdiff theorem

[SDiff α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma \ mb ∈ a \ b

Full source

theorem sdiff_mem_sdiff [SDiff α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma \ mbma \ mb ∈ a \ b := by simp [sdiff_def]; aesop

Set Difference Membership in Partial Values

Informal description

For any type $\alpha$ with a set difference operation $\setminus$, and for any partial values $a, b : \mathrm{Part}\,\alpha$ and elements $m_a, m_b \in \alpha$, if $m_a$ is in $a$ and $m_b$ is in $b$, then the set difference $m_a \setminus m_b$ is in the partial set difference $a \setminus b$.

Part.left_dom_of_sdiff_dom theorem

[SDiff α] {a b : Part α} (hab : Dom (a \ b)) : a.Dom

Full source

theorem left_dom_of_sdiff_dom [SDiff α] {a b : Part α} (hab : Dom (a \ b)) : a.Dom := hab.1

Domain of Left Operand in Partial Set Difference

Informal description

For any type $\alpha$ with a set difference operation $\setminus$ and partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \setminus b$ is true, then the domain of $a$ must also be true.

Part.right_dom_of_sdiff_dom theorem

[SDiff α] {a b : Part α} (hab : Dom (a \ b)) : b.Dom

Full source

theorem right_dom_of_sdiff_dom [SDiff α] {a b : Part α} (hab : Dom (a \ b)) : b.Dom := hab.2

Domain of Right Operand in Partial Set Difference

Informal description

For any type $\alpha$ with a set difference operation $\setminus$ and any partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \setminus b$ is true, then the domain of $b$ must also be true.

Part.sdiff_get_eq theorem

 [SDiff α] (a b : Part α) (hab : Dom (a \ b)) :
  (a \ b).get hab = a.get (left_dom_of_sdiff_dom hab) \ b.get (right_dom_of_sdiff_dom hab)

Full source

@[simp]
theorem sdiff_get_eq [SDiff α] (a b : Part α) (hab : Dom (a \ b)) :
    (a \ b).get hab = a.get (left_dom_of_sdiff_dom hab) \ b.get (right_dom_of_sdiff_dom hab) := by
  simp [sdiff_def]; aesop

Value of Partial Set Difference: $(a \setminus b).\mathrm{get} = a.\mathrm{get} \setminus b.\mathrm{get}$

Informal description

For any type $\alpha$ equipped with a set difference operation $\setminus$ and any partial values $a, b : \mathrm{Part}\,\alpha$, if the domain of $a \setminus b$ is true (denoted by $\mathrm{Dom}(a \setminus b)$), then the value of $a \setminus b$ is equal to the set difference of the values of $a$ and $b$ under their respective domain proofs. That is, $$(a \setminus b).\mathrm{get}(h_{ab}) = a.\mathrm{get}(h_a) \setminus b.\mathrm{get}(h_b),$$ where $h_a$ and $h_b$ are proofs that $a$ and $b$ are defined (i.e., $\mathrm{Dom}(a)$ and $\mathrm{Dom}(b)$ hold).

Part.some_sdiff_some theorem

[SDiff α] (a b : α) : some a \ some b = some (a \ b)

Full source

theorem some_sdiff_some [SDiff α] (a b : α) : somesome a \ some b = some (a \ b) := by simp [sdiff_def]

Set Difference of Partial Some Values: $\text{some } a \setminus \text{some } b = \text{some } (a \setminus b)$

Informal description

For any type $\alpha$ with a set difference operation $\setminus$ and any elements $a, b \in \alpha$, the set difference of the partial values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (a \setminus b)$. That is, $\text{some } a \setminus \text{some } b = \text{some } (a \setminus b)$.

Mathlib.Data.Part

Main declarations

Notation