# Zulip Chat Archive

## Stream: general

### Topic: simps and new structure cmd

#### Yury G. Kudryashov (Dec 22 2020 at 22:46):

How do I customize `simps`

projections for new-style structures like docs#homeomorph?

#### Yury G. Kudryashov (Dec 22 2020 at 22:49):

I want to generate `simp`

lemmas at least for `apply`

and `symm_apply`

.

#### Yury G. Kudryashov (Dec 22 2020 at 22:49):

Another question about `simps`

: can I generate both `simp`

lemmas for non-applied coercions and non-simp lemmas for applied coercions?

#### Johan Commelin (Dec 23 2020 at 06:44):

@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 (Dec 23 2020 at 23:23):

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 (Dec 23 2020 at 23:31):

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

#### Yury G. Kudryashov (Dec 23 2020 at 23:33):

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

#### Yury G. Kudryashov (Dec 23 2020 at 23:34):

@Floris van Doorn ?

#### Eric Wieser (Dec 23 2020 at 23:38):

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 (Dec 24 2020 at 00:47):

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 (Dec 24 2020 at 00:47):

Related issue: #3837

#### Floris van Doorn (Dec 24 2020 at 00:52):

Question: does using `old_structure_cmd`

for `homeomorph`

break other things? It would at least "solve" this problem.

#### Yury G. Kudryashov (Dec 24 2020 at 04:37):

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 (Dec 24 2020 at 04:38):

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 (Dec 24 2020 at 09:13):

Presumably ideally you'd like the entire api of `equiv`

to be duplicated on your type?

#### Eric Wieser (Dec 24 2020 at 09:13):

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

structures

#### Eric Wieser (Dec 24 2020 at 09:15):

Having no polymorphism associated with the `extends`

feature seems to be a recurring pain

#### Yury G. Kudryashov (Dec 24 2020 at 21:01):

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

#### Yury G. Kudryashov (Dec 24 2020 at 21:03):

`homeomorph.trans`

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

Last updated: May 11 2021 at 00:31 UTC