Zulip Chat Archive

Stream: new members

Topic: Definitional reductions for recursive definitions

Henry Towsner (May 01 2023 at 22:55):

When I define something by recursion, it's defined by what the lean reference calls the definitional reductions,

 F (constructor a b) = f b ... (λ d : δᵢⱼ, F (b d)) ...

Is there an easy way to get these definitional reductions in a way that can be passed to rw or simp or the like?

They're easy to prove using the constructor tactic, but the only way I've found to do that is to manually prove n trivial lemmas, one for each constructor, after each inductive definition. On the other hand, things like rw F, unfold F, or simp [F] all replace F with the whole recursive definition, which is inconvenient when there are inductive hypotheses stated interms of F.

Kevin Buzzard (May 01 2023 at 23:05):

Is this lean 3 or lean 4? In either case probably the correct answer is that if you're making the definition then it's your job to make the API, so state the things you want, give them good names, prove them with rfl and tag them with simp, and Bob's your uncle.

Kevin Buzzard (May 01 2023 at 23:07):

You might find that prepending @[simps] to your definition does some of this automatically -- you can check what it did with whatsnew in in lean 4 and #print prefix <declname> in Lean 3

Henry Towsner (May 01 2023 at 23:42):

It's lean 3. I take it @[simps] is lean 4 only for definitions (it's telling me the target is not a structure when I try to add it). Is there a lean 3 analog?

Yaël Dillies (May 01 2023 at 23:47):

Yes, it's @[simps]. You will have to give us more context on what you're doing, in particular on what the type of F is.

Henry Towsner (May 01 2023 at 23:57):

For a simple example, say I want to define the 2^n operation inductively on nat, by

def pow2 (n:nat) : nat :=
nat.rec_on n
(λn i, 2*i)

The equality I'd expect to get in this case is pow2 (succ n) = 2*(pow 2 n). (Of course I can prove it manually very easily, but once there are more constructors and a lot of inductive definitions, it starts to get tedious, and given that these equalities are literally the definition of what the recursor is supposed to do, I was hoping there was an easier way to get them.)

Yaël Dillies (May 01 2023 at 23:59):

In fact, they are already autogenerated. Do #print prefix pow2

Yaël Dillies (May 02 2023 at 00:00):

But these equation lemmas are not meant for human consumption. The idiomatic thing to do is to rw pow2 or to write the autogenerated lemmas yourself and give them nice names.

Yaël Dillies (May 02 2023 at 00:01):

Also note that, when pattern-matching on several arguments, your cases might be unexpectedly split up. It is then wiser to write the equation lemmas yourself to keep control of the situation.

Eric Wieser (May 02 2023 at 00:27):

If you use pattern matching instead of rec_on lean writes these lemmas for you

def pow2 : nat -> nat
| 0 := 1
| (succ n) := 2*(pow2 n)

Henry Towsner (May 02 2023 at 01:00):

Thanks! That was exactly what I was looking for.

Adam Topaz (May 02 2023 at 02:35):

Hi Henry! I'm sure you have already noticed, but you don't need the constructor tactic, as these are true by definition:

def pow2 (n:nat) : nat :=
nat.rec_on n
(λn i, 2*i)

lemma pow2_zero : pow2 0 = 1 := rfl

lemma pow2_succ (n) : pow2 (n+1) = 2 * pow2 n := rfl

Last updated: Dec 20 2023 at 11:08 UTC