Question regarding Pascal's triangle exercise in math2001

Stream: new members

[calofmijuck]

Hello, This is an exercise from math2001, Exercise 6.5.4 (2).

import Library.Basic

def pascal : ℕ → ℕ → ℕ
  | a, 0 => 1
  | 0, b + 1 => 1
  | a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)
termination_by _ a b => a + b

example (a : ℕ) : pascal a 1 = a + 1 := by
  simple_induction a with k IH
  · calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  · calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by rw [pascal] -- unsolved goals
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [IH]
      _ = k + 1 + 1 := by ring

The proof seems completely normal to me, but lean does not accept the line with comment, which is exactly the definition.

Why is this happening? Thanks in advance.

[Kim Morrison]

Can you post this as a #mwe, with imports that work in the online code editor? It's hard to debug code that uses a specific courses libraries.

[Kim Morrison]

Presumably this is Heather's course?

[calofmijuck]

Yes, it is. I'll fix that.

[Kim Morrison]

import Mathlib

def pascal : ℕ → ℕ → ℕ
  | a, 0 => 1
  | 0, b + 1 => 1
  | a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)
termination_by a b => a + b

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih => calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by simp [pascal]
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [ih]
      _ = k + 1 + 1 := by ring

[Kim Morrison]

I couldn't reproduce your proof state, but the error message is what you need to look at: what were the unsolved goals after rw [pascal]?

[calofmijuck]

Thanks for fixing the code. I was going to fix it but you were faster.
image.png

[calofmijuck]

Maybe this is a bug with the simple_induction tactic?

[calofmijuck]

This is strange, your code works fine...

[calofmijuck]

Also, this course seems to have the simp tactic disabled. I changed simp to rw and it doesn't work with the same error message.

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih => calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by rw [pascal]
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [ih]
      _ = k + 1 + 1 := by ring

So then my question would be why the rw doesn't work.

[Kim Morrison]

You need to show us what the goals are after rw [pascal]

[Kim Morrison]

The error message is not saying that the rw doesn't work. It's saying that there's still something more to do afterwards.

[calofmijuck]

It outputs the following:

k : ℕ
ih : pascal k 1 = k + 1
⊢ pascal (k + 1) 0 + pascal k 1 = succ k + 1

[Kim Morrison]

e.g. maybe you need to rwreite by the definition again?

[Kim Morrison]

Maybe you need to think about why this is true on paper. :-)

[calofmijuck]

Um.. is there an invalid step in my original proof?

[calofmijuck]

Isn't the goal obviously true by definition and the induction hypothesis?
That's why I wrote the remaining part of the proof in that way. Am I missing something?

[Kim Morrison]

The invalid step is that there is an unsolved goal after the rw [pascal], as the error message says.

[calofmijuck]

I don't understand the part where the existence of an unsolved goal implies an invalid step.
Doesn't it happen normally when the proof is not finished?
I think I gave the remaining steps of the proof.

I found a workaround and eventually got it accepted. Why does this work? It essentially follows the same steps, I think.

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih =>
    rw [pascal]
    rw [pascal]
    rw [ih]
    calc
      _ = k + 1 + 1 := by ring

[calofmijuck]

Actually I'm new to lean, and I'm in the learning process, this is the first material I'm going through.
So maybe the confusion is from me having no idea what the tactics do in detail?

[Kim Morrison]

I'm going to move this thread to the new members stream. You'll get better help there. :-)

[calofmijuck]

Thank you for your time.

[Johan Commelin]

calofmijuck said:

I don't understand the part where the existence of an unsolved goal implies an invalid step.
Doesn't it happen normally when the proof is not finished?
I think I gave the remaining steps of the proof.

Unfinished proofs indeed give errors, if you don't explicitly silence them using sorry

[calofmijuck]

Right. So I gave the remaining proof, but it wasn't accepted.

[calofmijuck]

Summary

