Zulip Chat Archive

Stream: general

Topic: can meta `def`?


view this post on Zulip Johan Commelin (Sep 05 2018 at 18:40):

Can you have meta code that writes definitions and lemmas for you? Probably yes, and this is how things like to_additive work. Is that right?

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:42):

Is this somehow what add_decl is for?

view this post on Zulip Simon Hudon (Sep 05 2018 at 18:46):

Yes it is

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:47):

Ok cool! I could imagine some uses for it.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:47):

For example, you define multiplication of matrices, and immediately afterwards, there is a simp-lemma mul_val. This happens a lot. Couldn't we auto-generate those?

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:48):

I feel like at least half of the simp lemmas after definitions could be auto-generated.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:50):

Here is a claim: every lemma that is proved by rfl is a good candidate for being auto-generated.

view this post on Zulip Simon Hudon (Sep 05 2018 at 18:50):

Yes, they can be generated. But could it be that you could get rid of the lemmas altogether by tagging your definition as simp?

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:50):

Hmm, I think usually there is notation introduced in between.

view this post on Zulip Simon Hudon (Sep 05 2018 at 18:54):

But the notation doesn't affect rewriting.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:55):

Hmm... then I'm just really confused.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:56):

Take https://github.com/leanprover-community/mathlib/blob/noetherian/ring_theory/ideals.lean#L176 for example.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:56):

Those lines have completely predictable names (even to me), and are completely boring statements.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:56):

I would definitely forget to write them, until I need the after 50 other lines, and then only write half of them.

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:58):

Do you think stuff like this could be automated?

view this post on Zulip Johan Commelin (Sep 05 2018 at 18:59):

Maybe the question is to general...

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:00):

I think the issue there is the combination of coe (which comes from a type class) and its underlying definition.

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:00):

At least I got an answer to the original question. And I am glad that it was positive. I'll keep it in mind, because I'm sure it will come in handy at some point.

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:00):

It is not as trivial as I thought but there might be something to do with it.

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:02):

In general, maybe the question is to do simp lemmas from a type class instance which is just built on top of stand alone definitions

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:04):

If you have

instance : my_class my_type :=
{ op := my_type.op }

we can take all the equations of my_type.op, replace the occurrences of my_type.op with my_class.op and label the result as simp

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:05):

Right. That sounds useful. But I don't know what the experts think (-;

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:06):

More import still: does it seem like a generalization of the problem you were asking about?

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:08):

Yes, I think so... although there might also be other cases. For example https://github.com/leanprover/mathlib/pull/316/files#diff-dcac36203421953a8cefa07fecd35a79R71 might be enhanced to also define a functor along the way.

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:08):

But I'm not suggesting that these are special cases of one sort of automation.

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:09):

It is just that they could both benefit from some add_decl if I'm not mistaken.

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:11):

If you want, I can walk you through the construction of the solution I suggested and then we can see if something similar can be done for your second example

view this post on Zulip Johan Commelin (Sep 05 2018 at 19:14):

Ok, would definitely like to do that. But maybe not tonight (-; I need to catch up with some sleep, so I'll be gone in a couple of minutes.

view this post on Zulip Simon Hudon (Sep 05 2018 at 19:15):

Sure, let me know when you're ready and I'll give you a hand

view this post on Zulip Johannes Hölzl (Sep 05 2018 at 19:28):

Just for your information: Isabelle has a tool called lift_definition which lifts a term along subtypes / quotients / other relations etc.
If one wants to define a function lift f : {a : A // p a} -> {b : B // q b}, it provides one with the following two goals:
the function itself: f : A -> B and a proof forall a : A, p a -> q (f b). The nice thing is that this also works for quotients, but in Isabelle this is done by assuming that there is a canonical projection (i.e. quot.out) which we may want to avoid, and instead use a more generic lifting constant.

My idea for a lift function would be: get typing information (which includes the information for which types the representation should change) and the term to lift. Then it puts lift or cases around the term to translate into the other type. All further proofs are left as subgoals to the user. Finally it produces the constant itself, and a rewrite rule which adds coercions etc at all places necessary to remove all lift constants.


Last updated: May 14 2021 at 02:15 UTC