## Stream: new members

### Topic: First order recurrence

#### Adrián Doña Mateo (Nov 04 2020 at 13:54):

I have a first order recurrence relation and I want to prove that if two terms in the sequence are the same, then their successive terms are also the same. How can I get past the nat.rec after unfolding the definition of a?

noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

/-- A first order recurrence relation -/
def a (a₀ : ℕ) : ℕ → ℕ :=
assume n : ℕ,
nat.rec_on n a₀
(assume n an, if h : ∃ k : ℕ, k * k = an then classical.some h else an + 3)

/-- If two terms of the sequence are equal, so are their successors -/
lemma foo (a₀ : ℕ) (m n : ℕ) (h : a a₀ m = a a₀ n) :
a a₀ (m + 1) = a a₀ (n + 1) :=
begin
unfold a,
sorry
end


#### Kevin Buzzard (Nov 04 2020 at 14:11):

begin
unfold a,
change (if h : ∃ k : ℕ, k * k = a a₀ m then classical.some h else a a₀ m + 3) =
(if h : ∃ k : ℕ, k * k = a a₀ n then classical.some h else a a₀ n + 3),
rw h,
end


#### Kevin Buzzard (Nov 04 2020 at 14:15):

change works because the goal we want to see is definitionally equal to the goal we have.

#### Adrián Doña Mateo (Nov 04 2020 at 15:10):

Thanks! Do you know why dsimp doesn't do this for you?

#### Johan Commelin (Nov 04 2020 at 15:17):

If you don't mind using mathlib, this works:

import data.nat.sqrt

noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

/-- A first order recurrence relation -/
noncomputable
def a (a₀ : ℕ) : ℕ → ℕ
| 0     := a₀
| (n+1) := if ∃ k, k * k = a n then nat.sqrt (a n) else 3 * a n

/-- If two terms of the sequence are equal, so are their successors -/
lemma foo (a₀ : ℕ) (m n : ℕ) (h : a a₀ m = a a₀ n) :
a a₀ (m + 1) = a a₀ (n + 1) :=
begin
unfold a,
rw h,
end


#### Johan Commelin (Nov 04 2020 at 15:18):

I used import data.nat.sqrt to write a different version of your recurrence relation. (I personally find it hard to parse the nat.rec version.)

#### Johan Commelin (Nov 04 2020 at 15:19):

And if you don't mind using simp, then you can golf the proof to

/-- If two terms of the sequence are equal, so are their successors -/
lemma foo (a₀ : ℕ) (m n : ℕ) (h : a a₀ m = a a₀ n) :
a a₀ (m + 1) = a a₀ (n + 1) :=
by simp [a, h]


#### Johan Commelin (Nov 04 2020 at 15:20):

by rw [a, a, h] also works

#### Reid Barton (Nov 04 2020 at 15:26):

Yes, using the equation compiler will make unfold do something more useful.

#### Reid Barton (Nov 04 2020 at 15:27):

In the original code dsimp is looking for nat.rec applied to nat.succ m, not to m + 1.

#### Mario Carneiro (Nov 04 2020 at 15:29):

You can also easily make it computable using

import data.nat.sqrt

/-- A first order recurrence relation -/
def a (a₀ : ℕ) : ℕ → ℕ
| 0     := a₀
| (n+1) :=
let k := nat.sqrt (a n) in
if k * k = a n then k else 3 * a n


#### Adrián Doña Mateo (Nov 04 2020 at 15:30):

Johan Commelin said:

If you don't mind using mathlib, this works:

import data.nat.sqrt

noncomputable theory
local attribute [instance, priority 0] classical.prop_decidable

/-- A first order recurrence relation -/
noncomputable
def a (a₀ : ℕ) : ℕ → ℕ
| 0     := a₀
| (n+1) := if ∃ k, k * k = a n then nat.sqrt (a n) else 3 * a n

/-- If two terms of the sequence are equal, so are their successors -/
lemma foo (a₀ : ℕ) (m n : ℕ) (h : a a₀ m = a a₀ n) :
a a₀ (m + 1) = a a₀ (n + 1) :=
begin
unfold a,
rw h,
end


I initially tried to do it with pattern matching too but the equation compiler would complain that the VM doesn't have code for 'classical.choice'. I seenat.sqrt avoids having to use this. It's great to not have to use rec. Thank you!

#### Reid Barton (Nov 04 2020 at 15:31):

actually it's adding noncomputable which avoids that error--I don't understand why it is required when there is noncomputable theory already

#### Johan Commelin (Nov 04 2020 at 15:31):

I saw that complaint... it's a bit silly, because there was noncomputable theory at the top of the file. Don't know why it still complained.