automatic simp lemmas

Stream: general

[Reid Barton]

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]

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]

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

[Reid Barton]

But now I have a pseudo-spec

[Johan Commelin]

See also https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/sheaves.20and.20sites/near/148770849 for something that might qualify as pre-semi-pseudo-spec.

[Johan Commelin]

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]

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]

@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?

[Johan Commelin]

(deleted)

[Simon Hudon]

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

[Johan Commelin]

@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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Sounds cool btw!

[Keeley Hoek]

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

[Sebastian Ullrich]

tk "private rfl_lemma"

omg

[Kevin Buzzard]

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

[Johan Commelin]

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]

@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]

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

[Sebastian Ullrich]

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

[Keeley Hoek]

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

[Keeley Hoek]

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]

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

[Keeley Hoek]

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]

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?

[Sebastian Ullrich]

Right... oops

[Keeley Hoek]

:D

[Keeley Hoek]

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]

BTW, here's a "live demo"

[Keeley Hoek]

(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]

Nice. Any reason it's not an attribute?

[Keeley Hoek]

That's cool

[Keeley Hoek]

@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]

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]

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.