Pruebas de length (replicate n x) = n

José A. Alonso

29-07-2024

En Lean4 están definidas las funciones length y replicate tales que

(length xs) es la longitud de la lista xs. Por ejemplo,
```
length [1,2,5,2] = 4
```
(replicate n x) es la lista que tiene el elemento x n veces. Por ejemplo,
```
replicate 3 7 = [7, 7, 7]
```

Demostrar que

length (replicate n x) = n

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Data.List.Basic
open Nat
open List

variable {α : Type}
variable (x : α)
variable (n : ℕ)

example :
  length (replicate n x) = n :=
by sorry

1. Demostración en lenguaje natural

Por inducción en n

Caso base:

length (replicate 0 x) = length []
                       = 0

Paso de inducción: Se supone la hipótesis de inducción

length (replicate n x) = n    (HI)

Entonces,

length (replicate (n+1) x)
= length (x :: replicate n x)
= length (replicate n x) + 1
= n + 1                         [por la HI]

2. Demostraciones con Lean4

import Mathlib.Data.List.Basic
open Nat
open List

variable {α : Type}
variable (x : α)
variable (n : ℕ)

-- 1ª demostración
-- ===============

example :
  length (replicate n x) = n :=
by
  induction' n with n HI
  . calc length (replicate 0 x)
          = length []                   := rfl
        _ = 0                           := length_nil
  . calc length (replicate (n+1) x)
         = length (x :: replicate n x)  := congr_arg length (replicate_succ x n)
       _ = length (replicate n x) + 1   := length_cons x (replicate n x)
       _ = n + 1                        := congrArg (. + 1) HI

-- 2ª demostración
-- ===============

example :
  length (replicate n x) = n :=
by
  induction' n with n HI
  . calc length (replicate 0 x)
          = length []                   := rfl
        _ = 0                           := rfl
  . calc length (replicate (n+1) x)
         = length (x :: replicate n x)  := rfl
       _ = length (replicate n x) + 1   := rfl
       _ = n + 1                        := by rw [HI]

-- 3ª demostración
-- ===============

example : length (replicate n x) = n :=
by
  induction' n with n HI
  . rfl
  . dsimp
    rw [HI]

-- 4ª demostración
-- ===============

example : length (replicate n x) = n :=
by
  induction' n with n HI
  . simp
  . simp [HI]

-- 5ª demostración
-- ===============

example : length (replicate n x) = n :=
by induction' n <;> simp [*]

-- 6ª demostración
-- ===============

example : length (replicate n x) = n :=
length_replicate n x

-- 7ª demostración
-- ===============

example : length (replicate n x) = n :=
by simp

-- 8ª demostración
-- ===============

lemma length_replicate_1 n (x : α) :
  length (replicate n x) = n :=
by induction n with
  | zero => calc
    length (replicate 0 x)
      = length ([] : List α)         := by simp only [replicate_zero]
    _ = 0                            := length_nil
  | succ n HI => calc
    length (replicate  (n + 1) x)
      = length (x :: replicate n x) := by simp only [replicate_succ]
    _ = length (replicate n x) + 1  := by simp only [length_cons]
    _ = n + 1                       := by simp only [succ_eq_add_one, HI]

-- 9ª demostración
-- ===============

lemma length_replicate_2 n (x : α) :
  length (replicate n x) = n :=
by induction n with
  | zero => calc
    length (replicate 0 x)
      = length ([] : List α)        := rfl
    _ = 0                           := rfl
  | succ n HI => calc
    length (replicate  (n + 1) x)
      = length (x :: replicate n x) := rfl
    _ = length (replicate n x) + 1  := rfl
    _ = n + 1                       := congrArg (. + 1) HI

-- 10ª demostración
-- ================

lemma length_replicate_3 n (x : α) :
  length (replicate n x) = n :=
by induction n with
  | zero      => simp
  | succ n HI => simp only [HI, replicate_succ, length_cons, Nat.succ_eq_add_one]

-- 11ª demostración
-- ===============

lemma length_replicate_4 :
  ∀ n, length (replicate n x) = n
| 0     => by simp
| (n+1) => by simp [*]

-- Lemas usados
-- ============

-- variable (xs : List α)
-- #check (length_cons x xs : length (x :: xs) = length xs + 1)
-- #check (length_nil : length [] = 0)
-- #check (length_replicate n x : length (replicate n x) = n)
-- #check (replicate_succ x n : replicate (n + 1) x = x :: replicate n x)
-- #check (replicate_zero x : replicate 0 x = [])
-- #check (succ_eq_add_one n : succ n = n + 1)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory "Pruebas_de_length_(repeat_x_n)_Ig_n"
imports Main
begin

(* 1ª demostración⁾*)

lemma "length (replicate n x) = n"
proof (induct n)
  have "length (replicate 0 x) = length ([] :: 'a list)"
    by (simp only: replicate.simps(1))
  also have "… = 0"
    by (rule list.size(3))
  finally show "length (replicate 0 x) = 0"
    by this
next
  fix n
  assume HI : "length (replicate n x) = n"
  have "length (replicate (Suc n) x) =
        length (x # replicate n x)"
    by (simp only: replicate.simps(2))
  also have "… = length (replicate n x) + 1"
    by (simp only: list.size(4))
  also have "… = Suc n"
    by (simp only: HI)
  finally show "length (replicate (Suc n) x) = Suc n"
    by this
qed

(* 2ª demostración⁾*)

lemma "length (replicate n x) = n"
proof (induct n)
  show "length (replicate 0 x) = 0"
    by simp
next
  fix n
  assume "length (replicate n x) = n"
  then show "length (replicate (Suc n) x) = Suc n"
    by simp
qed

(* 3ª demostración⁾*)

lemma "length (replicate n x) = n"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed

(* 4ª demostración⁾*)

lemma "length (replicate n x) = n"
  by (rule length_replicate)

end