La semana en Calculemus (16 de septiembre de 2023)

Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades:

1. En ℝ, |a| – |b| ≤ |a – b|
2. Si x, y, z ∈ ℕ, entonces x divide a yxz
3. Si x divide a w, entonces también divide a y(xz)+x²+w²
4. Conmutatividad del máximo común divisor
5. En los retículos, x ⊓ y = y ⊓ x

A continuación se muestran las soluciones.

1. En ℝ, |a| – |b| ≤ |a – b|

Demostrar con Lean4 que si $a$ y $b$ números reales, entonces
$|a| – |b| \leq |a – b|$

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

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

example : |a| - |b| ≤ |a - b| :=
by sorry

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

example : |a| - |b| ≤ |a - b| :=

by sorry

Demostraciones en lenguaje natural (LN)

1ª demostración en LN

Por la siguiente cadena de desigualdades
$\begin{align} |a| – |b| &= |a – b + b| – |b| \\ &\leq (|a – b| + |b|) – |b| &&\text{[por la desigualdad triangular]}\\ &= |a – b| \end{align}$

2ª demostración en LN

Por la desigualdad triangular
$|a – b + b| \leq |a – b| + |b|$
simplificando en la izquierda
$|a| \leq |a – b| + |b|$
y, pasando $|b|$ a la izquierda
$|a| – |b| ≤ |a – b|$

Demostraciones con Lean4

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

-- 1ª demostración (basada en la 1ª en LN)
example : |a| - |b| ≤ |a - b| :=
calc |a| - |b|
     = |a - b + b| - |b| :=
          congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm
   _ ≤ (|a - b| + |b|) - |b| :=
           sub_le_sub_right (abs_add (a - b) b) (|b|)
   _ = |a - b| :=
          add_sub_cancel (|a - b|) (|b|)

-- 2ª demostración (basada en la 1ª en LN)
example : |a| - |b| ≤ |a - b| :=
calc |a| - |b|
     = |a - b + b| - |b| := by
          rw [sub_add_cancel]
   _ ≤ (|a - b| + |b|) - |b| := by
          apply sub_le_sub_right
          apply abs_add
   _ = |a - b| := by
          rw [add_sub_cancel]

-- 3ª demostración (basada en la 2ª en LN)
example : |a| - |b| ≤ |a - b| :=
by
  have h1 : |a - b + b| ≤ |a - b| + |b| := abs_add (a - b) b
  rw [sub_add_cancel] at h1
  exact abs_sub_abs_le_abs_sub a b

-- 4ª demostración
example : |a| - |b| ≤ |a - b| :=
abs_sub_abs_le_abs_sub a b

import Mathlib.Data.Real.Basic

variable (a b : ℝ)

-- 1ª demostración (basada en la 1ª en LN)

example : |a| - |b| ≤ |a - b| :=

calc |a| - |b|

= |a - b + b| - |b| :=

congrArg (fun x => |x| - |b|) (sub_add_cancel a b).symm

_ ≤ (|a - b| + |b|) - |b| :=

sub_le_sub_right (abs_add (a - b) b) (|b|)

_ = |a - b| :=

add_sub_cancel (|a - b|) (|b|)

-- 2ª demostración (basada en la 1ª en LN)

example : |a| - |b| ≤ |a - b| :=

calc |a| - |b|

= |a - b + b| - |b| := by

rw [sub_add_cancel]

_ ≤ (|a - b| + |b|) - |b| := by

apply sub_le_sub_right

apply abs_add

_ = |a - b| := by

rw [add_sub_cancel]

-- 3ª demostración (basada en la 2ª en LN)

example : |a| - |b| ≤ |a - b| :=

have h1 : |a - b + b| ≤ |a - b| + |b| := abs_add (a - b) b

rw [sub_add_cancel] at h1

exact abs_sub_abs_le_abs_sub a b

-- 4ª demostración

example : |a| - |b| ≤ |a - b| :=

abs_sub_abs_le_abs_sub a b

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 18.

2. Si x, y, z ∈ ℕ, entonces x divide a yxz

Demostrar con Lean4 que si $x,y,z \in \mathbb{N}$ , entonces $x \mid yxz$ .

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

import Mathlib.Data.Real.Basic
variable (x y z : ℕ)

example : x ∣ y * x * z :=
by sorry

