refine_struct and opt_param

Stream: general

[Sebastien Gouezel]

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]

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]

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]

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]

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]

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]

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]

Oof, that sounds pretty fragile.

[Sebastien Gouezel]

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]

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).

[Sebastien Gouezel]

#7084

[Sebastien Gouezel]

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?

[Scott Morrison]

Looking now.

[Scott Morrison]

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]

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]

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]

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.

[Eric Wieser]

Is there any way to contruct a pexpr for a struct literal (ie, an instance of that macro) from within a tactic?

[Eric Wieser]

Eg something such that mk_literal [`foo, `bar] = ``({ foo := _, bar := _ })

[Eric Wieser]

Ah, docs#pexpr.mk_structure_instance