equivalence relations are symmetric

Stream: mathlib4

[Kevin Buzzard]

In core Init.Core we have

structure Equivalence {α : Sort u} (r : α → α → Prop) : Prop where
  /-- An equivalence relation is reflexive: `x ~ x` -/
  refl  : ∀ x, r x x
  /-- An equivalence relation is symmetric: `x ~ y` implies `y ~ x` -/
  symm  : ∀ {x y}, r x y → r y x
  /-- An equivalence relation is transitive: `x ~ y` and `y ~ z` implies `x ~ z` -/
  trans : ∀ {x y z}, r x y → r y z → r x z

and in Mathlib.Init.Logic we have

def Symmetric := ∀ ⦃x y⦄, x ≺ y → y ≺ x

Now this doesn't work:

import Mathlib.Init.Logic

variable (h : Equivalence r) -- autoImplicit is sometimes v cool

#check (h.symm : Symmetric r)
/-
type mismatch
  Equivalence.symm h
has type
  r ?m.52 ?m.53 → r ?m.53 ?m.52 : Prop
but is expected to have type
  Symmetric r : Prop
-/

Is it because of the {x y} vs ⦃x y⦄ clash? Should I write a function from Equivalence r to Symmetric r called Equivalence.Symmetric or something?

def Equivalence.Symmetric (h : Equivalence r) : Symmetric r :=
λ _ _ => h.symm

(and same question for trans -- and the coercion does work with refl but should Equivalence.Reflexive be written too?)

[Mario Carneiro]

Sure

[Mario Carneiro]

how about Equivalence.symmetric et al? (lowercase because it's a proof)

[Kevin Buzzard]

I could just do this:

import Mathlib.Init.Logic
import Mathlib.Init.Function

section Comap

variable {r : β → β → Prop}

infixl:2  " on " => Function.on_fun

theorem Reflexive.comap (h : Reflexive r) (f : α → β) : Reflexive (r on f) := fun a => h (f a)

theorem Symmetric.comap (h : Symmetric r) (f : α → β) : Symmetric (r on f) := fun _ _ hab => h hab

theorem Transitive.comap (h : Transitive r) (f : α → β) : Transitive (r on f) := fun _ _ _ hab hbc => h hab hbc

-- works fine
theorem Equivalence.comap (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=
  ⟨fun a => h.refl (f a), fun hab => h.symm hab, fun hab hbc => h.trans hab hbc⟩

-- Lean 3 proof nicer though:
-- ⟨h.1.comap f, h.2.1.comap f, h.2.2.comap f⟩

Actually I can't even get Equivalence.symmetric to work:

def Equivalence.symmetric (h : Equivalence r) : Symmetric r :=
  λ _ _ => h.symm

theorem Equivalence.comap' (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=
  ⟨Reflexive.comap h.refl f, Symmetric.comap h.symmetric f, sorry⟩
/-
type mismatch
  Symmetric.comap (symmetric h) f
has type
  Symmetric (r on f) : Prop
but is expected to have type
  Function.on_fun r f x✝ y✝ → Function.on_fun r f y✝ x✝ : Prop
the following variables have been introduced by the implicit lambda feature
  x✝ : ?m.657
  y✝ : ?m.657
you can disable implict lambdas using `@` or writing a lambda expression with `{}` or `[]` binder annotations.
-/

[Mario Carneiro]

try @(Symmetric.comap h.symmetric f)?

[Mario Carneiro]

or Symmetric.comap h.symmetric f ..

[Kevin Buzzard]

I can't get the dots one working but the @ is the trick I was missing: thanks! In fact dot notation also works: I've got this compiling

theorem Equivalence.comap' (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=
  ⟨h.reflexive.comap f, @(h.symmetric.comap f), @(h.transitive.comap f)⟩

which I think is fine.