eqv_gen

Stream: mathlib4

[Kevin Buzzard]

In core Lean 3, in init.data.quot we had

variable (r : α → α → Prop)

inductive eqv_gen : α → α → Prop
| rel : Π x y, r x y → eqv_gen x y
| refl : Π x, eqv_gen x x
| symm : Π x y, eqv_gen x y → eqv_gen y x
| trans : Π x y z, eqv_gen x y → eqv_gen y z → eqv_gen x z

(the equivalence relation generated by a relation) which kind of feels to me like a fundamental thing, so I was surprised I couldn't find it in Lean 4 even though we have Quot and Quotient. I looked for EqvGen and variants. Shall I just make my own and put it in Mathlib.Init.Data.Quot or did I miss it?

[Mario Carneiro]

Yes, it should go in Mathlib.Init.Data.Quot. The main reason it was front-loaded so early in lean 3 was because it is used in the statement of docs#quot.exact, but this is basically a curiosity and not actually used anywhere to my knowledge.

[Yakov Pechersky]

@Anne Baanen has EqvGen in their PR

[Mario Carneiro]

It probably makes more sense to move it to logic.relation if we are in a refactoring mood

[Kevin Buzzard]

Nice -- I have logic.relation completely working apart from the last few lines which mention EqvGen, and I've just pulled into St Pancras International.

[Junyan Xu]

The main reason it was front-loaded so early in lean 3 was because it is used in the statement of docs#quot.exact, but this is basically a curiosity and not actually used anywhere to my knowledge.

docs#quotient.eq seems to be used a lot of times, e.g. here, and this recent question also uses docs#quotient.decidable_eq. Does Lean 4 directly establish the setoid version without going through the eqv_gen version for general relations?