Relación entre los índices de las subsucesiones y los de la sucesión

Para extraer una subsucesión se aplica una función de extracción que conserva el orden; por ejemplo, la subsucesión

   uₒ, u₂, u₄, u₆, ...

1	uₒ, u₂, u₄, u₆, ...

se ha obtenido con la función de extracción φ tal que φ(n) = 2*n.

En Lean, se puede definir que φ es una función de extracción por

   def extraccion (φ : ℕ → ℕ) :=
     ∀ {n m}, n < m → φ n < φ m

1 2	def extraccion (φ : ℕ → ℕ) := ∀ {n m}, n < m → φ n < φ m

Demostrar que si φ es una función de extracción, entonces

   ∀ n, n ≤ φ n

1	∀ n, n ≤ φ n

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

import tactic
open nat

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ) :=
  ∀ {n m}, n < m → φ n < φ m

example :
  extraccion φ → ∀ n, n ≤ φ n :=
sorry

import tactic

open nat

variable {φ : ℕ → ℕ}

def extraccion (φ : ℕ → ℕ) :=

∀ {n m}, n < m → φ n < φ m

example :

extraccion φ → ∀ n, n ≤ φ n :=

sorry

[expand title=»Soluciones con Lean»]

import tactic
open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

def extraccion (φ : ℕ → ℕ) :=
  ∀ {n m}, n < m → φ n < φ m

-- 1ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    have h1 : m < succ m := lt_add_one m,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h h1, },
end

-- 2ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
begin
  intros h n,
  induction n with m HI,
  { exact nat.zero_le (φ 0), },
  { apply nat.succ_le_of_lt,
    calc m ≤ φ m        : HI
       ... < φ (succ m) : h (lt_add_one m), },
end

-- 3ª demostración
example :
  extraccion φ → ∀ n, n ≤ φ n :=
assume h : extraccion φ,
assume n,
nat.rec_on n
  ( show 0 ≤ φ 0,
      from nat.zero_le (φ 0) )
  ( assume m,
    assume HI : m ≤ φ m,
    have h1 : m < succ m,
      from lt_add_one m,
    have h2 : m < φ (succ m), from
      calc m ≤ φ m        : HI
         ... < φ (succ m) : h h1,
    show succ m ≤ φ (succ m),
      from nat.succ_le_of_lt h2)

import tactic

open nat

variable {φ : ℕ → ℕ}

set_option pp.structure_projections false

def extraccion (φ : ℕ → ℕ) :=

∀ {n m}, n < m → φ n < φ m

-- 1ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

have h1 : m < succ m := lt_add_one m,

calc m ≤ φ m : HI

... < φ (succ m) : h h1, },

end

-- 2ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

begin

intros h n,

induction n with m HI,

{ exact nat.zero_le (φ 0), },

{ apply nat.succ_le_of_lt,

calc m ≤ φ m : HI

... < φ (succ m) : h (lt_add_one m), },

end

-- 3ª demostración

example :

extraccion φ → ∀ n, n ≤ φ n :=

assume h : extraccion φ,

assume n,

nat.rec_on n

( show 0 ≤ φ 0,

from nat.zero_le (φ 0) )

( assume m,

assume HI : m ≤ φ m,

have h1 : m < succ m,

from lt_add_one m,

have h2 : m < φ (succ m), from

calc m ≤ φ m : HI

... < φ (succ m) : h h1,

show succ m ≤ φ (succ m),

from nat.succ_le_of_lt h2)

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones con Isabelle/HOL»]

theory Relacion_entre_los_indices_de_las_subsucesiones_y_de_la_sucesion
imports Main
begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where
  "extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

(* En la demostración se usará el siguiente lema *)
lemma extraccionE:
  assumes "extraccion φ"
          "n < m"
  shows   "φ n < φ m"
proof -
  have "∀ n m. n < m ⟶ φ n < φ m"
    using assms(1) by (unfold extraccion_def)
  then have "n < m ⟶ φ n < φ m"
    by (elim allE)
  then show "φ n < φ m"
    using assms(2) by (rule mp)
qed

(* 1ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "φ n < φ (Suc n)"
  proof -
    have "n < Suc n"
      by (rule lessI)
    with assms show "φ n < φ (Suc n)"
      by (rule extraccionE)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 2ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
  using assms
  proof (rule extraccionE)
    show "n < Suc n"
      by (rule lessI)
  qed
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 3ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by (rule le0)
next
  fix n
  assume "n ≤ φ n"
  also have "… < φ (Suc n)"
    by (rule extraccionE [OF assms lessI])
  finally show "Suc n ≤ φ (Suc n)"
    by (rule Suc_leI)
qed

(* 4ª demostración *)
lemma
  assumes "extraccion φ"
  shows   "n ≤ φ n"
proof (induct n)
  show "0 ≤ φ 0"
    by simp
next
  fix n
  assume HI : "n ≤ φ n"
  also have "φ n < φ (Suc n)"
    using assms extraccion_def by blast
  finally show "Suc n ≤ φ (Suc n)"
    by simp
qed

end

theory Relacion_entre_los_indices_de_las_subsucesiones_y_de_la_sucesion

imports Main

begin

definition extraccion :: "(nat ⇒ nat) ⇒ bool" where

"extraccion φ ⟷ (∀ n m. n < m ⟶ φ n < φ m)"

(* En la demostración se usará el siguiente lema *)

lemma extraccionE:

assumes "extraccion φ"

"n < m"

shows "φ n < φ m"

proof -

have "∀ n m. n < m ⟶ φ n < φ m"

using assms(1) by (unfold extraccion_def)

then have "n < m ⟶ φ n < φ m"

by (elim allE)

then show "φ n < φ m"

using assms(2) by (rule mp)

qed

(* 1ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "φ n < φ (Suc n)"

proof -

have "n < Suc n"

by (rule lessI)

with assms show "φ n < φ (Suc n)"

by (rule extraccionE)

qed

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 2ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "… < φ (Suc n)"

using assms

proof (rule extraccionE)

show "n < Suc n"

by (rule lessI)

qed

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 3ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by (rule le0)

fix n

assume "n ≤ φ n"

also have "… < φ (Suc n)"

by (rule extraccionE [OF assms lessI])

finally show "Suc n ≤ φ (Suc n)"

by (rule Suc_leI)

qed

(* 4ª demostración *)

lemma

assumes "extraccion φ"

shows "n ≤ φ n"

proof (induct n)

show "0 ≤ φ 0"

by simp

fix n

assume HI : "n ≤ φ n"

also have "φ n < φ (Suc n)"

using assms extraccion_def by blast

finally show "Suc n ≤ φ (Suc n)"

by simp

qed

end

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Share this:

Escribe un comentarioCancel reply