Theorems about type classes (preorder, equivalence)

Stream: general

[David Holmqvist]

Hey guys! I am experimenting a bit with structures vs. type classes. I am in the following situation:

class Preorder (r : α → α → Prop) where
  refl  : ∀ x, r x x
  trans : ∀ {x y z}, r x y → r y z → r x z

open Preorder

class Equivalence [Preorder r] (r : α → α → Prop) where
  symm : ∀ {x y}, r x y → r y x

open Equivalence

example [Preorder r] : Equivalence (fun x y ↦ r x y ∧ r y x)

I get an error because it cannot find an instance for Preorder (fun x y...), which I understand. I want to provide the data for the preorder instance by giving an equivalence. I understand I might have to write this using an instance declaration anyway.

I can always not extend the preorder and just redeclare the refl and trans fields in the equivalence, but this I find less nice.

Being very new to Lean I understand I might have misunderstood some basics; either way, I am grateful for some help!

[David Holmqvist]

Oh, if I let it extend Preorder instead it works out quite nice;

class Preorder (r : α → α → Prop) where
  refl  : ∀ x, r x x
  trans : ∀ {x y z}, r x y → r y z → r x z

open Preorder

class Equivalence (r : α → α → Prop) extends Preorder r where
  symm : ∀ {x y}, r x y → r y x

open Equivalence

theorem Equivalence.fromPreorder [Preorder r] : Equivalence (fun x y ↦ r x y ∧ r y x) where
  refl := by intro x
             apply And.intro
             exact refl x
             exact refl x
  trans := by intro x y z r₁ r₂
              apply And.intro
              exact trans r₁.left r₂.left
              exact trans r₂.right r₁.right
  symm := by intro x y r
             apply And.intro
             exact r.right
             exact r.left

[Kevin Buzzard]

In your first code block you maybe have two different rs in your definition of Equivalence? One probably ends up with a dagger after its name and becomes inaccessible.

[David Holmqvist]

@Kevin Buzzard Oh, right! I tried swapping the order, but still same problem with the first approach. But I guess the second approach is what you would have to go for to show such things, otherwise it's kind of a catch 22.