issue #1639: `to_additive` should copy `simps` and `exten...

Stream: triage

[Random Issue Bot]

Today I chose issue 1639 for discussion!

to_additive should copy simps and extensionality
Created by @Scott Morrison (@semorrison) on 2019-10-31
Labels: feature-request, meta

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 1639 for discussion!

to_additive should copy simps and extensionality
Created by @Scott Morrison (@semorrison) on 2019-10-31
Labels: meta, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

[Alex J. Best]

I think this is closed by #5487 as @Floris van Doorn said there, @Scott Morrison is there anything else you can think of that to_additive should be able to do but can't right now?

[Heather Macbeth]

I tried to to_additive-ize has_continuous_smul to has_continuous_vadd the other day and couldn't get anything working ... but I didn't investigate why it didn't work, nor do I know whether it's supposed to be in scope.

[Alex J. Best]

The definition of the class won't work as its a structure I think, but any subsequent lemmas should work.

[Alex J. Best]

In order to generate structures properly in a nice way I think lean core has to be modified to expose some more functions to tactics.

[Heather Macbeth]

I did try it that way, and I believe it still failed. Let me try to reconstruct.

[Heather Macbeth]

@[to_additive] failed. Type mismatch in additive declaration.
For help, see the docstring of `to_additive.attr`, section `Troubleshooting`.
Failed to add declaration
<theorem filter.tendsto.vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [_inst_1 : topological_space M]
[_inst_2 : topological_space α] [_inst_3 : has_vadd M α] [_inst_4 : has_continuous_smul M α] {f : β → M}
{g : β → α} {l : filter β} {c : M} {a : α},
  tendsto f l (𝓝 c) → tendsto g l (𝓝 a) → tendsto (λ (x : β), f x +ᵥ g x) l (𝓝 (c +ᵥ a)) := λ
{M : Type u_1} {α : Type u_2} {β : Type u_3} [_inst_1 : topological_space M] [_inst_2 : topological_space α]
[_inst_3 : has_vadd M α] [_inst_4 : has_continuous_smul M α] {f : β → M} {g : β → α} {l : filter β} {c : M}
{a : α} (hf : tendsto f l (𝓝 c)) (hg : tendsto g l (𝓝 a)),
  (continuous_smul.tendsto (c, a)).comp (hf.prod_mk_nhds hg)>

Nested error message:

type mismatch at application
  @has_continuous_smul M α _inst_3
term
  _inst_3
has type
  has_vadd M α
but is expected to have type
  has_scalar M α

[Heather Macbeth]

branch#has_continuous_vadd

[Heather Macbeth]

Let me know if I'm doing it wrong!

[Alex J. Best]

Ah the problem is that to_additive doesn't know its meant to turn has_continuous_smul into has_continuous_vadd, if you add attribute [to_additive has_continuous_vadd] has_continuous_smul after you've manually defined has_continuous_vadd, I believe the filter lemma below will to_additive properly

[Heather Macbeth]

#10227

Thanks @Alex J. Best!

[Floris van Doorn]

Yes, this issue is resolved, I closed it.