Relation.lean

/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
-/
module

public import Mathlib.Logic.Relator
public import Mathlib.Tactic.Use
public import Mathlib.Tactic.MkIffOfInductiveProp
public import Mathlib.Tactic.SimpRw
public import Mathlib.Order.Defs.Prop
public import Mathlib.Order.Defs.Unbundled
public import Batteries.Logic
public import Batteries.Tactic.Trans

/-!
# Relation closures

This file defines the reflexive, symmetric, transitive, reflexive transitive and equivalence
closures of relations and proves some basic results on them.

Note that this is about unbundled relations, that is terms of types of the form `α → β → Prop`. For
the bundled version, see `Rel`.

## Definitions

* `Relation.ReflGen`: Reflexive closure. `ReflGen r` relates everything `r` related, plus for all
  `a` it relates `a` with itself. So `ReflGen r a b ↔ r a b ∨ a = b`.
* `Relation.SymmGen`: Symmetric closure. This is also the comparability relation,
  such that `SymmGen r a b` means that either `r a b` or `r b a` (see `Mathlib.Order.Comparable`)
* `Relation.TransGen`: Transitive closure. `TransGen r` relates everything `r` related
  transitively. So `TransGen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b`.
* `Relation.ReflTransGen`: Reflexive transitive closure. `ReflTransGen r` relates everything
  `r` related transitively, plus for all `a` it relates `a` with itself. So
  `ReflTransGen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b`. It is the same as
  the reflexive closure of the transitive closure, or the transitive closure of the reflexive
  closure. In terms of rewriting systems, this means that `a` can be rewritten to `b` in a number of
  rewrites.
* `Relation.EqvGen`: Equivalence closure. `EqvGen r` relates everything `ReflTransGen r` relates,
  plus for all related pairs it relates them in the opposite order.
* `Relation.Comp`:  Relation composition. We provide notation `∘r`. For `r : α → β → Prop` and
  `s : β → γ → Prop`, `r ∘r s` relates `a : α` and `c : γ` iff there exists `b : β` that's related
  to both.
* `Relation.Map`: Image of a relation under a pair of maps. For `r : α → β → Prop`, `f : α → γ`,
  `g : β → δ`, `Map r f g` is the relation `γ → δ → Prop` relating `f a` and `g b` for all `a`, `b`
  related by `r`.
* `Relation.Join`: Join of a relation. For `r : α → α → Prop`, `Join r a b ↔ ∃ c, r a c ∧ r b c`. In
  terms of rewriting systems, this means that `a` and `b` can be rewritten to the same term.
-/

@[expose] public section


open Function

variable {α β γ δ ε ζ : Type*}

