Menu Close

Mes: septiembre 2021

Igualdad de bloques de una partición cuando tienen elementos comunes

Este ejercicio es el primero de una serie cuyo objetivo es demostrar que el tipo de las particiones de un conjunto X es isomorfo al tipo de las relaciones de equivalencia sobre X. El desarrollo de dicha serie está basado en la cuarta parte de la primera sesión del curso de Kevin Buzzard Formalising mathematics: workshop 1 — logic, sets, functions, relations.

Una partición de un conjunto A es un conjunto de subconjuntos no vacíos de A tal que todo elemento de A está exactamente en uno de dichos subconjuntos. Es decir, una famila de conjuntos C es una partición de A si se verifican las siguientes condiciones:

  • Los conjuntos de C son no vacíos; es decir,
     ∀ X ∈ C, X ≠ ∅.
  • Los conjuntos de C recubren A; es decir,
     ∀ a ∈ A, ∃ X ∈ C, a ∈ X
  • Los conjuntos de C son disjuntos entre sí; es decir,
     ∀ X Y ∈ C, X ∩ Y ≠ ∅ → X = Y

En Lean, se puede definir el tipo de las particiones sobre un tipo A mediante una estructura con 4 campos:

  • Un conjunto de subconjuntos de A llamados los bloques de la partición.
  • Una prueba de que los bloques son no vacíos.
  • Una prueba de que cada término de tipo A está en uno de los bloques.
  • Una prueba de que dos bloques con intersección no vacía son iguales.

Su definición es

    @[ext] structure particion (A : Type) :=
    (Bloques    : set (set A))
    (Hno_vacios : ∀ X ∈ Bloques, (X : set A).nonempty)
    (Hrecubren  : ∀ a, ∃ X ∈ Bloques, a ∈ X)
    (Hdisjuntos : ∀ X Y ∈ Bloques, (X ∩ Y : set A).nonempty → X = Y)

Con la definición anterior,

  • P : particion A expresa que P es una partición de A.
  • Bloques P es el conjunto de los bloque de P.
  • Hno_vacios P prueba que los bloques de P son no vacíos.
  • Hrecubren P prueba que los bloque de P recubren a A.
  • Hdisjuntos P prueba que los bloques de P son disjuntos entre sí

Demostrar que si dos bloques de una partición tienen un elemento en común, entonces son iguales.

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

import tactic
 
@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios :  X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  :  a,  X ∈ Bloques, a ∈ X)
(Hdisjuntos :  X Y ∈ Bloques, (X ∩ Y : set A).nonempty  X = Y)
 
namespace particion
 
variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}
 
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
sorry
 
end particion
Soluciones con Lean
import tactic
 
@[ext] structure particion (A : Type) :=
(Bloques    : set (set A))
(Hno_vacios :  X ∈ Bloques, (X : set A).nonempty)
(Hrecubren  :  a,  X ∈ Bloques, a ∈ X)
(Hdisjuntos :  X Y ∈ Bloques, (X ∩ Y : set A).nonempty  X = Y)
 
namespace particion
 
variable  {A : Type}
variable  {P : particion A}
variables {X Y : set A}
 
-- 1ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { rw set.nonempty_def,
    use a,
    split,
    { exact haX, },
    { exact haY, }},
end
 
-- 2ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { use a,
    exact ⟨haX, haY⟩, },
end
 
-- 3ª demostración
example
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
begin
  apply P.Hdisjuntos,
  { exact hX, },
  { exact hY, },
  { exact ⟨a, haX, haY⟩, },
end
 
-- 4ª demostración
lemma iguales_si_comun
  (hX : X ∈ Bloques P)
  (hY : Y ∈ Bloques P)
  {a : A}
  (haX : a ∈ X)
  (haY : a ∈ Y)
  : X = Y :=
Hdisjuntos P X Y hX hY ⟨a, haX, haY⟩
 
end particion

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>

Identidad de Brahmagupta-Fibonacci

Demostrar la identidad de Brahmagupta-Fibonacci

   (a² + b²)(c² + d²) = (ac - bd)² + (ad + bc)²

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

import data.real.basic
 
variables (a b c d : )
 
example :
  (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
sorry
Soluciones con Lean
import data.real.basic
 
variables (a b c d : )
 
-- 1ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
calc (a^2 + b^2) * (c^2 + d^2)
     = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)
         : right_distrib (a^2) (b^2) (c^2 + d^2)
 ... = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)
         : congr_arg2 (+) (left_distrib (a^2) (c^2) (d^2)) rfl
 ... = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)
         : congr_arg2 (+) rfl (left_distrib (b^2) (c^2) (d^2))
 ... = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)
         : by ring
 ... = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)
         : by ring
 ... = (a*c - b*d)^2 + (a*d + b*c)^2
         : by ring
 
