Best way to formalize finite sequences

Stream: new members

[Pablo Donato]

I am wondering if there exists any formalization of finite sequences in mathlib? In solving some exercise involving finite sequences of real numbers, I have considered the three following possible definitions:

1. As lists:

def RFinSeq := List ℝ

2. As functions from $\{0, 1, 2, \ldots, n\}$ with $n \in \mathbb{N}$ the sequence's length:

def RFinSeq := ∀ n, Fin n → ℝ

3. As functions from $\mathbb{N}$:

def RFinSeq := ℕ → ℝ

While definitions 1. and 2. are more accurate, I ended up choosing definition 3. (which in fact describes infinite sequences) because proofs were much simpler, and finiteness did not play any role in this specific exercise. Indeed, the use of dependent types in definition 2. brought the infamous transport hell, making rewriting infeasible with occurrences of cast all over the place. I actually haven't tried definition 1., but I suspect it would make accessing any element in a sequence and combining sequences very awkward.

[Violeta Hernández]

I believe Fin n → α is generally the preferred form

[Violeta Hernández]

But of course, if ℕ → α is enough for what you're doing, you'll probably be better off using that

[Mitchell Lee]

List is designed to be the formalization of finite sequences. It can be used with reasoning. To access elements of a List, use getD (docs#List.getD) or getI (docs#List.getI), which can be used even if the provided index is out of bounds.

[Pablo Donato]

thanks for your answers! I have tried redoing the exercise with List for a challenge, but it gets a bit hairy at some point. I don't have time to dig deeper, so I'll let my partial solution here if anyone is interested:

import Mathlib

/-
  Given a finite sequence $S=(a_1,a_2,\ldots ,a_n)$ of $n$ real numbers, let $A(S)$ be the
  sequence $\left(\frac{a_1+a_2}{2},\frac{a_2+a_3}{2},\ldots ,\frac{a_{n-1}+a_n}{2}\right)$ of $n-1$
  real numbers. Define $A^1(S)=A(S)$ and, for each integer $m$, $2\le m\le n-1$, define
  $A^m(S)=A(A^{m-1}(S))$. Suppose $x>0$, and let $S=(1,x,x^2,\ldots ,x^{100})$. If
  $A^{100}(S)=(1/2^{50})$, then what is $x$? $\mathrm{(A) \ } 1-\frac{\sqrt{2}}{2}\qquad \mathrm{(B)
  \ } \sqrt{2}-1\qquad \mathrm{(C) \ } \frac{1}{2}\qquqquad \mathrm{(D) \ } 2-\sqrt{2}\qquad
  \mathrm{(E) \ }  \frac{\sqrt{2}}{2}$
-/

open Real List

/-- Geometric sequence with n terms -/
def geom_seq (n : ℕ) (x : ℝ) : List ℝ :=
  List.range (n + 1) |>.map (x ^ ·)

/-- Definition of A(·) for lists - averages adjacent terms -/
noncomputable def A (s : List ℝ) : List ℝ :=
  List.zipWith (fun a b => (a + b) / 2) (s.take (s.length - 1)) s.tail

theorem algebra_1166 (x : ℝ) (hx : x > 0) :
    let S := geom_seq 100;
    A^[100] (S x) = [1 / 2 ^ 50] →
    x = √2 - 1 := by
  intro S h
  /- In general,
  $A^n(S)=\left(\frac{(x+1)^n}{2^n},\frac{x(x+1)^n}{2^n},...,\frac{x^{100-n}(x+1)^n}{2^n}\right)$
  such that $A^n(s)$ has $101-n$ terms. -/
  have A_iter_value : ∀ (n : ℕ),
      A^[n] (S x) = (List.range (101 - n)).map (fun i => x ^ i * (x + 1) ^ n / 2 ^ n) := by {
    intro n
    induction n with
    | zero =>
      simp [S, geom_seq]
    | succ n ih =>
      simp only [Function.iterate_succ', Function.comp_apply, Nat.reduceSubDiff]
      rw [ih]
      generalize he : (fun i ↦ x ^ i * (x + 1) ^ n / 2 ^ n) = e
      generalize he' : (fun i ↦ x ^ i * (x + 1) ^ (n + 1) / 2 ^ (n + 1)) = e'
      let E := fun k => (fun i ↦ x ^ i * (x + 1) ^ k / 2 ^ k)
      have eqEe : e = E n := by sorry
      have eqEe' : e' = E (n + 1) := by sorry
      rw [eqEe, eqEe']
      simp only [A]
      generalize hl : map (E n) (range (101 - n)) = l
      sorry -- I get stuck here
  }
  /- Specifically, $A^{100}(S)=\frac{(x+1)^{100}}{2^{100}}$. -/
  specialize A_iter_value 100
  rw [h] at A_iter_value
  simp only [range, range.loop, map_cons, pow_zero, one_mul, map_nil, cons.injEq,
    and_true] at A_iter_value
  have eq1 : 1 / 2 ^ 50 = (x + 1) ^ 100 / 2 ^ 100 := by rw [← A_iter_value]
  /- so $(1+x)^{100}=2^{50}$, -/
  have eq2 : (x + 1) ^ 100 = 2 ^ 50 := by
    calc (x + 1) ^ 100 = (x + 1) ^ 100 / 2 ^ 100 * 2 ^ 100 := by field_simp
                     _ = 1 / 2 ^ 50  * 2 ^ 100 := by rw [← eq1]
                     _ = 2 ^ 50 := by ring
  /- and because $x>0$, we have $x=\boxed{\sqrt{2}-1}$. -/
  calc x = (x + 1) - 1 := by ring
       _ = ((x + 1) ^ 100) ^ (↑(100 : ℕ) : ℝ)⁻¹ - 1 := by rw [pow_rpow_inv_natCast] <;> linarith
       _ = (2 ^ 50) ^ ((1 / 100) : ℝ) - 1 := by rw [eq2]; field_simp
       _ = 2 ^ ((50 * (1 / 100)) : ℝ) - 1 := by rw [← rpow_natCast, ← rpow_mul _ _]; simp; linarith
       _ = 2 ^ ((1 / 2) : ℝ) - 1 := by norm_num
       _ = √2 - 1 := by rw [← sqrt_eq_rpow]

[Pablo Donato]

and here is the simple solution when generalizing to infinite sequences:

import Mathlib

/-
  Given a finite sequence $S=(a_1,a_2,\ldots ,a_n)$ of $n$ real numbers, let $A(S)$ be the
  sequence $\left(\frac{a_1+a_2}{2},\frac{a_2+a_3}{2},\ldots ,\frac{a_{n-1}+a_n}{2}\right)$ of $n-1$
  real numbers. Define $A^1(S)=A(S)$ and, for each integer $m$, $2\le m\le n-1$, define
  $A^m(S)=A(A^{m-1}(S))$. Suppose $x>0$, and let $S=(1,x,x^2,\ldots ,x^{100})$. If
  $A^{100}(S)=(1/2^{50})$, then what is $x$? $\mathrm{(A) \ } 1-\frac{\sqrt{2}}{2}\qquad \mathrm{(B)
  \ } \sqrt{2}-1\qquad \mathrm{(C) \ } \frac{1}{2}\qquad \mathrm{(D) \ } 2-\sqrt{2}\qquad
  \mathrm{(E) \ }  \frac{\sqrt{2}}{2}$
-/

open Real

/- Definition of $A(S)$ -/
noncomputable def A (S : ℕ → ℝ) : ℕ → ℝ := fun i => (S i + S (i + 1)) / 2

/- Definition of $A^m(S)$ -/
noncomputable def A_iter (m : ℕ) (S : ℕ → ℝ) : ℕ → ℝ :=
  match m with
  | 0 => S
  | m + 1 => A (A_iter m S)

theorem algebra_1166 (x : ℝ) (hx : x > 0) :
    let S := fun (x : ℝ) => (x ^ ·);
    A_iter 100 (S x) 0 = 1 / 2 ^ 50 →
    x = √2 - 1 := by
  intro S h
  /- In general,
  $A^n(S)=\left(\frac{(x+1)^n}{2^n},\frac{x(x+1)^n}{2^n},...,\frac{x^{100-n}(x+1)^n}{2^n}\right)$
  such that $A^n(s)$ has $101-n$ terms. -/
  have A_iter_value : ∀ (n : ℕ), A_iter n (S x) = fun i => x ^ i * (x + 1) ^ n / 2 ^ n := by {
    intro n
    induction n with
    | zero =>
      funext i
      simp [A_iter]
    | succ n ih =>
      funext i
      simp only [A_iter]
      rw [ih]
      simp only [A]
      ring
  }
  /- Specifically, $A^{100}(S)=\frac{(x+1)^{100}}{2^{100}}$. -/
  specialize A_iter_value 100
  apply funext_iff.1 at A_iter_value
  specialize A_iter_value 0
  rw [pow_zero, one_mul] at A_iter_value
  /- To find x, we need only solve the equation $\frac{(x+1)^{100}}{2^{100}}=\frac{1}{2^{50}}$. -/
  have eq1 : 1 / 2 ^ 50 = (x + 1) ^ 100 / 2 ^ 100 := by rw [← h, ← A_iter_value]
  /- so $(1+x)^{100}=2^{50}$, -/
  have eq2 : (x + 1) ^ 100 = 2 ^ 50 := by
    calc (x + 1) ^ 100 = (x + 1) ^ 100 / 2 ^ 100 * 2 ^ 100 := by field_simp
                     _ = 1 / 2 ^ 50  * 2 ^ 100 := by rw [← eq1]
                     _ = 2 ^ 50 := by ring
  /- and because $x>0$, we have $x=\boxed{\sqrt{2}-1}$. -/
  calc x = (x + 1) - 1 := by ring
       _ = ((x + 1) ^ 100) ^ (↑(100 : ℕ) : ℝ)⁻¹ - 1 := by rw [pow_rpow_inv_natCast] <;> linarith
       _ = (2 ^ 50) ^ ((1 / 100) : ℝ) - 1 := by rw [eq2]; field_simp
       _ = 2 ^ ((50 * (1 / 100)) : ℝ) - 1 := by rw [← rpow_natCast, ← rpow_mul _ _]; simp; linarith
       _ = 2 ^ ((1 / 2) : ℝ) - 1 := by norm_num
       _ = √2 - 1 := by rw [← sqrt_eq_rpow]