symmetric closure definition

Stream: mathlib4

[Chris Henson]

@Snir Broshi recently pointed out to me that the symmetric closure of a relation appears as docs#CompRel. This is a leaf file with respect to Mathlib, but is used in the CGT repo (cc @Violeta Hernández ).

This definition seems to be an outlier with respect to TransGen in core and other closures in Mathlib.Logic.Relation in terms of naming and its being a Prop-valued def versus an inductive. Especially if one were inclined to define the transitive symmetric closure, this is a bit awkward.

My question is if adding an inductive SymmGen to Mathlib.Logic.Relation makes sense, and if so should CompRel be deprecated in favor of this or just proven to be equivalent? There is also docs#IncompRel to consider here.

[Bhavik Mehta]

TransGen and ReflTransGen can (essentially) only really be defined as inductives, but the symmetric closure of a relation has a much simpler definition, so I think it's reasonable to use the simpler definition here (and doing induction on it is just the eliminator for Or!). The symmetric transitive closure should be the same as TransGen (CompRel r). In particular, the transitive closure of a symmetric relation should be symmetric, with proof looking similar to https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Relation.html#Relation.ReflTransGen.symmetric

[Bhavik Mehta]

import Mathlib.Logic.Relation

open Relation

theorem TransGen.symmetric {α : Type*} {r : α → α → Prop} (h : Symmetric r) :
    Symmetric (TransGen r) := by
  intro x y h
  induction h with
  | single i => exact .single (h i)
  | tail h1 h2 h3 => exact .head (h h2) h3

(the person who added the ReflTransGen version to mathlib really should've done the TransGen one too...)

[Bhavik Mehta]

Added in #34382

[Chris Henson]

My primary concern here is with naming. Given CompRel is in a different module and doesn't follow the naming pattern, it's a bit hard to discover.

Bhavik Mehta said:

TransGen and ReflTransGen can (essentially) only really be defined as inductives, but the symmetric closure of a relation has a much simpler definition, so I think it's reasonable to use the simpler definition here (and doing induction on it is just the eliminator for Or!).

This is true, I just wondered if this is consistent with how for instance ReflGen is an inductive and docs#Relation.reflGen_iff is generated by mk_iff. I think it is nice when the constructor names are consistent.

The symmetric transitive closure should be the same as TransGen (CompRel r)?

Yes. I was wondering if this should follow the same pattern as the simp theorems docs#Relation.reflGen_transGen and docs#Relation.transGen_reflGen.

[Bhavik Mehta]

Yeah I agree the naming is a little weird in that context, though the other factor is that CompRel makes sense as the name in the context of order theory, in which case CompRel (· ≤ ·) gives the comparability relation, and calling that the symmetric closure feels a little strange? Perhaps it's not as bad though.

[Chris Henson]

If it were just CompRel I'd be more confident in arguing to rename it, but stranding IncompRel would be awkward too...

[Bhavik Mehta]

Note there's also docs#AntisymmRel

[Chris Henson]

Yes, and there is API connecting them in Mathlib.Order.Comparable. If it is sufficient to just use AntisymmRel (which I guess is a question for CGT since IncompRel is not used elsewhere in Mathlib) then I would confidently argue to deprecate the module and rename CompRel to Relation.SymmGen.

[Bhavik Mehta]

I don't think it's sufficient to just use AntisymmRel, and in particular I think the TODO in the CompRel file should be applied and CompRel should be used to define IsChain

[Chris Henson]

Hmm, I hadn't seen that. I can't think of a nice way (i.e. not involving duplicate definitions) to resolve the naming incongruity given these overlapping but distinct uses.

[Chris Henson]

It seems that the conclusion here is that CompRel should be left as is. So if we want theorems like ReflTransGen (CompRel r) = EqvGen r (this is in CSLib at the moment) relating it to the other closures, it seems these should go into Mathlib.Logic.Relation? Maybe that helps a bit with discovery.

[Bhavik Mehta]

Yeah I think it's reasonable for that theorem to be in mathlib. I'm warming to the idea of renaming CompRel to SymmGen to be honest

[Violeta Hernández]

Is the proposal to rename CompRel to SymmGen?

[Violeta Hernández]

I don't really mind. At the moment this is not used anywhere, I mostly just added it for parity with IncompRel.

[Chris Henson]

I have opened #34428, just renaming CompRel.

[Eric Wieser]

What's the purpose of the Gen(erator) token in these names? Should they instead be ReflClosure, SymmClosure, etc? Or are we willing to use Gen to mean Closure for brevity?

[Eric Wieser]

(to me Gen seems to be pointing out the definition happens to be inductive, but that's largely an implementation detail!)

[Chris Henson]

I assume it was a decision made for consistency with docs#Relation.TransGen, which is in core.

[Eric Wieser]

Ah, I missed that core made the decision; though I suspect it was made long ago in Lean 3

[Eric Wieser]

Violeta Hernández said:

Is the proposal to rename CompRel to Relation.SymmGen?

Given the PR seems to indicate yes, can interested parties :+1:/:minus:/:-1: this message to indicate if you are in favor?

[Chris Henson]

So it looks like of those responding at this point, opinion ranges from neutral to in favor.

[Violeta Hernández]

Again, I have no use for CompRel, so I don't mind what it's called.

[Eric Wieser]

I'm happy to go ahead with the rename given the above, hence removing the awaiting-zulip label from the PR

[Eric Wieser]

So is the thought that we rename IncompRel to Relation.AsymmGen? or similar?

[Aaron Liu]

that's not

[Aaron Liu]

no

[Aaron Liu]

r a b doesn't imply IncompRel r a b

[Aaron Liu]

so it's not anything Gen

[Chris Henson]

It would be consistent naming-wise, but odd mathematically. If you interpret it as a closure, it's saying to discard the relation, not something we usually give a name.

[Chris Henson]

I guess the point here is that there are two concepts (symmetric closure and comparability) that happen to coincide definitionally but is awkward for the negation.

[Bhavik Mehta]

Yes I agree with Chris, no further renames are necessary: "symmetric closure" and "comparability relation" happen to be the same informal name for the same concept used in different areas. But IncompRel/AntisymmRel and TransGen/ReflTransGen don't really have analogues on the other side. So we have this slightly odd inconsistency between SymmGen and IncompRel, but it's less odd than the old CompRel/TransGen, and Chris' change makes all of these concepts more discoverable and more closely linked, and so imo no further action is needed