simps and new structure cmd

Stream: general

[Yury G. Kudryashov]

How do I customize simps projections for new-style structures like docs#homeomorph?

[Yury G. Kudryashov]

I want to generate simp lemmas at least for apply and symm_apply.

[Yury G. Kudryashov]

Another question about simps: can I generate both simp lemmas for non-applied coercions and non-simp lemmas for applied coercions?

[Johan Commelin]

@Yury G. Kudryashov I only know simps via cargo cult, but are you looking for something like this:

structure locally_constant (X Y : Type*) [topological_space X] :=
(to_fun : X → Y)
(is_locally_constant : is_locally_constant to_fun)

namespace locally_constant

instance : has_coe_to_fun (locally_constant X Y) := ⟨_, locally_constant.to_fun⟩

initialize_simps_projections locally_constant (to_fun → apply)
-- ^^^^^^^^^^^^^^^^^

[Yury G. Kudryashov]

I found the code for equiv. The problem with homeomorph is that there is no homeomorph.to_fun, only equiv.to_fun (homeomorph.to_equiv _)

[Eric Wieser]

Can you add a custom simps projection like docs#equiv.simps.inv_fun?

[Yury G. Kudryashov]

I don't know how should I name them to make attr#simps recognize them.

[Yury G. Kudryashov]

@Floris van Doorn ?

[Eric Wieser]

At a guess, adding a lemma homeomorph.simps.to_equiv with a lemma statement of what you expect apply to be might make progress

[Floris van Doorn]

I'm afraid that @[simps] currently doesn't support making a custom projection that is a composition of two projections.
If I understand correctly, you have the following problem: right out of the box @[simps] will state lemmas using ⇑(f.to_equiv), and you want them to be stated using ⇑f. These are definitionally equal, but not syntactically so.

Let me see if I can add the functionality to @[simps] (at some point). Can you give me an explicit example (maybe from the library) of a definition and the precise simp lemmas you want to generate?

[Floris van Doorn]

Related issue: #3837

[Floris van Doorn]

Question: does using old_structure_cmd for homeomorph break other things? It would at least "solve" this problem.

[Yury G. Kudryashov]

You can take any definition about homeomorph (e.g., docs#homeomorph.trans). I want to have ⇑(h₁.trans h₂) x = h₂ (h₁ x) and ⇑(h₁.trans h₂).symm x = h₁.symm (h₂.symm x).

[Yury G. Kudryashov]

Ideally, I want to have the following lemmas (possibly, with other names):

import topology.homeomorph

namespace homeomorph

variables {α β γ : Type*} [topological_space α] [topological_space β] [topological_space γ] (hab : α ≃ₜ β) (hbc : β ≃ₜ γ)

@[simp] lemma trans_to_equiv (hab.trans hbc).to_equiv = hab.to_equiv.trans hbc.to_equiv := rfl

@[simp] lemma coe_trans : ⇑(hab.trans hbc) = hbc ∘ hab := rfl

@[simp] lemma coe_trans_symm : ⇑(hab.trans hbc).symm = hab.symm ∘ hbc.symm := rfl

lemma trans_apply (x) : hab.trans hbc x = hbc (hab x) := rfl

lemma trans_symm_apply (x) : (hab.trans hbc).symm x = hab.symm (hbc.symm x) := rfl

[Eric Wieser]

Presumably ideally you'd like the entire api of equiv to be duplicated on your type?

[Eric Wieser]

Which sounds like the same pain point as we have with the _hom structures

[Eric Wieser]

Having no polymorphism associated with the extends feature seems to be a recurring pain

[Yury G. Kudryashov]

Here I'm not talking about this problem. It's about @[simps]

[Yury G. Kudryashov]

homeomorph.trans is just an example. Actually, I'm more interested in definitions like sin_local_homeomorph