Relation properties duplication

Stream: mathlib4

[Snir Broshi]

Mathlib and Std combined have 3 versions of many properties of relations:

	Std class	Mathlib class	Mathlib prop
reflexive relation	docs#Std.Refl	docs#IsRefl	docs#Reflexive
irreflexive relation	docs#Std.Irrefl	docs#IsIrrefl	docs#Irreflexive
symmetric relation	docs#Std.Symm	docs#IsSymm	docs#Symmetric
antisymmetric relation	docs#Std.Antisymm	docs#IsAntisymm	docs#AntiSymmetric
asymmetric relation	docs#Std.Asymm	docs#IsAsymm
total relation	docs#Std.Total	docs#IsTotal	docs#Total
transitive relation	docs#Trans (more generic)	docs#IsTrans	docs#Transitive
equivalence relation	docs#Equivalence (structure)	docs#IsEquiv

There are also classes for orders which were upstreamed to core because of the new grind, although the situation here is different because of bundling:

	Std class using LE	Mathlib class using LE	Mathlib unbundled class
preorder	docs#Std.IsPreorder	docs#Preorder	docs#IsPreorder
partial order	docs#Std.IsPartialOrder	docs#PartialOrder	docs#IsPartialOrder
linear order	docs#Std.IsLinearOrder	docs#LinearOrder	docs#IsLinearOrder

I also found docs#emptyRelation and docs#EmptyRelation.

Some relations have instances/theorems for all classes/props, some only for some:

docs#Eq: Equivalence ✓, IsEquiv ✓
docs#Ne: Std.Irrefl x (docs#Ne.irrefl is close), IsIrrefl x, Irreflexive x, Std.Symm x (docs#Ne.symm is close), IsSymm x, Symmetric x
docs#Iff: Equivalence x, IsEquiv ✓
docs#Relation.ReflGen: Std.Refl x, IsRefl ✓, Reflexive ✓
docs#Relation.TransGen: Trans ✓, IsTrans ✓, Transitive ✓
docs#Relation.ReflTransGen: Std.Refl x, IsRefl ✓, Reflexive ✓, Trans ✓, IsTrans ✓, Transitive ✓
docs#Relation.EqvGen: Equivalence ✓, IsEquiv x

I think we should either fill the missing ones and add instances relating everything (already exist for transitive and the order ones) and theorems for the classes to imply the props (already exist for reflexive and transitive), or deprecate Mathlib's classes and props where possible, or at least document this table somewhere.

Thoughts? I assume this has been brought up before but I couldn't find it.

[Kim Morrison]

The order classes require more discussion (particularly LinearOrder, which is a mess.)

But personally I would be happy to see docs#IsAntisymm deprecated in favour of Std.Antisymm (and similarly for everything in the first table).

[Markus Himmel]

Snir Broshi said:

There are also classes for orders which were upstreamed to core because of the new grind,

Just noting that grind was not the primary motivation for adding these classes. Rather, they were added to support various future standard library developments like consolidating the lemmas for List.min? and adding verified sorting algorithms, binary search, and more. The fact that the classes are useful for grind was more of a happy accident.

[Wrenna Robson]

I'm extremely enthusiastic about tidying up this situation.

[Ruben Van de Velde]

I'm currently working on Total

[Ruben Van de Velde]

Which is now #30855

[Ruben Van de Velde]

If anyone has thoughts on deduplicating relation properties like IsTotal/Std.Total, please have a look at #30855.

[Violeta Hernández]

I've been wanting this unification for a very long time, thank you!

[Snir Broshi]

EmptyRelation #33204

[Snir Broshi]

IsSymm #33325

[Snir Broshi]

IsAsymm #33503

[Snir Broshi]

IsAntisymm #33685

[Snir Broshi]

IsIrrefl #33717

[Snir Broshi]

IsRefl #33755

[Ruben Van de Velde]

Please feel free to take over / redo #30855 if you have time.

[Snir Broshi]

Ruben Van de Velde said:

Please feel free to take over / redo #30855 if you have time.

Do you prefer I open another PR or push to yours w/ an invitation?

[Ruben Van de Velde]

Either way - I invited you

[Snir Broshi]

Ruben Van de Velde said:

Either way - I invited you

Wrong repo

