Zulip Chat Archive

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!