Using (-1) between N and Z

Stream: new members

[Divya Ranjan]

I'm trying to prove by induction the definition of a function that is recursively defined and uses $(-1)^n$, somehow even though I'm getting 2 = 2 rfl claims they are not definitionally equivalent.

Here's the lemma:

import Mathlib
--set_option diagnostics true
open Finset BigOperators
open Ring
open Nat

def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | 2 => 5
  | (n + 1) => f n + 2 * f (n - 1)
#check (f)

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp
    #check 2
    rw [show f 0 = 2 by rfl]

I've tried using abs in the lemma statement, or using functions like natAbs but that still doesn't work, despite the fact that the #check 2 shows that $2$ is of type $\mathbb{N}$

[Julian Berman]

I think this is saying f 0 is indeed 2 but the proof is not rfl. I don't recall the technical details, it's something like that def gives you something that is partially irreducible. I think perhaps you simply want abbrev instead, in which case the proof will be rfl:

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| 2 => 5
| (n + 1) => f n + 2 * f (n - 1)

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · have : f 0 = 2 := rfl
    simp
    rw [show f 0 = 2 from rfl]
  · sorry

Or alternatively if you do want a def you can define some API for f.

[Julian Berman]

(In your original code rw [show f 0 = 2 by simp only [f]] will work as well for unfolding f.)

[Divya Ranjan]

Julian Berman said:

I think this is saying f 0 is indeed 2 but the proof is not rfl. I don't recall the technical details, it's something like that def gives you something that is partially irreducible. I think perhaps you simply want abbrev instead, in which case the proof will be rfl:

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| 2 => 5
| (n + 1) => f n + 2 * f (n - 1)

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · have : f 0 = 2 := rfl
    simp
    rw [show f 0 = 2 from rfl]
  · sorry

Or alternatively if you do want a def you can define some API for f.

Okay, that was unbeknownst to me. Where can I read about abbrev and its differences with def? I tried searching for it in Theorem Proving in Lean but haven't found anything. A link to some documentation would be of great help. Thank you, Julian.

[Eric Wieser]

I think you actual want

def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | (n + 2) => f (n + 1) + 2 * f n

which by avoiding n-1 makes the function structurally recursive

[Julian Berman]

