Zulip Chat Archive

Stream: general

Topic: refine_struct and opt_param


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

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

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

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

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

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

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

view this post on Zulip Floris van Doorn (Apr 05 2021 at 18:26):

Oof, that sounds pretty fragile.

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

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

view this post on Zulip Sebastien Gouezel (Apr 07 2021 at 10:58):

#7084

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

view this post on Zulip Scott Morrison (Apr 07 2021 at 12:54):

Looking now.

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

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

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

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