Unfold all definitions

Stream: new members

[Henning Dieterichs]

I'm spending much of my time figuring out which definition is reducible and can be unfolded. Often I just want to unfold everything that can be unfolded until I need "cases" to continue unfolding more definitions.
Is there a tactic that unfolds all definitions that can be unfolded (but not more than n to fix termination issues)?

[Mario Carneiro]

simp!

[Mario Carneiro]

at least, that's my understanding of what that does

[Henning Dieterichs]

simp! does not seem to work for me... It just fails.

[Mario Carneiro]

do you have a #mwe?

[Henning Dieterichs]

def f1 (x: nat) := x
def f2 (x: nat) := f1 x
def f3 (x: nat) := f2 x
def f4 (x: nat) := f3 x

lemma f (x: nat): f4 x = x :=
begin
    rw f4,
    rw f3,
    rw f2,
    rw f1,
end

[Henning Dieterichs]

I'm looking for a better way to prove f than just rewriting all the definitions. finish does the job, but in my actual scenario, finish cannot close the goal, so it fails

[Henning Dieterichs]

simp! and simp fails directly

[Mario Carneiro]

refl?

[Henning Dieterichs]

Does work here, but not in my case. Better mwe:

def f1 (x: nat) := x
def f2 (x: nat) := if f1 x = x then x else 0
def f3 (x: nat) := if f2 x = x then x else 0
def f4 (x: nat) := if f3 x = x then x else 0

lemma f (x: nat): f4 x = x :=
begin
    unfold f4,
    unfold f3,
    unfold f2,
    unfold f1,
    simp
end

[Mario Carneiro]

The ! seems to like equation compiler definitions specifically:

def f1 : ℕ → ℕ | (x: nat) := x
def f2 : ℕ → ℕ | (x: nat) := f1 x
def f3 : ℕ → ℕ | (x: nat) := f2 x
def f4 : ℕ → ℕ | (x: nat) := f3 x

lemma f (x: nat): f4 x = x :=
by simp!

[Mario Carneiro]

I think the recommendation is just simp [f1,f2,f3,f4], or local attribute [simp] f1 f2 f3 f4 then simp

[Kevin Buzzard]

If you make definitions then you're responsible for making the API to make those definitions usable, right? Isn't that the philosophy? Isn't what's happening here that eg f2 is made with no API so anything that mentions it directly or indirectly is going to be hard to use. Shouldn't one be training simp here or something?

[Henning Dieterichs]

What do you mean with API? I'm quite new to lean ;) How would one make fn more usable? Do you mean putting attribute [simp] to it?

[Reid Barton]

I agree with Kevin but, in this case, you can also use (with mathlib) conv_lhs { whnf } to reduce all the definitions away

[Kevin Buzzard]

I mean that if you look at any definition in mathlib, say the cardinality of a finite set, then after one definition there are 20 theorems which enable you to use the definition without having to unfold it.

[Kevin Buzzard]

Those theorems are the API, or the interface, to the object. It's like when we define addition in the natural number game and then prove associativity and commutativity and about four other things. Then you can tag stuff with simp and get the simplifier to do all the dirty work for you

[Mario Carneiro]

Generally if you have to unfold more than one layer of definitions in a given theorem then you don't have enough API theorems

[Kevin Buzzard]

Kenny has impressed upon me the principle that if you're unfolding a definition, you're doing it wrong, unless you're making the API directly after the definition

[Mario Carneiro]

for example, in your mwe before proving f4 x = x we would first prove f1 x = x, f2 x = x and f3 x = x; that way in each theorem we only have one function to unfold

[Henning Dieterichs]

I see. In my case, I often have to unfold _match_n and custom map functions (I'm doing program verification - I somehow feel that program verification usually has less depth than math, but one has to deal with a lot more of definitions)

[Mario Carneiro]

In program verification you should probably just mark all your definitions as @[simp] def ...

[Kevin Buzzard]

There's a reason that hardly anyone uses multisets and yet data.multiset is (or at least was) thousands of lines long -- this stuff is used in the definition of finite sets and it's all API.

[Henning Dieterichs]

:D

[Mario Carneiro]

at least for definitions by pattern matching, that's pretty much always what you want. For definitions not by pattern matching you may want to be more controlled, but these definitions are more rare, stuff like the definition of a hoare triple

[Henning Dieterichs]

thank you for all your input! I think it might really help me if I try to provide more "trivial" lemmas for low-level stuff that just make simplification easier. I guess efficient usage of simp is a real art to learn.