Zulip Chat Archive

Stream: general

Topic: simps and new structure cmd


view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 22:46):

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

view this post on Zulip Yury G. Kudryashov (Dec 22 2020 at 22:49):

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

view this post on Zulip 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?

view this post on Zulip 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)
-- ^^^^^^^^^^^^^^^^^

view this post on Zulip 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 _)

view this post on Zulip Eric Wieser (Dec 23 2020 at 23:31):

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

view this post on Zulip Yury G. Kudryashov (Dec 23 2020 at 23:33):

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

view this post on Zulip Yury G. Kudryashov (Dec 23 2020 at 23:34):

@Floris van Doorn ?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Floris van Doorn (Dec 24 2020 at 00:47):

Related issue: #3837

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip Eric Wieser (Dec 24 2020 at 09:13):

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

view this post on Zulip Eric Wieser (Dec 24 2020 at 09:13):

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

view this post on Zulip Eric Wieser (Dec 24 2020 at 09:15):

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

view this post on Zulip Yury G. Kudryashov (Dec 24 2020 at 21:01):

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

view this post on Zulip 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