import Mathlib.Data.Real.Basic

variable (x y z : ℕ)

example : x ∣ y * x * z :=

by sorry

Demostración en lenguaje natural

Por la transitividad de la divisibilidad aplicada a las relaciones
$\begin{align} x &\mid yx \\ yx &\mid yxz \end{align}$

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable (x y z : ℕ)

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

example : x ∣ y * x * z :=
by
  have h1 : x ∣ y * x :=
    dvd_mul_left x y
  have h2 : (y * x) ∣ (y * x * z) :=
    dvd_mul_right (y * x) z
  show x ∣ y * x * z
  exact dvd_trans h1 h2

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

example : x ∣ y * x * z :=
dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)

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

example : x ∣ y * x * z :=
by
  apply dvd_mul_of_dvd_left
  apply dvd_mul_left


-- Los lemas utilizados son:
#check (dvd_mul_left x y : x ∣ y * x)
#check (dvd_mul_right x y : x ∣ x * y)
#check (dvd_trans : x ∣ y → y ∣ z → x ∣ z)

import Mathlib.Data.Real.Basic

variable (x y z : ℕ)

-- 1ª demostración

-- ===============

example : x ∣ y * x * z :=

have h1 : x ∣ y * x :=

dvd_mul_left x y

have h2 : (y * x) ∣ (y * x * z) :=

dvd_mul_right (y * x) z

show x ∣ y * x * z

exact dvd_trans h1 h2

-- 2ª demostración

-- ===============

example : x ∣ y * x * z :=

dvd_trans (dvd_mul_left x y) (dvd_mul_right (y * x) z)

-- 3ª demostración

-- ===============

example : x ∣ y * x * z :=

apply dvd_mul_of_dvd_left

apply dvd_mul_left

-- Los lemas utilizados son:

#check (dvd_mul_left x y : x ∣ y * x)

#check (dvd_mul_right x y : x ∣ x * y)

#check (dvd_trans : x ∣ y → y ∣ z → x ∣ z)

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 19.

3. Si x divide a w, entonces también divide a y(xz)+x²+w²

Demostrar con Lean4 que si $x$ divide a $w$ , entonces también divide a $y(xz)+x^2+w^2$ .

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

import Mathlib.Data.Real.Basic
variable (w x y z : ℕ)

example
  (h : x ∣ w)
  : x ∣ y * (x * z) + x^2 + w^2 :=
by sorry

import Mathlib.Data.Real.Basic

variable (w x y z : ℕ)

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

by sorry

Demostración en lenguaje natural

Por la divisibilidad de la suma basta probar que
$\begin{align} x &\mid yxz \tag{1} \\ x &\mid x^2 \tag{2} \\ x &\mid w^2 \tag{3} \end{align}$

Para demostrar (1), por la divisibilidad del producto se tiene
$x \mid xz$
y, de nuevo por la divisibilidad del producto,
$x \mid y(xz)$

La propiedad (2) se tiene por la definición de cuadrado y la divisibilidad del producto.

La propiedad (3) se tiene por la definición de cuadrado, la hipótesis y la divisibilidad del producto.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable (w x y z : ℕ)

-- 1ª demostración
example
  (h : x ∣ w)
  : x ∣ y * (x * z) + x^2 + w^2 :=
by
  have h1 : x ∣ x * z :=
    dvd_mul_right x z
  have h2 : x ∣ y * (x * z) :=
    dvd_mul_of_dvd_right h1 y
  have h3 : x ∣ x^2 := by
    apply dvd_mul_left
  have h4 : x ∣ w * w :=
    dvd_mul_of_dvd_left h w
  have h5 : x ∣ w^2 := by
    rwa [← pow_two w] at h4
  have h6 : x ∣ y * (x * z) + x^2 :=
    dvd_add h2 h3
  show x ∣ y * (x * z) + x^2 + w^2
  exact dvd_add h6 h5

-- 2ª demostración
example
  (h : x ∣ w)
  : x ∣ y * (x * z) + x^2 + w^2 :=
by
  apply dvd_add
  { apply dvd_add
    { apply dvd_mul_of_dvd_right
      apply dvd_mul_right }
    { rw [pow_two]
      apply dvd_mul_right }}
  { rw [pow_two]
    apply dvd_mul_of_dvd_left h }

-- 3ª demostración
example
  (h : x ∣ w)
  : x ∣ y * (x * z) + x^2 + w^2 :=
