How to apply the induction hyp. inside proof by matching

Stream: new members

[Nowhere Dense]

I'm once again asking for your support. This time I'm struggling with induction. I have managed to write some induction proofs but I struggle with others, and I think the following code produces a good MWE of what I don't understand.

def F: ℕ → ℤ
| 0 => 0
| 1 => 1
| (n+1) => F n

theorem F_equality  (n : ℕ) (h: n≥1) : F n = 1 :=
  by match n with
  | 0 => contradiction
  | 1 => rfl
  | (n+1) =>
    have IH := F_equality n
    calc
    F (n+1) = F n      := by rw [F,h]  -- This part is wrong (1)
                _ = 1          := by rw [IH,h]  -- This part is also wrong (2)

Here I want to do induction starting at n=1, so I need to add the hypothesis n≥1 to the statement. But this hypothesis is not letting me apply the definition of F or the induction hypothesis inside the inductive step. Lean infoview is giving me the following messages:

tactic 'rewrite' failed, equality or iff proof expected
  n + 1 ≥ 1
n✝ n : ℕ
h : n + 1 ≥ 1
h1 : n ≥ 1 → F n = 1
⊢ F n = F n

unsolved goals
n✝ n : ℕ
h : n + 1 ≥ 1
h1 : n ≥ 1 → F n = 1
⊢ n ≥ 1

Apparently the hypothesis h becomes (n + 1 ≥ 1) inside the n+1 matching case, and that is not letting me apply h1 or the definition of F (that maybe I should call with F.eq_def?). Any help is welcome!

[Luigi Massacci]

I would suggest you rewrite the last case of your F as (n+2) => F (n+1)

[Nowhere Dense]

Luigi Massacci said:

I would suggest you rewrite the last case of your F as (n+2) => F (n+1)

I tried doing this and I get the error "failed to rewrite using equation theorems for 'F'. Try rewriting with 'F.eq_def'. "

[Ruben Van de Velde]

You can do this with a custom induction principle

[Ruben Van de Velde]

And don't forget to add your imports when asking questions

[Ruben Van de Velde]

import Mathlib

def F: ℕ → ℤ
| 0 => 0
| 1 => 1
| (n+1) => F n

theorem F_equality  (n : ℕ) (h: n≥1) : F n = 1 := by
  induction n, h using Nat.le_induction with
  | base => sorry
  | succ n hmn _ => sorry

[Nowhere Dense]

@Ruben Van de Velde
Thank you! I managed to fill the details and it works perfectly.

[Luigi Massacci]

I realised only now I forgot to reply to you. My apologies, the problem was that you had to change things appropriately also in your proof, like this:

import Mathlib

def F: ℕ → ℤ
| 0 => 0
| 1 => 1
| (n+2) => F (n+1)

theorem F_equality  (n : ℕ) (h: n≥1) : F n = 1 :=
  by match n with
  | 0 => contradiction
  | 1 => rfl
  | (n+2) =>
    have IH := F_equality (n + 1)
    calc
    F (n+2) = F (n +1)  := by rfl -- rw [F] also works
          _ = 1 := by
            rw [IH]
            simp
           -- note that after rw [IH] you are just left to prove just n + 1 ≥ 1
           -- exact? will also work