## 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_1which 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

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,
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, using equational lemmas associated 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

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: May 13 2021 at 16:25 UTC