MATHLIBANNEX / EXACT SOURCE

Mathlib/Logic/Relation.lean

Mathlib · fixed commit 360da6fa66c1273b76b6b2d8c5666fd5ac2e3b56

Fixed original declaration · Raw UTF-8 source · Back to the referring Card

Technical identity

33808 bytes · SHA-256 0747f9f7b69c986ecb393711d51b0af9980875a85ca8fbc2bbaf6c7d9767ba65

1/-2Copyright (c) 2018 Johannes Hölzl. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Johannes Hölzl5-/6module78public import Mathlib.Logic.Relator9public import Mathlib.Tactic.Use10public import Mathlib.Tactic.MkIffOfInductiveProp11public import Mathlib.Tactic.SimpRw12public import Mathlib.Order.Defs.Unbundled13public import Batteries.Logic14public import Batteries.Tactic.Trans1516/-!17# Relation closures1819This file defines the reflexive, symmetric, transitive, reflexive transitive and equivalence20closures of relations and proves some basic results on them.2122Note that this is about unbundled relations, that is terms of types of the form `α → β → Prop`. For23the bundled version, see `Rel`.2425## Definitions2627* `Relation.ReflGen`: Reflexive closure. `ReflGen r` relates everything `r` related, plus for all28  `a` it relates `a` with itself. So `ReflGen r a b ↔ r a b ∨ a = b`.29* `Relation.SymmGen`: Symmetric closure. This is also the comparability relation,30  such that `SymmGen r a b` means that either `r a b` or `r b a` (see `Mathlib.Order.Comparable`)31* `Relation.TransGen`: Transitive closure. `TransGen r` relates everything `r` related32  transitively. So `TransGen r a b ↔ ∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b`.33* `Relation.ReflTransGen`: Reflexive transitive closure. `ReflTransGen r` relates everything34  `r` related transitively, plus for all `a` it relates `a` with itself. So35  `ReflTransGen r a b ↔ (∃ x₀ ... xₙ, r a x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ b) ∨ a = b`. It is the same as36  the reflexive closure of the transitive closure, or the transitive closure of the reflexive37  closure. In terms of rewriting systems, this means that `a` can be rewritten to `b` in a number of38  rewrites.39* `Relation.EqvGen`: Equivalence closure. `EqvGen r` relates everything `ReflTransGen r` relates,40  plus for all related pairs it relates them in the opposite order.41* `Relation.Comp`:  Relation composition. We provide notation `∘r`. For `r : α → β → Prop` and42  `s : β → γ → Prop`, `r ∘r s` relates `a : α` and `c : γ` iff there exists `b : β` that's related43  to both.44* `Relation.Map`: Image of a relation under a pair of maps. For `r : α → β → Prop`, `f : α → γ`,45  `g : β → δ`, `Map r f g` is the relation `γ → δ → Prop` relating `f a` and `g b` for all `a`, `b`46  related by `r`.47* `Relation.Join`: Join of a relation. For `r : α → α → Prop`, `Join r a b ↔ ∃ c, r a c ∧ r b c`. In48  terms of rewriting systems, this means that `a` and `b` can be rewritten to the same term.49-/5051@[expose] public section525354open Function5556variable {α β γ δ ε ζ : Sort*}5758section NeImp5960variable {r : α → α → Prop}6162@[deprecated (since := "2026-03-27")] alias Std.Refl.reflexive := refl6364@[deprecated (since := "2026-01-09")] alias IsRefl.reflexive := refl6566/-- To show a reflexive relation `r : α → α → Prop` holds over `x y : α`,67it suffices to show it holds when `x ≠ y`. -/68theorem Std.Refl.rel_of_ne_imp [Std.Refl r] {x y : α} (hr : x ≠ y → r x y) : r x y := by69  grind [Std.Refl]7071@[deprecated (since := "2026-03-27")] alias Reflexive.rel_of_ne_imp := Std.Refl.rel_of_ne_imp7273/-- If a reflexive relation `r : α → α → Prop` holds over `x y : α`,74then it holds whether or not `x ≠ y`. -/75theorem Std.Refl.ne_imp_iff [Std.Refl r] {x y : α} : x ≠ y → r x y ↔ r x y :=76  ⟨Std.Refl.rel_of_ne_imp, fun hr _ ↦ hr⟩7778@[deprecated (since := "2026-03-27")] alias Reflexive.ne_imp_iff := Std.Refl.ne_imp_iff7980@[deprecated (since := "2026-03-27")] alias reflexive_ne_imp_iff := Std.Refl.ne_imp_iff8182theorem refl_iff_subrelation_eq : Std.Refl r ↔ Subrelation Eq r := by83  grind [Std.Refl, Subrelation]8485@[deprecated (since := "2026-03-27")] alias reflexive_iff_subrelation_eq := refl_iff_subrelation_eq8687theorem irrefl_iff_subrelation_ne : Std.Irrefl r ↔ Subrelation r Ne := by88  grind [Std.Irrefl, Subrelation]8990@[deprecated (since := "2026-02-12")]91alias irreflexive_iff_subrelation_ne := irrefl_iff_subrelation_ne9293protected theorem Std.Symm.iff [Std.Symm r] (x y : α) : r x y ↔ r y x :=94  ⟨symm_of r, symm_of r⟩9596@[deprecated (since := "2026-06-10")] protected alias Symmetric.iff := Std.Symm.iff9798theorem Std.Symm.flip_eq [Std.Symm r] : flip r = r :=99  funext₂ fun _ _ ↦ propext <| Std.Symm.iff (r := r) ..100101@[deprecated (since := "2026-06-10")] alias Symmetric.flip_eq := Std.Symm.flip_eq102103theorem Std.Symm.swap_eq [Std.Symm r] : swap r = r :=104  Std.Symm.flip_eq105106@[deprecated (since := "2026-06-10")] alias Symmetric.swap_eq := Std.Symm.swap_eq107108theorem flip_eq_iff : flip r = r ↔ Std.Symm r :=109  ⟨fun h ↦ ⟨fun _ _ ↦ congr_fun₂ h .. |>.mp⟩, fun _ ↦ Std.Symm.flip_eq⟩110111theorem swap_eq_iff : swap r = r ↔ Std.Symm r :=112  flip_eq_iff113114end NeImp115116section Comap117118variable {r : β → β → Prop}119120instance Std.Refl.comap [Std.Refl r] (f : α → β) : Std.Refl (r on f) where121  refl a := refl <| f a122123@[deprecated (since := "2026-03-27")] alias Reflexive.comap := Std.Refl.comap124125instance Std.Symm.comap [Std.Symm r] (f : α → β) : Std.Symm (r on f) where126  symm _ _ hab := symm_of r hab127128@[deprecated (since := "2026-06-10")] alias Symmetric.comap := Std.Symm.comap129130instance IsTrans.comap [IsTrans β r] (f : α → β) : IsTrans α (r on f) where131  trans _ _ _ := trans_of r132133@[deprecated (since := "2026-02-21")] alias Transitive.comap := IsTrans.comap134135instance IsEquiv.comap [IsEquiv β r] (f : α → β) : IsEquiv α (r on f) where136137theorem Equivalence.comap (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=138  ⟨fun a ↦ h.refl (f a), h.symm, h.trans⟩139140end Comap141142namespace Relation143144section Comp145146variable {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop}147148/-- The composition of two relations, yielding a new relation.  The result149relates a term of `α` and a term of `γ` if there is an intermediate150term of `β` related to both.151-/152def Comp (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : Prop :=153  ∃ b, r a b ∧ p b c154155@[inherit_doc]156local infixr:80 " ∘r " => Relation.Comp157158@[simp]159theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by160  ext x y161  simp [Comp]162163@[simp]164theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..165166@[simp]167theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) := by168  ext x y169  simp [Comp]170171@[simp]172theorem eq_comp : (· = ·) ∘r r = r := fun_eq_comp ..173174@[simp]175theorem iff_comp {r : Prop → α → Prop} : (· ↔ ·) ∘r r = r := by176  grind [eq_comp]177178@[simp]179theorem comp_iff {r : α → Prop → Prop} : r ∘r (· ↔ ·) = r := by180  grind [comp_eq]181182theorem comp_assoc : (r ∘r p) ∘r q = r ∘r p ∘r q := by183  funext a d184  apply propext185  constructor186  · exact fun ⟨c, ⟨b, hab, hbc⟩, hcd⟩ ↦ ⟨b, hab, c, hbc, hcd⟩187  · exact fun ⟨b, hab, c, hbc, hcd⟩ ↦ ⟨c, ⟨b, hab, hbc⟩, hcd⟩188189theorem flip_comp : flip (r ∘r p) = flip p ∘r flip r := by190  funext c a191  apply propext192  constructor193  · exact fun ⟨b, hab, hbc⟩ ↦ ⟨b, hbc, hab⟩194  · exact fun ⟨b, hbc, hab⟩ ↦ ⟨b, hab, hbc⟩195196end Comp197198section Fibration199200variable (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)201202/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all203  `a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image204  of some `a' : α` under `f`, and `a'` and `a` are related by `rα`. -/205def Fibration :=206  ∀ ⦃a b⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b207208variable {rα rβ}209210/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is211  accessible under `rα`, then `f a` is accessible under `rβ`. -/212theorem _root_.Acc.of_fibration (fib : Fibration rα rβ f) {a} (ha : Acc rα a) : Acc rβ (f a) := by213  induction ha with | intro a _ ih => ?_214  refine Acc.intro (f a) fun b hr ↦ ?_215  obtain ⟨a', hr', rfl⟩ := fib hr216  exact ih a' hr'217218theorem _root_.Acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b) (a : α)219    (ha : Acc (InvImage rβ f) a) : Acc rβ (f a) :=220  ha.of_fibration f fun a _ h ↦221    let ⟨a', he⟩ := dc h222    ⟨a', by simp_all [InvImage], he⟩223224end Fibration225226section Map227variable {r : α → β → Prop} {f : α → γ} {g : β → δ} {c : γ} {d : δ}228229/-- The map of a relation `r` through a pair of functions pushes the230relation to the codomains of the functions.  The resulting relation is231defined by having pairs of terms related if they have preimages232related by `r`.233-/234protected def Map (r : α → β → Prop) (f : α → γ) (g : β → δ) : γ → δ → Prop := fun c d ↦235  ∃ a b, r a b ∧ f a = c ∧ g b = d236237lemma map_apply : Relation.Map r f g c d ↔ ∃ a b, r a b ∧ f a = c ∧ g b = d := Iff.rfl238239@[simp] lemma map_map (r : α → β → Prop) (f₁ : α → γ) (g₁ : β → δ) (f₂ : γ → ε) (g₂ : δ → ζ) :240    Relation.Map (Relation.Map r f₁ g₁) f₂ g₂ = Relation.Map r (f₂ ∘ f₁) (g₂ ∘ g₁) := by241  grind [Relation.Map]242243@[simp]244lemma map_apply_apply (hf : Injective f) (hg : Injective g) (r : α → β → Prop) (a : α) (b : β) :245    Relation.Map r f g (f a) (g b) ↔ r a b := by simp [Relation.Map, hf.eq_iff, hg.eq_iff]246247@[simp] lemma map_id_id (r : α → β → Prop) : Relation.Map r id id = r := by ext; simp [Relation.Map]248249instance [Decidable (∃ a b, r a b ∧ f a = c ∧ g b = d)] : Decidable (Relation.Map r f g c d) :=250  ‹Decidable _›251252lemma _root_.Std.Refl.map {r : α → α → Prop} [Std.Refl r] {f : α → β} (hf : f.Surjective) :253    Std.Refl (Relation.Map r f f) where254  refl x := by255    obtain ⟨y, rfl⟩ := hf x256    exact ⟨y, y, refl y, rfl, rfl⟩257258@[deprecated (since := "2026-03-27")] alias map_reflexive := Std.Refl.map259260instance _root_.Std.Symm.map {r : α → α → Prop} [Std.Symm r] (f : α → β) :261    Std.Symm (Relation.Map r f f) where262  symm _ _ := by263    rintro ⟨x, y, hxy, rfl, rfl⟩264    exact ⟨y, x, symm hxy, rfl, rfl⟩265266@[deprecated (since := "2026-06-10")] alias map_symmetric := Std.Symm.map267268lemma _root_.IsTrans.map {r : α → α → Prop} [IsTrans α r] {f : α → β}269    (hf : ∀ x y, f x = f y → r x y) : IsTrans β (Relation.Map r f f) := by270  refine ⟨fun _ _ _ ⟨x, y, hxy, hx, hy⟩ ⟨y', z, hyz, hy', hz⟩ ↦ ?_⟩271  exact ⟨x, z, trans_of r hxy <| trans_of r (hf y y' <| hy' ▸ hy) hyz, hx, hz⟩272273@[deprecated (since := "2026-03-27")] alias isTrans_map := IsTrans.map274275@[deprecated (since := "2026-02-21")] alias map_transitive := isTrans_map276277lemma map_equivalence {r : α → α → Prop} (hr : Equivalence r) (f : α → β) (hf : f.Surjective)278    (hf_ker : ∀ x y, f x = f y → r x y) : Equivalence (Relation.Map r f f) where279  refl := hr.stdRefl.map hf |>.refl280  symm := @(hr.stdSymm.map f |>.symm)281  trans := @(hr.isTrans.map hf_ker |>.trans)282283-- TODO: state this using `≤`, after adjusting imports.284lemma map_mono {r s : α → β → Prop} {f : α → γ} {g : β → δ} (h : ∀ x y, r x y → s x y) :285    ∀ x y, Relation.Map r f g x y → Relation.Map s f g x y :=286  fun _ _ ⟨x, y, hxy, hx, hy⟩ => ⟨x, y, h _ _ hxy, hx, hy⟩287288lemma le_onFun_map {r : α → α → Prop} (f : α → β) : Subrelation r (Relation.Map r f f on f) := by289  intro290  grind [Relation.Map]291292lemma onFun_map_eq_of_injective {r : α → α → Prop} {f : α → β} (hinj : f.Injective) :293    (Relation.Map r f f on f) = r := by294  ext x y295  exact ⟨fun ⟨x', y', hr, hx, hy⟩ ↦ hinj hx ▸ hinj hy ▸ hr, fun h ↦ ⟨x, y, h, rfl, rfl⟩⟩296297lemma map_onFun_le {r : β → β → Prop} (f : α → β) : Subrelation (Relation.Map (r on f) f f) r := by298  intro299  grind [Relation.Map]300301lemma map_onFun_eq_of_surjective {r : β → β → Prop} {f : α → β} (hsurj : f.Surjective) :302    Relation.Map (r on f) f f = r := by303  ext x y304  have _ := hsurj x305  have _ := hsurj y306  grind [Relation.Map]307308lemma map_onFun_map_eq_map {r : α → α → Prop} (f : α → β) :309    Relation.Map (Relation.Map r f f on f) f f = Relation.Map r f f := by310  grind [Relation.Map]311312lemma onFun_map_onFun_eq_onFun {r : β → β → Prop} (f : α → β) :313    (Relation.Map (r on f) f f on f) = (r on f) := by314  grind [Relation.Map]315316lemma onFun_map_onFun_iff_onFun {r : β → β → Prop} (f : α → β) (a₁ a₂ : α) :317    Relation.Map (r on f) f f (f a₁) (f a₂) ↔ r (f a₁) (f a₂) := by318  grind [Relation.Map]319320end Map321322variable {r : α → α → Prop} {a b c : α}323324/-- `ReflTransGen r`: reflexive transitive closure of `r` -/325@[mk_iff ReflTransGen.cases_tail_iff, grind]326inductive ReflTransGen (r : α → α → Prop) (a : α) : α → Prop327  | refl : ReflTransGen r a a328  | tail {b c : α} : ReflTransGen r a b → r b c → ReflTransGen r a c329330attribute [refl] ReflTransGen.refl331332/-- `ReflGen r`: reflexive closure of `r` -/333@[mk_iff, grind]334inductive ReflGen (r : α → α → Prop) (a : α) : α → Prop335  | refl : ReflGen r a a336  | single {b : α} : r a b → ReflGen r a b337338attribute [refl] ReflGen.refl339attribute [grind =] reflGen_iff340341/-- `SymmGen r`: symmetric closure of `r`. This is also the comparability relation, such342  that `SymmGen r a b` means that either `r a b` or `r b a` (see `Mathlib.Order.Comparable`). -/343def SymmGen (r : α → α → Prop) (a b : α) : Prop :=344  r a b ∨ r b a345346variable (r) in347/-- `EqvGen r`: equivalence closure of `r`. -/348@[mk_iff]349inductive EqvGen : α → α → Prop350  | rel x y : r x y → EqvGen x y351  | refl x : EqvGen x x352  | symm x y : EqvGen x y → EqvGen y x353  | trans x y z : EqvGen x y → EqvGen y z → EqvGen x z354355attribute [mk_iff] TransGen356attribute [grind] TransGen357358namespace ReflGen359360theorem to_reflTransGen : ∀ {a b}, ReflGen r a b → ReflTransGen r a b361  | a, _, refl => by rfl362  | _, _, single h => ReflTransGen.tail ReflTransGen.refl h363364theorem mono {p : α → α → Prop} (hp : ∀ a b, r a b → p a b) : ∀ {a b}, ReflGen r a b → ReflGen p a b365  | a, _, ReflGen.refl => by rfl366  | a, b, single h => single (hp a b h)367368instance : Std.Refl (ReflGen r) :=369  ⟨@refl α r⟩370371instance stdSymm [Std.Symm r] : Std.Symm (ReflGen r) where372  symm _ _373    | refl => refl374    | single h => single <| symm h375376@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm377378instance [IsTrans α r] : IsTrans α (ReflGen r) where379  trans a b c h₁ h₂ := by380    obtain (rfl | h₂) := h₂381    · exact h₁382    obtain (rfl | h₁) := h₁383    · exact single h₂384    exact single (trans_of r h₁ h₂)385386end ReflGen387388namespace SymmGen389390theorem of_rel (h : r a b) : SymmGen r a b :=391  Or.inl h392393theorem of_rel_symm (h : r b a) : SymmGen r a b :=394  Or.inr h395396theorem swap (h : SymmGen r b a) : SymmGen (swap r) a b := by397  induction h with398  | inl hba => exact of_rel hba399  | inr hab => exact of_rel_symm hab400401@[simp, refl]402theorem refl (r : α → α → Prop) [Std.Refl r] (a : α) : SymmGen r a a :=403  .of_rel (_root_.refl _)404405theorem rfl [Std.Refl r] : SymmGen r a a := .refl ..406407instance [Std.Refl r] : Std.Refl (SymmGen r) where408  refl := .refl r409410@[symm]411theorem symm : SymmGen r a b → SymmGen r b a :=412  Or.symm413414instance : Std.Symm (SymmGen r) where415  symm _ _ := SymmGen.symm416417instance decidableRel [DecidableRel r] : DecidableRel (SymmGen r) :=418  fun _ _ ↦ inferInstanceAs (Decidable (_ ∨ _))419420theorem of_le {α : Type*} [LE α] {a b : α} (h : a ≤ b) : SymmGen (· ≤ ·) a b := .of_rel h421theorem of_ge {α : Type*} [LE α] {a b : α} (h : b ≤ a) : SymmGen (· ≤ ·) a b := .of_rel_symm h422423alias _root_.LE.le.symmGen := SymmGen.of_le424alias _root_.LE.le.symmGen_symm := SymmGen.of_ge425426end SymmGen427428namespace ReflTransGen429430@[trans]431theorem trans (hab : ReflTransGen r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by432  induction hbc with433  | refl => assumption434  | tail _ hcd hac => exact hac.tail hcd435436theorem single (hab : r a b) : ReflTransGen r a b :=437  refl.tail hab438439theorem head (hab : r a b) (hbc : ReflTransGen r b c) : ReflTransGen r a c := by440  induction hbc with441  | refl => exact refl.tail hab442  | tail _ hcd hac => exact hac.tail hcd443444instance stdSymm [Std.Symm r] : Std.Symm (ReflTransGen r) where445  symm x y h := by446    induction h with447    | refl => rfl448    | tail _ b c => apply c.head <| symm b449450@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm451452theorem cases_tail : ReflTransGen r a b → b = a ∨ ∃ c, ReflTransGen r a c ∧ r c b :=453  (cases_tail_iff r a b).1454455@[elab_as_elim]456theorem head_induction_on {motive : ∀ a : α, ReflTransGen r a b → Prop} {a : α}457    (h : ReflTransGen r a b) (refl : motive b refl)458    (head : ∀ {a c} (h' : r a c) (h : ReflTransGen r c b), motive c h → motive a (h.head h')) :459    motive a h := by460  induction h with461  | refl => exact refl462  | @tail b c _ hbc ih =>463  apply ih464  · exact head hbc _ refl465  · exact fun h1 h2 ↦ head h1 (h2.tail hbc)466467@[elab_as_elim]468theorem trans_induction_on {motive : ∀ {a b : α}, ReflTransGen r a b → Prop} {a b : α}469    (h : ReflTransGen r a b) (refl : ∀ a, @motive a a refl)470    (single : ∀ {a b} (h : r a b), motive (single h))471    (trans : ∀ {a b c} (h₁ : ReflTransGen r a b) (h₂ : ReflTransGen r b c), motive h₁ → motive h₂ →472      motive (h₁.trans h₂)) : motive h := by473  induction h with474  | refl => exact refl a475  | tail hab hbc ih => exact trans hab (.single hbc) ih (single hbc)476477theorem cases_head (h : ReflTransGen r a b) : a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by478  induction h using Relation.ReflTransGen.head_induction_on <;> grind479480theorem cases_head_iff : ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b := by481  use cases_head482  rintro (rfl | ⟨c, hac, hcb⟩)483  · rfl484  · exact head hac hcb485486theorem total_of_right_unique (U : Relator.RightUnique r) (ab : ReflTransGen r a b)487    (ac : ReflTransGen r a c) : ReflTransGen r b c ∨ ReflTransGen r c b := by488  induction ab with489  | refl => exact Or.inl ac490  | tail _ bd IH =>491    rcases IH with (IH | IH)492    · rcases cases_head IH with (rfl | ⟨e, be, ec⟩)493      · exact Or.inr (single bd)494      · cases U bd be495        exact Or.inl ec496    · exact Or.inr (IH.tail bd)497498end ReflTransGen499500namespace TransGen501502theorem to_reflTransGen {a b} (h : TransGen r a b) : ReflTransGen r a b := by503  induction h with504  | single h => exact ReflTransGen.single h505  | tail _ bc ab => exact ReflTransGen.tail ab bc506507theorem trans_left (hab : TransGen r a b) (hbc : ReflTransGen r b c) : TransGen r a c := by508  induction hbc with509  | refl => assumption510  | tail _ hcd hac => exact hac.tail hcd511512attribute [trans] trans513514theorem head' (hab : r a b) (hbc : ReflTransGen r b c) : TransGen r a c :=515  trans_left (single hab) hbc516517theorem tail' (hab : ReflTransGen r a b) (hbc : r b c) : TransGen r a c := by518  induction hab generalizing c with519  | refl => exact single hbc520  | tail _ hdb IH => exact tail (IH hdb) hbc521522theorem head (hab : r a b) (hbc : TransGen r b c) : TransGen r a c :=523  head' hab hbc.to_reflTransGen524525@[elab_as_elim]526theorem head_induction_on {motive : ∀ a : α, TransGen r a b → Prop} {a : α} (h : TransGen r a b)527    (single : ∀ {a} (h : r a b), motive a (single h))528    (head : ∀ {a c} (h' : r a c) (h : TransGen r c b), motive c h → motive a (h.head h')) :529    motive a h := by530  induction h with531  | single h => exact single h532  | @tail b c _ hbc h_ih =>533  apply h_ih534  · exact fun h ↦ head h (.single hbc) (single hbc)535  · exact fun hab hbc ↦ head hab _536537@[elab_as_elim]538theorem trans_induction_on {motive : ∀ {a b : α}, TransGen r a b → Prop} {a b : α}539    (h : TransGen r a b) (single : ∀ {a b} (h : r a b), motive (single h))540    (trans : ∀ {a b c} (h₁ : TransGen r a b) (h₂ : TransGen r b c), motive h₁ → motive h₂ →541      motive (h₁.trans h₂)) :542    motive h := by543  induction h with544  | single h => exact single h545  | tail hab hbc h_ih => exact trans hab (.single hbc) h_ih (single hbc)546547theorem trans_right (hab : ReflTransGen r a b) (hbc : TransGen r b c) : TransGen r a c := by548  induction hbc with549  | single hbc => exact tail' hab hbc550  | tail _ hcd hac => exact hac.tail hcd551552theorem tail'_iff : TransGen r a c ↔ ∃ b, ReflTransGen r a b ∧ r b c := by553  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ tail' hab hbc⟩554  cases h with555  | single hac => exact ⟨_, by rfl, hac⟩556  | tail hab hbc => exact ⟨_, hab.to_reflTransGen, hbc⟩557558theorem head'_iff : TransGen r a c ↔ ∃ b, r a b ∧ ReflTransGen r b c := by559  refine ⟨fun h ↦ ?_, fun ⟨b, hab, hbc⟩ ↦ head' hab hbc⟩560  induction h with561  | single hac => exact ⟨_, hac, by rfl⟩562  | tail _ hbc IH =>563  rcases IH with ⟨d, had, hdb⟩564  exact ⟨_, had, hdb.tail hbc⟩565566instance stdSymm [Std.Symm r] : Std.Symm (TransGen r) where567  symm x y h := by568    induction h with569    | single i => exact .single <| symm i570    | tail _ h₁ h₂ => exact .head (symm h₁) h₂571572@[deprecated (since := "2026-06-10")] alias symmetric := stdSymm573574instance [Std.Refl r] : Std.Refl (TransGen r) where575  refl x := .single (refl x)576577end TransGen578579section reflGen580581@[grind =]582lemma reflGen_eq_self [Std.Refl r] : ReflGen r = r := by583  ext x y584  simpa only [reflGen_iff, or_iff_right_iff_imp] using fun h ↦ h ▸ refl y585586@[deprecated inferInstance (since := "2026-03-27")]587lemma reflexive_reflGen : Std.Refl (ReflGen r) := inferInstance588589lemma reflGen_minimal {r' : α → α → Prop} [Std.Refl r'] (h : ∀ x y, r x y → r' x y) {x y : α}590    (hxy : ReflGen r x y) : r' x y := by591  simpa [reflGen_eq_self] using ReflGen.mono h hxy592593end reflGen594595section SymmGen596597theorem symmGen_swap (r : α → α → Prop) : SymmGen (swap r) = SymmGen r :=598  funext₂ fun _ _ ↦ propext or_comm599600theorem symmGen_swap_apply (r : α → α → Prop) : SymmGen (swap r) a b ↔ SymmGen r a b :=601  or_comm602603theorem symmGen_comm {a b : α} : SymmGen r a b ↔ SymmGen r b a :=604  or_comm605606@[simp]607theorem symmGen_of_total [Std.Total r] (a b : α) : SymmGen r a b :=608  Std.Total.total a b609610end SymmGen611612section TransGen613614instance : IsTrans α (TransGen r) :=615  ⟨@TransGen.trans α r⟩616617instance : Trans (TransGen r) r (TransGen r) :=618  ⟨TransGen.tail⟩619620instance : Trans r (TransGen r) (TransGen r) :=621  ⟨TransGen.head⟩622623instance : Trans (TransGen r) (ReflTransGen r) (TransGen r) :=624  ⟨TransGen.trans_left⟩625626instance : Trans (ReflTransGen r) (TransGen r) (TransGen r) :=627  ⟨TransGen.trans_right⟩628629@[grind =]630theorem transGen_eq_self [IsTrans α r] : TransGen r = r :=631  funext₂ fun a b ↦ propext <|632    ⟨fun h ↦ by633      induction h with634      | single hc => exact hc635      | tail _ hcd hac => exact IsTrans.trans _ _ _ hac hcd, TransGen.single⟩636637@[deprecated inferInstance (since := "2026-02-21")]638theorem transitive_transGen : IsTrans α (TransGen r) := inferInstance639640@[deprecated transGen_eq_self (since := "2026-03-27"), grind =]641theorem transGen_idem : TransGen (TransGen r) = TransGen r :=642  transGen_eq_self643644theorem TransGen.lift {p : β → β → Prop} {a b : α} (f : α → β) (h : ∀ a b, r a b → p (f a) (f b))645    (hab : TransGen r a b) : TransGen p (f a) (f b) := by646  induction hab with647  | single hac => exact TransGen.single (h a _ hac)648  | tail _ hcd hac => exact TransGen.tail hac (h _ _ hcd)649650theorem TransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)651    (h : ∀ a b, r a b → TransGen p (f a) (f b)) (hab : TransGen r a b) :652    TransGen p (f a) (f b) := by653  simpa [transGen_eq_self] using hab.lift f h654655theorem TransGen.closed {p : α → α → Prop} :656    (∀ a b, r a b → TransGen p a b) → TransGen r a b → TransGen p a b :=657  TransGen.lift' id658659lemma TransGen.closed' {P : α → Prop} (dc : ∀ {a b}, r a b → P b → P a)660    {a b : α} (h : TransGen r a b) : P b → P a :=661  h.head_induction_on dc fun hr _ hi ↦ dc hr ∘ hi662663theorem TransGen.mono {p : α → α → Prop} :664    (∀ a b, r a b → p a b) → TransGen r a b → TransGen p a b :=665  TransGen.lift id666667lemma transGen_minimal {r' : α → α → Prop} [IsTrans α r'] (h : ∀ x y, r x y → r' x y) {x y : α}668    (hxy : TransGen r x y) : r' x y := by669  simpa [transGen_eq_self] using TransGen.mono h hxy670671theorem TransGen.swap (h : TransGen r b a) : TransGen (swap r) a b := by672  induction h with673  | single h => exact TransGen.single h674  | tail _ hbc ih => exact ih.head hbc675676theorem transGen_swap : TransGen (swap r) a b ↔ TransGen r b a :=677  ⟨TransGen.swap, TransGen.swap⟩678679end TransGen680681section ReflTransGen682683open ReflTransGen684685@[grind =]686theorem reflTransGen_iff_eq (h : ∀ b, ¬r a b) : ReflTransGen r a b ↔ b = a := by687  rw [cases_head_iff]; simp [h, eq_comm]688689@[grind =]690theorem reflTransGen_iff_eq_or_transGen : ReflTransGen r a b ↔ b = a ∨ TransGen r a b := by691  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩692  · cases h with693    | refl => exact Or.inl rfl694    | tail hac hcb => exact Or.inr (TransGen.tail' hac hcb)695  · rcases h with (rfl | h)696    · rfl697    · exact h.to_reflTransGen698699theorem ReflTransGen.lift {p : β → β → Prop} {a b : α} (f : α → β)700    (h : ∀ a b, r a b → p (f a) (f b)) (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) :=701  ReflTransGen.trans_induction_on hab (fun _ ↦ refl) (ReflTransGen.single ∘ h _ _) fun _ _ ↦ trans702703theorem ReflTransGen.mono {p : α → α → Prop} : (∀ a b, r a b → p a b) →704    ReflTransGen r a b → ReflTransGen p a b :=705  ReflTransGen.lift id706707@[grind =]708theorem reflTransGen_eq_self [Std.Refl r] [IsTrans α r] : ReflTransGen r = r :=709  funext₂ fun a b ↦ propext710    ⟨fun h ↦ by711      induction h with712      | refl => exact refl a713      | tail _ h₂ IH => exact IsTrans.trans _ _ _ IH h₂, single⟩714715instance : Trans r (ReflTransGen r) (ReflTransGen r) :=716  ⟨head⟩717718instance : Trans (ReflTransGen r) r (ReflTransGen r) :=719  ⟨tail⟩720721instance : Std.Refl (ReflTransGen r) :=722  ⟨@ReflTransGen.refl α r⟩723724@[deprecated inferInstance (since := "2026-03-27")]725theorem reflexive_reflTransGen : Std.Refl (ReflTransGen r) := inferInstance726727instance : IsTrans α (ReflTransGen r) :=728  ⟨@ReflTransGen.trans α r⟩729730@[deprecated inferInstance (since := "2026-02-21")]731theorem transitive_reflTransGen : IsTrans α (ReflTransGen r) := inferInstance732733@[deprecated reflTransGen_eq_self (since := "2026-03-27"), grind =]734theorem reflTransGen_idem : ReflTransGen (ReflTransGen r) = ReflTransGen r :=735  reflTransGen_eq_self736737theorem ReflTransGen.lift' {p : β → β → Prop} {a b : α} (f : α → β)738    (h : ∀ a b, r a b → ReflTransGen p (f a) (f b))739    (hab : ReflTransGen r a b) : ReflTransGen p (f a) (f b) := by740  simpa [reflTransGen_eq_self] using hab.lift f h741742theorem reflTransGen_closed {p : α → α → Prop} :743    (∀ a b, r a b → ReflTransGen p a b) → ReflTransGen r a b → ReflTransGen p a b :=744  ReflTransGen.lift' id745746theorem ReflTransGen.swap (h : ReflTransGen r b a) : ReflTransGen (swap r) a b := by747  induction h with748  | refl => rfl749  | tail _ hbc ih => exact ih.head hbc750751theorem reflTransGen_swap : ReflTransGen (swap r) a b ↔ ReflTransGen r b a :=752  ⟨ReflTransGen.swap, ReflTransGen.swap⟩753754@[simp, grind =] lemma reflGen_transGen : ReflGen (TransGen r) = ReflTransGen r := by755  ext x y756  simp_rw [reflTransGen_iff_eq_or_transGen, reflGen_iff]757758@[simp, grind =] lemma transGen_reflGen : TransGen (ReflGen r) = ReflTransGen r := by759  ext x y760  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩761  · simpa [reflTransGen_eq_self] using (h.mono fun _ _ ↦ ReflGen.to_reflTransGen).to_reflTransGen762  · obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h763    · exact .single .refl764    · exact TransGen.mono (fun _ _ ↦ .single) h765766@[simp, grind =] lemma reflTransGen_reflGen : ReflTransGen (ReflGen r) = ReflTransGen r := by767  simp only [← transGen_reflGen, reflGen_eq_self]768769@[simp, grind =] lemma reflTransGen_transGen : ReflTransGen (TransGen r) = ReflTransGen r := by770  simp only [← reflGen_transGen, transGen_eq_self]771772@[grind =]773lemma reflTransGen_eq_transGen [Std.Refl r] : ReflTransGen r = TransGen r := by774  rw [← transGen_reflGen, reflGen_eq_self]775776@[grind =]777lemma reflTransGen_eq_reflGen [IsTrans α r] : ReflTransGen r = ReflGen r := by778  rw [← reflGen_transGen, transGen_eq_self]779780end ReflTransGen781782namespace EqvGen783784variable (r)785786theorem is_equivalence : Equivalence (@EqvGen α r) :=787  Equivalence.mk EqvGen.refl (EqvGen.symm _ _) (EqvGen.trans _ _ _)788789/-- `EqvGen.setoid r` is the setoid generated by a relation `r`.790791The motivation for this definition is that `Quot r` behaves like `Quotient (EqvGen.setoid r)`,792see for example `Quot.eqvGen_exact` and `Quot.eqvGen_sound`. -/793@[implicit_reducible]794def setoid : Setoid α :=795  Setoid.mk _ (EqvGen.is_equivalence r)796797theorem mono {r p : α → α → Prop} (hrp : ∀ a b, r a b → p a b) (h : EqvGen r a b) :798    EqvGen p a b := by799  induction h with800  | rel a b h => exact EqvGen.rel _ _ (hrp _ _ h)801  | refl => exact EqvGen.refl _802  | symm a b _ ih => exact EqvGen.symm _ _ ih803  | trans a b c _ _ hab hbc => exact EqvGen.trans _ _ _ hab hbc804805end EqvGen806807/-- The join of a relation on a single type is a new relation for which808pairs of terms are related if there is a third term they are both809related to.  For example, if `r` is a relation representing rewrites810in a term rewriting system, then *confluence* is the property that if811`a` rewrites to both `b` and `c`, then `join r` relates `b` and `c`812(see `Relation.church_rosser`).813-/814def Join (r : α → α → Prop) : α → α → Prop := fun a b ↦ ∃ c, r a c ∧ r b c815816section Join817818open ReflTransGen ReflGen819820/-- A sufficient condition for the Church-Rosser property. -/821theorem church_rosser (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d)822    (hab : ReflTransGen r a b) (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c := by823  induction hab with824  | refl => exact ⟨c, hac, refl⟩825  | @tail d e _ hde ih =>826    rcases ih with ⟨b, hdb, hcb⟩827    have : ∃ a, ReflTransGen r e a ∧ ReflGen r b a := by828      clear hcb829      induction hdb with830      | refl => exact ⟨e, refl, ReflGen.single hde⟩831      | @tail f b _ hfb ih =>832        rcases ih with ⟨a, hea, hfa⟩833        cases hfa with834        | refl => exact ⟨b, hea.tail hfb, ReflGen.refl⟩835        | single hfa =>836          rcases h _ _ _ hfb hfa with ⟨c, hbc, hac⟩837          exact ⟨c, hea.trans hac, hbc⟩838    rcases this with ⟨a, hea, hba⟩839    cases hba with840    | refl => exact ⟨b, hea, hcb⟩841    | single hba => exact ⟨a, hea, hcb.tail hba⟩842843844theorem join_of_single [Std.Refl r] (hab : r a b) : Join r a b :=845  ⟨b, hab, refl b⟩846847protected instance Join.symm : Std.Symm (Join r) where848  symm _ _ := fun ⟨c, hac, hcb⟩ ↦ ⟨c, hcb, hac⟩849850@[deprecated (since := "2026-06-10")] alias symmetric_join := Join.symm851852protected instance Join.refl [Std.Refl r] : Std.Refl (Join r) where853  refl a := ⟨a, _root_.refl a, _root_.refl a⟩854855@[deprecated (since := "2026-06-10")] alias reflexive_join := Join.refl856857theorem isTrans_join [IsTrans α r] (h : ∀ a b c, r a b → r a c → Join r b c) :858    IsTrans α (Join r) :=859  ⟨fun _a b _c ⟨x, hax, hbx⟩ ⟨y, hby, hcy⟩ ↦860  let ⟨z, hxz, hyz⟩ := h b x y hbx hby861  ⟨z, trans_of r hax hxz, trans_of r hcy hyz⟩⟩862863@[deprecated (since := "2026-02-21")] alias transitive_join := isTrans_join864865theorem equivalence_join [Std.Refl r] [IsTrans α r] (h : ∀ a b c, r a b → r a c → Join r b c) :866    Equivalence (Join r) :=867  ⟨Join.refl.refl, Join.symm.symm _ _, isTrans_join h |>.trans _ _ _⟩868869theorem equivalence_join_reflTransGen870    (h : ∀ a b c, r a b → r a c → ∃ d, ReflGen r b d ∧ ReflTransGen r c d) :871    Equivalence (Join (ReflTransGen r)) :=872  equivalence_join fun _ _ _ ↦ church_rosser h873874theorem join_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) (h : ∀ a b, r' a b → r a b) :875    Join r' a b → r a b876  | ⟨_, hac, hbc⟩ => hr.trans (h _ _ hac) (hr.symm <| h _ _ hbc)877878theorem reflTransGen_of_isTrans_reflexive {r' : α → α → Prop} [Std.Refl r] [IsTrans α r]879    (h : ∀ a b, r' a b → r a b) (h' : ReflTransGen r' a b) : r a b := by880  simpa [reflTransGen_eq_self] using ReflTransGen.mono h h'881882@[deprecated (since := "2026-02-21")]883alias reflTransGen_of_transitive_reflexive := reflTransGen_of_isTrans_reflexive884885@[deprecated (since := "2025-12-17")] alias reflTransGen_minimal :=886  reflTransGen_of_transitive_reflexive887888theorem reflTransGen_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) :889    (∀ a b, r' a b → r a b) → ReflTransGen r' a b → r a b :=890  @reflTransGen_of_isTrans_reflexive _ _ _ _ _ hr.stdRefl hr.isTrans891892end Join893894end Relation895896section EqvGen897898open Relation899900variable {r : α → α → Prop} {a b : α}901902theorem Quot.eqvGen_exact (H : Quot.mk r a = Quot.mk r b) : EqvGen r a b :=903  @Quotient.exact _ (EqvGen.setoid r) a b (congrArg904    (Quot.lift (Quotient.mk (EqvGen.setoid r)) (fun x y h ↦ Quot.sound (EqvGen.rel x y h))) H)905906theorem Quot.eqvGen_sound (H : EqvGen r a b) : Quot.mk r a = Quot.mk r b :=907  EqvGen.rec908    (fun _ _ h ↦ Quot.sound h)909    (fun _ ↦ rfl)910    (fun _ _ _ IH ↦ Eq.symm IH)911    (fun _ _ _ _ _ IH₁ IH₂ ↦ Eq.trans IH₁ IH₂)912    H913914theorem Equivalence.eqvGen_iff (h : Equivalence r) : EqvGen r a b ↔ r a b :=915  Iff.intro916    (by917      intro h918      induction h with919      | rel => assumption920      | refl => exact h.1 _921      | symm => apply h.symm; assumption922      | trans _ _ _ _ _ hab hbc => exact h.trans hab hbc)923    (EqvGen.rel a b)924925theorem Equivalence.eqvGen_eq (h : Equivalence r) : EqvGen r = r :=926  funext fun _ ↦ funext fun _ ↦ propext <| h.eqvGen_iff927928end EqvGen