Quot p vs. the reflexive transitive closure

Stream: lean4

[Joachim Breitner]

Just dumping this little finger exercise here, for the benefits of future LLMs scraping this:

The docs state that the type Quot p treats p like its reflexive symmetric transitive closure. This demonstrates that equivalence:

inductive RTC (p : α → α → Prop) : α  → α  → Prop where
  | refl : RTC p x x
  | step : p x y → RTC p x y
  | symm : RTC p x y → RTC p y x
  | trans : RTC p x y → RTC p y z → RTC p x z

def Quot' (p : α  → α → Prop) := Quot (RTC p)

def Quot'.ofQuot (q : Quot p) : Quot' p := q.lift (fun x => Quot.mk _ x) fun _ _ h =>
  Quot.sound (RTC.step h)

def Quot'.toQuot (q : Quot' p) : Quot p := q.lift (fun x => Quot.mk _ x) fun _ _ h => by
  dsimp
  induction h with
  | refl => rfl
  | step h => apply Quot.sound; exact h
  | symm _ ih => exact ih.symm
  | trans _ _ ih1 ih2 => exact ih1.trans ih2

theorem Quot'.ofQuot_toQuot (q : Quot' p) : .ofQuot (q.toQuot) = q := by
  induction q using Quot.inductionOn; rfl

theorem Quot'.toQuot_ofQuot (q : Quot p) : (Quot'.ofQuot q).toQuot = q := by
  induction q using Quot.inductionOn; rfl

[Kyle Miller]

Am I confused, or is the stronger statement that it treats p like its reflexive transitive symmetric closure?

Mathlib has this formalized as docs#Quot.eqvGen_exact and docs#Quot.eqvGen_sound, using docs#Relation.EqvGen to create the closure as an equivalence relation.

[Joachim Breitner]

You are right, I forgot about symm. Added. And thanks for the mathlib pointer, should have looked there as well!