-- 2ª demostración
example : (a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2 :=
by ring

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>

Soluciones con Isabelle/HOL
theory "Identidad_de_Brahmagupta-Fibonacci"
imports Main HOL.Real
begin
 
(* 1ª demostración *)
lemma
  fixes a b c d :: real
  shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"
proof -
  have "(a^2 + b^2) * (c^2 + d^2) = a^2 * (c^2 + d^2) + b^2 * (c^2 + d^2)"
    by (simp only: distrib_right)
  also have "… = (a^2*c^2 + a^2*d^2) + b^2 * (c^2 + d^2)"
    by (simp only: distrib_left)
  also have "… = (a^2*c^2 + a^2*d^2) + (b^2*c^2 + b^2*d^2)"
    by (simp only: distrib_left)
  also have "… = ((a*c)^2 + (b*d)^2) + ((a*d)^2 + (b*c)^2)"
    by algebra
  also have "… = ((a*c)^2 - 2*a*c*b*d + (b*d)^2) + ((a*d)^2 + 2*a*d*b*c + (b*c)^2)"
    by algebra
  also have "… = (a*c - b*d)^2 + (a*d + b*c)^2"
    by algebra
  finally show "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2" .
qed
 
(* 2ª demostración *)
lemma
  fixes a b c d :: real
  shows "(a^2 + b^2) * (c^2 + d^2) = (a*c - b*d)^2 + (a*d + b*c)^2"
by algebra
 
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>

Suma de potencias de dos

Demostrar que

   1 + 2 + 2² + 2³ + ... + 2⁽ⁿ⁻¹⁾ = 2ⁿ - 1

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

import algebra.big_operators
import tactic
open finset nat
 
open_locale big_operators
 
variable (n : )
 
example :
  ∑ k in range n, 2^k = 2^n - 1 :=
sorry
Soluciones con Lean
import algebra.big_operators
import tactic
open finset nat
 
open_locale big_operators
set_option pp.structure_projections false
 
variable (n : )
 
example :
  ∑ k in range n, 2^k = 2^n - 1 :=
begin
  induction n with n HI,
  { simp, },
  { calc ∑ k in range (succ n), 2^k
         = ∑ k in range n, 2^k + 2^n
             : sum_range_succ (λ x, 2 ^ x) n
     ... = (2^n - 1) + 2^n
             : congr_arg2 (+) HI rfl
     ... = (2^n + 2^n) - 1
             : by omega
     ... = 2^n * 2 - 1
             : by {congr; simp}
     ... = 2^(succ n) - 1
             : by {congr' 1; ring_nf}, },
end

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>

Soluciones con Isabelle/HOL
theory Suma_de_potencias_de_dos
imports Main
begin
 
(* 1ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (∑k≤n. (2::nat)^k) + 2^Suc n"
    by simp
  also have "… = (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  also have "… = 2^(Suc n + 1) - 1"
    by simp
  finally show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1" .
qed
 
(* 2ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  show "(∑k≤0. (2::nat)^k) = 2^(0+1) - 1"
    by simp
next
  fix n
  assume HI : "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
  have "(∑k≤Suc n. (2::nat)^k) =
        (2^(n+1) - 1) + 2^Suc n"
    using HI by simp
  then show "(∑k≤Suc n. (2::nat)^k) = 2^(Suc n + 1) - 1"
    by simp
qed
 
(* 3ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  then show ?case by simp
qed
 
(* 4ª demostración *)
lemma "(∑k≤n. (2::nat)^k) = 2^(n+1) - 1"
by (induct n) simp_all

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

Fórmula de Gauss de la suma de los primeros números naturales

La fórmula de Gauss para la suma de los primeros números naturales es

   0 + 1 + 2 + ... + (n-1) = n(n-1)/2

En un ejercicio anterior se ha demostrado dicha fórmula por inducción. Otra forma de demostrarla, sin usar inducción, es la siguiente: La suma se puede escribir de dos maneras

   S = 0     + 1     + 2     + ... + (n-3) + (n-2) + (n-1)
   S = (n-1) + (n-2) + (n-3) + ... + 2     + 1     + 0

Al sumar, se observa que cada par de números de la misma columna da como suma (n-1), y puesto que hay n columnas en total, se sigue

   2S = n(n-1)

lo que prueba la fórmula.

Demostrar la fórmula de Gauss siguiendo el procedimiento anterior.

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

import algebra.big_operators.basic
import algebra.big_operators.intervals
 
open_locale big_operators
open finset nat
 
variables (n i : )
 
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
sorry
Soluciones con Lean
import algebra.big_operators.basic
import algebra.big_operators.intervals
 
open_locale big_operators
open finset nat
 
variables (n i : )
 
-- Lema auxiliar
-- =============
 
-- Se usará el siguiente lema auxiliar del que se presentan distintas
-- demostraciones.
 
-- 1ª demostración del lema auxiliar
example :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  replace hx : x < n := mem_range.1 hx,
  replace hx : x  n - 1 := le_pred_of_lt hx,
  exact nat.add_sub_cancel' hx,
end
 
-- 2ª demostración del lema auxiliar
example :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
begin
  intros x hx,
  exact nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx)),
end
 
-- 3ª demostración del lema auxiliar
lemma auxiliar :  x, x ∈ range n  x + (n - 1 - x) = n - 1 :=
λ x hx, nat.add_sub_cancel' (le_pred_of_lt (mem_range.1 hx))
 
-- Lema principal
-- ==============
 
-- 1ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, i)
         : mul_two _
 ... = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : congr_arg2 (+) rfl (sum_range_reflect id n).symm
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = card (range n)(n - 1)
         : sum_const (n - 1)
 ... = card (range n) * (n - 1)
         : nat.nsmul_eq_mul _ _
 ... = n * (n - 1)
         : congr_arg2 (*) (card_range n) rfl
 
-- 2ª demostración
example :
  (∑ i in range n, i) * 2 = n * (n - 1) :=
calc (∑ i in range n, i) * 2
     = (∑ i in range n, i) + (∑ i in range n, (n - 1 - i))
         : by rw [sum_range_reflect (λ i, i) n, mul_two]
 ... = ∑ i in range n, (i + (n - 1 - i))
         : sum_add_distrib.symm
 ... = ∑ i in range n, (n - 1)
         : sum_congr rfl (auxiliar n)
 ... = n * (n - 1)
         : by rw [sum_const, card_range, nat.nsmul_eq_mul]

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>

Soluciones con Isabelle/HOL
theory Formula_de_Gauss_de_la_suma
imports Main
begin
 
lemma
  fixes n :: nat
  shows "2 * (∑i<n. i) = n * (n - 1)"
proof -
  have "2 * (∑i<n. i) = (∑i<n. i) + (∑i<n. i)"
    by simp
  also have "… = (∑i<n. i) + (∑i<n. n - Suc i)"
    using sum.nat_diff_reindex [where g = id] by auto
  also have "… = (∑i<n. (i + (n - Suc i)))"
    using sum.distrib [where A = "{..<n}" and
                             g = id and
                             h = "λi. n - Suc i"] by auto
  also have "… = (∑i<n. n - 1)"
    by simp
  also have "… = n * (n -1)"
    using sum_constant by auto
  finally show "2 * (∑i<n. i) = n * (n - 1)" .
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>

Prueba de (1+p)ⁿ ≥ 1+np

Sean p ∈ ℝ y n ∈ ℕ tales que p > -1. Demostrar que

   (1 + p)ⁿ ≥ 1 + np

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

import data.real.basic
open nat
 
variable (p : )
variable (n : )
 
example
  (h : p > -1)
  : (1 + p)^n  1 + n*p :=
begin
sorry
Soluciones con Lean
import data.real.basic
open nat
 
variable (p : )
variable (n : )
 
set_option pp.structure_projections false
 
example
  (h : p > -1)
  : (1 + p)^n  1 + n*p :=
begin
  induction n with n HI,
  { simp, },
  { have h1 : 1 + p > 0 := iff.mp neg_lt_iff_pos_add' h,
    have h2 : p*p  0 := mul_self_nonneg p,
    replace h2 : ↑n*(p*p)  0 := mul_nonneg (cast_nonneg n) h2,
    calc (1 + p)^succ n
         = (1 + p)^n * (1 + p)
             : pow_succ' (1 + p) n
     ...  (1 + n * p) * (1 + p)
             : (mul_le_mul_right h1).mpr HI
     ... = (1 + p + n*p) + n*(p*p)
             : by ring !
     ...  1 + p + n*p
             : le_add_of_nonneg_right h2
     ... = 1 + (n + 1) * p
             : by ring !
     ... = 1 +(succ n) * p
             : by norm_num },
end

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>

Soluciones con Isabelle/HOL
theory "Prueba_de_(1+p)^n_mayor_o_igual_que_1+np"
imports Main HOL.Real
begin
 
lemma
  fixes p :: real
  assumes "p > -1"
  shows "(1 + p)^n ≥ 1 + n*p"
proof (induct n)
  show "(1 + p) ^ 0 ≥ 1 + real 0 * p"
    by simp
next
  fix n
  assume HI : "(1 + p)^n ≥ 1 +  n * p"
  have "1 + Suc n * p = 1 + (n + 1) * p"
    by simp
  also have "… = 1 + n*p + p"
    by (simp add: distrib_right)
  also have "… ≤ (1 + n*p + p) + n*(p*p)"
    by simp
  also have "… = (1 + n * p) * (1 + p)"
    by algebra
  also have "… ≤ (1 + p)^n * (1 + p)"
    using HI assms by simp
  also have "… = (1 + p)^(Suc n)"
    by simp
  finally show "1 + Suc n * p ≤ (1 + p)^(Suc n)" .
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>