unfold and let

Stream: new members

[Paul Rowe]

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]

Is this let in term mode or tactic mode?

[Paul Rowe]

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

[Kevin Buzzard]

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]

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]

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]

(also full definitions are usually more useful than excerpts)

[Kenny Lau]

as in:

```
[code goes here]
```

[Paul Rowe]

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]

my advice is to avoid let unless necessary

[Kenny Lau]

actually maybe it is necessary in this case

[Jalex Stark]

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

[Kenny Lau]

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

I actually don't know how to solve this myself

[Paul Rowe]

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]

unfold and rw and dsimp only all give me ._match_1

[Kenny Lau]

I remember being told that let works fine with other things

[Mario Carneiro]

@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]

but my experience tells me to avoid it

[Kenny Lau]

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

[Mario Carneiro]

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

[Mario Carneiro]

because you pattern matched on it being a pair

[Kenny Lau]

aha

[Kenny Lau]

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]

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

[Kenny Lau]

I just discovered this today

[Kenny Lau]

as in, instead of unfold fib2._match_1 or something like that

[Reid Barton]

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]

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]

@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]

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]

Whatever is necessary to know that it is a pair

[Reid Barton]

Like, what do you expect it to unfold to?

[Reid Barton]

oh I see your example now

[Reid Barton]

oh but I can't run it

[Paul Rowe]

Ah ok! I got it.

[Paul Rowe]

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]

@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]

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

[Mario Carneiro]

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]

the interesting step is rw [fib2] on the second line, which could also be unfold fib2, simp [fib2] or refl