Lumenary.EquivalenceRelations

Formal library

• ReflexivedefDefinitionNo axioms

  /-- A relation is **reflexive** if every element is related to itself: `a R a` for all `a`. -/
  def Reflexive {α : Type} (R : α → α → Prop) : Prop := ∀ a, R a a

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• SymmetricdefDefinitionNo axioms

  /-- A relation is **symmetric** if `a R b` always implies `b R a`. -/
  def Symmetric {α : Type} (R : α → α → Prop) : Prop := ∀ a b, R a b → R b a

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• TransitivedefDefinitionNo axioms

  /-- A relation is **transitive** if `a R b` and `b R c` always imply `a R c`. -/
  def Transitive {α : Type} (R : α → α → Prop) : Prop := ∀ a b c, R a b → R b c → R a c

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• equivalence_ifftheoremProved here from basic factsNo axioms

  /-- Core Lean's `Equivalence R` is exactly our definition: reflexive, symmetric and transitive. -/
  theorem equivalence_iff {α : Type} (R : α → α → Prop) :
      Equivalence R ↔ Reflexive R ∧ Symmetric R ∧ Transitive R := by
    constructor
    · intro h
      exact ⟨h.refl, fun _ _ hab => h.symm hab, fun _ _ _ hab hbc => h.trans hab hbc⟩
    · intro ⟨hr, hs, ht⟩
      exact ⟨hr, fun {a b} hab => hs a b hab, fun {a b c} hab hbc => ht a b c hab hbc⟩

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• tableReldefDefinitionpropext, Classical.choice, Quot.sound

  /-- A relation on the three-element set `{0, 1, 2}`, given as a list of ordered pairs:
  `{(0,0), (1,1), (2,2), (0,1), (1,0)}`. `a` is related to `b` when the list contains `(a, b)`. -/
  def tableRel (a b : Fin 3) : Prop :=
    [(0, 0), (1, 1), (2, 2), (0, 1), (1, 0)].contains (a, b) = true

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• table_exampletheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- `tableRel` is an equivalence relation (its classes are `{0, 1}` and `{2}`). Lean checks all
  three properties by running through every case: `3` cases for reflexivity, `9` for symmetry and
  `27` for transitivity. On a finite set, checking every case *is* a proof. -/
  theorem table_example : Reflexive tableRel ∧ Symmetric tableRel ∧ Transitive tableRel := by
    unfold Reflexive Symmetric Transitive tableRel
    decide

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• lt_not_symmetrictheoremProved here from basic factsNo axioms

  /-- "Is less than" is not symmetric. One counterexample suffices: `0 < 1` but not `1 < 0`. -/
  theorem lt_not_symmetric : ¬ Symmetric (fun a b : Int => a < b) := by
    intro h
    have h10 : (1 : Int) < 0 := h 0 1 (by decide)
    exact absurd h10 (by decide)

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• lt_transitivetheoremProved here from basic factspropext, Quot.sound

  /-- "Is less than" is transitive: from `a < b` and `b < c` we get `a < c`. -/
  theorem lt_transitive : Transitive (fun a b : Int => a < b) := by
    intro a b c hab hbc
    omega

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• NeardefDefinitionNo axioms

  /-- "Differ by at most 1": `a` and `b` are *near* if `|a − b| ≤ 1`. -/
  def Near (a b : Int) : Prop := a - b ≤ 1 ∧ b - a ≤ 1

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• near_reflexive_symmetrictheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- "Differ by at most 1" is reflexive and symmetric … -/
  theorem near_reflexive_symmetric : Reflexive Near ∧ Symmetric Near := by
    constructor
    · intro a
      show a - a ≤ 1 ∧ a - a ≤ 1
      omega
    · intro a b ⟨h1, h2⟩
      exact ⟨h2, h1⟩

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• near_not_transitivetheoremProved here from basic factsNo axioms

  /-- … but not transitive: `0` is near `1` and `1` is near `2`, yet `0` is not near `2`.
  So "differ by at most 1" is **not** an equivalence relation. -/
  theorem near_not_transitive : ¬ Transitive Near := by
    intro h
    have h02 : Near 0 2 := h 0 1 2 ⟨by decide, by decide⟩ ⟨by decide, by decide⟩
    exact absurd h02.2 (by decide)

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• symm_trans_not_refltheoremProved here from basic factsNo axioms

  /-- A tempting false "proof": from `a R b`, symmetry gives `b R a`, and transitivity gives `a R a`.
  The flaw is the first step — there may be no `b` with `a R b` at all. Here is a relation on the
  natural numbers that is symmetric and transitive but not reflexive: `a R b` means `a = 0 ∧ b = 0`.
  The number `1` is related to nothing, not even to itself. -/
  theorem symm_trans_not_refl :
      ∃ R : Nat → Nat → Prop, Symmetric R ∧ Transitive R ∧ ¬ Reflexive R := by
    refine ⟨fun a b => a = 0 ∧ b = 0, ?_, ?_, ?_⟩
    · intro a b ⟨ha, hb⟩
      exact ⟨hb, ha⟩
    · intro a b c ⟨ha, _⟩ ⟨_, hc⟩
      exact ⟨ha, hc⟩
    · intro h
      exact absurd (h 1).1 (by decide)

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• refl_of_symm_transtheoremProved here from basic factsNo axioms

  /-- The tempting argument *does* work when every element is related to **something**:
  pick `b` with `a R b`; symmetry gives `b R a`; transitivity gives `a R a`. -/
  theorem refl_of_symm_trans {α : Type} (R : α → α → Prop) (hs : Symmetric R) (ht : Transitive R)
      (hsome : ∀ a, ∃ b, R a b) : Reflexive R := by
    intro a
    obtain ⟨b, hab⟩ := hsome a
    exact ht a b a hab (hs a b hab)

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• clsdefDefinitionNo axioms

  /-- The **equivalence class** of `a`: the set `[a] = {x | x R a}`, represented as a predicate.
  `cls R a x` says "x belongs to the class of a". -/
  def cls {α : Type} (R : α → α → Prop) (a : α) : α → Prop := fun x => R x a

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• mem_cls_selftheoremProved here from basic factsNo axioms

  /-- Every element belongs to its own class (by reflexivity), so classes are never empty. -/
  theorem mem_cls_self {α : Type} {R : α → α → Prop} (h : Equivalence R) (a : α) : cls R a a :=
    h.refl a

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• cls_eq_of_reltheoremProved here from basic factspropext, Quot.sound

  /-- If `a R b` then `[a] = [b]`. If `x R a`, then `x R b` by transitivity; if `x R b`, then
  `b R a` (symmetry) and transitivity give `x R a`. Two sets with the same members are equal
  (`funext` and `propext` express this in Lean). -/
  theorem cls_eq_of_rel {α : Type} {R : α → α → Prop} (h : Equivalence R) {a b : α} (hab : R a b) :
      cls R a = cls R b := by
    funext x
    apply propext
    constructor
    · intro hxa
      exact h.trans hxa hab
    · intro hxb
      exact h.trans hxb (h.symm hab)

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• cls_eq_ifftheoremProved here from basic factspropext, Quot.sound

  /-- `[a] = [b]` exactly when `a R b`. (For "only if": `a ∈ [a] = [b]`, so `a R b`.) -/
  theorem cls_eq_iff {α : Type} {R : α → α → Prop} (h : Equivalence R) (a b : α) :
      cls R a = cls R b ↔ R a b := by
    constructor
    · intro e
      have ha : cls R a a := mem_cls_self h a
      rw [e] at ha
      exact ha
    · exact cls_eq_of_rel h

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• cls_eq_or_disjointtheoremProved here from basic factspropext, Classical.choice, Quot.sound

  /-- **Two equivalence classes are either equal or disjoint.** Either `a R b`, and then
  `[a] = [b]`; or not, and then no `x` can lie in both — otherwise `a R x` (symmetry) and `x R b`
  would give `a R b` (transitivity). The case split uses the law of excluded middle. -/
  theorem cls_eq_or_disjoint {α : Type} {R : α → α → Prop} (h : Equivalence R) (a b : α) :
      cls R a = cls R b ∨ ∀ x, ¬ (cls R a x ∧ cls R b x) := by
    cases Classical.em (R a b) with
    | inl hab => exact Or.inl (cls_eq_of_rel h hab)
    | inr hnot =>
      right
      intro x ⟨hxa, hxb⟩
      exact hnot (h.trans (h.symm hxa) hxb)

  Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• IsPartitionstructureDefinitionNo axioms

  /-- A family `P` of subsets of `α` is a **partition** of `α` if every block is non-empty, every
  element lies in some block, and two blocks that share an element are equal (equivalently:
  different blocks are disjoint). Here a subset is a predicate `B : α → Prop`, and `P B` says
  "`B` is one of the blocks". -/
  structure IsPartition {α : Type} (P : (α → Prop) → Prop) : Prop where
    nonempty : ∀ B, P B → ∃ x, B x
    covers : ∀ x, ∃ B, P B ∧ B x
    disjoint : ∀ B C, P B → P C → (∃ x, B x ∧ C x) → B = C

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• classesdefDefinitionNo axioms

  /-- The family of all equivalence classes of `R`: `B` belongs to it when `B = [a]` for some `a`. -/
  def classes {α : Type} (R : α → α → Prop) : (α → Prop) → Prop := fun B => ∃ a, B = cls R a

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• classes_partitiontheoremProved here from basic factspropext, Quot.sound

  /-- **The equivalence classes of an equivalence relation form a partition.** Classes are non-empty
  and cover everything because `a ∈ [a]`; two classes sharing an element `x` are equal because
  `x R a` and `x R b` give `a R b`, so `[a] = [b]`. -/
  theorem classes_partition {α : Type} {R : α → α → Prop} (h : Equivalence R) :
      IsPartition (classes R) where
    nonempty := by
      intro B ⟨a, hB⟩
      exact ⟨a, hB ▸ mem_cls_self h a⟩
    covers := fun x => ⟨cls R x, ⟨x, rfl⟩, mem_cls_self h x⟩
    disjoint := by
      intro B C ⟨a, hB⟩ ⟨b, hC⟩ ⟨x, hxB, hxC⟩
      rw [hB] at hxB
      rw [hC] at hxC
      rw [hB, hC]
      exact cls_eq_of_rel h (h.trans (h.symm hxB) hxC)

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• SameBlockdefDefinitionNo axioms

  /-- The relation defined by a partition: `a` and `b` are related when they lie in the same block. -/
  def SameBlock {α : Type} (P : (α → Prop) → Prop) (a b : α) : Prop := ∃ B, P B ∧ B a ∧ B b

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• same_block_equivalencetheoremProved here from basic factsNo axioms

  /-- **"Lie in the same block" is an equivalence relation.** Reflexive: every element lies in
  some block. Symmetric: obvious. Transitive: if `a, b ∈ B` and `b, c ∈ C`, then `B` and `C` share
  `b`, so `B = C`, and `a, c` lie in the same block. -/
  theorem same_block_equivalence {α : Type} {P : (α → Prop) → Prop} (hP : IsPartition P) :
      Equivalence (SameBlock P) where
    refl := by
      intro a
      obtain ⟨B, hB, ha⟩ := hP.covers a
      exact ⟨B, hB, ha, ha⟩
    symm := by
      intro a b ⟨B, hB, ha, hb⟩
      exact ⟨B, hB, hb, ha⟩
    trans := by
      intro a b c ⟨B, hB, ha, hb⟩ ⟨C, hC, hb', hc⟩
      have hBC : B = C := hP.disjoint B C hB hC ⟨b, hb, hb'⟩
      rw [← hBC] at hc
      exact ⟨B, hB, ha, hc⟩

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• same_block_classestheoremProved here from basic factsNo axioms

  /-- Round trip 1: start with an equivalence relation `R`, form its classes, and ask "same class?".
  You get `R` back: `a` and `b` lie in a common class exactly when `a R b`. -/
  theorem same_block_classes {α : Type} {R : α → α → Prop} (h : Equivalence R) (a b : α) :
      SameBlock (classes R) a b ↔ R a b := by
    constructor
    · intro ⟨B, ⟨c, hB⟩, ha, hb⟩
      rw [hB] at ha hb
      exact h.trans ha (h.symm hb)
    · intro hab
      exact ⟨cls R b, ⟨b, rfl⟩, hab, mem_cls_self h b⟩

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• classes_same_blocktheoremProved here from basic factspropext, Quot.sound

  /-- Round trip 2: start with a partition `P`, form the relation "same block", and take its
  classes. You get exactly the blocks of `P` back. Together with round trip 1 this says that
  equivalence relations and partitions are two descriptions of the same thing, and that each
  partition comes from exactly one equivalence relation. -/
  theorem classes_same_block {α : Type} {P : (α → Prop) → Prop} (hP : IsPartition P)
      (B : α → Prop) : classes (SameBlock P) B ↔ P B := by
    constructor
    · intro ⟨a, hB⟩
      obtain ⟨C, hC, haC⟩ := hP.covers a
      -- The class of `a` is the block `C` containing `a`.
      have hcls : cls (SameBlock P) a = C := by
        funext x
        apply propext
        constructor
        · intro ⟨D, hD, hxD, haD⟩
          have hDC : D = C := hP.disjoint D C hD hC ⟨a, haD, haC⟩
          rw [← hDC]
          exact hxD
        · intro hxC
          exact ⟨C, hC, hxC, haC⟩
      rw [hB, hcls]
      exact hC
    · intro hB
      obtain ⟨a, haB⟩ := hP.nonempty B hB
      refine ⟨a, ?_⟩
      funext x
      apply propext
      constructor
      · intro hxB
        exact ⟨B, hB, hxB, haB⟩
      · intro ⟨D, hD, hxD, haD⟩
        have hDB : D = B := hP.disjoint D B hD hB ⟨a, haD, haB⟩
        rw [← hDB]
        exact hxD

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• same_output_equivalencetheoremProved here from basic factsNo axioms

  /-- For any function `f`, "has the same output under `f`" is an equivalence relation. "Same
  remainder", "same colour", "same birth month" and "same last digit" are all of this kind. -/
  theorem same_output_equivalence {α β : Type} (f : α → β) :
      Equivalence (fun a b => f a = f b) where
    refl := fun _ => rfl
    symm := fun hab => hab.symm
    trans := fun hab hbc => hab.trans hbc

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• SameRemainderdefDefinitionNo axioms

  /-- `a` and `b` have the **same remainder** on division by `n`. (Lean's `%` on `Int` gives the
  remainder between `0` and `n − 1` for `n > 0`, also for negative `a`: `-1 % 3 = 2`.) -/
  def SameRemainder (n a b : Int) : Prop := a % n = b % n

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• same_remainder_equivalencetheoremProved here from basic factsNo axioms

  /-- "Same remainder on division by `n`" is an equivalence relation: it is "same output" for the
  function `a ↦ a % n`. -/
  theorem same_remainder_equivalence (n : Int) : Equivalence (SameRemainder n) :=
    same_output_equivalence (fun a => a % n)

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• remainder_examplestheoremProved here from basic factsNo axioms

  /-- Examples, checked by calculation: `17` and `2` have the same remainder on division by `3`;
  so do `-1` and `5` (remainder `2`); but `4` and `6` do not. -/
  theorem remainder_examples :
      SameRemainder 3 17 2 ∧ SameRemainder 3 (-1) 5 ∧ ¬ SameRemainder 3 4 6 := by
    unfold SameRemainder
    decide

  Axioms used: No axiomsformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

