## Stream: new members

### Topic: Introducing sequence defined by a recurrence relation

#### 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 ?

#### 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.

#### 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


#### 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.

#### 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

#### 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 ?

Note: you can use double $for latex in zulip #### Adam Topaz (Aug 16 2020 at 16:06): E.g. $a+b = f(x)$ gives $a+b=f(x)$ #### 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)),  #### 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!) #### Adam Topaz (Aug 16 2020 at 16:12): 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 (Aug 16 2020 at 16:39): Thanks a lot ! #### 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 ? #### Kenny Lau (Aug 17 2020 at 08:14): it means add the following after your imports: noncomputable theory open_locale classical  #### 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$,$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 (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


#### 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

#### 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