refactor: remove duplicate type classes in Iris/Std/Classes.lean and reuse definitions from core libraries

[alvinylt]

Description

Addresses #468.

This PR involves four commits, one for each set of changes.

• The first commit removes the type classes Reflexive and Transitive from Iris/Std/Classes.lean and replaces them with Refl in Init/Core.lean and Trans in Init/Prelude.lean, respectively.

  • The custom type class Preorder remains in Iris/Std/Classes.lean and adjusted to use the built-in type classes.
  • By annotating the theorem BIBase.Entails.rfl in BI.lean with @[refl], we are able to use the tactic rfl to tackle goals in the form P ⊢ P as an alternative to by apply .rfl.

• The second commit eliminates the custom type class Preorder and replaces it with IsPreorder in Init/Data/Order/Classes.lean. In fact, the type class IsPreorder is relatively new (see Lean 4.25.0 documentation).

  • In order for the type class IsPreorder to work for BI PROP, there must be an instance of LE PROP. At this point my approach was to extend the type class BIBase:

    class BIBase (PROP : Type u) extends LE PROP

    But this is not really ideal, as the BI entailment (⊢) is now definitionally equal to ≤ in the type class LE, which means simp may possibly unfold ⊢ as ≤, and the @[refl] annotation introduced in the first commit would not achieve its purpose because rfl would require the @[refl] annotation directly for ≤.

• The third commit addresses the problem with LE PROP in a different way.

  • Instead of modifying BIBase and having Std.IsPreorder PROP as a field of BI, we instead have the bare propositions of reflexivity and transitivity as two fields of BI:

    entails_refl {P : PROP} : P ⊢ P
    entails_trans {P Q R : PROP} : (P ⊢ Q) → (Q ⊢ R) → P ⊢ R

  • We then prove that there exist LE PROP and IsPreorder PROP as separate instances in terms of entails_refl and entails_trans. This is more consistent with how other Lean code is organised.
  • This reverts the definition ⊢ as ≤ in the previous commit.

• The fourth commit eliminates Iris/Std/Classes.lean entirely.

  • There is a number of type class instances in BI/DerivedLaws.lean using definitions from Iris/Std/Classes.lean. There are similar type classes for commutativity, associativity, antisymmetry, LeftAbsorb, RightAbsorb, LeftId and RightId in Init/Core.lean, but they are expressed in terms of equality rather than bi-entailment.
  • I would suggest leaving these type class instances in BI/DerivedLaws.lean out until the built-in type classes are compatible with this use case, rather than using a mixture of built-in type classes and custom, more generic type classes. (Perhaps ongoing development regarding bi-entailment as equality might help?)
  • Iris/Std/Classes.lean defines the notation ⊤ for the top element for instances of the type class Top. This is used only once in CoPset.lean, so I moved to the notation there.
  • Similarly, the notation ## for disjointness is used only once in GenSets.lean and thus defined there directly. The notation ## for disjointness is used in GenSets.lean and Namespaces.lean.

Remarks

Step-indexing (PR #515) further involves irreflexivity, total relations and strict orders. At the moment, I have introduced these three new definitions into Iris/Std/Classes.lean. If we decide to deprecate Iris/Std/Classes.lean, we can directly use irrefl and total from Init/Core.lean, as well as IsPartialOrder from Init/Data/Order/Classes.lean. Not aware that a type class for strict orders (irreflexivity + transitivity) exists though.

Would be great to discuss whether to adopt any of these changes.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

Looks good by me, with two small comments.

[alvinylt]

For future reference, here is the summary of the changes.

Type class in Iris/Std/Classes.lean	Changes	Remarks
Reflexivity	Replaced by Refl from Init/Core.lean	Exact same definition.
Transitivity	Replaced by Trans from Init/Prelude.lean	Instances of Trans enable calc-style proofs. The built-in type class Trans is also more generic than Transitivity as the former is parametrised over three relations.
Preorder	Replaced by IsPreorder from Init/Data/Order/Classes.lean	Useful for grind.
Commutative, Associative, Idempotent, LeftId, RightId, LeftAbsorb, RightAbsorb, Associative, Antisymmetric	None	Similar to the type classes in Init/Core.lean but those are not generic enough as they are formulated in terms of equality (=) rather than any binary relation.
Top	None	Same definition available in Mathlib (Mathlib/Order/Notation.lean) but not in the core libraries.
Disjoint	None	Available as a definition in Mathlib (Mathlib/Order/Disjoint.lean) rather than a type class.