Deprecate Iris/Std/Classes.lean

[markusdemedeiros]

The classes seem to be sparsely used now. We should look and see if they can be removed.

[alvinylt]

It seems like most of these type classes are already defined in Init.Core.

I have started porting step-indexing for Transfinite Iris. There are some type classes (e.g. irreflexivity, strict order, partial order, antisymmetry) that are not available in Iris/Std/Classes.lean. So we'll have to decide whether to introduce the missing ones into the file or reuse built-in definitions.

Are there particular reasons to prefer Iris/Std/Classes.lean over Init.Core? If not, shall we use the latter throughout the codebase for consistency?

[alvinylt]

Also, the built-in type class Trans (for transitivity) enables calc-style proofs. Currently BIBase.Entails.trans is a theorem expressed in terms of Iris.Std.Transitive while entails_trans in DerivedLaws.lean is an instance of Trans.

As a side note we can perhaps also annotate the reflexivity theorem with @[refl]:

@[simp, refl]
theorem BIBase.Entails.rfl [BI PROP] {P : PROP} : P ⊢ P := refl

This allows us to use the tactic rfl. Example:

example [BI PROP] (P : PROP) : P ⊢ P := by rfl

as an alternative to .rfl or by exact .rfl.

[lzy0505]

We should use the built-in typeclasses throughout.