Zulip Chat Archive

Stream: general

Topic: How do I configure an `equiv` to work with `simps`?

Scott Morrison (Apr 06 2021 at 09:40):

For example, in

import topology.instances.real
import topology.algebra.group_with_zero

noncomputable theory

/-- The map `λ x, a * x + b`, as a homeomorphism from `ℝ` to itself, when `a ≠ 0`. -/
def affine_homeo (a b : ) (h : a  0) :  ≃ₜ  :=
{ to_fun := λ x, a * x + b,
  inv_fun := λ y, (y - b) / a,
  left_inv := λ x, by { simp only [add_sub_cancel], exact mul_div_cancel_left x h, },
  right_inv := λ y, by { simp [mul_div_cancel' _ h], }, }

@[simps] doesn't generate the lemmas I want: they look like

[simps] > adding projection affine_homeo_to_equiv_apply:
        >  (a b : ) (h : a  0) (x : ), ((affine_homeo a b h).to_equiv) x = a * x + b

whereas I'd prefer just

@[simp] lemma affine_homeo_apply (a b : ) (h : a  0) (x : ) :
  affine_homeo a b h x = a * x + b := rfl

Is there some magic incantation that will cause simps to do this in the first place? @Floris van Doorn?

Johan Commelin (Apr 06 2021 at 09:44):

Do you need something like

initialize_simps_projections homeo (to_fun  apply)

Eric Wieser (Apr 06 2021 at 09:45):

It looks like ≃ₜ is missing a has_coe_to_fun?

Eric Wieser (Apr 06 2021 at 09:46):

https://leanprover-community.github.io/mathlib_docs/notes.html#function%20coercion may be relevant. I don't know what ≃ₜ is so can't look at the docs for it

Johan Commelin (Apr 06 2021 at 09:47):

I think it's homeomorph (test: docs#homeomorph)

Johan Commelin (Apr 06 2021 at 09:48):


Eric Wieser (Apr 06 2021 at 09:50):

I think this is because homeomorph is not an old_structure_cmd like the other equivs

Eric Wieser (Apr 06 2021 at 09:51):

But your suggestion may still work

Floris van Doorn (Apr 06 2021 at 15:46):

This is unfortunately not supported yet.
As Eric said, the reason is that homeomorph is not an old_structure_cmd, so therefore, there is no single projection homeomorph a b -> (a -> b). Therefore, to support this, simps would have to look at a composition of projections and a custom projection for that. That is not supported yet, but it is at the top of the list of #5489. I'll see if I can implement it soon(ish).

Kevin Buzzard (Apr 06 2021 at 16:03):

Why don't we make all structures old structures?

Floris van Doorn (Apr 07 2021 at 03:30):

This is implemented in #7074.
still have to test it in some examples of mathlib.

Are there other structures like homeomorph that extend a structure without old_structure_cmd and that have a coercion to functions?

Eric Wieser (Apr 07 2021 at 07:09):

docs#rel_embedding, and probably everything in that file

Yury G. Kudryashov (Apr 09 2021 at 00:39):


Last updated: Aug 03 2023 at 10:10 UTC