by
  repeat' apply dvd_add
  { apply dvd_mul_of_dvd_right
    apply dvd_mul_right }
  { rw [pow_two]
    apply dvd_mul_right }
  { rw [pow_two]
    apply dvd_mul_of_dvd_left h }

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

-- #check (dvd_add : x ∣ y → x ∣ z → x ∣ y + z)
-- #check (dvd_mul_left x y : x ∣ y * x)
-- #check (dvd_mul_right x y : x ∣ x * y)
-- #check (dvd_mul_of_dvd_left : x ∣ y → ∀ (c : ℕ), x ∣ y * c)
-- #check (dvd_mul_of_dvd_right : x ∣ y → ∀ (c : ℕ), x ∣ c * y)
-- #check (pow_two x : x ^ 2 = x * x)

import Mathlib.Data.Real.Basic

variable (w x y z : ℕ)

-- 1ª demostración

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

have h1 : x ∣ x * z :=

dvd_mul_right x z

have h2 : x ∣ y * (x * z) :=

dvd_mul_of_dvd_right h1 y

have h3 : x ∣ x^2 := by

apply dvd_mul_left

have h4 : x ∣ w * w :=

dvd_mul_of_dvd_left h w

have h5 : x ∣ w^2 := by

rwa [← pow_two w] at h4

have h6 : x ∣ y * (x * z) + x^2 :=

dvd_add h2 h3

show x ∣ y * (x * z) + x^2 + w^2

exact dvd_add h6 h5

-- 2ª demostración

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

apply dvd_add

{ apply dvd_add

{ apply dvd_mul_of_dvd_right

apply dvd_mul_right }

{ rw [pow_two]

apply dvd_mul_right }}

{ rw [pow_two]

apply dvd_mul_of_dvd_left h }

-- 3ª demostración

example

(h : x ∣ w)

: x ∣ y * (x * z) + x^2 + w^2 :=

repeat' apply dvd_add

{ apply dvd_mul_of_dvd_right

apply dvd_mul_right }

{ rw [pow_two]

apply dvd_mul_right }

{ rw [pow_two]

apply dvd_mul_of_dvd_left h }

-- Lemas usados

-- ============

-- #check (dvd_add : x ∣ y → x ∣ z → x ∣ y + z)

-- #check (dvd_mul_left x y : x ∣ y * x)

-- #check (dvd_mul_right x y : x ∣ x * y)

-- #check (dvd_mul_of_dvd_left : x ∣ y → ∀ (c : ℕ), x ∣ y * c)

-- #check (dvd_mul_of_dvd_right : x ∣ y → ∀ (c : ℕ), x ∣ c * y)

-- #check (pow_two x : x ^ 2 = x * x)

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 19.

4. Conmutatividad del máximo común divisor

Demostrar con Lean4 que si $m, n \in \mathbb{N}$ son números naturales, entonces
$\gcd(m, n) = \gcd(n, m)$

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

import Mathlib.Data.Real.Basic
variable (k m n : ℕ)

open Nat

example : gcd m n = gcd n m :=
by sorry

import Mathlib.Data.Real.Basic

variable (k m n : ℕ)

open Nat

example : gcd m n = gcd n m :=

by sorry

Demostración en lenguaje natural

Es consecuencia del siguiente lema auxiliar
$(\forall x, y \in \mathbb{N})[\gcd(x,y) \mid \gcd(y,x)] \tag{1}$
En efecto, sustituyendo en (1) $x$ por $m$ e $y$ por $n$ , se tiene
$\gcd(m, n) \mid \gcd(n, m) \tag{2}$
y, sustituyendo en (1) $x$ por $n$ e $y$ por $m$ , se tiene
$\gcd(n, m) \mid \gcd(m, n) \tag{3}$
Finalmente, aplicando la propiedad antisimétrica de la divisibilidad a (2) y (3), se tiene
$\gcd(m, n) = \gcd(n, m)$

Para demostrar (1), por la definición del máximo común divisor, basta demostrar las siguientes relaciones
$\begin{align} \gcd(m, n) &\mid n \\ \gcd(m, n) &\mid m \end{align}$
y ambas se tienen por la definición del máximo común divisor.

Demostraciones con Lean4

import Mathlib.Data.Real.Basic
variable (k m n : ℕ)