[Snir Broshi]

IsTotal #33797

[Snir Broshi]

We're close to being done with the (non-order) classes, few last points:

[Snir Broshi]

1) docs#Equivalence is a structure and doesn't extend Std.Refl/Std.Symm/IsTrans, so I think we should leave docs#IsEquiv as-is, add an iff theorem between them, and perhaps RFC in core for a new Std.Equiv (though docs#IsPreorder vs docs#Std.IsPreorder might be a blocker)

[Snir Broshi]

2) Mathlib's docs#IsTrans vs core's docs#Trans: I suggest changing IsTrans to abbrev IsTrans α r := Trans r r r, but this creates universe problems:

import Mathlib.Tactic.TypeStar
/--
error: Type mismatch
  Trans r r r
has type
  Sort (max 1 u_1)
of sort `Type (max 1 u_1)` but is expected to have type
  Prop
of sort `Type`
-/
#guard_msgs in
abbrev IsTrans (α : Sort*) (r : α → α → Prop) : Prop := Trans r r r

[Snir Broshi]

3) lean4#10945 introduced docs#Std.Trichotomous which is ¬r a b → ¬r b a → a = b,
which seems to replace docs#IsTrichotomous but that is r a b ∨ a = b ∨ r b a.
They're of course logically equivalent, but deprecating one for the other seems nontrivial.
Which do you prefer? Should I go ahead and deprecate, or do we prefer mathlib's version and want to suggest it to core?

[Snir Broshi]

