Base case of recursive definition

Stream: general

[Heather Macbeth]

I'm used to being able to get out the base case of a recursive definition by rfl:

def two_pow : ℕ → ℕ
| 0 := 1
| (i + 1) := 2 * two_pow i

example : two_pow 0 = 1 := rfl

In the following example, it doesn't seem to work. Is there another way?

def pascal : ℕ → ℕ → ℕ
| 0 j := 1
| i 0 := 1
| (i + 1) (j + 1) := pascal i (j + 1) + pascal (i + 1) j

example : pascal 0 0 = 1 := rfl -- fails

This seems pretty similar to a question from a couple of months ago, but I can't get the cases trick from there to work.

[Adam Topaz]

unfold pascal works, but this is indeed strange. I would have expected refl to work!

[Mario Carneiro]

it's proved by well founded recursion, those don't compute by rfl

[Mario Carneiro]

It is possible to restructure the definition to be structurally recursive, in which case all the theorems are by rfl (except the overlapping patterns)

def pascal_succ (f : ℕ → ℕ) : ℕ → ℕ
| 0 := 1
| (j + 1) := f (j + 1) + pascal_succ j

def pascal : ℕ → ℕ → ℕ
| 0 j := 1
| (i + 1) j := pascal_succ (pascal i) j

theorem zero_pascal (j) : pascal 0 j = 1 := rfl
theorem pascal_zero (i) : pascal i 0 = 1 := by cases i; refl
theorem pascal_succ_succ (i j) :
  pascal (i + 1) (j + 1) = pascal i (j + 1) + pascal (i + 1) j := rfl

[Mario Carneiro]

If you want to keep the original definition, you still can prove the equations using the generated equation lemmas:

def pascal : ℕ → ℕ → ℕ
| 0 j := 1
| i 0 := 1
| (i + 1) (j + 1) := pascal i (j + 1) + pascal (i + 1) j

theorem zero_pascal (j) : pascal 0 j = 1 := by cases j; simp [pascal]
theorem pascal_zero (i) : pascal i 0 = 1 := by cases i; simp [pascal]
theorem pascal_succ_succ (i j) :
  pascal (i + 1) (j + 1) = pascal i (j + 1) + pascal (i + 1) j := by simp [pascal]

[Kevin Buzzard]

Rule of thumb: when there are two variables involved but you're only defining the answer in three cases not four, the "it's all rfl" model breaks down sometimes.

[Heather Macbeth]

Thanks all!

[Adam Topaz]

Kevin Buzzard said:

Rule of thumb: when there are two variables involved but you're only defining the answer in three cases not four, the "it's all rfl" model breaks down sometimes.

I'm not so sure about this....

def pascal : ℕ → ℕ → ℕ
| 0 0 := 1
| 0 (j+1) := 1
| i 0 := 1
| (i + 1) (j + 1) := pascal i (j + 1) + pascal (i + 1) j

example : pascal 0 0 = 1 := rfl -- fails

[Adam Topaz]

it seems that the equation compiler still splits up the original definition into the four cases?!

import tactic

def pascal : ℕ → ℕ → ℕ
| 0 j := 1
| i 0 := 1
| (i + 1) (j + 1) := pascal i (j + 1) + pascal (i + 1) j

#check pascal.equations._eqn_1
#check pascal.equations._eqn_2
#check pascal.equations._eqn_3
#check pascal.equations._eqn_4

[Patrick Johnson]

Adam Topaz said:

Kevin Buzzard said:

Rule of thumb: when there are two variables involved but you're only defining the answer in three cases not four, the "it's all rfl" model breaks down sometimes.

I'm not so sure about this....

Let P="two variables and three cases" and Q="it's all rfl". What Kevin asserts is that P → ¬Q (sometimes), which doesn't imply ¬P → Q.

[Patrick Johnson]

Although, there is an example of P → Q (two variables, three cases, but all-rfl works):

def f : ℕ → ℕ → ℕ
| a 0 := 1
| a 1 := 2
| a (b+2) := 3

example {a : ℕ}   : f a 0 = 1     := rfl
example {a : ℕ}   : f a 1 = 2     := rfl
example {a b : ℕ} : f a (b+2) = 3 := rfl

[Kyle Miller]

@Adam Topaz I think the pascal function is demonstrating that the equation lemmas are more of a rule of thumb of what you might expect rfl to prove, but they're actually not always what rfl can prove! For example, unfold pascal works but dunfold pascal does not.

[Kyle Miller]

You can see the whole definition in all its well-founded glory with delta pascal pascal._main._pack

[Adam Topaz]

yeah I tried that too... it's terrible. But I guess this is a good reminder that unfold doesn't necessarily preserve definitional equality!

[Adam Topaz]

How is pascal.equations._eqn_1 proved under the hood?

[Floris van Doorn]

#print pascal._main._pack.equations._eqn_1 gives you the answer (in a way...)

[Kyle Miller]

I wonder if we should have a refl-like tactic that operates by unfold-ing definitions? Like simp [pascal] but where you don't need to write pascal. The simp! tactic is not quite right since it uses delta unfolding.

The reason I suggest this is that rfl not being able to compute when there is well-founded recursion is a recurring question.

Another option is some sort of reduce tactic that uses all the equation lemmas. I'm imagining we could have a dec_trivial variant that uses it.

[Mario Carneiro]

simp! uses the equation lemmas IIUC

[Kyle Miller]

I checked, and simp! gives the has_well_founded.wf.fix ... term here