## Stream: new members

### Topic: Unfold all definitions

#### Henning Dieterichs (Nov 29 2020 at 12:26):

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 (Nov 29 2020 at 12:26):

simp!

#### Mario Carneiro (Nov 29 2020 at 12:27):

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

#### Henning Dieterichs (Nov 29 2020 at 12:28):

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

#### Mario Carneiro (Nov 29 2020 at 12:33):

do you have a #mwe?

#### Henning Dieterichs (Nov 29 2020 at 12:33):

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 (Nov 29 2020 at 12:34):

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 (Nov 29 2020 at 12:34):

simp! and simp fails directly

#### Mario Carneiro (Nov 29 2020 at 12:38):

refl?

#### Henning Dieterichs (Nov 29 2020 at 12:39):

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 (Nov 29 2020 at 12:40):

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 (Nov 29 2020 at 12:42):

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

#### Kevin Buzzard (Nov 29 2020 at 13:15):

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 (Nov 29 2020 at 13:17):

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 (Nov 29 2020 at 13:17):

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 (Nov 29 2020 at 13:20):

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 (Nov 29 2020 at 13:21):

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 (Nov 29 2020 at 13:22):

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 (Nov 29 2020 at 13:23):

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 (Nov 29 2020 at 13:23):

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 (Nov 29 2020 at 13:24):

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 (Nov 29 2020 at 13:25):

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

#### Kevin Buzzard (Nov 29 2020 at 13:25):

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.

:D

#### Mario Carneiro (Nov 29 2020 at 13:26):

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 (Nov 29 2020 at 13:30):

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.

Last updated: May 16 2021 at 05:21 UTC