Definitional reductions for recursive definitions

Stream: new members

[Henry Towsner]

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]

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]

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]

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]

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]

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

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

[Yaël Dillies]

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]

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]

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]

Thanks! That was exactly what I was looking for.

[Adam Topaz]

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
1
(λn i, 2*i)

@[simp]
lemma pow2_zero : pow2 0 = 1 := rfl

@[simp]
lemma pow2_succ (n) : pow2 (n+1) = 2 * pow2 n := rfl