(https://lean-lang.org/doc/reference/latest/The-Lean-Language/Module-Contents/#The-Lean-Language-Reference--The-Lean-Language--Module-Contents--Commands-and-Declarations--Definition-Like-Commands FWIW is where I think will go over abbrev vs def but I see it isn't populated quite yet)

[Divya Ranjan]

Eric Wieser said:

I think you actual want

def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | (n + 2) => f (n + 1) + 2 * f n

which by avoiding n-1 makes the function structurally recursive

Well, how does that differ? I could also define it using f (n) directly but I'm not sure why recursively getting to f(n+1) would differ from directly defining it.

[Divya Ranjan]

Julian Berman said:

I think this is saying f 0 is indeed 2 but the proof is not rfl. I don't recall the technical details, it's something like that def gives you something that is partially irreducible. I think perhaps you simply want abbrev instead, in which case the proof will be rfl:

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| 2 => 5
| (n + 1) => f n + 2 * f (n - 1)

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · have : f 0 = 2 := rfl
    simp
    rw [show f 0 = 2 from rfl]
  · sorry

Or alternatively if you do want a def you can define some API for f.

This brings the same problem when doing the succ step of induction:

import Mathlib
--set_option diagnostics true
open Finset BigOperators
open Ring
open Nat

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| 2 => 5
| (n + 1) => f n + 2 * f (n - 1)

/-
def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | (n + 2) => f (n + 1) + 2 * f n
-/

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp
    rw [show f 0 = 2 from rfl]
  · rw [show f (n + 1) = f (n) + 2 * f (n - 1) by rfl]
    --have : f (n + 1) = f n + 2 * f (n - 1) := by ring
    -- apply
  sorry

This again gives:

tactic 'rfl' failed, the left-hand side
  f (n + 1)
is not definitionally equal to the right-hand side
  f n + 2 * f (n - 1)

[Abraham Solomon]

Divya Ranjan said:

Eric Wieser said:

I think you actual want

def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | (n + 2) => f (n + 1) + 2 * f n

which by avoiding n-1 makes the function structurally recursive

Well, how does that differ? I could also define it using f (n) directly but I'm not sure why recursively getting to f(n+1) would differ from directly defining it.

I think the difference is technical, but its about being able to make sense of (n-1):Nat for all n. (n+1), (n+2) is always easy to make sense of.

By default Nat has successor and 0, -1 isnt as easy to work with as n+1 and (n+1)+1 (being succ n and succ n (succ n))

[Divya Ranjan]

Abraham Solomon said:

Divya Ranjan said:

Eric Wieser said:

I think you actual want

def f (n : Nat) : ℤ :=
  match n with
  | 0 => 2
  | 1 => 1
  | (n + 2) => f (n + 1) + 2 * f n

which by avoiding n-1 makes the function structurally recursive

Well, how does that differ? I could also define it using f (n) directly but I'm not sure why recursively getting to f(n+1) would differ from directly defining it.

I think the difference is technical, but its about being able to make sense of (n-1):Nat for all n. (n+1), (n+2) is always easy to make sense of.

By default Nat has successor and 0, -1 isnt as easy to work with as n+1 and (n+1)+1 (being succ n and succ n (succ n))

Okay, that makes sense. Thank you.

[Ruben Van de Velde]

I think your issue is that n+1 could be 1 or 2 and those have different definitions

[Divya Ranjan]

Ruben Van de Velde said:

I think your issue is that n+1 could be 1 or 2 and those have different definitions

How so?

[Divya Ranjan]

Ruben Van de Velde said:

I think your issue is that n+1 could be 1 or 2 and those have different definitions

Because n could be 0 or 1?

[Divya Ranjan]

Should I be doing two base cases for 0 and 1?

[Divya Ranjan]

Divya Ranjan said:

Should I be doing two base cases for 0 and 1?

If so, how can I do that? Both the induction and induction' tactic seem to only create two implicit goals.

[Kevin Buzzard]

Can you ask your question in the form of a simple #mwe ?

[Kevin Buzzard]

The answer might be match n with

[Divya Ranjan]

Kevin Buzzard said:

Can you ask your question in the form of a simple #mwe ?

import Mathlib
open Finset BigOperators
open Ring
open Nat

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| 2 => 5
| (n + 1) => f n + 2 * f (n - 1)

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp
    rw [show f 0 = 2 from rfl]
  · -- rw [show f (n + 1) = f n + 2 * f (n - 1) by rfl]
    sorry

[Divya Ranjan]

Kevin Buzzard said:

The answer might be match n with

Where should I use it? After the opening induction statement?

[Eric Wieser]

In your example the commented show line is false, consider n = 0

[Divya Ranjan]

Eric Wieser said:

In your example the commented show line is false, consider n = 0

That is impossible though, because that would require us to define f(-1) which is outside of our scope, the proof is for all $n \in \mathbb{N}$.

[Eric Wieser]

Are you aware of what #eval 1 - 2 gives?

[Divya Ranjan]

Ah, I didn't know Lean gives 0 to attempts of producing a negative number. Okay, should I use rcases or cases here to handle the n=0, being 0and then proceed?

[Divya Ranjan]

But wait, that would lead to defining a contradictory version of f (1).

$f (0 + 1) = f (0) + 2 \cdot f (0 - 1) = 3 \cdot f (0) = 6 \neq 1$

[Ruben Van de Velde]

So the first step I'd suggest is to make sure you have no overlapping patterns in your definition, so n + 3 instead of n + 1, and adjust the formula accordingly

[Ruben Van de Velde]

Also the 2 case is redundant, so you could have patterns 0, 1, and n + 2

[Divya Ranjan]

Ruben Van de Velde said:

Also the 2 case is redundant, so you could have patterns 0, 1, and n + 2

Like this?

import Mathlib
open Finset BigOperators
open Ring
open Nat

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| (n + 2) => f (n + 1) + 2 * f n

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp
    rw [show f 0 = 2 from rfl]
  · -- rw [show f (n + 1) = f n + 2 * f (n - 1) by rfl]
    sorry

[Divya Ranjan]

Uncommenting the rw gives the same error:

tactic 'rfl' failed, the left-hand side
  f (n + 1)
is not definitionally equal to the right-hand side
  f n + 2 * f (n - 1)

[Eric Wieser]

I think the first n - 1 should be n, as it was in my post above

[Eric Wieser]

Also, you're still in trouble, because when n = 0 your commented line is still false

[Eric Wieser]

You need to handle the cases 0, 1, and n + 2, not 0 and n + 1

[Divya Ranjan]

Eric Wieser said:

I think the first n - 1 should be n, as it was in my post above

Indeed, a typo.

[Divya Ranjan]

Eric Wieser said:

You need to handle the cases 0, 1, and n + 2, not 0 and n + 1

But how? The code below only shows two goals: zero and succ:

import Mathlib
open Finset BigOperators
open Ring
open Nat

abbrev f : ℕ → ℤ
| 0 => 2
| 1 => 1
| (n + 2) => f (n + 1) + 2 * f n

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  . sorry
  . sorry

[Eric Wieser]

You can even ask Lean to tell you that it is false:

import Mathlib
import Plausible
open Finset BigOperators
open Ring
open Nat

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

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp [f]
  · have : f (n + 1) = f n + 2 * f (n - 1) := by
      plausible -- error, found counterexample
    rw [this]
    sorry

[Divya Ranjan]

Eric Wieser said:

You can even ask Lean to tell you that it is false:

import Mathlib
import Plausible
open Finset BigOperators
open Ring
open Nat

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

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp [f]
  · have : f (n + 1) = f n + 2 * f (n - 1) := by
      plausible -- error, found counterexample
    rw [this]
    sorry

Apologies if this is something trivial, but I fail to understand this. How are we to show the n=0 case in the have statement, you'd have to prove if f(1) = 6 which is contradictory. After the last simp in the zero case, Lean asks to prove f (1) = 6:

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := by
  induction' n with n ih
  · simp [f]
  · have : f (n + 1) = f n + 2 * f (n - 1) := by
     · cases n with
     | zero =>
            simp
            rw [show f 0 = 2 by rfl]
            simp
     | succ zero => sorry
    rw [this]
    rw [pow_add, pow_one, mul_two]
    sorry

[Eric Wieser]

Divya Ranjan said:

How are we to show the n=0 case in the have statement, you'd have to prove if f(1) = 6 which is contradictory.

We are not able to prove this; but plausible gives an error message that tells you about this contradiction.

[Eric Wieser]

Lean is happy to continue the rest of the proof as though it were fine though, since it already told you that it was wrong the first time.

[Eric Wieser]

This is a feature, because it means Lean checks as much of your proof as possible, rather than stopping after the first error.

[Divya Ranjan]

So I should just put a plausible and continue with the rest?

[Eric Wieser]

No! but you should use plausible to check if your goals are false

[Eric Wieser]

And then if they are, rewrite your proof until your goal is not false!

[Divya Ranjan]

Okay, so that have statement is not correct, and I should come up with something else..

[Eric Wieser]

Your example above with cases above is close, but you should do the cases before the have

[Eric Wieser]

(you might also need to move the cases before the induction, I don't remember whether it matters)

[Divya Ranjan]

Eric Wieser said:

Your example above with cases above is close, but you should do the cases before the have

Okay, just so I don't continue being confused, the cases should be zero, succ zero and succ _, right?

[Eric Wieser]

No, they should be zero, succ zero, and succ (succ _)

[Eric Wieser]

Aka 0, 1, and n + 2

[Divya Ranjan]

Understood, I was wondering that. Thanks, let me try.

[Eric Wieser]

Which as Kevin alludes to earlier, you can get more directly using match instead of induction/cases. It would be a good exercise to write the proof once in each style

[Divya Ranjan]

Eric Wieser said:

Which as Kevin alludes to earlier, you can get more directly using match instead of induction/cases. It would be a good exercise to write the proof once in each style

You can do an inductive proof with just the match tactic, without induction/induction'?

[Ruben Van de Velde]

Yeah, and instead of an explicit induction hypothesis, you use the name of the lemma itself

[Kevin Buzzard]

import Mathlib
open Finset BigOperators
open Ring
open Nat

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

lemma functional_equation {n : Nat} : f n = 2^n + (-1)^n := match n with
  | 0 => by simp [f]
  | 1 => by simp [f]
  | (n + 2) => by
    have hn : f n = 2^n + (-1)^n := @functional_equation n
    have hnsucc : f (n + 1) = 2^(n + 1) + (-1)^(n + 1) := @functional_equation (n + 1)
    simp [f] -- simplifies f (n + 2)
    -- off you go
    sorry

[Divya Ranjan]

Thanks a lot @Kevin Buzzard and @Eric Wieser , finally finished with the proof. And just to have better knowledge, I tried to do it with cases/induction but somehow couldn't figure out which statement comes first, if any of you could share a resource with examples, I'd be glad.

[Kevin Buzzard]

If you want to do bare induction then you will have to think hard about exactly what statement you want to prove by induction on n, remembering that in the d + 1 case you will only have access to a statement about d, and in particular even if in your mental model you have "already proved the d-1 case", that's not how induction works in a theorem prover, you will not have access to it. So you would have to prove something like "for all n, f n = 2^n + (-1)^n and also f(n+1)=2^(n+1)+(-1)^(n+1)" by induction on n if you just used the induction tactic without any bells and whistles. However there will be a trick where you can use something like induction n using Nat.two_step_induction or whatever it's called, where you drop in the appropriate induction hypothesis which it uses instead of the usual one, and then you won't have to do this workaround.

[Edward van de Meent]

i think there already is a trick where instead of Nat.two_step_induction you use f.induct

[Edward van de Meent]

(lean generates some usefull lemmas for structurally recursive functions)