open Nat

-- 1ª demostración del lema auxiliar
lemma aux : gcd m n ∣ gcd n m :=
by
  have h1 : gcd m n ∣ n :=
    gcd_dvd_right m n
  have h2 : gcd m n ∣ m :=
    gcd_dvd_left m n
  show gcd m n ∣ gcd n m
  exact dvd_gcd h1 h2

-- 2ª demostración del lema auxiliar
example : gcd m n ∣ gcd n m :=
dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)

-- 1ª demostración
example : gcd m n = gcd n m :=
by
  have h1 : gcd m n ∣ gcd n m := aux m n
  have h2 : gcd n m ∣ gcd m n := aux n m
  show gcd m n = gcd n m
  exact _root_.dvd_antisymm h1 h2

-- 2ª demostración
example : gcd m n = gcd n m :=
by
  apply _root_.dvd_antisymm
  { exact aux m n }
  { exact aux n m }

-- 3ª demostración
example : gcd m n = gcd n m :=
_root_.dvd_antisymm (aux m n) (aux n m)

-- 4ª demostración
example : gcd m n = gcd n m :=
-- by apply?
gcd_comm m n

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

-- #check (_root_.dvd_antisymm : m ∣ n → n ∣ m → m = n)
-- #check (dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n)
-- #check (gcd_comm m n : gcd m n = gcd n m)
-- #check (gcd_dvd_left  m n: gcd m n ∣ m)
-- #check (gcd_dvd_right m n : gcd m n ∣ n)

import Mathlib.Data.Real.Basic

variable (k m n : ℕ)

open Nat

-- 1ª demostración del lema auxiliar

lemma aux : gcd m n ∣ gcd n m :=

have h1 : gcd m n ∣ n :=

gcd_dvd_right m n

have h2 : gcd m n ∣ m :=

gcd_dvd_left m n

show gcd m n ∣ gcd n m

exact dvd_gcd h1 h2

-- 2ª demostración del lema auxiliar

example : gcd m n ∣ gcd n m :=

dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n)

-- 1ª demostración

example : gcd m n = gcd n m :=

have h1 : gcd m n ∣ gcd n m := aux m n

have h2 : gcd n m ∣ gcd m n := aux n m

show gcd m n = gcd n m

exact _root_.dvd_antisymm h1 h2

-- 2ª demostración

example : gcd m n = gcd n m :=

apply _root_.dvd_antisymm

{ exact aux m n }

{ exact aux n m }

-- 3ª demostración

example : gcd m n = gcd n m :=

_root_.dvd_antisymm (aux m n) (aux n m)

-- 4ª demostración

example : gcd m n = gcd n m :=

-- by apply?

gcd_comm m n

-- Lemas usados

-- ============

-- #check (_root_.dvd_antisymm : m ∣ n → n ∣ m → m = n)

-- #check (dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n)

-- #check (gcd_comm m n : gcd m n = gcd n m)

-- #check (gcd_dvd_left m n: gcd m n ∣ m)

-- #check (gcd_dvd_right m n : gcd m n ∣ n)

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 19.

5. En los retículos, x ⊓ y = y ⊓ x

Demostrar con Lean4 que en los retículos se verifica que
$x ⊓ y = y ⊓ x$

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

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)

example : x ⊓ y = y ⊓ x :=
by sorry

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

example : x ⊓ y = y ⊓ x :=

by sorry

Demostración en lenguaje natural

Es consecuencia del siguiente lema auxiliar
$(∀ a, b)[a ⊓ b ≤ b ⊓ a] \tag{1}$
En efecto, sustituyendo en (1) $a$ por $x$ y $b$ por $y$ , se tiene
$x ⊓ y ≤ y ⊓ x \tag{2}$
y sustituyendo en (1) $a$ por $y$ y $b$ por $x$ , se tiene
$y ⊓ x ≤ x ⊓ y \tag{3}$
Finalmente, aplicando la propiedad antisimétrica de la divisibilidad a (2) y (3), se tiene
$x ⊓ y = y ⊓ x$

Para demostrar (1), por la definición del ínfimo, basta demostrar las siguientes relaciones
$\begin{align} y ⊓ x &≤ x \\ y ⊓ x &≤ y \end{align}$
y ambas se tienen por la definición del ínfimo.

Demostraciones con Lean4

