Zulip Chat Archive
Stream: general
Topic: can meta `def`?
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?
Johan Commelin (Sep 05 2018 at 18:42):
Is this somehow what add_decl is for?
Simon Hudon (Sep 05 2018 at 18:46):
Yes it is
Johan Commelin (Sep 05 2018 at 18:47):
Ok cool! I could imagine some uses for it.
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?
Johan Commelin (Sep 05 2018 at 18:48):
I feel like at least half of the simp lemmas after definitions could be auto-generated.
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.
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?
Johan Commelin (Sep 05 2018 at 18:50):
Hmm, I think usually there is notation introduced in between.
Simon Hudon (Sep 05 2018 at 18:54):
But the notation doesn't affect rewriting.
Johan Commelin (Sep 05 2018 at 18:55):
Hmm... then I'm just really confused.
Johan Commelin (Sep 05 2018 at 18:56):
Take https://github.com/leanprover-community/mathlib/blob/noetherian/ring_theory/ideals.lean#L176 for example.
Johan Commelin (Sep 05 2018 at 18:56):
Those lines have completely predictable names (even to me), and are completely boring statements.
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.
Johan Commelin (Sep 05 2018 at 18:58):
Do you think stuff like this could be automated?
Johan Commelin (Sep 05 2018 at 18:59):
Maybe the question is to general...
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.
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.
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.
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
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
Johan Commelin (Sep 05 2018 at 19:05):
Right. That sounds useful. But I don't know what the experts think (-;
Simon Hudon (Sep 05 2018 at 19:06):
More import still: does it seem like a generalization of the problem you were asking about?
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.
Johan Commelin (Sep 05 2018 at 19:08):
But I'm not suggesting that these are special cases of one sort of automation.
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.
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
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.
Simon Hudon (Sep 05 2018 at 19:15):
Sure, let me know when you're ready and I'll give you a hand
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: Dec 20 2023 at 11:08 UTC