Menu Close

DAO: La semana en Calculemus (9 de septiembre de 2022)

José A. Alonso

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

A continuación se muestran las soluciones.

1. Si R es un anillo y a ∈ R, entonces 0 * a = 0

Demostrar que si R es un anillo y a ∈ R, entonces

0 * a = 0.

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

import algebra.ring
 
variables {R : Type*} [ring R]
variable (a : R)
 
example : 0 * a = 0 :=
sorry

Soluciones con Lean

import algebra.ring
 
variables {R : Type*} [ring R]
variable (a : R)
 
-- 1ª demostración
-- ===============
 
example : 0 * a = 0 :=
begin
  have h : 0 * a + 0 * a = 0 * a + 0,
    calc 0 * a + 0 * a
         = (0 + 0) * a : (add_mul 0 0 a).symm
     ... = 0 * a       : congr_arg (λ x, x * a) (add_zero 0)
     ... = 0 * a + 0   : self_eq_add_right.mpr rfl,
  rw add_left_cancel h
end
 
-- 2ª demostración
-- ===============
 
example : 0 * a = 0 :=
begin
  have h : 0 * a + 0 * a = 0 * a + 0,
    calc 0 * a + 0 * a
         = (0 + 0) * a : by rw add_mul
     ... = 0 * a       : by rw add_zero
     ... = 0 * a + 0   : by rw add_zero,
  rw add_left_cancel h
end
 
-- 3ª demostración
-- ===============
 
example : 0 * a = 0 :=
begin
  have h : 0 * a + 0 * a = 0 * a + 0,
  { rw [←add_mul, add_zero, add_zero] },
  rw add_left_cancel h
end
 
-- 4ª demostración
-- ===============
 
example : 0 * a = 0 :=
begin
  have h : 0 * a + 0 * a = 0 * a + 0,
    calc 0 * a + 0 * a
         = (0 + 0) * a : by simp
     ... = 0 * a       : by simp
     ... = 0 * a + 0   : by simp,
  simp,
end
 
-- 5ª demostración
-- ===============
 
example : 0 * a = 0 :=
by simp

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

2. Si R es un anillo y a,b∈R tales que a+b=0, entonces -a=b

Demostrar que Si R es un anillo y a, b ∈ R tales que

a + b = 0

entonces

-a = b

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

import algebra.ring
 
variables {R : Type*} [ring R]
variables {a b : R}
 
example
  (h : a + b = 0)
  : -a = b :=
sorry

Soluciones con Lean

import algebra.ring
 
variables {R : Type*} [ring R]
variables {a b : R}
 
-- 1ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : -a = b :=
calc
  -a  = -a + 0       : (add_zero (-a)).symm
  ... = -a + (a + b) : congr_arg (λ x, -a +x) h.symm
  ... = b            : neg_add_cancel_left a b
 
-- 2ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : -a = b :=
calc
  -a  = -a + 0       : by rw add_zero
  ... = -a + (a + b) : by rw h
  ... = b            : by rw neg_add_cancel_left
 
-- 3ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : -a = b :=
calc
  -a  = -a + 0       : by simp
  ... = -a + (a + b) : by simp [h]
  ... = b            : by simp
 
-- 4ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : -a = b :=
-- by library_search
add_eq_zero_iff_neg_eq.mp h

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

3. Si R es un anillo y a,b∈R tales que a+b=0, entonces a=-b

Demostrar que si R es un anillo y a, b ∈ R tales que

a + b = 0

entonces

a = -b

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

import algebra.ring
 
variables {R : Type*} [ring R]
variables {a b : R}
 
example
  (h : a + b = 0)
  : a = -b :=
sorry

Soluciones con Lean

import algebra.ring
 
variables {R : Type*} [ring R]
variables {a b : R}
 
-- 1ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : a = -b :=
calc
  a   = a + 0        : (add_zero a).symm
  ... = a + (b + -b) : congr_arg (λ x, a + x) (add_neg_self b).symm
  ... = (a + b) + -b : (add_assoc a b (-b)).symm
  ... = 0 + -b       : congr_arg (λ x, x + -b) h
  ... = -b           : zero_add (-b)
 