import Mathlib.Order.Lattice
variable {α : Type _} [Lattice α]
variable (x y z : α)

-- 1ª demostración del lema auxiliar
lemma aux : x ⊓ y ≤ y ⊓ x :=
by
  have h1 : x ⊓ y ≤ y :=
    inf_le_right
  have h2 : x ⊓ y ≤ x :=
    inf_le_left
  show x ⊓ y ≤ y ⊓ x
  exact le_inf h1 h2

-- 2ª demostración del lema auxiliar
example : x ⊓ y ≤ y ⊓ x :=
by
  apply le_inf
  { apply inf_le_right }
  { apply inf_le_left }

-- 3ª demostración del lema auxiliar
example : x ⊓ y ≤ y ⊓ x :=
le_inf inf_le_right inf_le_left

-- 1ª demostración
example : x ⊓ y = y ⊓ x :=
by
  have h1 : x ⊓ y ≤ y ⊓ x :=
    aux x y
  have h2 : y ⊓ x ≤ x ⊓ y :=
    aux y x
  show x ⊓ y = y ⊓ x
  exact le_antisymm h1 h2

-- 2ª demostración
example : x ⊓ y = y ⊓ x :=
by
  apply le_antisymm
  { apply aux }
  { apply aux }

-- 3ª demostración
example : x ⊓ y = y ⊓ x :=
le_antisymm (aux x y) (aux y x)

-- 4ª demostración
example : x ⊓ y = y ⊓ x :=
by apply le_antisymm; simp ; simp

-- 5ª demostración
example : x ⊓ y = y ⊓ x :=
-- by apply?
inf_comm

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

-- #check (inf_comm : x ⊓ y = y ⊓ x)
-- #check (inf_le_left : x ⊓ y ≤ x)
-- #check (inf_le_right : x ⊓ y ≤ y)
-- #check (le_antisymm : x ≤ y → y ≤ x → x = y)
-- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)

import Mathlib.Order.Lattice

variable {α : Type _} [Lattice α]

variable (x y z : α)

-- 1ª demostración del lema auxiliar

lemma aux : x ⊓ y ≤ y ⊓ x :=

have h1 : x ⊓ y ≤ y :=

inf_le_right

have h2 : x ⊓ y ≤ x :=

inf_le_left

show x ⊓ y ≤ y ⊓ x

exact le_inf h1 h2

-- 2ª demostración del lema auxiliar

example : x ⊓ y ≤ y ⊓ x :=

apply le_inf

{ apply inf_le_right }

{ apply inf_le_left }

-- 3ª demostración del lema auxiliar

example : x ⊓ y ≤ y ⊓ x :=

le_inf inf_le_right inf_le_left

-- 1ª demostración

example : x ⊓ y = y ⊓ x :=

have h1 : x ⊓ y ≤ y ⊓ x :=

aux x y

have h2 : y ⊓ x ≤ x ⊓ y :=

aux y x

show x ⊓ y = y ⊓ x

exact le_antisymm h1 h2

-- 2ª demostración

example : x ⊓ y = y ⊓ x :=

apply le_antisymm

{ apply aux }

-- 3ª demostración

example : x ⊓ y = y ⊓ x :=

le_antisymm (aux x y) (aux y x)

-- 4ª demostración

example : x ⊓ y = y ⊓ x :=

by apply le_antisymm; simp ; simp

-- 5ª demostración

example : x ⊓ y = y ⊓ x :=

-- by apply?

inf_comm

-- Lemas usados

-- ============

-- #check (inf_comm : x ⊓ y = y ⊓ x)

-- #check (inf_le_left : x ⊓ y ≤ x)

-- #check (inf_le_right : x ⊓ y ≤ y)

-- #check (le_antisymm : x ≤ y → y ≤ x → x = y)

-- #check (le_inf : z ≤ x → z ≤ y → z ≤ x ⊓ y)

Demostraciones interactivas

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

Referencias

J. Avigad y P. Massot. Mathematics in Lean, p. 20.

1. En ℝ, |a| – |b| ≤ |a – b|

2. Si x, y, z ∈ ℕ, entonces x divide a yxz

3. Si x divide a w, entonces también divide a y(xz)+x²+w²

4. Conmutatividad del máximo común divisor

5. En los retículos, x ⊓ y = y ⊓ x

Se puede imprimir o compartir con