Mathlib.Logic.Relation

IsRefl.reflexive theorem

[IsRefl α r] : Reflexive r

Full source

theorem IsRefl.reflexive [IsRefl α r] : Reflexive r := fun x ↦ IsRefl.refl x

Reflexive Property from Reflexive Relation Instance

Informal description

For any type $\alpha$ and relation $r$ on $\alpha$, if $r$ is reflexive (i.e., the `IsRefl` typeclass holds for $r$), then $r$ satisfies the reflexive property: for all $x \in \alpha$, $r\ x\ x$ holds.

Reflexive.rel_of_ne_imp theorem

(h : Reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y

Full source

/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`. -/
theorem Reflexive.rel_of_ne_imp (h : Reflexive r) {x y : α} (hr : x ≠ y → r x y) : r x y := by
  by_cases hxy : x = y
  · exact hxy ▸ h x
  · exact hr hxy

Reflexive Relation Criterion via Inequality Condition

Informal description

Let $r$ be a reflexive relation on a type $\alpha$. For any elements $x, y \in \alpha$, if $r(x, y)$ holds whenever $x \neq y$, then $r(x, y)$ holds for all $x, y \in \alpha$.

Reflexive.ne_imp_iff theorem

(h : Reflexive r) {x y : α} : x ≠ y → r x y ↔ r x y

Full source

/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`. -/
theorem Reflexive.ne_imp_iff (h : Reflexive r) {x y : α} : x ≠ yx ≠ y → r x y ↔ r x y :=
  ⟨h.rel_of_ne_imp, fun hr _ ↦ hr⟩

Reflexive Relation Characterization via Inequality Implication

Informal description

Let $r$ be a reflexive relation on a type $\alpha$. For any elements $x, y \in \alpha$, the implication $x \neq y \rightarrow r(x, y)$ holds if and only if $r(x, y)$ holds.

reflexive_ne_imp_iff theorem

[IsRefl α r] {x y : α} : x ≠ y → r x y ↔ r x y

Full source

/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,
then it holds whether or not `x ≠ y`. Unlike `Reflexive.ne_imp_iff`, this uses `[IsRefl α r]`. -/
theorem reflexive_ne_imp_iff [IsRefl α r] {x y : α} : x ≠ yx ≠ y → r x y ↔ r x y :=
  IsRefl.reflexive.ne_imp_iff

Reflexive Relation Characterization via Inequality Implication

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any elements $x, y \in \alpha$, the implication $x \neq y \rightarrow r(x, y)$ holds if and only if $r(x, y)$ holds.

Symmetric.iff theorem

(H : Symmetric r) (x y : α) : r x y ↔ r y x

Full source

protected theorem Symmetric.iff (H : Symmetric r) (x y : α) : r x y ↔ r y x :=
  ⟨fun h ↦ H h, fun h ↦ H h⟩

Symmetric Relation Characterization: $r(x, y) \leftrightarrow r(y, x)$

Informal description

For any symmetric relation $r$ on a type $\alpha$ and any elements $x, y \in \alpha$, the relation $r(x, y)$ holds if and only if $r(y, x)$ holds.

Symmetric.flip_eq theorem

(h : Symmetric r) : flip r = r

Full source

theorem Symmetric.flip_eq (h : Symmetric r) : flip r = r :=
  funext₂ fun _ _ ↦ propext <| h.iff _ _

Equality of Flipped Relation and Original Relation for Symmetric Relations

Informal description

For any symmetric relation $r$ on a type $\alpha$, the flipped relation $\text{flip}\,r$ (defined by $(\text{flip}\,r)(x, y) = r(y, x)$) is equal to $r$ itself.

Symmetric.swap_eq theorem

: Symmetric r → swap r = r

Full source

theorem Symmetric.swap_eq : Symmetric r → swap r = r :=
  Symmetric.flip_eq

Equality of Swapped Relation and Original Relation for Symmetric Relations

Informal description

For any symmetric relation $r$ on a type $\alpha$, the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is equal to $r$ itself.

flip_eq_iff theorem

: flip r = r ↔ Symmetric r

Full source

theorem flip_eq_iff : flipflip r = r ↔ Symmetric r :=
  ⟨fun h _ _ ↦ (congr_fun₂ h _ _).mp, Symmetric.flip_eq⟩

Characterization of Symmetric Relations via Flip Equality

Informal description

For any relation $r$ on a type $\alpha$, the flipped relation $\text{flip}\,r$ (defined by $(\text{flip}\,r)(x, y) = r(y, x)$) is equal to $r$ if and only if $r$ is symmetric.

swap_eq_iff theorem

: swap r = r ↔ Symmetric r

Full source

theorem swap_eq_iff : swapswap r = r ↔ Symmetric r :=
  flip_eq_iff

Characterization of Symmetric Relations via Swap Equality

Informal description

For any relation $r$ on a type $\alpha$, the swapped relation $\operatorname{swap} r$ (defined by $(\operatorname{swap} r)(x, y) = r(y, x)$) is equal to $r$ if and only if $r$ is symmetric.

Reflexive.comap theorem

(h : Reflexive r) (f : α → β) : Reflexive (r on f)

Full source

theorem Reflexive.comap (h : Reflexive r) (f : α → β) : Reflexive (r on f) := fun a ↦ h (f a)

Reflexivity Preservation under Relation Composition with a Function

Informal description

Let $r$ be a reflexive relation on a type $\beta$, and let $f \colon \alpha \to \beta$ be a function. Then the relation $r \text{ on } f$ defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ is reflexive on $\alpha$.

Symmetric.comap theorem

(h : Symmetric r) (f : α → β) : Symmetric (r on f)

Full source

theorem Symmetric.comap (h : Symmetric r) (f : α → β) : Symmetric (r on f) := fun _ _ hab ↦ h hab

Symmetry Preservation under Relation Composition with a Function

Informal description

Let $r$ be a symmetric relation on a type $\beta$, and let $f \colon \alpha \to \beta$ be a function. Then the relation $r \text{ on } f$ defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ is symmetric on $\alpha$.

Transitive.comap theorem

(h : Transitive r) (f : α → β) : Transitive (r on f)

Full source

theorem Transitive.comap (h : Transitive r) (f : α → β) : Transitive (r on f) :=
  fun _ _ _ hab hbc ↦ h hab hbc

Transitivity Preservation under Relation Composition with a Function

Informal description

Let $r$ be a transitive relation on a type $\beta$, and let $f \colon \alpha \to \beta$ be a function. Then the relation $r \text{ on } f$ defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ is transitive on $\alpha$.

Equivalence.comap theorem

(h : Equivalence r) (f : α → β) : Equivalence (r on f)

Full source

theorem Equivalence.comap (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=
  ⟨fun a ↦ h.refl (f a), h.symm, h.trans⟩

Equivalence Relation Preservation under Function Composition

Informal description

Given an equivalence relation $r$ on a type $\beta$ and a function $f \colon \alpha \to \beta$, the relation $(r \text{ on } f)$ defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ is also an equivalence relation on $\alpha$.

Relation.Comp definition

(r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : Prop

Full source

/-- The composition of two relations, yielding a new relation.  The result
relates a term of `α` and a term of `γ` if there is an intermediate
term of `β` related to both.
-/
def Comp (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : Prop :=
  ∃ b, r a b ∧ p b c

Composition of relations

Informal description

The composition of two relations $ r : \alpha \to \beta \to \text{Prop} $ and $ p : \beta \to \gamma \to \text{Prop} $ is a relation $ r \circ p : \alpha \to \gamma \to \text{Prop} $ defined by $ (r \circ p) \, a \, c $ if and only if there exists an intermediate element $ b : \beta $ such that $ r \, a \, b $ and $ p \, b \, c $ both hold.

Relation.comp_eq_fun theorem

(f : γ → β) : r ∘r (· = f ·) = (r · <| f ·)

Full source

@[simp]
theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by
  ext x y
  simp [Comp]

Composition of Relation with Function Equality Simplifies to Pointwise Application

Informal description

For any function $f \colon \gamma \to \beta$, the composition of a relation $r \colon \alpha \to \beta \to \text{Prop}$ with the equality relation $\big(\cdot = f(\cdot)\big)$ is equal to the relation $\big(r(\cdot, f(\cdot))\big)$. In other words, $r \circ (\lambda x y, y = f(x)) = \lambda x, r(x, f(x))$.

Relation.comp_eq theorem

: r ∘r (· = ·) = r

Full source

@[simp]
theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..

Composition with Equality Preserves Relation

Informal description

The composition of a relation $r \colon \alpha \to \alpha \to \text{Prop}$ with the equality relation $(\cdot = \cdot)$ is equal to $r$ itself, i.e., $r \circ (\cdot = \cdot) = r$.

Relation.fun_eq_comp theorem

(f : γ → α) : (f · = ·) ∘r r = (r <| f ·)

Full source

@[simp]
theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) := by
  ext x y
  simp [Comp]

Composition of Equality Relation with Function Equals Relation Applied to Function

Informal description

For any function $f \colon \gamma \to \alpha$, the composition of the equality relation $(f \cdot = \cdot)$ with a relation $r \colon \alpha \to \beta \to \text{Prop}$ is equal to the relation $r$ applied to $f$, i.e., $(f \cdot = \cdot) \circ r = r \circ f$.

Relation.iff_comp theorem

{r : Prop → α → Prop} : (· ↔ ·) ∘r r = r

Full source

@[simp]
theorem iff_comp {r : Prop → α → Prop} : (· ↔ ·) ∘r r = r := by
  have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
  rw [this, eq_comp]

Composition with Logical Equivalence Preserves Relation

Informal description

For any relation $r : \text{Prop} \to \alpha \to \text{Prop}$, the composition of the logical equivalence relation $(\cdot \leftrightarrow \cdot)$ with $r$ is equal to $r$ itself. In other words, $(\leftrightarrow) \circ r = r$.

Relation.comp_iff theorem

{r : α → Prop → Prop} : r ∘r (· ↔ ·) = r

Full source

@[simp]
theorem comp_iff {r : α → Prop → Prop} : r ∘r (· ↔ ·) = r := by
  have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
  rw [this, comp_eq]

Composition with Logical Equivalence Preserves Relation (Right Version)

Informal description

For any relation $r : \alpha \to \text{Prop} \to \text{Prop}$, the composition of $r$ with the logical equivalence relation $(\cdot \leftrightarrow \cdot)$ is equal to $r$ itself, i.e., $r \circ (\leftrightarrow) = r$.

Relation.comp_assoc theorem

: (r ∘r p) ∘r q = r ∘r p ∘r q

Full source

theorem comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q := by
  funext a d
  apply propext
  constructor
  · exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩
  · exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩

Associativity of Relation Composition

Informal description

For any relations $r : \alpha \to \beta \to \text{Prop}$, $p : \beta \to \gamma \to \text{Prop}$, and $q : \gamma \to \delta \to \text{Prop}$, the composition of relations is associative, i.e., $(r \circ p) \circ q = r \circ (p \circ q)$.

Relation.flip_comp theorem

: flip (r ∘r p) = flip p ∘r flip r

Full source

theorem flip_comp : flip (r ∘r p) = flipflip p ∘r flip r := by
  funext c a
  apply propext
  constructor
  · exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩
  · exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩

Flip of Relation Composition Equals Reverse Composition of Flips

Informal description

For any relations $r : \alpha \to \beta \to \text{Prop}$ and $p : \beta \to \gamma \to \text{Prop}$, the flip of their composition equals the composition of their flips in reverse order. That is, $\text{flip}(r \circ p) = \text{flip}(p) \circ \text{flip}(r)$.

Relation.Fibration definition

Full source

/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
  `a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image
  of some `a' : α` under `f`, and `a'` and `a` are related by `rα`. -/
def Fibration :=
  ∀ ⦃a b⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b

Fibration between relations

Informal description

A function $f \colon \alpha \to \beta$ is called a *fibration* between relations $r_\alpha$ (on $\alpha$) and $r_\beta$ (on $\beta$) if for any $a \in \alpha$ and $b \in \beta$ such that $b$ is related to $f(a)$ under $r_\beta$, there exists some $a' \in \alpha$ that is related to $a$ under $r_\alpha$ and satisfies $f(a') = b$.

Acc.of_fibration theorem

(fib : Fibration rα rβ f) {a} (ha : Acc rα a) : Acc rβ (f a)

Full source

/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
  accessible under `rα`, then `f a` is accessible under `rβ`. -/
theorem _root_.Acc.of_fibration (fib : Fibration rα rβ f) {a} (ha : Acc rα a) : Acc rβ (f a) := by
  induction ha with | intro a _ ih => ?_
  refine Acc.intro (f a) fun b hr ↦ ?_
  obtain ⟨a', hr', rfl⟩ := fib hr
  exact ih a' hr'

Accessibility Preservation under Fibration

Informal description

Let $f \colon \alpha \to \beta$ be a fibration between relations $r_\alpha$ (on $\alpha$) and $r_\beta$ (on $\beta$). If an element $a \in \alpha$ is accessible under $r_\alpha$, then its image $f(a) \in \beta$ is accessible under $r_\beta$.

Acc.of_downward_closed theorem

(dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b) (a : α) (ha : Acc (InvImage rβ f) a) : Acc rβ (f a)

Full source

theorem _root_.Acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b) (a : α)
    (ha : Acc (InvImage rβ f) a) : Acc rβ (f a) :=
  ha.of_fibration f fun a _ h ↦
    let ⟨a', he⟩ := dc h
    ⟨a', by simp_all [InvImage], he⟩

Accessibility of Image under Downward Closed Function

Informal description

Let $f \colon \alpha \to \beta$ be a function and $r_\beta$ a relation on $\beta$. If for any $a \in \alpha$ and $b \in \beta$ such that $r_\beta(b, f(a))$ holds, there exists $c \in \alpha$ with $f(c) = b$ (i.e., $f$ is downward closed), and if $a$ is accessible under the relation $\text{InvImage}\, r_\beta\, f$ (the relation on $\alpha$ induced by $r_\beta$ via $f$), then $f(a)$ is accessible under $r_\beta$.

Relation.Map definition

(r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop

Full source

/-- The map of a relation `r` through a pair of functions pushes the
relation to the codomains of the functions.  The resulting relation is
defined by having pairs of terms related if they have preimages
related by `r`.
-/
protected def Map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop := fun c d ↦
  ∃ a b, r a b ∧ f a = c ∧ g b = d

Image of a relation under a pair of maps

Informal description

Given a relation $r : \alpha \to \beta \to \text{Prop}$ and functions $f : \alpha \to \gamma$, $g : \beta \to \delta$, the mapped relation $\text{Relation.Map}\, r\, f\, g : \gamma \to \delta \to \text{Prop}$ relates $c \in \gamma$ and $d \in \delta$ if and only if there exist $a \in \alpha$ and $b \in \beta$ such that $r\, a\, b$ holds, $f(a) = c$, and $g(b) = d$.

Relation.map_apply theorem

: Relation.Map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d

Full source

lemma map_apply : Relation.MapRelation.Map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d := Iff.rfl

Characterization of Mapped Relation: $\text{Map}\, r\, f\, g\, c\, d \leftrightarrow \exists a\, b, r(a, b) \land f(a) = c \land g(b) = d$

Informal description

For a relation $r : \alpha \to \beta \to \text{Prop}$ and functions $f : \alpha \to \gamma$, $g : \beta \to \delta$, the mapped relation $\text{Map}\, r\, f\, g$ relates elements $c \in \gamma$ and $d \in \delta$ if and only if there exist $a \in \alpha$ and $b \in \beta$ such that $r(a, b)$ holds, $f(a) = c$, and $g(b) = d$.

Relation.map_map theorem

 (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) :
  Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁)

Full source

@[simp] lemma map_map (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) :
    Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) := by
  ext a b
  simp_rw [Relation.Map, Function.comp_apply, ← exists_and_right, @exists_comm γ, @exists_comm δ]
  refine exists₂_congr fun a b ↦ ⟨?_, fun h ↦ ⟨_, _, ⟨⟨h.1, rfl, rfl⟩, h.2⟩⟩⟩
  rintro ⟨_, _, ⟨hab, rfl, rfl⟩, h⟩
  exact ⟨hab, h⟩

Composition of Mapped Relations

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$ and functions $f_1 : \alpha \to \gamma$, $g_1 : \beta \to \delta$, $f_2 : \gamma \to \epsilon$, $g_2 : \delta \to \zeta$, the composition of mapped relations satisfies: \[ \text{Relation.Map}\, (\text{Relation.Map}\, r\, f_1\, g_1)\, f_2\, g_2 = \text{Relation.Map}\, r\, (f_2 \circ f_1)\, (g_2 \circ g_1). \]

Relation.map_apply_apply theorem

 (hf : Injective f) (hg : Injective g) (r : α → β → Prop) (a : α) (b : β) : Relation.Map r f g (f a) (g b) ↔ r a b

Full source

@[simp]
lemma map_apply_apply (hf : Injective f) (hg : Injective g) (r : α → β → Prop) (a : α) (b : β) :
    Relation.MapRelation.Map r f g (f a) (g b) ↔ r a b := by simp [Relation.Map, hf.eq_iff, hg.eq_iff]

Injective Mapping Preserves Relation: $\text{Map}\, r\, f\, g\, (f\, a)\, (g\, b) \leftrightarrow r\, a\, b$

Informal description

Let $f : \alpha \to \gamma$ and $g : \beta \to \delta$ be injective functions, and let $r : \alpha \to \beta \to \text{Prop}$ be a relation. For any $a \in \alpha$ and $b \in \beta$, the mapped relation $\text{Relation.Map}\, r\, f\, g$ relates $f(a)$ and $g(b)$ if and only if $r\, a\, b$ holds.

Relation.map_id_id theorem

(r : α → β → Prop) : Relation.Map r id id = r

Full source

@[simp] lemma map_id_id (r : α → β → Prop) : Relation.Map r id id = r := by ext; simp [Relation.Map]

Identity Mapping Preserves Relation

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$, the mapped relation $\text{Relation.Map}\, r\, \text{id}\, \text{id}$ is equal to $r$, where $\text{id}$ denotes the identity function on $\alpha$ and $\beta$ respectively.

Relation.instDecidableMapOfExistsAndEq instance

[Decidable (∃ a b, r a b ∧ f a = c ∧ g b = d)] : Decidable (Relation.Map r f g c d)

Full source

instance [Decidable (∃ a b, r a b ∧ f a = c ∧ g b = d)] : Decidable (Relation.Map r f g c d) :=
  ‹Decidable _›

Decidability of the Mapped Relation under Existence and Equality Conditions

Informal description

For any relation $r : \alpha \to \beta \to \text{Prop}$ and functions $f : \alpha \to \gamma$, $g : \beta \to \delta$, if there exists a decidable procedure to determine whether there are elements $a \in \alpha$ and $b \in \beta$ such that $r\, a\, b$ holds, $f(a) = c$, and $g(b) = d$, then the mapped relation $\text{Relation.Map}\, r\, f\, g\, c\, d$ is decidable.

Relation.map_reflexive theorem

{r : α → α → Prop} (hr : Reflexive r) {f : α → β} (hf : f.Surjective) : Reflexive (Relation.Map r f f)

Full source

lemma map_reflexive {r : α → α → Prop} (hr : Reflexive r) {f : α → β} (hf : f.Surjective) :
    Reflexive (Relation.Map r f f) := by
  intro x
  obtain ⟨y, rfl⟩ := hf x
  exact ⟨y, y, hr y, rfl, rfl⟩

Reflexivity Preservation under Relation Mapping with Surjective Function

Informal description

Let $r : \alpha \to \alpha \to \text{Prop}$ be a reflexive relation and $f : \alpha \to \beta$ be a surjective function. Then the mapped relation $\text{Relation.Map}\, r\, f\, f : \beta \to \beta \to \text{Prop}$ is reflexive.

Relation.map_symmetric theorem

{r : α → α → Prop} (hr : Symmetric r) (f : α → β) : Symmetric (Relation.Map r f f)

Full source

lemma map_symmetric {r : α → α → Prop} (hr : Symmetric r) (f : α → β) :
    Symmetric (Relation.Map r f f) := by
  rintro _ _ ⟨x, y, hxy, rfl, rfl⟩; exact ⟨_, _, hr hxy, rfl, rfl⟩

Symmetry Preservation under Relation Mapping

Informal description

Let $r : \alpha \to \alpha \to \text{Prop}$ be a symmetric relation and $f : \alpha \to \beta$ be a function. Then the mapped relation $\text{Relation.Map}\, r\, f\, f : \beta \to \beta \to \text{Prop}$ is also symmetric.

Relation.map_transitive theorem

 {r : α → α → Prop} (hr : Transitive r) {f : α → β} (hf : ∀ x y, f x = f y → r x y) : Transitive (Relation.Map r f f)

Full source

lemma map_transitive {r : α → α → Prop} (hr : Transitive r) {f : α → β}
    (hf : ∀ x y, f x = f y → r x y) :
    Transitive (Relation.Map r f f) := by
  rintro _ _ _ ⟨x, y, hxy, rfl, rfl⟩ ⟨y', z, hyz, hy, rfl⟩
  exact ⟨x, z, hr hxy <| hr (hf _ _ hy.symm) hyz, rfl, rfl⟩

Transitivity Preservation under Relation Mapping

Informal description

Let $r : \alpha \to \alpha \to \text{Prop}$ be a transitive relation and $f : \alpha \to \beta$ be a function such that for all $x, y \in \alpha$, if $f(x) = f(y)$ then $r(x, y)$ holds. Then the mapped relation $\text{Relation.Map}\, r\, f\, f$ is also transitive.

Relation.map_equivalence theorem

 {r : α → α → Prop} (hr : Equivalence r) (f : α → β) (hf : f.Surjective) (hf_ker : ∀ x y, f x = f y → r x y) :
  Equivalence (Relation.Map r f f)

Full source

lemma map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α → β)
    (hf : f.Surjective) (hf_ker : ∀ x y, f x = f y → r x y) :
    Equivalence (Relation.Map r f f) where
  refl := map_reflexive hr.reflexive hf
  symm := @(map_symmetric hr.symmetric _)
  trans := @(map_transitive hr.transitive hf_ker)

Equivalence Relation Preservation under Surjective Mapping with Kernel Condition

Informal description

Let $r : \alpha \to \alpha \to \text{Prop}$ be an equivalence relation, $f : \alpha \to \beta$ be a surjective function, and suppose that for all $x, y \in \alpha$, if $f(x) = f(y)$ then $r(x, y)$ holds. Then the mapped relation $\text{Relation.Map}\, r\, f\, f : \beta \to \beta \to \text{Prop}$ is also an equivalence relation.

Relation.map_mono theorem

 {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :
  ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y

Full source

lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :
    ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y :=
  fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩

Monotonicity of Relation Mapping

Informal description

Let $r, s : \alpha \to \beta \to \text{Prop}$ be relations and $f : \alpha \to \gamma$, $g : \beta \to \delta$ be functions. If for all $x \in \alpha$ and $y \in \beta$, $r(x, y)$ implies $s(x, y)$, then for any $x \in \gamma$ and $y \in \delta$, the mapped relation $\text{Relation.Map}\, r\, f\, g\, x\, y$ implies $\text{Relation.Map}\, s\, f\, g\, x\, y$.

Relation.ReflTransGen inductive

(r : α → α → Prop) (a : α) : α → Prop

Full source

/-- `ReflTransGen r`: reflexive transitive closure of `r` -/
@[mk_iff ReflTransGen.cases_tail_iff]
inductive ReflTransGen (r : α → α → Prop) (a : α) : α → Prop
  | refl : ReflTransGen r a a
  | tail {b c} : ReflTransGen r a b → r b c → ReflTransGen r a c

Reflexive transitive closure of a relation

Informal description

The reflexive transitive closure of a relation `r` on a type `α` is the smallest relation that contains `r` and is both reflexive and transitive. For any `a b : α`, `ReflTransGen r a b` holds if either `a = b` or there exists a finite sequence `x₀, ..., xₙ` such that `r a x₀`, `r x₀ x₁`, ..., `r xₙ b`. This represents the notion that `a` can be "rewritten" to `b` in zero or more steps according to the relation `r`.

Relation.ReflGen inductive

(r : α → α → Prop) (a : α) : α → Prop

Full source

/-- `ReflGen r`: reflexive closure of `r` -/
@[mk_iff]
inductive ReflGen (r : α → α → Prop) (a : α) : α → Prop
  | refl : ReflGen r a a
  | single {b} : r a b → ReflGen r a b

Reflexive closure of a relation

Informal description

The reflexive closure `ReflGen r` of a relation `r` on a type `α` is the smallest relation that contains `r` and is reflexive. For any elements `a` and `b` in `α`, `ReflGen r a b` holds if and only if either `r a b` holds or `a = b`.

Relation.EqvGen inductive

: α → α → Prop

Full source

/-- `EqvGen r`: equivalence closure of `r`. -/
@[mk_iff]
inductive EqvGen : α → α → Prop
  | rel x y : r x y → EqvGen x y
  | refl x : EqvGen x x
  | symm x y : EqvGen x y → EqvGen y x
  | trans x y z : EqvGen x y → EqvGen y z → EqvGen x z

Equivalence Closure of a Relation

Informal description

The inductive relation `EqvGen r` is the equivalence closure of a relation `r : α → α → Prop`. It is the smallest equivalence relation containing `r`, meaning it relates all elements that `r` relates, includes all reflexive pairs, is symmetric, and is transitive. Formally, `EqvGen r a b` holds if either: 1. `r a b` or `r b a` (symmetry), 2. `a = b` (reflexivity), or 3. There exists a chain of elements connected by `r` or its inverse (transitivity).

Relation.ReflGen.to_reflTransGen theorem

: ∀ {a b}, ReflGen r a b → ReflTransGen r a b

Full source

theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b
  | a, _, refl => by rfl
  | _, _, single h => ReflTransGen.tail ReflTransGen.refl h

Inclusion of Reflexive Closure in Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a$ is related to $b$ in the reflexive closure of $r$ (i.e., $\text{ReflGen}\, r\, a\, b$ holds), then $a$ is also related to $b$ in the reflexive transitive closure of $r$ (i.e., $\text{ReflTransGen}\, r\, a\, b$ holds).

Relation.ReflGen.mono theorem

{p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b

Full source

theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b
  | a, _, ReflGen.refl => by rfl
  | a, b, single h => single (hp a b h)

Monotonicity of Reflexive Closure

Informal description

Let $r$ and $p$ be relations on a type $\alpha$ such that for all $a, b \in \alpha$, if $r(a, b)$ holds then $p(a, b)$ holds. Then for any $a, b \in \alpha$, if $\text{ReflGen}\, r\, a\, b$ holds, then $\text{ReflGen}\, p\, a\, b$ also holds. Here $\text{ReflGen}\, r$ denotes the reflexive closure of $r$.

Relation.ReflGen.instIsRefl instance

: IsRefl α (ReflGen r)

Full source

instance : IsRefl α (ReflGen r) :=
  ⟨@refl α r⟩

Reflexivity of the Reflexive Closure

Informal description

For any relation $r$ on a type $\alpha$, the reflexive closure $\text{ReflGen}\, r$ is reflexive. That is, for every $a \in \alpha$, we have $\text{ReflGen}\, r\, a\, a$.

Relation.ReflTransGen.trans theorem

(hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

Full source

@[trans]
theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
  induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Transitivity of Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b, c \in \alpha$, if $\text{ReflTransGen}\, r\, a\, b$ and $\text{ReflTransGen}\, r\, b\, c$ hold, then $\text{ReflTransGen}\, r\, a\, c$ also holds. Here $\text{ReflTransGen}\, r$ denotes the reflexive transitive closure of $r$.

Relation.ReflTransGen.single theorem

(hab : r a b) : ReflTransGen r a b

Full source

theorem single (hab : r a b) : ReflTransGen r a b :=
  refl.tail hab

Single-step inclusion in reflexive transitive closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $r\, a\, b$ holds, then the reflexive transitive closure $\text{ReflTransGen}\, r\, a\, b$ also holds.

Relation.ReflTransGen.head theorem

(hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c

Full source

theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by
  induction hbc with
  | refl => exact refl.tail hab
  | tail _ hcd hac => exact hac.tail hcd

Head Step in Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b, c \in \alpha$, if $r\, a\, b$ holds and $\text{ReflTransGen}\, r\, b\, c$ holds, then $\text{ReflTransGen}\, r\, a\, c$ also holds. Here $\text{ReflTransGen}\, r$ denotes the reflexive transitive closure of $r$.

Relation.ReflTransGen.symmetric theorem

(h : Symmetric r) : Symmetric (ReflTransGen r)

Full source

theorem symmetric (h : Symmetric r) : Symmetric (ReflTransGen r) := by
  intro x y h
  induction h with
  | refl => rfl
  | tail _ b c => apply Relation.ReflTransGen.head (h b) c

Symmetry of Reflexive Transitive Closure for Symmetric Relations

Informal description

For any symmetric relation $r$ on a type $\alpha$, its reflexive transitive closure $\text{ReflTransGen}\, r$ is also symmetric. That is, if $\text{ReflTransGen}\, r\, a\, b$ holds for some $a, b \in \alpha$, then $\text{ReflTransGen}\, r\, b\, a$ also holds.

Relation.ReflTransGen.cases_tail theorem

: ReflTransGen r a b → b = a ∨ ∃ c, ReflTransGen r a c ∧ r c b

Full source

theorem cases_tail : ReflTransGen r a b → b = a ∨ ∃ c, ReflTransGen r a c ∧ r c b :=
  (cases_tail_iff r a b).1

Tail Decomposition of Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $\text{ReflTransGen}\, r\, a\, b$ holds, then either $b = a$ or there exists an element $c \in \alpha$ such that $\text{ReflTransGen}\, r\, a\, c$ and $r\, c\, b$ both hold.

Relation.ReflTransGen.head_induction_on theorem

 {P : ∀ a : α, ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b) (refl : P b refl)
  (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (h.head h')) : P a h

Full source

@[elab_as_elim]
theorem head_induction_on {P : ∀ a : α, ReflTransGen r a b → Prop} {a : α} (h : ReflTransGen r a b)
    (refl : P b refl)
    (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), P c h → P a (h.head h')) : P a h := by
  induction h with
  | refl => exact refl
  | @tail b c _ hbc ih =>
  apply ih
  · exact head hbc _ refl
  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)

Head Induction Principle for Reflexive Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$, and let $b \in \alpha$ be fixed. For any predicate $P$ on pairs $(a, h)$ where $a \in \alpha$ and $h$ is a proof that $\text{ReflTransGen}\, r\, a\, b$ holds, if: 1. (Reflexivity) $P(b, \text{refl})$ holds, where $\text{refl}$ is the proof that $\text{ReflTransGen}\, r\, b\, b$ holds, and 2. (Inductive step) For any $a, c \in \alpha$ and any $h'$ such that $r\, a\, c$ holds, if $P(c, h)$ holds for some proof $h$ that $\text{ReflTransGen}\, r\, c\, b$ holds, then $P(a, \text{head}\, h'\, h)$ also holds, then for any $a \in \alpha$ and any proof $h$ that $\text{ReflTransGen}\, r\, a\, b$ holds, $P(a, h)$ holds.

Relation.ReflTransGen.trans_induction_on theorem

 {P : ∀ {a b : α}, ReflTransGen r a b → Prop} {a b : α} (h : ReflTransGen r a b) (ih₁ : ∀ a, @P a a refl)
  (ih₂ : ∀ {a b} (h : r a b), P (single h))
  (ih₃ : ∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) : P h

Full source

@[elab_as_elim]
theorem trans_induction_on {P : ∀ {a b : α}, ReflTransGen r a b → Prop} {a b : α}
    (h : ReflTransGen r a b) (ih₁ : ∀ a, @P a a refl) (ih₂ : ∀ {a b} (h : r a b), P (single h))
    (ih₃ : ∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), P h₁ → P h₂ →
     P (h₁.trans h₂)) : P h := by
  induction h with
  | refl => exact ih₁ a
  | tail hab hbc ih => exact ih₃ hab (single hbc) ih (ih₂ hbc)

Induction Principle for Reflexive Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$, and let $P$ be a predicate on pairs of elements of $\alpha$ related by the reflexive transitive closure $\text{ReflTransGen}\, r$. For any $a, b \in \alpha$ and any proof $h$ that $\text{ReflTransGen}\, r\, a\, b$ holds, the predicate $P\, h$ is satisfied if: 1. (Reflexivity) For every $a \in \alpha$, $P$ holds for the reflexive case $\text{ReflTransGen.refl}\, a$. 2. (Base case) For any $a, b \in \alpha$ and any proof $h$ that $r\, a\, b$ holds, $P$ holds for the single-step case $\text{ReflTransGen.single}\, h$. 3. (Transitivity) For any $a, b, c \in \alpha$ and proofs $h_1$ that $\text{ReflTransGen}\, r\, a\, b$ and $h_2$ that $\text{ReflTransGen}\, r\, b\, c$ hold, if $P\, h_1$ and $P\, h_2$ hold, then $P$ holds for the transitive composition $h_1.\text{trans}\, h_2$.

Relation.ReflTransGen.cases_head theorem

(h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Full source

theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by
  induction h using Relation.ReflTransGen.head_induction_on
  · left
    rfl
  · right
    exact ⟨_, by assumption, by assumption⟩

Decomposition of Reflexive Transitive Closure into Reflexive or Transitive Step

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, if $\text{ReflTransGen}\, r\, a\, b$ holds, then either $a = b$ or there exists an element $c \in \alpha$ such that $r\, a\, c$ holds and $\text{ReflTransGen}\, r\, c\, b$ holds.

Relation.ReflTransGen.cases_head_iff theorem

: ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b

Full source

theorem cases_head_iff : ReflTransGenReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by
  use cases_head
  rintro (rfl | ⟨c, hac, hcb⟩)
  · rfl
  · exact head hac hcb

Characterization of Reflexive Transitive Closure via Reflexivity or Head Step

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, the reflexive transitive closure $\text{ReflTransGen}\, r\, a\, b$ holds if and only if either $a = b$ or there exists some $c \in \alpha$ such that $r\, a\, c$ holds and $\text{ReflTransGen}\, r\, c\, b$ holds.

Relation.ReflTransGen.total_of_right_unique theorem

 (U : Relator.RightUnique r) (ab : ReflTransGen r a b) (ac : ReflTransGen r a c) :
  ReflTransGen r b c ∨ ReflTransGen r c b

Full source

theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a b)
    (ac : ReflTransGen r a c) : ReflTransGenReflTransGen r b c ∨ ReflTransGen r c b := by
  induction ab with
  | refl => exact Or.inl ac
  | tail _ bd IH =>
    rcases IH with (IH | IH)
    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
      · exact Or.inr (single bd)
      · cases U bd be
        exact Or.inl ec
    · exact Or.inr (IH.tail bd)

Total Ordering Property of Reflexive Transitive Closure for Right-Unique Relations

Informal description

For any right-unique relation $r$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $a$ is reflexively transitively related to both $b$ and $c$ (i.e., $\text{ReflTransGen}\, r\, a\, b$ and $\text{ReflTransGen}\, r\, a\, c$ hold), then either $b$ is reflexively transitively related to $c$ or $c$ is reflexively transitively related to $b$.

Relation.TransGen.to_reflTransGen theorem

{a b} (h : TransGen r a b) : ReflTransGen r a b

Full source

theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by
  induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

Inclusion of Transitive Closure in Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a$ is transitively related to $b$ (i.e., $\text{TransGen}\, r\, a\, b$ holds), then $a$ is reflexively transitively related to $b$ (i.e., $\text{ReflTransGen}\, r\, a\, b$ holds).

Relation.TransGen.trans_left theorem

(hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c

Full source

theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by
  induction hbc with
  | refl => assumption
  | tail _ hcd hac => exact hac.tail hcd

Transitivity of Transitive Closure with Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $a$ is transitively related to $b$ (i.e., $\text{TransGen}\, r\, a\, b$ holds) and $b$ is reflexively transitively related to $c$ (i.e., $\text{ReflTransGen}\, r\, b\, c$ holds), then $a$ is transitively related to $c$ (i.e., $\text{TransGen}\, r\, a\, c$ holds).

Relation.TransGen.instTransReflTransGen instance

: Trans (TransGen r) (ReflTransGen r) (TransGen r)

Full source

instance : Trans (TransGen r) (ReflTransGen r) (TransGen r) :=
  ⟨trans_left⟩

Transitivity of Transitive Closure with Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the transitive closure operation $\text{TransGen}\, r$ is transitive with respect to the reflexive transitive closure $\text{ReflTransGen}\, r$. That is, if $a$ is transitively related to $b$ (i.e., $\text{TransGen}\, r\, a\, b$ holds) and $b$ is reflexively transitively related to $c$ (i.e., $\text{ReflTransGen}\, r\, b\, c$ holds), then $a$ is transitively related to $c$ (i.e., $\text{TransGen}\, r\, a\, c$ holds).

Relation.TransGen.instTrans_mathlib instance

: Trans (TransGen r) (TransGen r) (TransGen r)

Full source

instance : Trans (TransGen r) (TransGen r) (TransGen r) :=
  ⟨trans⟩

Transitivity of Transitive Closure

Informal description

The transitive closure operation `TransGen` is transitive. That is, for any relation `r` on a type `α`, if `TransGen r a b` and `TransGen r b c` hold, then `TransGen r a c` holds.

Relation.TransGen.head' theorem

(hab : r a b) (hbc : ReflTransGen r b c) : TransGen r a c

Full source

theorem head' (hab : r a b) (hbc : ReflTransGen r b c) : TransGen r a c :=
  trans_left (single hab) hbc

Transitive Path Extension via Direct Step and Reflexive-Transitive Path

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $a$ is related to $b$ via $r$ (i.e., $r(a, b)$ holds) and $b$ is reflexively transitively related to $c$ (i.e., $\text{ReflTransGen}\, r\, b\, c$ holds), then $a$ is transitively related to $c$ (i.e., $\text{TransGen}\, r\, a\, c$ holds).

Relation.TransGen.tail' theorem

(hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c

Full source

theorem tail' (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c := by
  induction hab generalizing c with
  | refl => exact single hbc
  | tail _ hdb IH => exact tail (IH hdb) hbc

Transitive Path Extension via Reflexive-Transitive Path and Direct Step

Informal description

For any relation `r` on a type `α`, if there is a reflexive-transitive path from `a` to `b` (i.e., `ReflTransGen r a b`) and a direct `r`-step from `b` to `c` (i.e., `r b c`), then there exists a transitive path from `a` to `c` (i.e., `TransGen r a c`).

Relation.TransGen.head theorem

(hab : r a b) (hbc : TransGen r b c) : TransGen r a c

Full source

theorem head (hab : r a b) (hbc : TransGen r b c) : TransGen r a c :=
  head' hab hbc.to_reflTransGen

Transitive Path Extension via Direct Step and Transitive Path

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b, c \in \alpha$, if $a$ is directly related to $b$ via $r$ (i.e., $r(a, b)$ holds) and $b$ is transitively related to $c$ (i.e., $\text{TransGen}\, r\, b\, c$ holds), then $a$ is transitively related to $c$ (i.e., $\text{TransGen}\, r\, a\, c$ holds).

Relation.TransGen.head_induction_on theorem

 {P : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b) (base : ∀ {a} (h : r a b), P a (single h))
  (ih : ∀ {a c} (h' : r a c) (h : TransGen r c b), P c h → P a (h.head h')) : P a h

Full source

@[elab_as_elim]
theorem head_induction_on {P : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b)
    (base : ∀ {a} (h : r a b), P a (single h))
    (ih : ∀ {a c} (h' : r a c) (h : TransGen r c b), P c h → P a (h.head h')) : P a h := by
  induction h with
  | single h => exact base h
  | @tail b c _ hbc h_ih =>
  apply h_ih
  · exact fun h ↦ ih h (single hbc) (base hbc)
  · exact fun hab hbc ↦ ih hab _

Head Induction Principle for Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$, and let $P$ be a predicate on elements $a \in \alpha$ and proofs $h$ that $a$ is transitively related to $b$ via $r$. For any transitive closure proof $h : \text{TransGen}\,r\,a\,b$, to prove $P\,a\,h$ it suffices to: 1. Show $P\,a\,(\text{single}\,h')$ for any direct relation proof $h' : r\,a\,b$ (base case) 2. Show that for any $a, c \in \alpha$, if there exists a direct relation $h' : r\,a\,c$ and a transitive closure proof $h : \text{TransGen}\,r\,c\,b$ with $P\,c\,h$, then $P\,a\,(h.\text{head}\,h')$ holds (inductive step)

Relation.TransGen.trans_induction_on theorem

 {P : ∀ {a b : α}, TransGen r a b → Prop} {a b : α} (h : TransGen r a b) (base : ∀ {a b} (h : r a b), P (single h))
  (ih : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) : P h

Full source

@[elab_as_elim]
theorem trans_induction_on {P : ∀ {a b : α}, TransGen r a b → Prop} {a b : α} (h : TransGen r a b)
    (base : ∀ {a b} (h : r a b), P (single h))
    (ih : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), P h₁ → P h₂ → P (h₁.trans h₂)) :
    P h := by
  induction h with
  | single h => exact base h
  | tail hab hbc h_ih => exact ih hab (single hbc) h_ih (base hbc)

Transitive Closure Induction Principle

Informal description

Let $r$ be a relation on a type $\alpha$, and let $P$ be a predicate on pairs $(a,b)$ with a transitive closure proof $h : \text{TransGen}\,r\,a\,b$. For any $h : \text{TransGen}\,r\,a\,b$, to prove $P\,h$ it suffices to: 1. Show $P\,(\text{single}\,h')$ for any direct relation proof $h' : r\,a\,b$ (base case) 2. Show that for any $h_1 : \text{TransGen}\,r\,a\,b$ and $h_2 : \text{TransGen}\,r\,b\,c$, if $P\,h_1$ and $P\,h_2$ hold, then $P\,(h_1.\text{trans}\,h_2)$ holds (inductive step)

Relation.TransGen.trans_right theorem

(hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c

Full source

theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c := by
  induction hbc with
  | single hbc => exact tail' hab hbc
  | tail _ hcd hac => exact hac.tail hcd

Transitive Path Composition via Reflexive-Transitive and Transitive Paths

Informal description

For any relation $r$ on a type $\alpha$, if there exists a reflexive-transitive path from $a$ to $b$ (i.e., $\text{ReflTransGen}\,r\,a\,b$) and a transitive path from $b$ to $c$ (i.e., $\text{TransGen}\,r\,b\,c$), then there exists a transitive path from $a$ to $c$ (i.e., $\text{TransGen}\,r\,a\,c$).

Relation.TransGen.instTransReflTransGen_1 instance

: Trans (ReflTransGen r) (TransGen r) (TransGen r)

Full source

instance : Trans (ReflTransGen r) (TransGen r) (TransGen r) :=
  ⟨trans_right⟩

Composition of Reflexive-Transitive and Transitive Closures

Informal description

For any relation $r$ on a type $\alpha$, the composition of a reflexive-transitive closure step $\text{ReflTransGen}\,r$ followed by a transitive closure step $\text{TransGen}\,r$ results in a transitive closure step $\text{TransGen}\,r$. In other words, if $a$ is related to $b$ via $\text{ReflTransGen}\,r$ and $b$ is related to $c$ via $\text{TransGen}\,r$, then $a$ is related to $c$ via $\text{TransGen}\,r$.

Relation.TransGen.tail'_iff theorem

: TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c

Full source

theorem tail'_iff : TransGenTransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c := by
  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩
  cases h with
  | single hac => exact ⟨_, by rfl, hac⟩
  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩

Transitive Path Characterization via Reflexive-Transitive Path and Direct Step

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, c \in \alpha$, there exists a transitive path from $a$ to $c$ (i.e., $\text{TransGen}\,r\,a\,c$) if and only if there exists an intermediate element $b \in \alpha$ such that there is a reflexive-transitive path from $a$ to $b$ (i.e., $\text{ReflTransGen}\,r\,a\,b$) and a direct $r$-step from $b$ to $c$ (i.e., $r\,b\,c$).

Relation.TransGen.head'_iff theorem

: TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c

Full source

theorem head'_iff : TransGenTransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c := by
  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩
  induction h with
  | single hac => exact ⟨_, hac, by rfl⟩
  | tail _ hbc IH =>
  rcases IH with ⟨d, had, hdb⟩
  exact ⟨_, had, hdb.tail hbc⟩

Transitive Path Characterization via Direct Step and Reflexive-Transitive Path

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, c \in \alpha$, the transitive closure $\text{TransGen}\,r\,a\,c$ holds if and only if there exists an element $b \in \alpha$ such that $r(a, b)$ holds and the reflexive-transitive closure $\text{ReflTransGen}\,r\,b\,c$ holds.

Relation.reflGen_eq_self theorem

(hr : Reflexive r) : ReflGen r = r

Full source

lemma reflGen_eq_self (hr : Reflexive r) : ReflGen r = r := by
  ext x y
  simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ hr y

Reflexive Closure of Reflexive Relation is Itself

Informal description

For any reflexive relation $r$ on a type $\alpha$, the reflexive closure of $r$ is equal to $r$ itself, i.e., $\text{ReflGen}(r) = r$.

Relation.reflexive_reflGen theorem

: Reflexive (ReflGen r)

Full source

lemma reflexive_reflGen : Reflexive (ReflGen r) := fun _ ↦ .refl

Reflexivity of Reflexive Closure

Informal description

The reflexive closure $\text{ReflGen}(r)$ of any relation $r$ on a type $\alpha$ is reflexive, meaning that for every element $a \in \alpha$, $\text{ReflGen}(r)(a, a)$ holds.

Relation.reflGen_minimal theorem

 {r' : α → α → Prop} (hr' : Reflexive r') (h : ∀ x y, r x y → r' x y) {x y : α} (hxy : ReflGen r x y) : r' x y

Full source

lemma reflGen_minimal {r' : α → α → Prop} (hr' : Reflexive r') (h : ∀ x y, r x y → r' x y) {x y : α}
    (hxy : ReflGen r x y) : r' x y := by
  simpa [reflGen_eq_self hr'] using ReflGen.mono h hxy

Minimality Property of Reflexive Closure

Informal description

Let $r$ and $r'$ be relations on a type $\alpha$ such that $r'$ is reflexive and satisfies $\forall x y, r(x,y) \rightarrow r'(x,y)$. Then for any $x, y \in \alpha$, if $\text{ReflGen}(r)(x,y)$ holds, then $r'(x,y)$ also holds.

Relation.transGen_eq_self theorem

(trans : Transitive r) : TransGen r = r

Full source

theorem transGen_eq_self (trans : Transitive r) : TransGen r = r :=
  funext fun a ↦ funext fun b ↦ propext <|
    ⟨fun h ↦ by
      induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact trans hac hcd, TransGen.single⟩

Transitive Closure Equals Original Relation for Transitive Relations

Informal description

For any transitive relation $r$ on a type $\alpha$, the transitive closure of $r$ is equal to $r$ itself, i.e., $\text{TransGen}(r) = r$.

Relation.transitive_transGen theorem

: Transitive (TransGen r)

Full source

theorem transitive_transGen : Transitive (TransGen r) := fun _ _ _ ↦ TransGen.trans

Transitivity of the Transitive Closure

Informal description

The transitive closure $\text{TransGen}(r)$ of a relation $r$ on a type $\alpha$ is itself transitive. That is, for any $x, y, z \in \alpha$, if $\text{TransGen}(r)(x, y)$ and $\text{TransGen}(r)(y, z)$ hold, then $\text{TransGen}(r)(x, z)$ also holds.

Relation.instIsTransTransGen instance

: IsTrans α (TransGen r)

Full source

instance : IsTrans α (TransGen r) :=
  ⟨@TransGen.trans α r⟩

Transitivity of the Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the transitive closure $\text{TransGen}\, r$ is transitive.

Relation.transGen_idem theorem

: TransGen (TransGen r) = TransGen r

Full source

theorem transGen_idem : TransGen (TransGen r) = TransGen r :=
  transGen_eq_self transitive_transGen

Idempotence of Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the transitive closure operation is idempotent, i.e., $\text{TransGen}(\text{TransGen}(r)) = \text{TransGen}(r)$.

Relation.TransGen.lift theorem

 {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b)) (hab : TransGen r a b) :
  TransGen p (f a) (f b)

Full source

theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))
    (hab : TransGen r a b) : TransGen p (f a) (f b) := by
  induction hab with
  | single hac => exact TransGen.single (h a _ hac)
  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)

Lifting Property of Transitive Closure under Function Application

Informal description

Let $r$ be a relation on a type $\alpha$ and $p$ a relation on a type $\beta$. Given a function $f : \alpha \to \beta$ such that for all $a, b \in \alpha$, if $r(a, b)$ holds then $p(f(a), f(b))$ holds, then for any $a, b \in \alpha$ such that $\text{TransGen}\, r(a, b)$ holds, we have $\text{TransGen}\, p(f(a), f(b))$ holds.

Relation.TransGen.lift' theorem

 {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :
  TransGen p (f a) (f b)

Full source

theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
    (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :
    TransGen p (f a) (f b) := by
simpa [transGen_idem] using hab.lift f h

Lifting Property of Transitive Closure under Function Application (Extended Version)

Informal description

Let $r$ be a relation on a type $\alpha$ and $p$ a relation on a type $\beta$. Given a function $f : \alpha \to \beta$ such that for all $a, b \in \alpha$, if $r(a, b)$ holds then $\text{TransGen}\, p(f(a), f(b))$ holds, then for any $a, b \in \alpha$ such that $\text{TransGen}\, r(a, b)$ holds, we have $\text{TransGen}\, p(f(a), f(b))$ holds.

Relation.TransGen.closed theorem

{p : α → α → Prop} : (∀ a b, r a b → TransGen p a b) → TransGen r a b → TransGen p a b

Full source

theorem TransGen.closed {p : α → α → Prop} :
    (∀ a b, r a b → TransGen p a b) → TransGen r a b → TransGen p a b :=
  TransGen.lift' id

Closure Property of Transitive Closure under Relation Inclusion

Informal description

For any relations $r$ and $p$ on a type $\alpha$, if for all $a, b \in \alpha$, $r(a, b)$ implies $\text{TransGen}\, p(a, b)$, then $\text{TransGen}\, r(a, b)$ implies $\text{TransGen}\, p(a, b)$. In other words, if every pair related by $r$ is in the transitive closure of $p$, then the transitive closure of $r$ is contained in the transitive closure of $p$.

Relation.TransGen.closed' theorem

{P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a) {a b : α} (h : TransGen r a b) : P b → P a

Full source

lemma TransGen.closed' {P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a)
    {a b : α} (h : TransGen r a b) : P b → P a :=
  h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi

Downward Closure Property of Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$ and $P$ a predicate on $\alpha$. If for all $a, b \in \alpha$, $r(a, b)$ and $P(b)$ imply $P(a)$, then for any $a, b \in \alpha$ such that $\text{TransGen}\,r\,a\,b$ holds, $P(b)$ implies $P(a)$.

Relation.TransGen.mono theorem

{p : α → α → Prop} : (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b

Full source

theorem TransGen.mono {p : α → α → Prop} :
    (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b :=
  TransGen.lift id

Monotonicity of Transitive Closure

Informal description

For any relations $r$ and $p$ on a type $\alpha$, if $r(a, b)$ implies $p(a, b)$ for all $a, b \in \alpha$, then the transitive closure of $r$ implies the transitive closure of $p$. That is, if $\text{TransGen}\, r(a, b)$ holds, then $\text{TransGen}\, p(a, b)$ also holds.

Relation.transGen_minimal theorem

 {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y) {x y : α} (hxy : TransGen r x y) : r' x y

Full source

lemma transGen_minimal {r' : α → α → Prop} (hr' : Transitive r') (h : ∀ x y, r x y → r' x y)
    {x y : α} (hxy : TransGen r x y) : r' x y := by
  simpa [transGen_eq_self hr'] using TransGen.mono h hxy

Minimality Property of Transitive Closure

Informal description

For any transitive relation $r'$ on a type $\alpha$, if $r(x, y)$ implies $r'(x, y)$ for all $x, y \in \alpha$, then the transitive closure of $r$ implies $r'$. That is, if $\text{TransGen}\, r(x, y)$ holds, then $r'(x, y)$ also holds.

Relation.TransGen.swap theorem

(h : TransGen r b a) : TransGen (swap r) a b

Full source

theorem TransGen.swap (h : TransGen r b a) : TransGen (swap r) a b := by
  induction h with
  | single h => exact TransGen.single h
  | tail _ hbc ih => exact ih.head hbc

Transitive Closure of Swapped Relation Implies Swapped Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, if $b$ is transitively related to $a$ via $r$ (i.e., $\text{TransGen}\, r\, b\, a$ holds), then $a$ is transitively related to $b$ via the swapped relation $\operatorname{swap} r$ (i.e., $\text{TransGen}\, (\operatorname{swap} r)\, a\, b$ holds), where $\operatorname{swap} r\, x\, y = r\, y\, x$.

Relation.transGen_swap theorem

: TransGen (swap r) a b ↔ TransGen r b a

Full source

theorem transGen_swap : TransGenTransGen (swap r) a b ↔ TransGen r b a :=
  ⟨TransGen.swap, TransGen.swap⟩

Transitive Closure of Swapped Relation is Equivalent to Swapped Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, the transitive closure of the swapped relation $\operatorname{swap} r$ relates $a$ to $b$ if and only if the transitive closure of $r$ relates $b$ to $a$. That is, $\text{TransGen}\, (\operatorname{swap} r)\, a\, b \leftrightarrow \text{TransGen}\, r\, b\, a$, where $\operatorname{swap} r\, x\, y = r\, y\, x$.

Relation.reflTransGen_iff_eq theorem

(h : ∀ b, ¬r a b) : ReflTransGen r a b ↔ b = a

Full source

theorem reflTransGen_iff_eq (h : ∀ b, ¬r a b) : ReflTransGenReflTransGen r a b ↔ b = a := by
  rw [cases_head_iff]; simp [h, eq_comm]

Reflexive Transitive Closure Reduces to Equality for Terminal Elements

Informal description

For a relation $r$ on a type $\alpha$ and an element $a \in \alpha$ such that $r\, a\, b$ does not hold for any $b \in \alpha$, the reflexive transitive closure $\text{ReflTransGen}\, r\, a\, b$ holds if and only if $b = a$.

Relation.reflTransGen_iff_eq_or_transGen theorem

: ReflTransGen r a b ↔ b = a ∨ TransGen r a b

Full source

theorem reflTransGen_iff_eq_or_transGen : ReflTransGenReflTransGen r a b ↔ b = a ∨ TransGen r a b := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · cases h with
    | refl => exact Or.inl rfl
    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)
  · rcases h with (rfl | h)
    · rfl
    · exact h.to_reflTransGen

Reflexive Transitive Closure Equals Equality or Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, the reflexive transitive closure $\text{ReflTransGen}\, r\, a\, b$ holds if and only if either $b = a$ or there exists a transitive path from $a$ to $b$ (i.e., $\text{TransGen}\, r\, a\, b$ holds).

Relation.ReflTransGen.lift theorem

 {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b)) (hab : ReflTransGen r a b) :
  ReflTransGen p (f a) (f b)

Full source

theorem ReflTransGen.lift {p : β → β → Prop} {a b : α} (f : α → β)
    (h : ∀ a b, r a b → p (f a) (f b)) (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) :=
  ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.singleReflTransGen.single ∘ h _ _) fun _ _ ↦ trans

Lifting Property of Reflexive Transitive Closure under Relation-Preserving Maps

Informal description

Let $r$ be a relation on a type $\alpha$ and $p$ a relation on a type $\beta$. Given a function $f : \alpha \to \beta$ such that for any $a, b \in \alpha$, if $r\, a\, b$ holds then $p\, (f\, a)\, (f\, b)$ holds, and given that $\text{ReflTransGen}\, r\, a\, b$ holds for some $a, b \in \alpha$, then $\text{ReflTransGen}\, p\, (f\, a)\, (f\, b)$ also holds.

Relation.ReflTransGen.mono theorem

{p : α → α → Prop} : (∀ a b, r a b → p a b) → ReflTransGen r a b → ReflTransGen p a b

Full source

theorem ReflTransGen.mono {p : α → α → Prop} : (∀ a b, r a b → p a b) →
    ReflTransGen r a b → ReflTransGen p a b :=
  ReflTransGen.lift id

Monotonicity of Reflexive Transitive Closure

Informal description

Let $r$ and $p$ be relations on a type $\alpha$. If for all $a, b \in \alpha$, $r\, a\, b$ implies $p\, a\, b$, then for any $a, b \in \alpha$, the reflexive transitive closure $\text{ReflTransGen}\, r\, a\, b$ implies $\text{ReflTransGen}\, p\, a\, b$.

Relation.reflTransGen_eq_self theorem

(refl : Reflexive r) (trans : Transitive r) : ReflTransGen r = r

Full source

theorem reflTransGen_eq_self (refl : Reflexive r) (trans : Transitive r) : ReflTransGen r = r :=
  funext fun a ↦ funext fun b ↦ propext <|
    ⟨fun h ↦ by
      induction h with
      | refl => apply refl
      | tail _ h₂ IH => exact trans IH h₂, single⟩

Reflexive Transitive Closure Equals Original Relation for Reflexive and Transitive Relations

Informal description

For any reflexive and transitive relation $r$ on a type $\alpha$, the reflexive transitive closure of $r$ is equal to $r$ itself, i.e., $\text{ReflTransGen}(r) = r$.

Relation.reflTransGen_minimal theorem

 {r' : α → α → Prop} (hr₁ : Reflexive r') (hr₂ : Transitive r') (h : ∀ x y, r x y → r' x y) {x y : α}
  (hxy : ReflTransGen r x y) : r' x y

Full source

lemma reflTransGen_minimal {r' : α → α → Prop} (hr₁ : Reflexive r') (hr₂ : Transitive r')
    (h : ∀ x y, r x y → r' x y) {x y : α} (hxy : ReflTransGen r x y) : r' x y := by
  simpa [reflTransGen_eq_self hr₁ hr₂] using ReflTransGen.mono h hxy

Minimality of Reflexive Transitive Closure

Informal description

Let $r$ and $r'$ be relations on a type $\alpha$. If $r'$ is reflexive and transitive, and for all $x, y \in \alpha$, $r(x, y)$ implies $r'(x, y)$, then for any $x, y \in \alpha$ such that $\text{ReflTransGen}(r)(x, y)$ holds, we have $r'(x, y)$. In other words, the reflexive transitive closure $\text{ReflTransGen}(r)$ is the smallest reflexive and transitive relation containing $r$.

Relation.reflexive_reflTransGen theorem

: Reflexive (ReflTransGen r)

Full source

theorem reflexive_reflTransGen : Reflexive (ReflTransGen r) := fun _ ↦ refl

Reflexivity of Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the reflexive transitive closure $\text{ReflTransGen}(r)$ is reflexive, meaning that for every element $a \in \alpha$, the relation $\text{ReflTransGen}(r)(a, a)$ holds.

Relation.transitive_reflTransGen theorem

: Transitive (ReflTransGen r)

Full source

theorem transitive_reflTransGen : Transitive (ReflTransGen r) := fun _ _ _ ↦ trans

Transitivity of Reflexive Transitive Closure

Informal description

The reflexive transitive closure $\text{ReflTransGen}(r)$ of any relation $r$ on a type $\alpha$ is transitive. That is, for any elements $a, b, c \in \alpha$, if $\text{ReflTransGen}(r)(a, b)$ and $\text{ReflTransGen}(r)(b, c)$ hold, then $\text{ReflTransGen}(r)(a, c)$ also holds.

Relation.instIsReflReflTransGen instance

: IsRefl α (ReflTransGen r)

Full source

instance : IsRefl α (ReflTransGen r) :=
  ⟨@ReflTransGen.refl α r⟩

Reflexivity of the Reflexive Transitive Closure

Informal description

The reflexive transitive closure $\text{ReflTransGen}(r)$ of any relation $r$ on a type $\alpha$ is reflexive. That is, for every $a \in \alpha$, we have $\text{ReflTransGen}(r)(a, a)$.

Relation.instIsTransReflTransGen instance

: IsTrans α (ReflTransGen r)

Full source

instance : IsTrans α (ReflTransGen r) :=
  ⟨@ReflTransGen.trans α r⟩

Transitivity of Reflexive Transitive Closure

Informal description

The reflexive transitive closure $\text{ReflTransGen}(r)$ of any relation $r$ on a type $\alpha$ is transitive. That is, for any elements $a, b, c \in \alpha$, if $\text{ReflTransGen}(r)(a, b)$ and $\text{ReflTransGen}(r)(b, c)$ hold, then $\text{ReflTransGen}(r)(a, c)$ also holds.

Relation.reflTransGen_idem theorem

: ReflTransGen (ReflTransGen r) = ReflTransGen r

Full source

theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
  reflTransGen_eq_self reflexive_reflTransGen transitive_reflTransGen

Idempotence of Reflexive Transitive Closure: $\text{ReflTransGen}^2(r) = \text{ReflTransGen}(r)$

Informal description

For any relation $r$ on a type $\alpha$, the reflexive transitive closure of the reflexive transitive closure of $r$ is equal to the reflexive transitive closure of $r$, i.e., $\text{ReflTransGen}(\text{ReflTransGen}(r)) = \text{ReflTransGen}(r)$.

Relation.ReflTransGen.lift' theorem

 {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → ReflTransGen p (f a) (f b)) (hab : ReflTransGen r a b) :
  ReflTransGen p (f a) (f b)

Full source

theorem ReflTransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)
    (h : ∀ a b, r a b → ReflTransGen p (f a) (f b))
    (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) := by
  simpa [reflTransGen_idem] using hab.lift f h

Lifting Property of Reflexive Transitive Closure under Relation-Preserving Maps (Generalized)

Informal description

Let $r$ be a relation on a type $\alpha$ and $p$ a relation on a type $\beta$. Given a function $f : \alpha \to \beta$ such that for any $a, b \in \alpha$, if $r\, a\, b$ holds then $\text{ReflTransGen}\, p\, (f\, a)\, (f\, b)$ holds, and given that $\text{ReflTransGen}\, r\, a\, b$ holds for some $a, b \in \alpha$, then $\text{ReflTransGen}\, p\, (f\, a)\, (f\, b)$ also holds.

Relation.reflTransGen_closed theorem

{p : α → α → Prop} : (∀ a b, r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b

Full source

theorem reflTransGen_closed {p : α → α → Prop} :
    (∀ a b, r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b :=
  ReflTransGen.lift' id

Closure Property of Reflexive Transitive Closure under Relation Inclusion

Informal description

For any relation $p$ on a type $\alpha$, if for all $a, b \in \alpha$, $r\, a\, b$ implies $\text{ReflTransGen}\, p\, a\, b$, then $\text{ReflTransGen}\, r\, a\, b$ implies $\text{ReflTransGen}\, p\, a\, b$.

Relation.ReflTransGen.swap theorem

(h : ReflTransGen r b a) : ReflTransGen (swap r) a b

Full source

theorem ReflTransGen.swap (h : ReflTransGen r b a) : ReflTransGen (swap r) a b := by
  induction h with
  | refl => rfl
  | tail _ hbc ih => exact ih.head hbc

Reflexive Transitive Closure Preserves Relation Swapping

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, if $b$ is related to $a$ under the reflexive transitive closure of $r$ (i.e., $\text{ReflTransGen}\, r\, b\, a$ holds), then $a$ is related to $b$ under the reflexive transitive closure of the swapped relation $\operatorname{swap} r$ (i.e., $\text{ReflTransGen}\, (\operatorname{swap} r)\, a\, b$ holds).

Relation.reflTransGen_swap theorem

: ReflTransGen (swap r) a b ↔ ReflTransGen r b a

Full source

theorem reflTransGen_swap : ReflTransGenReflTransGen (swap r) a b ↔ ReflTransGen r b a :=
  ⟨ReflTransGen.swap, ReflTransGen.swap⟩

Reflexive Transitive Closure of Swapped Relation Equals Reverse Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, the reflexive transitive closure of the swapped relation $\operatorname{swap} r$ relates $a$ to $b$ if and only if the reflexive transitive closure of $r$ relates $b$ to $a$. In other words, $\text{ReflTransGen}\, (\operatorname{swap} r)\, a\, b \leftrightarrow \text{ReflTransGen}\, r\, b\, a$.

Relation.reflGen_transGen theorem

: ReflGen (TransGen r) = ReflTransGen r

Full source

@[simp] lemma reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r := by
  ext x y
  simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]

Reflexive Closure of Transitive Closure Equals Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the reflexive closure of the transitive closure of $r$ is equal to the reflexive transitive closure of $r$. In other words, $\text{ReflGen}(\text{TransGen}(r)) = \text{ReflTransGen}(r)$.

Relation.transGen_reflGen theorem

: TransGen (ReflGen r) = ReflTransGen r

Full source

@[simp] lemma transGen_reflGen : TransGen (ReflGen r) = ReflTransGen r := by
  ext x y
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · simpa [reflTransGen_idem]
      using TransGen.to_reflTransGen <| TransGen.mono (fun _ _ ↦ ReflGen.to_reflTransGen) h
  · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
    · exact .single .refl
    · exact TransGen.mono (fun _ _ ↦ .single) h

Transitive Closure of Reflexive Closure Equals Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the transitive closure of the reflexive closure of $r$ is equal to the reflexive transitive closure of $r$, i.e., $\text{TransGen}(\text{ReflGen}(r)) = \text{ReflTransGen}(r)$.

Relation.reflTransGen_reflGen theorem

: ReflTransGen (ReflGen r) = ReflTransGen r

Full source

@[simp] lemma reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r := by
  simp only [← transGen_reflGen, reflGen_eq_self reflexive_reflGen]

Reflexive Transitive Closure of Reflexive Closure Equals Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the reflexive transitive closure of the reflexive closure of $r$ is equal to the reflexive transitive closure of $r$, i.e., $\text{ReflTransGen}(\text{ReflGen}(r)) = \text{ReflTransGen}(r)$.

Relation.reflTransGen_transGen theorem

: ReflTransGen (TransGen r) = ReflTransGen r

Full source

@[simp] lemma reflTransGen_transGen : ReflTransGen (TransGen r) = ReflTransGen r := by
  simp only [← reflGen_transGen, transGen_idem]

Reflexive Transitive Closure of Transitive Closure Equals Reflexive Transitive Closure

Informal description

For any relation $r$ on a type $\alpha$, the reflexive transitive closure of the transitive closure of $r$ is equal to the reflexive transitive closure of $r$, i.e., $\text{ReflTransGen}(\text{TransGen}(r)) = \text{ReflTransGen}(r)$.

Relation.reflTransGen_eq_transGen theorem

(hr : Reflexive r) : ReflTransGen r = TransGen r

Full source

lemma reflTransGen_eq_transGen (hr : Reflexive r) :
    ReflTransGen r = TransGen r := by
  rw [← transGen_reflGen, reflGen_eq_self hr]

Reflexive Transitive Closure Equals Transitive Closure for Reflexive Relations

Informal description

For any reflexive relation $r$ on a type $\alpha$, the reflexive transitive closure of $r$ is equal to its transitive closure, i.e., $\text{ReflTransGen}(r) = \text{TransGen}(r)$.

Relation.reflTransGen_eq_reflGen theorem

(hr : Transitive r) : ReflTransGen r = ReflGen r

Full source

lemma reflTransGen_eq_reflGen (hr : Transitive r) :
    ReflTransGen r = ReflGen r := by
  rw [← reflGen_transGen, transGen_eq_self hr]

Reflexive Transitive Closure Equals Reflexive Closure for Transitive Relations

Informal description

For any transitive relation $r$ on a type $\alpha$, the reflexive transitive closure of $r$ is equal to its reflexive closure, i.e., $\text{ReflTransGen}(r) = \text{ReflGen}(r)$.

Relation.EqvGen.is_equivalence theorem

: Equivalence (@EqvGen α r)

Full source

theorem is_equivalence : Equivalence (@EqvGen α r) :=
  Equivalence.mk EqvGen.refl (EqvGen.symm _ _) (EqvGen.trans _ _ _)

Equivalence Closure is an Equivalence Relation

Informal description

The equivalence closure $\text{EqvGen}(r)$ of a relation $r$ on a type $\alpha$ is itself an equivalence relation, meaning it is reflexive, symmetric, and transitive.

Relation.EqvGen.setoid definition

: Setoid α

Full source

/-- `EqvGen.setoid r` is the setoid generated by a relation `r`.

The motivation for this definition is that `Quot r` behaves like `Quotient (EqvGen.setoid r)`,
see for example `Quot.eqvGen_exact` and `Quot.eqvGen_sound`. -/
def setoid : Setoid α :=
  Setoid.mk _ (EqvGen.is_equivalence r)

Setoid generated by the equivalence closure of a relation

Informal description

The setoid (equivalence relation) generated by a relation `r` on a type `α`, where two elements are equivalent if they are related by the equivalence closure of `r`. This means that `a ≈ b` holds if and only if `EqvGen r a b` holds, i.e., if `a` and `b` are connected by a sequence of `r`-related steps (possibly in either direction) or are equal.

Relation.EqvGen.mono theorem

{r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) : EqvGen p a b

Full source

theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) :
    EqvGen p a b := by
  induction h with
  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)
  | refl => exact EqvGen.refl _
  | symm a b _ ih => exact EqvGen.symm _ _ ih
  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc

Monotonicity of Equivalence Closure with Respect to Relation Inclusion

Informal description

Let $r$ and $p$ be two relations on a type $\alpha$. If for all $a, b \in \alpha$, $r(a, b)$ implies $p(a, b)$, then for any $a, b \in \alpha$ related by the equivalence closure of $r$, they are also related by the equivalence closure of $p$. In other words, if $r \subseteq p$ (as relations), then $\text{EqvGen}(r) \subseteq \text{EqvGen}(p)$.

Relation.Join definition

(r : α → α → Prop) : α → α → Prop

Full source

/-- The join of a relation on a single type is a new relation for which
pairs of terms are related if there is a third term they are both
related to.  For example, if `r` is a relation representing rewrites
in a term rewriting system, then *confluence* is the property that if
`a` rewrites to both `b` and `c`, then `join r` relates `b` and `c`
(see `Relation.church_rosser`).
-/
def Join (r : α → α → Prop) : α → α → Prop := fun a b ↦ ∃ c, r a c ∧ r b c

Join of a relation

Informal description

Given a relation $ r $ on a type $ \alpha $, the join of $ r $ is a new relation on $ \alpha $ where two elements $ a $ and $ b $ are related if there exists a third element $ c $ such that both $ a $ and $ b $ are related to $ c $ via $ r $. In other words, $ \text{Join}\,r\,a\,b $ holds if and only if there exists $ c $ such that $ r\,a\,c $ and $ r\,b\,c $.

Relation.church_rosser theorem

 (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) (hab : ReflTransGen r a b)
  (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c

Full source

/-- A sufficient condition for the Church-Rosser property. -/
theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d)
    (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c := by
  induction hab with
  | refl => exact ⟨c, hac, refl⟩
  | @tail d e _ hde ih =>
    rcases ih with ⟨b, hdb, hcb⟩
    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by
      clear hcb
      induction hdb with
      | refl => exact ⟨e, refl, ReflGen.single hde⟩
      | @tail f b _ hfb ih =>
        rcases ih with ⟨a, hea, hfa⟩
        cases hfa with
        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩
        | single hfa =>
          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩
          exact ⟨c, hea.trans hac, hbc⟩
    rcases this with ⟨a, hea, hba⟩
    cases hba with
    | refl => exact ⟨b, hea, hcb⟩
    | single hba => exact ⟨a, hea, hcb.tail hba⟩

Church-Rosser Property for Reflexive Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$ such that for any elements $a, b, c \in \alpha$, if $r(a, b)$ and $r(a, c)$ hold, then there exists $d \in \alpha$ with $\text{ReflGen}\,r\,b\,d$ and $\text{ReflTransGen}\,r\,c\,d$. Then for any $a, b, c \in \alpha$ with $\text{ReflTransGen}\,r\,a\,b$ and $\text{ReflTransGen}\,r\,a\,c$, there exists $d' \in \alpha$ such that $\text{ReflTransGen}\,r\,b\,d'$ and $\text{ReflTransGen}\,r\,c\,d'$ hold (i.e., $b$ and $c$ are joinable under $\text{ReflTransGen}\,r$).

Relation.join_of_single theorem

(h : Reflexive r) (hab : r a b) : Join r a b

Full source

theorem join_of_single (h : Reflexive r) (hab : r a b) : Join r a b :=
  ⟨b, hab, h b⟩

Join Relation Contains Original Relation for Reflexive Relations

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$ such that $r(a, b)$ holds, the join relation $\text{Join}\,r$ relates $a$ and $b$.

Relation.symmetric_join theorem

: Symmetric (Join r)

Full source

theorem symmetric_join : Symmetric (Join r) := fun _ _ ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩

Symmetry of the Join Relation

Informal description

For any relation $r$ on a type $\alpha$, the join relation $\text{Join}\,r$ is symmetric. That is, for any elements $a$ and $b$ in $\alpha$, if $\text{Join}\,r\,a\,b$ holds, then $\text{Join}\,r\,b\,a$ also holds.

Relation.reflexive_join theorem

(h : Reflexive r) : Reflexive (Join r)

Full source

theorem reflexive_join (h : Reflexive r) : Reflexive (Join r) := fun a ↦ ⟨a, h a, h a⟩

Reflexivity of the Join Relation for Reflexive Relations

Informal description

For any reflexive relation $r$ on a type $\alpha$, the join relation $\text{Join}\,r$ is also reflexive. That is, for every $a \in \alpha$, we have $\text{Join}\,r\,a\,a$.

Relation.transitive_join theorem

(ht : Transitive r) (h : ∀ a b c, r a b → r a c → Join r b c) : Transitive (Join r)

Full source

theorem transitive_join (ht : Transitive r) (h : ∀ a b c, r a b → r a c → Join r b c) :
    Transitive (Join r) :=
  fun _ b _ ⟨x, hax, hbx⟩ ⟨y, hby, hcy⟩ ↦
  let ⟨z, hxz, hyz⟩ := h b x y hbx hby
  ⟨z, ht hax hxz, ht hcy hyz⟩

Transitivity of the Join Relation under Transitive Base Relation

Informal description

Let $r$ be a transitive relation on a type $\alpha$. Suppose that for any elements $a, b, c \in \alpha$, if $r\,a\,b$ and $r\,a\,c$ hold, then there exists some $d$ such that $\text{Join}\,r\,b\,d$ and $\text{Join}\,r\,c\,d$ hold. Then the join relation $\text{Join}\,r$ is transitive.

Relation.equivalence_join theorem

(hr : Reflexive r) (ht : Transitive r) (h : ∀ a b c, r a b → r a c → Join r b c) : Equivalence (Join r)

Full source

theorem equivalence_join (hr : Reflexive r) (ht : Transitive r)
    (h : ∀ a b c, r a b → r a c → Join r b c) : Equivalence (Join r) :=
  ⟨reflexive_join hr, @symmetric_join _ _, @transitive_join _ _ ht h⟩

Join of Reflexive Transitive Relation is an Equivalence Relation

Informal description

Let $r$ be a reflexive and transitive relation on a type $\alpha$. Suppose that for any elements $a, b, c \in \alpha$, if $r\,a\,b$ and $r\,a\,c$ hold, then there exists some $d$ such that $\text{Join}\,r\,b\,d$ and $\text{Join}\,r\,c\,d$ hold. Then the join relation $\text{Join}\,r$ is an equivalence relation on $\alpha$.

Relation.equivalence_join_reflTransGen theorem

(h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) : Equivalence (Join (ReflTransGen r))

Full source

theorem equivalence_join_reflTransGen
    (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) :
    Equivalence (Join (ReflTransGen r)) :=
  equivalence_join reflexive_reflTransGen transitive_reflTransGen fun _ _ _ ↦ church_rosser h

Equivalence of Join Relation under Reflexive Transitive Closure

Informal description

Let $r$ be a relation on a type $\alpha$ such that for any elements $a, b, c \in \alpha$, if $r(a, b)$ and $r(a, c)$ hold, then there exists $d \in \alpha$ with $\text{ReflGen}\,r\,b\,d$ and $\text{ReflTransGen}\,r\,c\,d$. Then the join relation $\text{Join}(\text{ReflTransGen}\,r)$ is an equivalence relation on $\alpha$.

Relation.join_of_equivalence theorem

{r' : α → α → Prop} (hr : Equivalence r) (h : ∀ a b, r' a b → r a b) : Join r' a b → r a b

Full source

theorem join_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) (h : ∀ a b, r' a b → r a b) :
    Join r' a b → r a b
  | ⟨_, hac, hbc⟩ => hr.trans (h _ _ hac) (hr.symm <| h _ _ hbc)

Join of a Subrelation of an Equivalence Relation is Contained in the Equivalence Relation

Informal description

Let $r$ be an equivalence relation on a type $\alpha$, and let $r'$ be another relation on $\alpha$ such that for any $a, b \in \alpha$, if $r'\,a\,b$ holds then $r\,a\,b$ holds. If $a$ and $b$ are related by the join of $r'$ (i.e., there exists some $c$ such that $r'\,a\,c$ and $r'\,b\,c$), then $a$ and $b$ are related by $r$.

Relation.reflTransGen_of_transitive_reflexive theorem

 {r' : α → α → Prop} (hr : Reflexive r) (ht : Transitive r) (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) :
  r a b

Full source

theorem reflTransGen_of_transitive_reflexive {r' : α → α → Prop} (hr : Reflexive r)
    (ht : Transitive r) (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by
  induction h' with
  | refl => exact hr _
  | tail _ hbc ih => exact ht ih (h _ _ hbc)

Reflexive Transitive Closure of Subrelation in Reflexive Transitive Relation

Informal description

Let $r$ and $r'$ be relations on a type $\alpha$ such that: 1. $r$ is reflexive and transitive, 2. For all $a, b \in \alpha$, if $r'\,a\,b$ holds then $r\,a\,b$ holds. If $\text{ReflTransGen}\,r'\,a\,b$ holds (i.e., $a$ can be rewritten to $b$ via zero or more applications of $r'$), then $r\,a\,b$ holds.

Relation.reflTransGen_of_equivalence theorem

{r' : α → α → Prop} (hr : Equivalence r) : (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b

Full source

theorem reflTransGen_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) :
    (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b :=
  reflTransGen_of_transitive_reflexive hr.1 (fun _ _ _ ↦ hr.trans)

Equivalence Relation Contains Reflexive Transitive Closure of Subrelation

Informal description

Let $r$ be an equivalence relation on a type $\alpha$, and let $r'$ be another relation on $\alpha$ such that for all $a, b \in \alpha$, $r'\,a\,b$ implies $r\,a\,b$. If $\text{ReflTransGen}\,r'\,a\,b$ holds (i.e., $a$ can be rewritten to $b$ via zero or more applications of $r'$), then $r\,a\,b$ holds.

Quot.eqvGen_exact theorem

(H : Quot.mk r a = Quot.mk r b) : EqvGen r a b

Full source

theorem Quot.eqvGen_exact (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=
  @Quotient.exact _ (EqvGen.setoid r) a b (congrArg
    (Quot.lift (Quotient.mk (EqvGen.setoid r)) (fun x y h ↦ Quot.sound (EqvGen.rel x y h))) H)

Exactness of Equivalence Closure for Quotient Construction

Informal description

For any relation $r$ on a type $\alpha$, if the equivalence classes of $a$ and $b$ under $r$ are equal (i.e., $\text{Quot.mk}\, r\, a = \text{Quot.mk}\, r\, b$), then $a$ and $b$ are related by the equivalence closure of $r$, denoted $\text{EqvGen}\, r\, a\, b$.

Quot.eqvGen_sound theorem

(H : EqvGen r a b) : Quot.mk r a = Quot.mk r b

Full source

theorem Quot.eqvGen_sound (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=
  EqvGen.rec
    (fun _ _ h ↦ Quot.sound h)
    (fun _ ↦ rfl)
    (fun _ _ _ IH ↦ Eq.symm IH)
    (fun _ _ _ _ _ IH₁ IH₂ ↦ Eq.trans IH₁ IH₂)
    H

Soundness of Equivalence Closure for Quotient Construction

Informal description

For any relation $r$ on a type $\alpha$, if the equivalence closure $\text{EqvGen}\, r$ relates elements $a$ and $b$, then the equivalence classes of $a$ and $b$ under $r$ are equal, i.e., $\text{Quot.mk}\, r\, a = \text{Quot.mk}\, r\, b$.

Equivalence.eqvGen_iff theorem

(h : Equivalence r) : EqvGen r a b ↔ r a b

Full source

theorem Equivalence.eqvGen_iff (h : Equivalence r) : EqvGenEqvGen r a b ↔ r a b :=
  Iff.intro
    (by
      intro h
      induction h with
      | rel => assumption
      | refl => exact h.1 _
      | symm => apply h.symm; assumption
      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)
    (EqvGen.rel a b)

Equivalence Closure Characterization for Equivalence Relations

Informal description

For any equivalence relation $r$ on a type $\alpha$, the equivalence closure $\text{EqvGen}\, r$ relates elements $a$ and $b$ if and only if $r$ relates $a$ and $b$, i.e., $\text{EqvGen}\, r\, a\, b \leftrightarrow r\, a\, b$.

Equivalence.eqvGen_eq theorem

(h : Equivalence r) : EqvGen r = r

Full source

theorem Equivalence.eqvGen_eq (h : Equivalence r) : EqvGen r = r :=
  funext fun _ ↦ funext fun _ ↦ propext <| h.eqvGen_iff

Equivalence Closure of an Equivalence Relation is Itself

Informal description

For any equivalence relation $r$ on a type $\alpha$, the equivalence closure $\text{EqvGen}\, r$ is equal to $r$, i.e., $\text{EqvGen}\, r = r$.

Definitions