# Zulip Chat Archive

## 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 see`nat.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.

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

there is a bug about this

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

Last updated: May 13 2021 at 21:12 UTC