Unfolding Definitions

Stream: Berkeley Lean Seminar

[Thomas Browning]

I was playing around with unfolding definitions and I was getting a little stuck. For example,

example : 0 ≤ 1 :=
begin
    dsimp[(≤)],
end

turns the goal into

⊢ 0.less_than_or_equal 1

but after that, how would you unfold/unravel the definition of "less_than_or_equal_to"?

[Kevin Buzzard]

Right click on the definition and peek it to see what it is.

[Kevin Buzzard]

If you know how something is defined, it's much easier to figure out how to deal with it.

[Kevin Buzzard]

Oh -- you'll have to write #check nat.less_than_or_equal -- we are still a couple of pull requests away from being able to click on stuff in the goal (it's coming soon)

[Thomas Browning]

Great, thanks!

[Kevin Buzzard]

So do you understand the definition?

[Thomas Browning]

I understand what it's doing, although I'm not familiar with some of the words/symbols used

[Kevin Buzzard]

The only command being used is inductive -- everything else is being defined. Did you look at chapter 7 of #tpil on inductive types?

[Thomas Browning]

I'll take a look at that. I guess I was asking more about unfolding definitions in general, rather than this specific one.

[Kevin Buzzard]

If you write #print prefix nat.less_than_or_equal you'll see all the things generated when Lean made that inductive type, but most of them were generated by a computer and are of no relevance to you. The key things are rec, refl and step; everything else is made from them.

[Kevin Buzzard]

To deal with unfolding in general you need to know what's going on. The techniques vary depending on what the thing you're trying to get to the bottom of is.

[Thomas Browning]

Got it

[Kevin Buzzard]

unfold X means something like simp only [X._equation_lemma_1, X._equation_lemma_2, ...] so it only works for things with equation lemmas, e.g. a definition made using the equation compiler and some other definitions. I'm not sure there's a general answer to your question. Often if you look at the definition of something then directly after it there's a lemma proved which shows you how to unfold the thing using a rewrite.

[Patrick Lutz]

My understanding is also that dsimp does things like $\beta$-reduction. Is that correct?

[Kevin Buzzard]

Yes I think it does, although you might be able to switch this off somehow with some option to dsimp

[Patrick Lutz]

What if you only want to do $\beta$-reduction and nothing else?

[Kevin Buzzard]

You can do it manually with change, or there might be some options to simp, or there will be some weird way of doing it using some meta command which does precisely beta reduction. You could ask in #general, preferably with an explicit example

[Kyle Miller]

Patrick Lutz said:

What if you only want to do $\beta$-reduction and nothing else?

I don't know exactly what it does, but dsimp only (short for dsimp only []) does $\beta$-reductions and seemingly little (if anything) else. I've been using @Kevin Buzzard's suggestion of change, too, for getting things into the right form. The convert_to tactic looks interesting, but I haven't tried it yet.

[Kyle Miller]

Kevin Buzzard said:

Right click on the definition and peek it to see what it is.

I haven't understood why it looks like

inductive less_than_or_equal (a : ℕ) : ℕ → Prop
| refl : less_than_or_equal a
| step : Π {b}, less_than_or_equal b → less_than_or_equal (succ b)

rather than something like

inductive my_less_than_or_equal : ℕ → ℕ → Prop
| refl {a} : my_less_than_or_equal a a
| step {a b} : my_less_than_or_equal a b → my_less_than_or_equal a (succ b)

Is it just a matter of taste to factor out the a? (I've seen this pattern elsewhere in the standard library and mathlib, too.)

[Kevin Buzzard]

Yes I think it's just a matter of taste. You could ask the experts to make sure