Proving theorems about match

Stream: mathlib4

[Gareth Ma]

How do I prove the following?

def f (k n : ℕ) : ℕ :=
match n with
| 0 => 1
| n + 1 => f k n

theorem ff : ∀ k, f k 0 ≠ 2 := by
  intro k

I want to rewrite the left hand side to be 1, but I can't find a way to do that :joy:

[Eric Wieser]

Does rw f work?

[Kyle Miller]

simp [f] will finish the proof

[Kyle Miller]

Using Eric's suggestion, another proof is

  rw [f]
  rintro ⟨⟩

where the rintro is short for intro h followed by cases h.

[Kyle Miller]

Or, since you know what the LHS is, you can use show:

theorem ff : ∀ k, f k 0 ≠ 2 := by
  intro k
  show 1 ≠ 2
  simp -- or however you want to complete this, including the `rintro` from before

[Gareth Ma]

Huh I swear simp [f] didn't work just now, maybe I changed something now that it works

[Gareth Ma]

Ah I see why, it says invalid 'simp', proposition expected. I think it's because my code is structured slightly differently. Do you mind taking a look?

def f (k n : ℕ) : List ℕ :=
match n with
| 0 => [1]
| n + 1 =>
  let data := f k n
  have h : f k n ≠ [] := by {
    induction n
    rw [f]
  }
  [data.head h]

[Kyle Miller]

I don't think you can use the definition of f from within f like that.

I'd probably structure it differently, where you give some definition for f then prove it has the property you want:

def f (k n : ℕ) : List ℕ :=
match n with
| 0 => [1]
| n + 1 =>
  let data := f k n
  [data.head!]

theorem f_ne_empty : f k n ≠ [] := by
  cases n <;> rintro ⟨⟩

theorem f_succ : f k (n + 1) = [(f k n).head f_ne_empty] := by
  simp only [f]
  rw [List.head!_of_head?]
  simp [← List.head?_eq_head]

[Gareth Ma]

Ohh that's way better, I didn't know about head! which works perfectly :D

[Gareth Ma]

Also learned some new syntax from the theorem haha

[Floris van Doorn]

@Gareth Ma : in your last code snippet, there is no way to prove f k n ≠ [], since you haven't defined f k n yet. Maybe you were going to define f k (n + 1) := [], and then your claim would be false for n >= 1.

[Gareth Ma]

Then what is f there, like why does it exist (or why can I use it)?

[Floris van Doorn]

It's a free variable that Lean allows you to use to write recursive function calls. It has no definition yet.
Lean will do various checks to make sure that what you write makes sense (e.g. without the partial keyword you cannot write | n + 1 => f k (n + 1), since that would not result in a total function)