-- 2ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : a = -b :=
calc
  a   = a + 0        : by rw add_zero
  ... = a + (b + -b) : by {congr ; rw add_neg_self}
  ... = (a + b) + -b : by rw add_assoc
  ... = 0 + -b       : by {congr; rw h}
  ... = -b           : by rw zero_add
 
-- 3ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : a = -b :=
calc
  a   = a + 0        : by simp
  ... = a + (b + -b) : by simp
  ... = (a + b) + -b : by simp
  ... = 0 + -b       : by simp [h]
  ... = -b           : by simp
 
-- 4ª demostración
-- ===============
 
example
  (h : a + b = 0)
  : a = -b :=
-- by library_search
add_eq_zero_iff_eq_neg.mp h

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

4. Si R es un anillo, entonces -0 = 0

Demostrar que si R es un anillo, entonces

-0 = 0

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

import algebra.ring
 
variables {R : Type*} [ring R]
 
example : (-0 : R) = 0 :=
sorry

Soluciones con Lean

import algebra.ring
 
variables {R : Type*} [ring R]
 
-- 1ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
begin
  have h : 0 - 0 = (-0 : R) := zero_sub 0,
  calc (-0 : R)
       = 0 - 0    : h.symm
   ... = -(0 - 0) : (neg_sub (0 : R) 0).symm
   ... = -(-0)    : congr_arg (λ x, -x) h
   ... = 0        : neg_neg 0
end
 
-- 2ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
begin
  have h : 0 - 0 = (-0 : R) := by rw zero_sub,
  calc (-0 : R)
       = 0 - 0    : by rw h
   ... = -(0 - 0) : by rw neg_sub
   ... = -(-0)    : by {congr; rw h}
   ... = 0        : by rw neg_neg
end
 
-- 3ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
by simpa only [zero_sub, neg_neg] using (neg_sub (0 : R) 0).symm
 
-- 4ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
neg_zero
 
-- 5ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
by simp
 
-- 6ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
begin
  apply neg_eq_of_add_eq_zero_right,
  rw add_zero,
end
 
-- 7ª demostración
-- ===============
 
example : (-0 : R) = 0 :=
neg_eq_of_add_eq_zero_right (add_zero 0)

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

5. Si R es un anillo y a ∈ R, entonces -(-a) = a

Demostrar que si R es un anillo y a ∈ R, entonces

-(-a) = a.

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

import algebra.ring
 
variables {R : Type*} [ring R]
variable a : R
 
example : -(-a) = a :=
sorry

Soluciones con Lean

import algebra.ring
 
variables {R : Type*} [ring R]
variable a : R
 
-- 1ª demostración
-- ===============
 
example : -(-a) = a :=
begin
  calc -(-a)
       = -(0 - a) : congr_arg (λ x, -x) (zero_sub a).symm
   ... = a - 0    : neg_sub (0 : R) a
   ... = a        : sub_zero a
end
 
-- 2ª demostración
-- ===============
 
example : -(-a) = a :=
begin
  calc -(-a)
       = -(0 - a) : by { congr; rw zero_sub}
   ... = a - 0    : by rw neg_sub
   ... = a        : by rw sub_zero
end
 
-- 3ª demostración
-- ===============
 
example : -(-a) = a :=
by simpa only [zero_sub, sub_zero] using (neg_sub (0 : R) a)
 
-- 4ª demostración
-- ===============
 
example : -(-a) = a :=
neg_neg a
 
-- 5ª demostración
-- ===============
 
example : -(-a) = a :=
by simp
 
-- 6ª demostración
-- ===============
 
example : -(-a) = a :=
begin
  apply neg_eq_of_add_eq_zero_right,
  rw neg_add_self a,
end
 
-- 7ª demostración
-- ===============
 
example : -(-a) = a :=
neg_eq_of_add_eq_zero_right (neg_add_self a)

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

Posted in ForMatUS