pretty printing Equiv

Stream: mathlib4

[Scott Morrison]

In

/-- `LeftInverse g f` means that g is a left inverse to f. That is, `g ∘ f = id`. -/
def LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x

/-- `RightInverse g f` means that g is a right inverse to f. That is, `f ∘ g = id`. -/
def RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv (α : Sort _) (β : Sort _) where
  toFun : α → β
  invFun : β → α
  left_inv : LeftInverse invFun toFun
  right_inv : RightInverse invFun toFun

infixl:25 " ≃ " => Equiv

namespace Equiv

instance : CoeFun (α ≃ β) fun _ => α → β := ⟨toFun⟩

protected def symm (e : α ≃ β) : β ≃ α := ⟨e.invFun, e.toFun, e.right_inv, e.left_inv⟩

@[simp] theorem apply_symm_apply (e : α ≃ β) (x : β) : e (e.symm x) = x := _

The goal at the final _ pretty prints as toFun e (toFun (Equiv.symm e) x) = x rather than just as e (e.symm x). That is, it doesn't use either the coercion or the dot notation in pretty printing. I hadn't really noticed this before. What can we do about this?

[Eric Wieser]

Does attribute [coe] Equiv.toFun help?

[Scott Morrison]

No, that results in toFun e x being printed as ↑x, which isn't what we want at all. @Gabriel Ebner, do you know if we have a solution for this?

[Mario Carneiro]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Please.20stop.20adding.20generalized.20API.20around.20coercions/near/311508319

[Gabriel Ebner]

You should probably implement FunLike for Equiv.

[Scott Morrison]

We have

instance : EquivLike (α ≃ β) α β where
  coe := toFun
  inv := invFun
  left_inv := left_inv
  right_inv := right_inv
  coe_injective' e₁ e₂ h₁ h₂ := by cases e₁; cases e₂; congr

[Eric Rodriguez]

it already has it @Gabriel Ebner

[Scott Morrison]

Oh, so maybe we need to remove the instance : CoeFun (α ≃ β) fun _ => α → β := ⟨toFun⟩ that comes immediately afterwards.

[Scott Morrison]

That causes a few errors, but it's clear the coercion already exists.

[Gabriel Ebner]

Right, we want all function coercions of FunLike things to be FunLike.coe.

[Scott Morrison]

Things are looking better. Still one error. I had to add Simps.apply in

/-- See Note [custom simps projection] -/
def Simps.apply (e : α ≃ β) : α → β := e
def Simps.symm_apply (e : α ≃ β) : β → α := e.symm

[Kevin Buzzard]

Does it lint yet?

[Scott Morrison]

Adding

theorem left_inv' (e : α ≃ β) : Function.LeftInverse e.symm e := e.left_inv
theorem right_inv' (e : α ≃ β) : Function.RightInverse e.symm e := e.right_inv

(i.e. written in terms of the coercions) allows fixing the last errors.

[Arien Malec]

This explains some weird issues I was seeing in Mathlib4#674

[Mario Carneiro]

The coe delaborator bug has been fixed in Std

[Eric Wieser]

Scott Morrison said:

Adding

theorem left_inv' (e : α ≃ β) : Function.LeftInverse e.symm e := e.left_inv
theorem right_inv' (e : α ≃ β) : Function.RightInverse e.symm e := e.right_inv

(i.e. written in terms of the coercions) allows fixing the last errors.

I'm pretty sure we already have those lemmas with different names

[Eric Wieser]

docs#equiv.left_inverse_symm