# Zulip Chat Archive

## Stream: new members

### Topic: unfold and let

#### Paul Rowe (May 12 2020 at 21:33):

I'm unclear how the `let`

operator works especially in regards to unfolding a definition that uses it. I tried unfolding the definition of a recursive function called `anno`

that uses `let`

and I get something like `anno._match_1 ...`

which I have no clue what to do with. Any ideas? I can provide some code if need be, but it's embedded in a bunch of dependencies so I may have to extract a MWE.

#### Kevin Buzzard (May 12 2020 at 21:34):

Is this `let`

in term mode or tactic mode?

#### Paul Rowe (May 12 2020 at 21:34):

It's used as part of the recursive definition in term mode.

#### Kevin Buzzard (May 12 2020 at 21:35):

If you get things compiling with `sorry`

then you can just #check `anno._match_1`

to see what it is. It will be part of the recursive definition.

#### Paul Rowe (May 12 2020 at 21:43):

Hmm... I'm not sure what to do with that information now that I have it. Here's a excerpt of the definition (there are more cases):

```
def anno : Term → ℕ → ℕ × AnnoTerm
| (asp x) i := (i+1, aasp (i, i+1) x)
| (att p x) i :=
let (j, a) := anno x (i+1) in
(j+1, aatt (i, j+1) p a)
| (lseq x y) i :=
let (j, a) := anno x i in
let (k, b) := anno y j in
(k, alseq (i, k) a b)
| (bseq s x y) i :=
let (j, a) := anno x (i+1) in
let (k, b) := anno y j in
(k+1, abseq (i, k+1) s a b)
| (bpar s x y) i :=
let (j, a) := anno x (i+1) in
let (k, b) := anno y j in
(k+1, abpar (i, k+1) s a b)
```

#check `anno._match_1`

tells me its type is Plc → ℕ → ℕ × AnnoTerm → ℕ × AnnoTerm.

Basically, I'm trying to prove a property about `anno`

by induction. The unfolding gives me a goal with `anno._match_1`

which can't be unfolded further to reduce it to the inductive hypothesis.

#### Jalex Stark (May 12 2020 at 21:48):

triple backticks give you nicer code blocks, like this

```
def anno : Term → ℕ → ℕ × AnnoTerm
| (asp x) i := (i+1, aasp (i, i+1) x)
| (att p x) i :=
let (j, a) := anno x (i+1) in
(j+1, aatt (i, j+1) p a)
```

#### Jalex Stark (May 12 2020 at 21:48):

(also full definitions are usually more useful than excerpts)

#### Kenny Lau (May 12 2020 at 21:49):

as in:

```
```
[code goes here]
```
```

#### Paul Rowe (May 12 2020 at 21:50):

Haha. Yeah. I was trying to do that but messed it up. It's formatted better now, and I added the rest of the definition.

#### Kenny Lau (May 12 2020 at 21:52):

my advice is to avoid `let`

unless necessary

#### Kenny Lau (May 12 2020 at 21:52):

actually maybe it is necessary in this case

#### Jalex Stark (May 12 2020 at 21:53):

can you also post the code where your induction proof is failing?

#### Kenny Lau (May 12 2020 at 21:55):

#mwe:

```
def fib2 : ℕ → ℕ × ℕ
| 0 := (0, 1)
| (n+1) := let (a, b) := fib2 n in (b, a+b)
def fib (n : ℕ) : ℕ :=
(fib2 n).1
theorem fib_add_two (n : ℕ) : fib (n + 2) = fib (n + 1) + fib n :=
sorry
```

#### Kenny Lau (May 12 2020 at 21:55):

I actually don't know how to solve this myself

#### Paul Rowe (May 12 2020 at 21:55):

Here's the code. I'm doing things **very** explicitly for learning purposes.

```
lemma anno_range :
∀ x i,
range (prod.snd (anno x i)) = (i, prod.fst (anno x i)) :=
begin
intro x, induction x,
{ intro i, unfold anno, unfold prod.snd,
unfold prod.fst, unfold range },
{ intro i, unfold anno,}
```

I end up with the following goal:

```
1 goal
x_a : Plc,
x_a_1 : Term,
x_ih : ∀ (i : ℕ), range (anno x_a_1 i).snd = (i, (anno x_a_1 i).fst),
i : ℕ
⊢ range (anno._match_1 x_a i (anno x_a_1 (i + 1))).snd = (i, (anno._match_1 x_a i (anno x_a_1 (i + 1))).fst)
```

#### Kenny Lau (May 12 2020 at 21:55):

`unfold`

and `rw`

and `dsimp only`

all give me `._match_1`

#### Kenny Lau (May 12 2020 at 21:56):

I remember being told that `let`

works fine with other things

#### Mario Carneiro (May 12 2020 at 21:56):

