## Stream: general

### Topic: automatic simp lemmas

#### Reid Barton (Dec 15 2018 at 05:24):

We have a lot of simp lemmas in category theory that describe the action of functors, natural isomorphisms, etc. on various things. Johan has a few open PRs adding more of these lemmas (eg #503, #505) and they prompted me to try to understand how to describe these lemmas systematically.

#### Reid Barton (Dec 15 2018 at 05:30):

I think we can build these rfl lemmas by applying the following algorithm.

• Start with the result type LHS = RHS, where LHS is the thing being defined and RHS is its definition (this is what just putting @[simp] on the definition would do).
• If the RHS is a Prop, then just throw away the equation (do nothing).
• Otherwise, if the RHS is a record constructor { f1 := R1, f2 := R2 }, recursively produce lemmas of the form LHS.f1 = R1, LHS.f2 = R2.
• Otherwise, if the RHS is a lambda \lam x, R x, recursively produce a lemma LHS x = R x.
• Otherwise, output a simp lemma stating LHS = RHS by rfl.

#### Reid Barton (Dec 15 2018 at 05:33):

@Simon Hudon, I guess we discussed something along these lines at some point

#### Reid Barton (Dec 15 2018 at 05:38):

But now I have a pseudo-spec

#### Johan Commelin (Dec 15 2018 at 06:22):

My PR's are the result of following Mario's creed "just go for it". But I definitely wouldn't mind if this was automated away.

#### Simon Hudon (Dec 15 2018 at 16:24):

I remember this conversation. In my mind, that kind of feature might be about translating lemmas about specific definitions into lemmas referring to a type class instance.

#### Johan Commelin (Dec 15 2018 at 17:06):

@Simon Hudon I'm not sure I understand what you mean. Is it close to what Reid wrote down, or do you want something (slightly) different?

(deleted)

#### Simon Hudon (Dec 15 2018 at 18:38):

Actually, I have a hard time remembering the details of that idea. I'll try to find the conversation again

#### Johan Commelin (Dec 15 2018 at 21:00):

@Simon Hudon If you want a good showcase of what Reid and I mean, I think you should look at the file on comma categories: https://github.com/leanprover-community/mathlib/blob/over_under/category_theory/comma.lean
I just started adding over categories to the mix (a special case of comma categories), and I'm restating all the simp lemmas. The signal-to-noise ratio is increasing rapidly.

#### Simon Hudon (Dec 15 2018 at 21:03):

Ah yes! That's also what I was going for I think. The way I was generalizing it is that we want to unfold specific projections. I think I had an idea of which ones to unfold but I'd have to get back into that mindset

#### Simon Hudon (Dec 15 2018 at 21:08):

The good news is that soon, I won't have to take care of finding an apartment and I will have only Lean and my dissertation to take care of.

#### Keeley Hoek (Dec 21 2018 at 09:54):

I'm sorry if I annoyingly keep coming on about this, but I have a command which does the constructor-half of this thing and has been tested on at least one (:D) category theory structure definition. It's called rfl_lemma (you use it on its own line like rfl_lemma inverse_equivalence map---which would tell you that an inverse equivalence of an equivalence has functor going the "forward way" equal to the functor going the "backward way" in the original equivalence), and is here:
https://github.com/semorrison/lean-tidy/blob/master/src/tidy/command/rfl_lemma.lean

It took multiple iterations because it turned out that getting the types right for the lemma I needed to generate turned out to be really quite hard (at least for me). I can give some examples to elabourate this point if anyone is interested. Making it do this for every projection of a structure instead of just the specified one is trivial.

#### Keeley Hoek (Dec 21 2018 at 09:56):

rfl_lemma? is meant to tell you what the code generated was, and private rfl_lemma ... makes a private definition.

#### Johan Commelin (Dec 21 2018 at 09:56):

How much does this depend on the lean-tidy repo?

Sounds cool btw!

#### Keeley Hoek (Dec 21 2018 at 09:57):

it depends on a few pieces of the lib folder in there, let me take a look

#### Sebastian Ullrich (Dec 21 2018 at 09:57):

tk "private rfl_lemma"


omg

#### Kevin Buzzard (Dec 21 2018 at 09:58):

Is that pushing the definition of "token" a bit far or something?

#### Johan Commelin (Dec 21 2018 at 09:58):

If it doesn't depend too much on lean-tidy, I'dd say: push it to a branch on the community repo. Then we can experiment with it.

#### Sebastian Ullrich (Dec 21 2018 at 09:59):

@Kevin Buzzard It is, but I guess it actually works. Though, @Keeley Hoek, have you taken a look at the decl_meta_info parameter?

#### Keeley Hoek (Dec 21 2018 at 10:00):

No I haven't Sebastian, and thanks, now I have an idea about what it's for :D

#### Sebastian Ullrich (Dec 21 2018 at 10:01):

Yeah, I don't think your current code would have worked anyway. There is no such registered token.

#### Keeley Hoek (Dec 21 2018 at 10:01):

The thing is, I'm pretty sure it did work! I'll try...

#### Keeley Hoek (Dec 21 2018 at 10:01):

also it was before I knew I could do stuff like parse a question mark after a token, so please forgive me... :D

#### Sebastian Ullrich (Dec 21 2018 at 10:02):

It will be parsed successfully, but it will still call the regular definition with private := tt in the meta info

#### Keeley Hoek (Dec 21 2018 at 10:04):

Unless you've run it and can prove I'm crazy, I just did and I'm quiiite confident a different one of those user_commands is being called depending on private or not

#### Keeley Hoek (Dec 21 2018 at 10:05):

Does it have something to do with the fact that for user_commands, unlike user_notations, you don't need to reserve tokens for them to work?

Right... oops

:D

#### Keeley Hoek (Dec 21 2018 at 10:06):

But no reason not to fix it up so it works properly... cheers! (and I only need a single definition now, not 2^2)

#### Keeley Hoek (Dec 21 2018 at 10:07):

BTW, here's a "live demo"

#### Keeley Hoek (Dec 21 2018 at 10:07):

(RE: the original post)

structure my_str :=
(a : ℕ)

def a_cnstr (b : ℕ) : my_str := ⟨b⟩
def a_cnstr' (b : ℕ) : my_str := ⟨b + 1⟩

rfl_lemma? a_cnstr a
private rfl_lemma? a_cnstr' a


#### Sebastian Ullrich (Dec 21 2018 at 10:09):

Nice. Any reason it's not an attribute?

That's cool

#### Keeley Hoek (Dec 21 2018 at 10:13):

@Johan Commelin Based on the pieces of lib which have ended up in mathlib now, I just need the lib.expr support file. My only reluctance comes from the fact that I will have to check whether a few of the functions at the bottom of that file are already in mathlib---at the time it was less effort just to write them.

#### Keeley Hoek (Dec 21 2018 at 10:19):

One more thing if anyone doing maths actually uses it: it adds a prime to the projection name you supply, seeing if that works, before trying without. Hopefully that's convenient

#### Reid Barton (Dec 21 2018 at 19:08):

The interface I had in mind was that you'd write something like @[simp_fields] def a_cnstr ... := ..., and it would automatically generate all of the appropriate lemmas.

Last updated: May 15 2021 at 23:13 UTC