## Stream: general

### Topic: refine_struct and opt_param

#### Sebastien Gouezel (Apr 05 2021 at 08:16):

Is there a way to tell refine_struct to use opt_params? In

import algebra.group.defs

structure my_struct :=
(foo : ℕ)
(bar : ℕ)
(qux : ℕ := 0)
(zbg : ℕ := 1)

def some : my_struct :=
begin
refine_struct { foo := 1 },
sorry
end


I'd like to have only bar to fill by hand, but it is also asking for qux and zbg.

#### Mario Carneiro (Apr 05 2021 at 08:26):

I think it is possible, but not easy. It looks like refine_struct reimplements a decent amount of the elaborator's implementation of struct literals

#### Mario Carneiro (Apr 05 2021 at 08:27):

you would basically have to look up whether any of the fields are opt_params or auto_params and apply the appropriate tactic

#### Sebastien Gouezel (Apr 05 2021 at 08:44):

It turns out that in my application just adding a field qux := _ is enough to do the trick (it is then filled by the command intros; ext; try { refl }; which is supposed to fill all the remaining fields, and picks somehow the opt_param).

#### Floris van Doorn (Apr 05 2021 at 14:50):

Is there a reason why

def some : my_struct :=
begin
refine { foo := 1, .. },
sorry
end


is not satisfactory? This version does use opt_params.

#### Sebastien Gouezel (Apr 05 2021 at 16:36):

It really depends on the situation. Sometimes refine works but refine_struct doesn't, sometimes the opposite, and I really can't say why (the status of metavariables at the end of both constructs is not the same, so it depends on what the rest of the proof does). Anyway, things are progressing steadily (see branch#nsmul_data) -- the only thing I have not been able to fix properly for now is in ordinal_notation, but I'm far from being done.

#### Sebastien Gouezel (Apr 05 2021 at 16:40):

For instance, I've just replaced

instance : monoid (M →ₗ[R] M) :=
by refine {mul := (*), one := 1, ..}; { intros, apply linear_map.ext, simp {proj := ff} }


which was failing with the message tactic failed, result contains meta-variables, by

instance : monoid (M →ₗ[R] M) :=
by refine_struct {mul := (*), one := (1 : M →ₗ[R] M), nspow := _};
intros; try { refl }; apply linear_map.ext; simp {proj := ff}


#### Floris van Doorn (Apr 05 2021 at 18:26):

Oof, that sounds pretty fragile.

#### Sebastien Gouezel (Apr 05 2021 at 19:22):

Yes. The refactor would be much easier if refine and refine_struct had a better behavior with respect to metavariables and autoparams, but since I have absolutely no clue at how they work, I just go the stupid way of fixing everything along the way (which is not so bad).

#### Sebastien Gouezel (Apr 05 2021 at 19:30):

Just to show the kind of things one gets with this refactor. In the file monoid_algebra.lean, there are the lines

While we were not able to define add_monoid_algebra k G = monoid_algebra k (multiplicative G) due
to definitional inconveniences, we can still show the types are isomorphic.


So I just checked, and with the new definitions the definitional inconvenience is gone:

lemma it_works [semiring k] [has_add G] : add_monoid_algebra k G = monoid_algebra k (multiplicative G) := rfl


(And I haven't done anything special about it in this file, it's just that things are better definitionally now).

#7084

#### Sebastien Gouezel (Apr 07 2021 at 12:53):

I'd need some help on this from someone who knows its category theory library, because a proof becomes too slow after the change. The reason is probably that there are now more fields in rings, so it slows down some proofs, and a proof that was on the edge just becomes too slow. @Scott Morrison , maybe?

Looking now.

#### Scott Morrison (Apr 07 2021 at 13:46):

Okay, I've fixed this --- but only by dividing the two failing defs up into their constituent parts, not by actually understanding and fixing the slow-down.

#### Scott Morrison (Apr 07 2021 at 13:54):

While I'm completely in favour of this PR, I hope we're not suffering from Stockholm syndrome regarding "forgetful inheritance" here: it is a disappointing failure of Lean that we have to do this in mathlib, and we should hope that some magical future theorem prover makes this design issue irrelevant.

#### Sebastien Gouezel (Apr 07 2021 at 13:58):

I completely agree with that: ideally, we could register subsingletons instances so that the kernel considers them as defeq from this point on.

#### Sebastien Gouezel (Apr 07 2021 at 14:00):

Scott Morrison said:

Okay, I've fixed this --- but only by dividing the two failing defs up into their constituent parts, not by actually understanding and fixing the slow-down.

Thanks! I just checked, and the original proof is also very slow on master, so the PR is not changing so much here.

Last updated: May 13 2021 at 21:12 UTC