Zulip Chat Archive

Stream: new members

Topic: Introducing sequence defined by a recurrence relation


view this post on Zulip Alain Muller (Aug 16 2020 at 14:03):

Is it possible to define a sequence defined by a recurrence relation in tactic mode ? If I were writing mathematics on paper I would write : let (u_n) be the sequence defined by u_0 = 0 (say) and for all n \in \N, u_{n+1} = f(u_n) (for some function f) and I would procede with the proof.

Is there a lean equivalent ? And if such a formulation exists, is there any way to introduce mutual recuresive definitions ?

view this post on Zulip Adam Topaz (Aug 16 2020 at 14:11):

I think you can probably say let u : nat -> A := nat.rec _ _ and fill in the holes.

view this post on Zulip Adam Topaz (Aug 16 2020 at 14:41):

For example:

example :  (f :   ),  i, f i > 0 :=
begin
  let f :    := nat.rec 1 (λ _ a : , 1 + a * a),
  use f,
  intro i,
  sorry,
end

view this post on Zulip Kevin Buzzard (Aug 16 2020 at 14:42):

Mutual recursives are compiled down to primitive recursives in the kernel, rather inefficiently apparently (I never use them) and people here usually discourage users from using mutual inductive types.

view this post on Zulip Mario Carneiro (Aug 16 2020 at 14:47):

You can use an auxiliary definition for this as well, which gives you the niceties of the equation compiler like definitional equations. Or you can reuse an existing definition, for example the sequence you wrote is also known as \lam n, f^[n] 0

view this post on Zulip Alain Muller (Aug 16 2020 at 15:58):

I am trying a different approach (from the tutorial) to prove the intermediate value theorem (problem number 0081).

example (f :   ) (hf :  x, continuous_at_pt f x) (h₀ : f 0 < 0) (h₁ : f 1 > 0) :
 x₀  I, f x₀ = 0 :=
begin
  sorry
end

What would be the better way to define two sequences (a_n) and (b_n) in tactic mode such that a_0 = 0, b_0 = 1 and for all n \in \N, if f((a_n + b_n)/2) \leq 0 ,a_{n+1} = (a_n + b_n)/2 and b_{n+1} = b_n else a_{n+1} = a_n and b_{n+1} = (a_n + b_n) /2 ?

view this post on Zulip Adam Topaz (Aug 16 2020 at 16:06):

Note: you can use double $ for latex in zulip

view this post on Zulip Adam Topaz (Aug 16 2020 at 16:06):

E.g. $$a+b = f(x)$$ gives a+b=f(x)a+b=f(x)

view this post on Zulip Patrick Massot (Aug 16 2020 at 16:10):

let ab :    ×  := λ n, nat.rec_on n (0, 1)
    (λ k uv, if f ((uv.1 + uv.2)/2)  0 then ((uv.1 + uv.2)/2, uv.2)
                                       else (uv.1, (uv.1 + uv.2)/2)),

view this post on Zulip Patrick Massot (Aug 16 2020 at 16:10):

But note that nothing in this tutorial prepared you for this, so you'll be on your own (you can ask questions here of course!)

view this post on Zulip Adam Topaz (Aug 16 2020 at 16:12):

To extract the sequences aia_i and bib_i from Patrick's code, you can compose with the projections from \R \x \R to \R

view this post on Zulip Alain Muller (Aug 16 2020 at 16:39):

Thanks a lot !

view this post on Zulip Alain Muller (Aug 17 2020 at 08:13):

I managed to do nothing inside the proof, so I wanted to play a little bit with the definition given by Patrick.

In a new file I added

import data.real.basic

def ab (f :   ) :    ×  := λ n, nat.rec_on n (0, 1)
    (λ k uv, if f ((uv.1 + uv.2)/2)  0 then ((uv.1 + uv.2)/2, uv.2)
                                       else (uv.1, (uv.1 + uv.2)/2))

Lean display this message : definition 'ab' is noncomputable, it depends on 'real.decidable_linear_order'

Can someone explain what does it mean and how to get rid of it ?

view this post on Zulip Kenny Lau (Aug 17 2020 at 08:14):

it means add the following after your imports:

noncomputable theory
open_locale classical

view this post on Zulip Alain Muller (Aug 17 2020 at 11:14):

I don't know how to handle if ... then ... else statements in a definition. If I define a constant sequence using this complicated definition :

import data.real.basic

noncomputable theory
open_locale classical

def ab (f :   ) :    ×  := λ n, nat.rec_on n (0, 1)
    (λ k uv, if f ((uv.1 + uv.2)/2)  0 then (uv.1, uv.2) else (uv.1, uv.2))

I am not able to prove that for all n n , $ab n = (0, 1) $$

I tried

example (f :   ) :  n : , ((ab f) n).1 = 0 :=
begin
  intro n,
  induction n with n hn,
  refl,
  by_cases f ( ((ab f n).1 + (ab f n).2)/2 )  0,
  sorry,
end

and I am stuck. Trying rw ab I thought it would change the goal to something clearer, but that is not the case. Is there something to do at this point ?

view this post on Zulip Patrick Massot (Aug 17 2020 at 12:12):

example (f :   ) :  n : , ((ab f) n).1 = 0 :=
begin
  intro n,
  induction n with n hn,
  { refl },
  { dsimp [ab] at *,
    split_ifs ; assumption }
end

view this post on Zulip Alain Muller (Aug 17 2020 at 14:14):

Thanks a lot, it was VERY helpful. I've been struggling with searching through the documentation without finding anything

view this post on Zulip Jalex Stark (Aug 18 2020 at 01:57):

what keywords did you search? we could try to add them to the documentation for split_ifs


Last updated: May 09 2021 at 18:17 UTC