theorem Subrelation.antisymm {r r' : α → α → Prop} (h1 : Subrelation r r') (h2 : Subrelation r' r) :
    r = r' :=
  funext₂ fun _ _ => propext ⟨h1, h2⟩

section NeImp

variable {r : α → α → Prop}

@[deprecated (since := "2026-03-27")] alias Std.Refl.reflexive := refl

@[deprecated (since := "2026-01-09")] alias IsRefl.reflexive := refl

/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,
it suffices to show it holds when `x ≠ y`. -/
theorem Std.Refl.rel_of_ne_imp [Std.Refl r] {x y : α} (hr : x ≠ y → r x y) : r x y := by
  grind [Std.Refl]

@[deprecated (since := "2026-03-27")] alias Reflexive.rel_of_ne_imp := Std.Refl.rel_of_ne_imp

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

@[deprecated (since := "2026-03-27")] alias Reflexive.ne_imp_iff := Std.Refl.ne_imp_iff
@[deprecated (since := "2026-03-27")] alias reflexive_ne_imp_iff := Std.Refl.ne_imp_iff

theorem refl_iff_eq_le : Std.Refl r ↔ Eq ≤ r := by
  unfold Pi.hasLe Prop.le
  grind [Std.Refl]

@[deprecated (since := "2026-06-30")] alias refl_iff_subrelation_eq := refl_iff_eq_le
@[deprecated (since := "2026-03-27")] alias reflexive_iff_subrelation_eq := refl_iff_eq_le

theorem irrefl_iff_le_ne : Std.Irrefl r ↔ r ≤ Ne := by
  unfold Pi.hasLe Prop.le
  grind [Std.Irrefl]

@[deprecated (since := "2026-06-30")] alias irrefl_iff_subrelation_ne := irrefl_iff_le_ne
@[deprecated (since := "2026-02-12")] alias irreflexive_iff_subrelation_ne := irrefl_iff_le_ne

protected theorem Std.Symm.iff [Std.Symm r] (x y : α) : r x y ↔ r y x :=
  ⟨symm_of r, symm_of r⟩

@[deprecated (since := "2026-06-10")] protected alias Symmetric.iff := Std.Symm.iff

theorem Std.Symm.flip_eq [Std.Symm r] : flip r = r :=
  funext₂ fun _ _ ↦ propext <| Std.Symm.iff (r := r) ..

@[deprecated (since := "2026-06-10")] alias Symmetric.flip_eq := Std.Symm.flip_eq

theorem Std.Symm.swap_eq [Std.Symm r] : swap r = r :=
  Std.Symm.flip_eq

@[deprecated (since := "2026-06-10")] alias Symmetric.swap_eq := Std.Symm.swap_eq

theorem flip_eq_iff : flip r = r ↔ Std.Symm r :=
  ⟨fun h ↦ ⟨fun _ _ ↦ congr_fun₂ h .. |>.mp⟩, fun _ ↦ Std.Symm.flip_eq⟩

theorem swap_eq_iff : swap r = r ↔ Std.Symm r :=
  flip_eq_iff

end NeImp

section Comap

variable {r : β → β → Prop}

instance Std.Refl.comap [Std.Refl r] (f : α → β) : Std.Refl (r on f) where
  refl a := refl <| f a

@[deprecated (since := "2026-03-27")] alias Reflexive.comap := Std.Refl.comap

instance Std.Symm.comap [Std.Symm r] (f : α → β) : Std.Symm (r on f) where
  symm _ _ hab := symm_of r hab

@[deprecated (since := "2026-06-10")] alias Symmetric.comap := Std.Symm.comap

instance IsTrans.comap [IsTrans β r] (f : α → β) : IsTrans α (r on f) where
  trans _ _ _ := trans_of r

@[deprecated (since := "2026-02-21")] alias Transitive.comap := IsTrans.comap

instance IsEquiv.comap [IsEquiv β r] (f : α → β) : IsEquiv α (r on f) where

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

end Comap

namespace Relation

section Comp

variable {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}

/-- 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

@[inherit_doc]
local infixr:80 " ∘r " => Relation.Comp

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

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

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

@[simp]
theorem eq_comp : (· = ·) ∘r r = r := fun_eq_comp ..

@[simp]
theorem iff_comp {r : Prop → α → Prop} : (· ↔ ·) ∘r r = r := by
  grind [eq_comp]

@[simp]
theorem comp_iff {r : α → Prop → Prop} : r ∘r (· ↔ ·) = r := by
  grind [comp_eq]

theorem comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q := by
  grind [Comp]

theorem flip_comp : flip (r ∘r p) = flip 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⟩

end Comp

section Fibration

variable (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)

/-- 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

variable {rα rβ}

/-- 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'

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⟩

end Fibration

section Map
variable {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ} {d : δ}

/-- 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

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

@[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
  grind [Relation.Map]

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

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

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

lemma _root_.Std.Refl.map {r : α → α → Prop} [Std.Refl r] {f : α → β} (hf : f.Surjective) :
    Std.Refl (Relation.Map r f f) where
  refl x := by
    obtain ⟨y, rfl⟩ := hf x
    exact ⟨y, y, refl y, rfl, rfl⟩

@[deprecated (since := "2026-03-27")] alias map_reflexive := Std.Refl.map

instance _root_.Std.Symm.map {r : α → α → Prop} [Std.Symm r] (f : α → β) :
    Std.Symm (Relation.Map r f f) where
  symm _ _ := by
    rintro ⟨x, y, hxy, rfl, rfl⟩
    exact ⟨y, x, symm hxy, rfl, rfl⟩

@[deprecated (since := "2026-06-10")] alias map_symmetric := Std.Symm.map

lemma _root_.IsTrans.map {r : α → α → Prop} [IsTrans α r] {f : α → β}
    (hf : ∀ x y, f x = f y → r x y) : IsTrans β (Relation.Map r f f) := by
  grind [isTrans_def, Relation.Map]

@[deprecated (since := "2026-03-27")] alias isTrans_map := IsTrans.map

@[deprecated (since := "2026-02-21")] alias map_transitive := isTrans_map

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 := hr.stdRefl.map hf |>.refl
  symm := @(hr.stdSymm.map f |>.symm)
  trans := @(hr.isTrans.map hf_ker |>.trans)

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

lemma le_onFun_map {r : α → α → Prop} (f : α → β) : r ≤ (Relation.Map r f f on f) := by
  unfold Pi.hasLe Prop.le
  grind [Relation.Map]

lemma onFun_map_eq_of_injective {r : α → α → Prop} {f : α → β} (hinj : f.Injective) :
    (Relation.Map r f f on f) = r := by
  ext x y
  exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩

lemma map_onFun_le {r : β → β → Prop} (f : α → β) : Relation.Map (r on f) f f ≤ r := by
  unfold Pi.hasLe Prop.le
  grind [Relation.Map]

lemma map_onFun_eq_of_surjective {r : β → β → Prop} {f : α → β} (hsurj : f.Surjective) :
    Relation.Map (r on f) f f = r := by
  ext x y
  have _ := hsurj x
  have _ := hsurj y
  grind [Relation.Map]

lemma map_onFun_map_eq_map {r : α → α → Prop} (f : α → β) :
    Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f := by
  grind [Relation.Map]

lemma onFun_map_onFun_eq_onFun {r : β → β → Prop} (f : α → β) :
    (Relation.Map (r on f) f f on f) = (r on f) := by
  grind [Relation.Map]

lemma onFun_map_onFun_iff_onFun {r : β → β → Prop} (f : α → β) (a₁ a₂ : α) :
    Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂) := by
  grind [Relation.Map]

end Map

variable {r : α → α → Prop} {a b c : α}

/-- `ReflTransGen r`: reflexive transitive closure of `r` -/
@[mk_iff ReflTransGen.cases_tail_iff, grind]
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

attribute [refl] ReflTransGen.refl

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

attribute [refl] ReflGen.refl
attribute [grind =] reflGen_iff

/-- `SymmGen r`: symmetric closure of `r`. This is also the comparability relation, such
  that `SymmGen r a b` means that either `r a b` or `r b a` (see `Mathlib.Order.Comparable`). -/
def SymmGen (r : α → α → Prop) (a b : α) : Prop :=
  r a b ∨ r b a

variable (r) in
/-- `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

attribute [mk_iff] TransGen
attribute [grind] TransGen

theorem reflGen_le_reflTransGen : ReflGen r ≤ ReflTransGen r
  | a, _, .refl => by rfl
  | _, _, .single h => ReflTransGen.tail ReflTransGen.refl h

namespace ReflGen

theorem to_reflTransGen {a b} : ReflGen r a b → ReflTransGen r a b :=
  reflGen_le_reflTransGen a b

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

instance : Std.Refl (ReflGen r) :=
  ⟨@refl α r⟩

instance stdSymm [Std.Symm r] : Std.Symm (ReflGen r) where
  symm _ _
    | refl => refl
    | single h => single <| symm h

@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm

instance [IsTrans α r] : IsPreorder α (ReflGen r) where
  trans := by grind [isTrans_def]

end ReflGen

namespace SymmGen

theorem of_rel (h : r a b) : SymmGen r a b :=
  Or.inl h

theorem of_rel_symm (h : r b a) : SymmGen r a b :=
  Or.inr h

theorem swap (h : SymmGen r b a) : SymmGen (swap r) a b := by
  induction h with
  | inl hba => exact of_rel hba
  | inr hab => exact of_rel_symm hab

@[simp, refl]
theorem refl (r : α → α → Prop) [Std.Refl r] (a : α) : SymmGen r a a :=
  .of_rel (_root_.refl _)

theorem rfl [Std.Refl r] : SymmGen r a a := .refl ..

instance [Std.Refl r] : Std.Refl (SymmGen r) where
  refl := .refl r

@[symm]
theorem symm : SymmGen r a b → SymmGen r b a :=
  Or.symm

instance : Std.Symm (SymmGen r) where
  symm _ _ := SymmGen.symm

instance decidableRel [DecidableRel r] : DecidableRel (SymmGen r) :=
  fun _ _ ↦ inferInstanceAs (Decidable (_ ∨ _))

theorem of_le {α : Type*} [LE α] {a b : α} (h : a ≤ b) : SymmGen (· ≤ ·) a b := .of_rel h
theorem of_ge {α : Type*} [LE α] {a b : α} (h : b ≤ a) : SymmGen (· ≤ ·) a b := .of_rel_symm h

alias _root_.LE.le.symmGen := SymmGen.of_le
alias _root_.LE.le.symmGen_symm := SymmGen.of_ge

end SymmGen

namespace ReflTransGen

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

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

theorem le_reflTransGen : r ≤ ReflTransGen r :=
  fun _ _ ↦ single

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

instance stdSymm [Std.Symm r] : Std.Symm (ReflTransGen r) where
  symm x y h := by
    induction h with
    | refl => rfl
    | tail _ b c => apply c.head <| symm b

@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm

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

@[elab_as_elim]
theorem head_induction_on {motive : ∀ a : α, ReflTransGen r a b → Prop} {a : α}
    (h : ReflTransGen r a b) (refl : motive b refl)
    (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a (h.head h')) :
    motive 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)

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

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 <;> grind

theorem cases_head_iff : ReflTransGen 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

theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a b)
    (ac : ReflTransGen r a c) : ReflTransGen r b c ∨ ReflTransGen r c b := by
  induction ab with
  | refl => exact Or.inl ac
  | tail _ bd IH =>
    rcases IH with (IH | IH)
    · grind [cases_head IH, Relator.RightUnique]
    · exact Or.inr (IH.tail bd)

end ReflTransGen

theorem transGen_le_reflTransGen : TransGen r ≤ ReflTransGen r := by
  intro a _ h
  induction h with
  | single h => exact ReflTransGen.single h
  | tail _ bc ab => exact ReflTransGen.tail ab bc

namespace TransGen

theorem to_reflTransGen {a b} : TransGen r a b → ReflTransGen r a b :=
  transGen_le_reflTransGen a b

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

attribute [trans] trans

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

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

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

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

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

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

theorem tail'_iff : TransGen 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⟩

theorem head'_iff : TransGen 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⟩

instance stdSymm [Std.Symm r] : Std.Symm (TransGen r) where
  symm x y h := by
    induction h with
    | single i => exact .single <| symm i
    | tail _ h₁ h₂ => exact .head (symm h₁) h₂

@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm

instance : IsTrans α (TransGen r) where
  trans _ _ _ := TransGen.trans

instance [Std.Refl r] : IsPreorder α (TransGen r) where
  refl x := .single (refl x)

end TransGen

section reflGen

@[grind =]
lemma reflGen_eq_self [Std.Refl r] : ReflGen r = r := by
  ext x y
  simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ refl y

@[deprecated inferInstance (since := "2026-03-27")]
lemma reflexive_reflGen : Std.Refl (ReflGen r) := inferInstance

lemma reflGen_minimal {r' : α → α → Prop} [Std.Refl r'] (h : r ≤ r') : ReflGen r ≤ r' := by
  simpa [reflGen_eq_self] using ReflGen.mono h

end reflGen

section SymmGen

theorem symmGen_swap (r : α → α → Prop) : SymmGen (swap r) = SymmGen r :=
  funext₂ fun _ _ ↦ propext or_comm

theorem symmGen_swap_apply (r : α → α → Prop) : SymmGen (swap r) a b ↔ SymmGen r a b :=
  or_comm

theorem symmGen_comm {a b : α} : SymmGen r a b ↔ SymmGen r b a :=
  or_comm

@[simp]
theorem symmGen_of_total [Std.Total r] (a b : α) : SymmGen r a b :=
  Std.Total.total a b

end SymmGen

section TransGen

instance : Trans (TransGen r) r (TransGen r) :=
  ⟨TransGen.tail⟩

instance : Trans r (TransGen r) (TransGen r) :=
  ⟨TransGen.head⟩

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

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

@[grind =]
theorem transGen_eq_self [IsTrans α r] : TransGen r = r :=
  funext₂ fun a b ↦ propext <|
    ⟨fun h ↦ by
      induction h with
      | single hc => exact hc
      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd, TransGen.single⟩

@[deprecated inferInstance (since := "2026-02-21")]
theorem transitive_transGen : IsTrans α (TransGen r) := inferInstance

@[deprecated transGen_eq_self (since := "2026-03-27"), grind =]
theorem transGen_idem : TransGen (TransGen r) = TransGen r :=
  transGen_eq_self

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

theorem TransGen.lift' {p : β → β → Prop} (f : α → β) (h : r ≤ (TransGen p on f)) :
    TransGen r ≤ (TransGen p on f) := by
  intro _ _ hab
  simpa [transGen_eq_self] using hab.lift f h

theorem TransGen.closed {p : α → α → Prop} : r ≤ TransGen p → TransGen r ≤ TransGen p :=
  TransGen.lift' id

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

theorem TransGen.mono {p : α → α → Prop} : r ≤ p → TransGen r ≤ TransGen p :=
  TransGen.lift id

lemma transGen_minimal {r' : α → α → Prop} [IsTrans α r'] (h : r ≤ r') : TransGen r ≤ r' := by
  simpa [transGen_eq_self] using TransGen.mono h

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

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

end TransGen

section ReflTransGen

open ReflTransGen

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

@[grind =]
theorem reflTransGen_iff_eq_or_transGen : ReflTransGen 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

theorem ReflTransGen.lift {p : β → β → Prop} (f : α → β) (h : r ≤ (p on f)) :
    ReflTransGen r ≤ (ReflTransGen p on f) :=
  fun _ _ hab ↦ trans_induction_on hab (fun _ ↦ refl) (single ∘ h _ _) fun _ _ ↦ trans

theorem ReflTransGen.mono {p : α → α → Prop} : r ≤ p → ReflTransGen r ≤ ReflTransGen p :=
  ReflTransGen.lift id

@[grind =]
theorem reflTransGen_eq_self [Std.Refl r] [IsTrans α r] : ReflTransGen r = r :=
  funext₂ fun a b ↦ propext
    ⟨fun h ↦ by
      induction h with
      | refl => exact refl a
      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂, single⟩

instance : Trans r (ReflTransGen r) (ReflTransGen r) :=
  ⟨head⟩

instance : Trans (ReflTransGen r) r (ReflTransGen r) :=
  ⟨tail⟩

instance : IsPreorder α (ReflTransGen r) where
  refl := @ReflTransGen.refl α r
  trans := @ReflTransGen.trans α r

@[deprecated inferInstance (since := "2026-03-27")]
theorem reflexive_reflTransGen : Std.Refl (ReflTransGen r) := inferInstance

@[deprecated inferInstance (since := "2026-02-21")]
theorem transitive_reflTransGen : IsTrans α (ReflTransGen r) := inferInstance

@[deprecated reflTransGen_eq_self (since := "2026-03-27"), grind =]
theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=
  reflTransGen_eq_self

theorem ReflTransGen.lift' {p : β → β → Prop} (f : α → β) (h : r ≤ (ReflTransGen p on f)) :
    ReflTransGen r ≤ (ReflTransGen p on f) := by
  intro _ _ hab
  simpa [reflTransGen_eq_self] using hab.lift f h

theorem reflTransGen_closed {p : α → α → Prop} :
    r ≤ ReflTransGen p → ReflTransGen r ≤ ReflTransGen p :=
  ReflTransGen.lift' id

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

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

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

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

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

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

@[grind =]
lemma reflTransGen_eq_transGen [Std.Refl r] : ReflTransGen r = TransGen r := by
  rw [← transGen_reflGen, reflGen_eq_self]

@[grind =]
lemma reflTransGen_eq_reflGen [IsTrans α r] : ReflTransGen r = ReflGen r := by
  rw [← reflGen_transGen, transGen_eq_self]

end ReflTransGen

namespace EqvGen

variable (r)

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

instance : IsEquiv α (EqvGen r) := is_equivalence _ |>.isEquiv

/-- `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`. -/
@[implicit_reducible]
def setoid : Setoid α :=
  Setoid.mk _ (EqvGen.is_equivalence r)

theorem mono {r p : α → α → Prop} (hrp : r ≤ p) : EqvGen r ≤ EqvGen p := by
  intro _ _ h
  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

lemma eqvGen_le {r r' : α → α → Prop} [IsEquiv α r'] (h : Subrelation r r') :
    Subrelation (EqvGen r) r'
  | _, _, .refl _ => _root_.refl _
  | _, _, .symm _ _ hxy => _root_.symm (eqvGen_le h hxy :)
  | _, _, .trans _ _ _ hxy hyz => _root_.trans (eqvGen_le h hxy :) (eqvGen_le h hyz :)
  | _, _, .rel _ _ hab => h hab

lemma eqvGen_mono {r r' : α → α → Prop} (h : Subrelation r r') : Subrelation (EqvGen r) (EqvGen r')
  | _, _, .refl _ => .refl _
  | _, _, .symm _ _ hxy => .symm _ _ (eqvGen_mono h hxy)
  | _, _, .trans _ _ _ hxy hyz => .trans _ _ _ (eqvGen_mono h hxy) (eqvGen_mono h hyz)
  | _, _, .rel _ _ hab => .rel _ _ (h hab)

lemma reflGen_le_eqvGen : Subrelation (ReflGen r) (EqvGen r)
  |  _, _, .refl => .refl _
  |  _, _, .single h => .rel _ _ h

lemma symmGen_le_eqvGen : Subrelation (SymmGen r) (EqvGen r)
  | _, _, .inl h => .rel _ _ h
  | _, _, .inr h => _root_.symm <| .rel _ _ h

lemma transGen_le_eqvGen : Subrelation (TransGen r) (EqvGen r) := by
  intro _ _ h
  induction h using TransGen.trans_induction_on with
  | trans _ _ h1 h2 => exact _root_.trans h1 h2
  | single h => exact .rel _ _ h

lemma reflTransGen_le_eqvGen : Subrelation (ReflTransGen r) (EqvGen r) := by
  intro _ _ h
  induction h using ReflTransGen.trans_induction_on with
  | refl => exact .refl _
  | trans _ _ h1 h2 => exact _root_.trans h1 h2
  | single h => exact .rel _ _ h

@[simp, grind =]
lemma eqvGen_reflGen : EqvGen (ReflGen r) = EqvGen r :=
  Subrelation.antisymm
    (eqvGen_le (reflGen_le_eqvGen _)) (eqvGen_mono (.single))

@[simp, grind =]
lemma eqvGen_transGen : EqvGen (TransGen r) = EqvGen r :=
  Subrelation.antisymm
    (eqvGen_le (transGen_le_eqvGen _)) (eqvGen_mono .single)

@[simp, grind =]
lemma eqvGen_symmGen : EqvGen (SymmGen r) = EqvGen r :=
  Subrelation.antisymm
    (eqvGen_le (symmGen_le_eqvGen _)) (eqvGen_mono .inl)

@[simp, grind =]
lemma eqvGen_reflTransGen : EqvGen (ReflTransGen r) = EqvGen r :=
  Subrelation.antisymm
    (eqvGen_le (reflTransGen_le_eqvGen _)) (eqvGen_mono .single)

@[grind =]
lemma eqvGen_eq_reflTransGen [Std.Symm r] : EqvGen r = ReflTransGen r :=
  have : IsEquiv α (ReflTransGen r) := ⟨⟩
  Subrelation.antisymm (eqvGen_le .single) (reflTransGen_le_eqvGen _)

lemma reflTransGen_symmGen : ReflTransGen (SymmGen r) = EqvGen r := by
  rw [← eqvGen_eq_reflTransGen, eqvGen_symmGen]

end EqvGen

/-- 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

section Join

open ReflTransGen ReflGen

/-- 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⟩

theorem le_join_of_refl [Std.Refl r] : r ≤ Join r :=
  fun _ b hab ↦ ⟨b, hab, refl b⟩

@[deprecated (since := "2026-06-30")] alias join_of_single := le_join_of_refl

protected instance Join.symm : Std.Symm (Join r) where
  symm _ _ := fun ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩

@[deprecated (since := "2026-06-10")] alias symmetric_join := Join.symm

protected instance Join.refl [Std.Refl r] : Std.Refl (Join r) where
  refl a := ⟨a, _root_.refl a, _root_.refl a⟩

@[deprecated (since := "2026-06-10")] alias reflexive_join := Join.refl

theorem isTrans_join [IsTrans α r] (h : ∀ a b c, r a b → r a c → Join r b c) :
    IsTrans α (Join r) := by
  grind [isTrans_def, Join]

@[deprecated (since := "2026-02-21")] alias transitive_join := isTrans_join

theorem equivalence_join [IsPreorder α r] (h : ∀ a b c, r a b → r a c → Join r b c) :
    Equivalence (Join r) :=
  ⟨Join.refl.refl, Join.symm.symm _ _, isTrans_join h |>.trans _ _ _⟩

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 fun _ _ _ ↦ church_rosser h

theorem join_le_of_equivalence_of_le {r' : α → α → Prop} (hr : Equivalence r) (h : r' ≤ r) :
    Join r' ≤ r :=
  fun a b ⟨c, hac, hbc⟩ ↦ hr.trans (h a c hac) (hr.symm <| h b c hbc)

@[deprecated (since := "2026-06-30")] alias join_of_equivalence := join_le_of_equivalence_of_le

theorem reflTransGen_le_of_le {r' : α → α → Prop} [Std.Refl r] [IsTrans α r]
    (h : r' ≤ r) : ReflTransGen r' ≤ r := by
  simpa [reflTransGen_eq_self] using ReflTransGen.mono h

@[deprecated (since := "2026-06-30")]
alias reflTransGen_of_isTrans_reflexive := reflTransGen_le_of_le

@[deprecated (since := "2026-02-21")]
alias reflTransGen_of_transitive_reflexive := reflTransGen_le_of_le

@[deprecated (since := "2025-12-17")] alias reflTransGen_minimal := reflTransGen_le_of_le

theorem reflTransGen_le_of_equivalence_of_le {r' : α → α → Prop} (hr : Equivalence r) :
    r' ≤ r → ReflTransGen r' ≤ r :=
  @reflTransGen_le_of_le _ _ _ hr.stdRefl hr.isTrans

@[deprecated (since := "2026-06-30")]
alias reflTransGen_of_equivalence := reflTransGen_le_of_equivalence_of_le

end Join

end Relation

section EqvGen

open Relation

variable {r : α → α → Prop} {a b : α}

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)

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

theorem Equivalence.eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=
  ⟨by intro h; induction h <;> grind [Equivalence], .rel a b⟩

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

end EqvGen