Zulip Chat Archive

Stream: new members

Topic: First order recurrence


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Adrián Doña Mateo (Nov 04 2020 at 15:10):

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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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]

view this post on Zulip Johan Commelin (Nov 04 2020 at 15:20):

by rw [a, a, h] also works

view this post on Zulip Reid Barton (Nov 04 2020 at 15:26):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:31):

there is a bug about this

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:32):

lean#451


Last updated: May 13 2021 at 21:12 UTC