The following proof doesn't work. It says that there are unsolved goals just after the line with comment.

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih => calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by rw [pascal] -- here
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [ih]
      _ = k + 1 + 1 := by ring

Lean says that the unsolved goal is the following:

k : ℕ
ih : pascal k 1 = k + 1
⊢ pascal (k + 1) 0 + pascal k 1 = succ k + 1

I found a workaround:

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih =>
    rw [pascal]
    rw [pascal]
    rw [ih]
    calc
      _ = k + 1 + 1 := by ring

This was accepted by lean.

Question

Why is the first proof not accepted? The second workaround I found seems to essentially follow the same steps.

[Heather Macbeth]

@calofmijuck You'll find that this works:

  · calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by rw [pascal, pascal, pascal]
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [IH]
      _ = k + 1 + 1 := by ring

i.e., changing rw [pascal] to rw [pascal, pascal, pascal].

[Heather Macbeth]

It's a quirk of rw that it only rewrites one occurrence of an equation lemma for a definition like pascal, and in this case, the first occurrence is not the one that actually needs replacing.

[Heather Macbeth]

Elsewhere in the book I use rfl rather to avoid this rw [x, x, x, ...] problem -- see for example
https://hrmacbeth.github.io/math2001/06_Induction.html#two-step-starting-point
I'm a bit surprised this doesn't work here.

[Heather Macbeth]

@Joachim Breitner On the Lean version current in the web editor, the following rfl works:

import Mathlib

def pascal : ℕ → ℕ → ℕ
  | a, 0 => 1
  | 0, b + 1 => 1
  | a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)

example : pascal (k + 1) (0 + 1) = pascal (k + 1) 0 + pascal k (0 + 1) := rfl

But it fails if termination_by a b => a + b is added to the recursive definition. Is this expected?

[calofmijuck]

Wow professor thank you for your explanation! Now I think I see what happened here.
I intuitively thought that rw would match the first occurence in the goal, so the LHS would be rewritten.

[Joachim Breitner]

Interesting example! I expect the inferred termination argument is termination_by a b => (a, b) here, so that's one source of differences. I am surprised it changes DefEq behavior though?

Anyways, we should probably limit well-founded recursive definitions from unfolding, it is a common source of painful slow-downs.

[Mario Carneiro]

I would assume the change in rfl behavior is simply because the first version is using structural recursion and adding termination_by forces it to be a WF recursion

[Joachim Breitner]

Is it structural though? I see two recursive calls and neither argument gets smaller in both. (Still waking up so only phone in hand and no tea in brain yet)

[Mario Carneiro]

It should be structural recursive by nested recursion first on the first argument and then the second, i.e. in wf terms this is recursion on a b => (a, b)

[Mario Carneiro]

I stand corrected, the version on the web editor (which is 4.7.0) is also using WF recursion, but it is apparently able to compute with that recursion enough to prove the rfl lemma

[Joachim Breitner]

That's what I expected, I don't think lean does nested structural recursion (it would be bad if it did, because then we couldn't use the Ackerman function as an example for a function that needs wf anymore…)

[Daniel Weber]

import Mathlib

def pascal : ℕ → ℕ → ℕ
  | a, 0 => 1
  | 0, b + 1 => 1
  | a + 1, b + 1 => pascal (a + 1) b + pascal a (b + 1)
termination_by a b => a + b

example (a : ℕ) : pascal a 1 = a + 1 := by
  induction a with
  | zero => calc
      _ = 1 := by rw [pascal]
      _ = 0 + 1 := by ring
  | succ k ih => calc
      pascal (k + 1) 1 = pascal (k + 1) 0 + pascal k 1 := by conv => lhs; rw [pascal]
      _ = 1 + pascal k 1 := by rw [pascal]
      _ = 1 + (k + 1) := by rw [ih]
      _ = k + 1 + 1 := by ring

Also works (that is, only rewriting on the LHS)

[calofmijuck]

I was thinking about a tactic that would rewrite the LHS. Thanks for the suggestion!