DAO: La semana en Calculemus (2 de septiembre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b
- 2. Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a
- 3. Si R es un anillo y a, b, c ∈ R tales que a + b = a + c, entonces b = c
- 4. Si R es un anillo y a, b, c ∈ R tales que a + b = c + b, entonces a = c
- 5. Si R es un anillo y a ∈ R, entonces a * 0 = 0
A continuación se muestran las soluciones.
1. Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b
En Lean, se declara que R es un anillo mediante la expresión
1 |
variables {R : Type*} [ring R] |
y, como consecuencia, se tienen los siguientes axiomas
1 2 3 4 5 6 7 8 9 |
add_assoc : ∀ a b c : R, (a + b) + c = a + (b + c) add_comm : ∀ a b : R, a + b = b + a zero_add : ∀ a : R, 0 + a = a add_left_neg : ∀ a : R, -a + a = 0 mul_assoc : ∀ a b c : R, a * b * c = a * (b * c) mul_one : ∀ a : R, a * 1 = a one_mul : ∀ a : R, 1 * a = a mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c |
Demostrar que si R es un anillo, entonces
1 |
∀ a b : R, -a + (a + b) = b |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables a b : R example : -a + (a + b) = b := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R -- 1ª demostración example : -a + (a + b) = b := calc -a + (a + b) = (-a + a) + b : by rw ← add_assoc ... = 0 + b : by rw add_left_neg ... = b : by rw zero_add -- 2ª demostración example : -a + (a + b) = b := begin rw ←add_assoc, rw add_left_neg, rw zero_add, end -- 3ª demostración example : -a + (a + b) = b := by rw [←add_assoc, add_left_neg, zero_add] -- 4ª demostración example : -a + (a + b) = b := -- by library_search neg_add_cancel_left a b -- 5ª demostración example : -a + (a + b) = b := -- by hint by finish |
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>
2. Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a
Demostrar que si R es un anillo, entonces
1 |
∀ a b : R, (a + b) + -b = a |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R example : (a + b) + -b = a := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 |
import algebra.ring variables {R : Type*} [ring R] variables a b : R -- 1ª demostración -- =============== example : (a + b) + -b = a := calc (a + b) + -b = a + (b + -b) : by rw add_assoc ... = a + 0 : by rw add_right_neg ... = a : by rw add_zero -- 2ª demostración -- =============== example : (a + b) + -b = a := begin rw add_assoc, rw add_right_neg, rw add_zero, end -- 3ª demostración -- =============== example : (a + b) + -b = a := by rw [add_assoc, add_right_neg, add_zero] -- 4ª demostración -- =============== example : (a + b) + -b = a := -- by library_search add_neg_eq_of_eq_add rfl -- 5ª demostración -- =============== example : (a + b) + -b = a := -- by hint by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
3. Si R es un anillo y a, b, c ∈ R tales que a + b = a + c, entonces b = c
Demostrar que si R es un anillo y a, b, c ∈ R tales que
1 |
a + b = a + c |
entonces
1 |
b = c |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {a b c : R} example (h : a + b = a + c) : b = c := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {a b c : R} -- 1ª demostración -- =============== example (h : a + b = a + c) : b = c := calc b = 0 + b : by rw zero_add ... = (-a + a) + b : by rw add_left_neg ... = -a + (a + b) : by rw add_assoc ... = -a + (a + c) : by rw h ... = (-a + a) + c : by rw ←add_assoc ... = 0 + c : by rw add_left_neg ... = c : by rw zero_add -- 2ª demostración -- =============== example (h : a + b = a + c) : b = c := calc b = 0 + b : by simp ... = (-a + a) + b : by simp ... = -a + (a + b) : by simp ... = -a + (a + c) : by rw h ... = (-a + a) + c : by simp ... = 0 + c : by simp ... = c : by simp -- 3ª demostración -- =============== lemma aux : -a + (a + b) = b := by finish example (h : a + b = a + c) : b = c := calc b = -a + (a + b) : aux.symm ... = -a + (a + c) : congr_arg (λ x, -a + x) h ... = c : aux -- 4ª demostración -- =============== example (h : a + b = a + c) : b = c := -- by library_search (add_right_inj a).mp h -- 4ª demostración -- =============== example (h : a + b = a + c) : b = c := -- by hint by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
4. Si R es un anillo y a, b, c ∈ R tales que a + b = c + b, entonces a = c
Demostrar que si R es un anillo y a, b, c ∈ R tales que
1 |
a + b = c + b |
entonces
1 |
a = c |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 8 9 10 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {a b c : R} example (h : a + b = c + b) : a = c := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 |
import algebra.ring import tactic variables {R : Type*} [ring R] variables {a b c : R} -- 1ª demostración -- =============== example (h : a + b = c + b) : a = c := calc a = a + 0 : by rw add_zero ... = a + (b + -b) : by rw add_right_neg ... = (a + b) + -b : by rw add_assoc ... = (c + b) + -b : by rw h ... = c + (b + -b) : by rw ← add_assoc ... = c + 0 : by rw ← add_right_neg ... = c : by rw add_zero -- 2ª demostración -- =============== example (h : a + b = c + b) : a = c := calc a = a + 0 : by simp ... = a + (b + -b) : by simp ... = (a + b) + -b : by simp ... = (c + b) + -b : by rw h ... = c + (b + -b) : by simp ... = c + 0 : by simp ... = c : by simp -- 3ª demostración -- =============== lemma aux : (a + b) + -b = a := by finish example (h : a + b = c + b) : a = c := calc a = (a + b) + -b : aux.symm ... = (c + b) + -b : congr_arg (λ x, x + -b) h ... = c : aux -- 4ª demostración -- =============== example (h : a + b = c + b) : a = c := by finish |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
5. Si R es un anillo y a ∈ R, entonces a * 0 = 0
Demostrar que Si R es un anillo y a ∈ R, entonces
1 |
a * 0 = 0 |
Para ello, completar la siguiente teoría de Lean:
1 2 3 4 5 6 7 |
import algebra.ring variables {R : Type*} [ring R] variable a : R example : a * 0 = 0 := sorry |
Soluciones con Lean
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 |
import algebra.ring variables {R : Type*} [ring R] variable a : R -- 1ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : (mul_add a 0 0).symm ... = a * 0 : congr_arg (λ x, a * x) (add_zero 0) ... = a * 0 + 0 : (add_zero (a * 0)).symm, rw add_left_cancel h end -- 2ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : by rw ←mul_add ... = a * 0 : by rw add_zero ... = a * 0 + 0 : by rw add_zero, rw add_left_cancel h end -- 3ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, { rw [←mul_add, add_zero, add_zero] }, rw add_left_cancel h end -- 4ª demostración -- =============== example : a * 0 = 0 := begin have h : a * 0 + a * 0 = a * 0 + 0, calc a * 0 + a * 0 = a * (0 + 0) : by simp ... = a * 0 : by simp ... = a * 0 + 0 : by simp, simp, end -- 5ª demostración -- =============== example : a * 0 = 0 := by simp -- 6ª demostración -- =============== example : a * 0 = 0 := -- by library_search mul_zero a |
Se puede interactuar con la prueba anterior en esta sesión con Lean.