@Paul Rowe `anno._match_1`

is probably the function `\lam (j, a), (j+1, aatt (i, j+1) p a)`

representing the remainder of the `att`

case after the `let`

#### Kenny Lau (May 12 2020 at 21:56):

but my experience tells me to avoid it

#### Kenny Lau (May 12 2020 at 21:56):

@Mario Carneiro what tactic would you use for my theorem?

#### Mario Carneiro (May 12 2020 at 21:56):

In order to unfold it, the last argument to the auxiliary function must be a pair

#### Mario Carneiro (May 12 2020 at 21:57):

because you pattern matched on it being a pair

#### Kenny Lau (May 12 2020 at 21:58):

aha

#### Kenny Lau (May 12 2020 at 21:58):

```
def fib2 : ℕ → ℕ × ℕ
| 0 := (0, 1)
| (n+1) := let (a, b) := fib2 n in (b, a+b)
def fib (n : ℕ) : ℕ :=
(fib2 n).1
theorem fib_add_two (n : ℕ) : fib (n + 2) = fib (n + 1) + fib n :=
begin
unfold fib fib2,
cases fib2 n with a b,
-- ⊢ (fib2._match_1 (fib2._match_1 (a, b))).fst = (fib2._match_1 (a, b)).fst + (a, b).fst
unfold fib2,
-- ⊢ (a + b, b + (a + b)).fst = (b, a + b).fst + (a, b).fst
dsimp only,
rw add_comm
end
```

#### Kenny Lau (May 12 2020 at 21:59):

@Paul Rowe after you make the input a pair you can actually use `unfold fib2`

#### Kenny Lau (May 12 2020 at 21:59):

I just discovered this today

#### Kenny Lau (May 12 2020 at 21:59):

as in, instead of `unfold fib2._match_1`

or something like that

#### Reid Barton (May 12 2020 at 22:01):

Oh neat, it made an equational lemma for matching on the let:

```
fib2._match_1.equations._eqn_1 : ∀ (a b : ℕ), fib2._match_1 (a, b) = (b, a + b)
```

#### Reid Barton (May 12 2020 at 22:01):

And indeed `unfold`

is

Given defined constants

`e₁ ... eₙ`

,`unfold e₁ ... eₙ`

iteratively unfolds all occurrences in the target of the main goal, usingequational lemmasassociated with the definitions.

#### Kevin Buzzard (May 12 2020 at 22:02):

@Paul Rowe you might want to try `#print prefix anno`

just to find out all the things which Lean has created under the hood

#### Paul Rowe (May 12 2020 at 22:06):

Maybe I'm just being slow at the end of long day. What do I need to do to get the pair as an argument to further unfold?

#### Reid Barton (May 12 2020 at 22:06):

Whatever is necessary to know that it is a pair

#### Reid Barton (May 12 2020 at 22:06):

Like, what do you expect it to unfold to?

#### Reid Barton (May 12 2020 at 22:07):

oh I see your example now

#### Reid Barton (May 12 2020 at 22:07):

oh but I can't run it

#### Paul Rowe (May 12 2020 at 22:07):

Ah ok! I got it.

#### Paul Rowe (May 12 2020 at 22:09):

I used `cases (anno x_a_1 (i+1)) with a b`

and that allowed me to further unfold the definition to produce the inductive hypothesis

#### Paul Rowe (May 12 2020 at 22:11):

@Reid Barton Yeah, I'm trying to port another project over from Coq as a learning method, so there are just too many dependencies to create a working example out of the real code. Thanks, @Kenny Lau for posting a more self-contained example! And thanks to everyone who chimed in! You saved from finishing my work day in a bad mood :)

#### Reid Barton (May 12 2020 at 22:12):

I'm glad what was at best a very vague answer of mine helped you :upside_down:

#### Mario Carneiro (May 12 2020 at 22:17):

Not sure if this is the easiest proof, but this works:

```
def fib2 : ℕ → ℕ × ℕ
| 0 := (0, 1)
| (n+1) := let (a, b) := fib2 n in (b, a+b)
def fib (n : ℕ) : ℕ :=
(fib2 n).1
theorem fib_add_two (n : ℕ) : fib (n + 2) = fib (n + 1) + fib n :=
begin
have : ∀ n, fib2 n = (fib n, fib (n+1)),
{ intro n, rw [fib, fib, fib2], cases fib2 n, rw [fib2] },
have H := this (n+1),
rw [fib2, this, fib2, add_comm (fib n)] at H,
injection H with _ H, exact H.symm,
end
```

#### Mario Carneiro (May 12 2020 at 22:17):

the interesting step is `rw [fib2]`

on the second line, which could also be `unfold fib2`

, `simp [fib2]`

or `refl`

Last updated: Dec 20 2023 at 11:08 UTC