Zulip Chat Archive

Stream: new members

Topic: unfold and let


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 12 2020 at 21:34):

Is this let in term mode or tactic mode?

view this post on Zulip Paul Rowe (May 12 2020 at 21:34):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Jalex Stark (May 12 2020 at 21:48):

(also full definitions are usually more useful than excerpts)

view this post on Zulip Kenny Lau (May 12 2020 at 21:49):

as in:

```
[code goes here]
```

view this post on Zulip 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.

view this post on Zulip Kenny Lau (May 12 2020 at 21:52):

my advice is to avoid let unless necessary

view this post on Zulip Kenny Lau (May 12 2020 at 21:52):

actually maybe it is necessary in this case

view this post on Zulip Jalex Stark (May 12 2020 at 21:53):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 12 2020 at 21:55):

I actually don't know how to solve this myself

view this post on Zulip 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)

view this post on Zulip Kenny Lau (May 12 2020 at 21:55):

unfold and rw and dsimp only all give me ._match_1

view this post on Zulip Kenny Lau (May 12 2020 at 21:56):

I remember being told that let works fine with other things

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 12 2020 at 21:56):

but my experience tells me to avoid it

view this post on Zulip Kenny Lau (May 12 2020 at 21:56):

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

view this post on Zulip Mario Carneiro (May 12 2020 at 21:56):

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

view this post on Zulip Mario Carneiro (May 12 2020 at 21:57):

because you pattern matched on it being a pair

view this post on Zulip Kenny Lau (May 12 2020 at 21:58):

aha

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 12 2020 at 21:59):

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

view this post on Zulip Kenny Lau (May 12 2020 at 21:59):

I just discovered this today

view this post on Zulip Kenny Lau (May 12 2020 at 21:59):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 12 2020 at 22:06):

Whatever is necessary to know that it is a pair

view this post on Zulip Reid Barton (May 12 2020 at 22:06):

Like, what do you expect it to unfold to?

view this post on Zulip Reid Barton (May 12 2020 at 22:07):

oh I see your example now

view this post on Zulip Reid Barton (May 12 2020 at 22:07):

oh but I can't run it

view this post on Zulip Paul Rowe (May 12 2020 at 22:07):

Ah ok! I got it.

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip 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:

view this post on Zulip 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

view this post on Zulip 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