• exactly_n_classestheoremProved here from basic factspropext, Quot.sound

  /-- **"Same remainder on division by `n`" has exactly `n` classes** (for `n > 0`): every integer
  `a` is related to exactly one of `0, 1, …, n − 1`, namely its remainder `r = a % n`. So the
  classes are `[0], [1], …, [n − 1]`, and these are all different. -/
  theorem exactly_n_classes (n : Int) (hn : 0 < n) (a : Int) :
      ∃ r, 0 ≤ r ∧ r < n ∧ SameRemainder n a r ∧
        ∀ s, 0 ≤ s → s < n → SameRemainder n a s → s = r := by
    refine ⟨a % n, Int.emod_nonneg a (by omega), Int.emod_lt_of_pos a hn, ?_, ?_⟩
    · -- `a % n` has the same remainder as `a`: taking the remainder twice changes nothing.
      show a % n = a % n % n
      exact (Int.emod_emod_of_dvd a (Int.dvd_refl n)).symm
    · intro s hs0 hsn hsame
      -- A number between `0` and `n - 1` is its own remainder.
      have hss : s % n = s := Int.emod_eq_of_lt hs0 hsn
      show s = a % n
      rw [hsame, hss]

  Axioms used: propext, Quot.soundformal/Lumenary/EquivalenceRelations.leanTry it in the Lean web editor