4) Can I proceed to deprecating the prop versions (e.g. docs#Total / docs#AntiSymmetric)? Their docstrings say e.g. "Std.Total as a definition, suitable for use in proofs", but the classes can also be used in proofs, I don't see a reason to keep them.

[Snir Broshi]

cc @Wrenna Robson for trichotomous

[Wrenna Robson]

We did deliberately choose the version we have there, essentially because it is then the natural counterpart of antisymm.

[Wrenna Robson]

As I recall Mathlib's version feels like a good idea but in practice it doesn't work amazingly.

[Wrenna Robson]

I think you probably just want to prove that as a theorem if you don't already have it.

[Snir Broshi]

So we should deprecate Mathlib's version, yes?

[Wrenna Robson]

Yes, I think so.

[Wrenna Robson]

I am sorry that that is nontrivial. I'm happy to help with review chores and things.

[Snir Broshi]

No worries, thanks!

[Snir Broshi]

IsTrichotomous #34349

[Snir Broshi]

Total #34351

[Snir Broshi]

AntiSymmetric #35025

[Snir Broshi]

Irreflexive #35191

[Yaël Dillies]

Are we sure we want to be using typeclasses as fields to structures? Now that #35191 is merged, the following code doesn't work:

import Mathlib.Combinatorics.SimpleGraph.Dart

/-- The graph obtained by contracting a dart in an existing graph. -/
def contractDart {V : Type*} (G : SimpleGraph V) (e : G.Dart) :
    SimpleGraph {x : V // x ≠ e.snd} where
  Adj x y :=
      G.Adj x.val y.val
    ∨ x.val = e.fst ∧ y.val ≠ e.fst ∧ G.Adj e.snd y.val
    ∨ y.val = e.fst ∧ x.val ≠ e.fst ∧ G.Adj x.val e.snd
  symm := sorry
  loopless
    | x, .inl x_adj_x => G.loopless x.val x_adj_x
    | x, .inr <| .inl x_problem => by tauto
    | x, .inr <| .inr x_problem => by tauto

and one needs to instead do

/-- The graph obtained by contracting a dart in an existing graph. -/
def contractDart {V : Type*} (G : SimpleGraph V) (e : G.Dart) :
    SimpleGraph {x : V // x ≠ e.snd} where
  Adj x y :=
      G.Adj x.val y.val
    ∨ x.val = e.fst ∧ y.val ≠ e.fst ∧ G.Adj e.snd y.val
    ∨ y.val = e.fst ∧ x.val ≠ e.fst ∧ G.Adj x.val e.snd
  symm := sorry
  loopless := by
    constructor
    exact fun
    | x, .inl x_adj_x => G.loopless.1 x.val x_adj_x
    | x, .inr <| .inl x_problem => by tauto
    | x, .inr <| .inr x_problem => by tauto

[Snir Broshi]

Relevant

[Snir Broshi]

FWIW I think the by constructor; exact fun construction isn't so bad if in return we get better interop with core's relation properties and possibly typeclass inference for properties where possible

[Anne Baanen]

(I wouldn't be too hopeful for typeclass inference to do too much here, it seems like aesop_graph autoparams is the way to go.)

[Anne Baanen]

But yes, I think this extra abstraction barrier is annoying but is less bad than unbundling. Especially since choosing a consistent spelling makes it easier to copy fields between different structures.

Note that where notation also works as:

import Mathlib.Combinatorics.SimpleGraph.Dart

/-- The graph obtained by contracting a dart in an existing graph. -/
def contractDart {V : Type*} (G : SimpleGraph V) (e : G.Dart) :
    SimpleGraph {x : V // x ≠ e.snd} where
  Adj x y :=
      G.Adj x.val y.val
    ∨ x.val = e.fst ∧ y.val ≠ e.fst ∧ G.Adj e.snd y.val
    ∨ y.val = e.fst ∧ x.val ≠ e.fst ∧ G.Adj x.val e.snd
  symm := sorry
  loopless.irrefl -- <- changed here
    | x, .inl x_adj_x => G.loopless.irrefl x.val x_adj_x
    | x, .inr <| .inl x_problem => by tauto
    | x, .inr <| .inr x_problem => by tauto

[Yaël Dillies]

Ah yes, I knew I was missing something. Annoying that you must go one deeper, but it's workable with

[Snir Broshi]

Transitive #35592

[Jovan Gerbscheid]

About transivity, we currently have IsTrans (in mathlib) and Trans (from core), and they are separate type classes with a loop like this:

/-- `IsTrans X r` means the binary relation `r` on `X` is transitive. -/
class IsTrans (α : Sort*) (r : α → α → Prop) : Prop where
  trans : ∀ a b c, r a b → r b c → r a c

instance {α : Sort*} {r : α → α → Prop} [IsTrans α r] : Trans r r r :=
  ⟨IsTrans.trans _ _ _⟩

instance (priority := 100) {α : Sort*} {r : α → α → Prop} [Trans r r r] : IsTrans α r :=
  ⟨fun _ _ _ => Trans.trans⟩

Wouldn't it make more sense to avoid the loop and simply make it an abbrev?

abbrev IsTrans (α : Sort*) (r : α → α → Prop) : Prop := Trans r r r

I suppose this would be a breaking change because the argument implicitness in the trans field is different...

[Violeta Hernández]

I've always thought of Trans as an implementation detail of the trans tactic, I don't think you're really supposed to use it in mathematical code.

[Wrenna Robson]

Unfortunately I think we do

[Jovan Gerbscheid]

The trans tactic is in batteries so Trans wasn't made for the trans. Trans is part of the implementation of calc though.

[Jovan Gerbscheid]

Another case of duplicated relation properties is IsWellFounded and WellFounded, which are the exact same thing, except one is a class and the other isn't. Why don't we replace

/-- A well-founded relation. Not to be confused with `IsWellOrder`. -/
@[mk_iff] class IsWellFounded (α : Type u) (r : α → α → Prop) : Prop where
  /-- The relation is `WellFounded`, as a proposition. -/
  wf : WellFounded r

with

attribute [class] WellFounded

We can still have both APIs for using it as a class or passing it around explicitly.

[Snir Broshi]

Jovan Gerbscheid said:

Wouldn't it make more sense to avoid the loop and simply make it an abbrev?

abbrev IsTrans (α : Sort*) (r : α → α → Prop) : Prop := Trans r r r

I agree, but see #mathlib4 > Relation properties duplication @ 💬 above, this doesn't work.
I don't know why Trans has max 1 in the universes though. It allows the relations to produce Sort* rather than Prop.

[Snir Broshi]

I was planning on RFCing a new Std.Trans to core to half fix this, so that they would solve the duplication

[Aaron Liu]

Snir Broshi said:

I don't know why Trans has max 1 in the universes though. It allows the relations to produce Sort* rather than Prop.

I just wanted to comment that, the max 1 is technically unnecessary and you can get rid of it but it's a total pain and breaks a lot of automation