Introducing sequence defined by a recurrence relation

Stream: new members

[Alain Muller]

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 ?

[Adam Topaz]

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

[Adam Topaz]

For example:

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

[Kevin Buzzard]

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.

[Mario Carneiro]

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

[Alain Muller]

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 ?

[Adam Topaz]

Note: you can use double $ for latex in zulip

[Adam Topaz]

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

[Patrick Massot]

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)),

[Patrick Massot]

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!)

[Adam Topaz]

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

[Alain Muller]

Thanks a lot !

[Alain Muller]

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 ?

[Kenny Lau]

it means add the following after your imports:

noncomputable theory
open_locale classical

[Alain Muller]

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$, $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 ?

[Patrick Massot]

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

[Alain Muller]

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

[Jalex Stark]

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