Formal exercises

Each exercise contains a sorry for you to replace. Open it in the Lean web editor, or clone the repository and run lake build.

/-- Show that "same remainder on division by `n`" is an equivalence relation.
Hint: `SameRemainder n a b` unfolds to `a % n = b % n`, so this is "same output" for the function
`a ↦ a % n`. Either use `same_output_equivalence`, or give the three fields yourself:
`refl := fun _ => rfl`, and use `Eq.symm` and `Eq.trans` for the other two. -/
theorem same_remainder_equivalence (n : Int) : Equivalence (SameRemainder n) := by
  sorry

/-- "Same remainder on division by `n`" is an equivalence relation: it is "same output" for the
function `a ↦ a % n`. -/
theorem same_remainder_equivalence (n : Int) : Equivalence (SameRemainder n) :=
  same_output_equivalence (fun a => a % n)

/-- Symmetry and transitivity give reflexivity **when every element is related to something**.
Hint: `intro a`, then `obtain ⟨b, hab⟩ := hsome a`. Now `hs a b hab : R b a`, and `ht` chains
`a R b` with `b R a`. -/
theorem refl_of_symm_trans {α : Type} (R : α → α → Prop) (hs : Symmetric R) (ht : Transitive R)
    (hsome : ∀ a, ∃ b, R a b) : Reflexive R := by
  sorry

/-- The tempting argument *does* work when every element is related to **something**:
pick `b` with `a R b`; symmetry gives `b R a`; transitivity gives `a R a`. -/
theorem refl_of_symm_trans {α : Type} (R : α → α → Prop) (hs : Symmetric R) (ht : Transitive R)
    (hsome : ∀ a, ∃ b, R a b) : Reflexive R := by
  intro a
  obtain ⟨b, hab⟩ := hsome a
  exact ht a b a hab (hs a b hab)