DAO: La semana en Calculemus (28 de octubre de 2022)
Esta semana he publicado en Calculemus las demostraciones con Lean de las siguientes propiedades:
- 1. Si R es un retículo tal que x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), entonces (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
- 2. Si R es un retículo tal que x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z), entonces (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
- 3. Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a
- 4. Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b
- 5. Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces ac ≤ bc
A continuación se muestran las soluciones.
1. Si R es un retículo tal que x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), entonces (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)
Demostrar que si R es un retículo tal que
|
1 |
(∀ x y z ∈ R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z))), |
entonces
|
1 |
(∀ a b c ∈ R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c)) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z)) : ∀ a b c : R, (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) := begin intros a b c, calc (a ⊔ b) ⊓ c = c ⊓ (a ⊔ b) : by rw inf_comm ... = (c ⊓ a) ⊔ (c ⊓ b) : by rw h ... = (a ⊓ c) ⊔ (c ⊓ b) : by rw [@inf_comm _ _ c a] ... = (a ⊓ c) ⊔ (b ⊓ c) : by rw [@inf_comm _ _ c b] end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.
2. Si R es un retículo tal que x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z), entonces (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c)
Demostrar que Si R es un retículo tal que
|
1 |
∀ x y z : α, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z) |
entonces
|
1 |
∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 |
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := sorry |
Soluciones con Lean
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import order.lattice variables {R : Type*} [lattice R] example (h : ∀ x y z : R, x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z)) : ∀ a b c : R, (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) := begin intros a b c, calc (a ⊓ b) ⊔ c = c ⊔ (a ⊓ b) : by rw sup_comm ... = (c ⊔ a) ⊓ (c ⊔ b) : by rw h ... = (a ⊔ c) ⊓ (c ⊔ b) : by rw [@sup_comm _ _ c a] ... = (a ⊔ c) ⊓ (b ⊔ c) : by rw [@sup_comm _ _ c b] end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.
3. Si R es un anillo ordenado, entonces ∀ a b ∈ R, a ≤ b → 0 ≤ b – a
Demostrar que si R es un anillo ordenado y a b ∈ R, entonces
|
1 |
a ≤ b → 0 ≤ b - a |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : a ≤ b → 0 ≤ 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 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R -- 1ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := begin intro h, calc 0 = a - a : (sub_self a).symm ... ≤ b - a : sub_le_sub_right h a end -- 2ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := -- by library_search sub_nonneg.mpr -- 3ª demostración -- =============== example : a ≤ b → 0 ≤ b - a := -- by hint by simp |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.
4. Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b – a → a ≤ b
Demostrar que si R es un anillo ordenado y a, b ∈ R, entonces
|
1 |
0 ≤ b - a → a ≤ b |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R example : 0 ≤ b - a → a ≤ 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 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b : R -- 1ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := begin intro h, calc a = 0 + a : (zero_add a).symm ... ≤ (b - a) + a : add_le_add_right h a ... = b : sub_add_cancel b a end -- 2ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := -- by library_search sub_nonneg.mp -- 3ª demostración -- =============== example : 0 ≤ b - a → a ≤ b := -- by hint by simp |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.
5. Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces ac ≤ bc
Demostrar que si R es un anillo ordenado y a, b, c ∈ R tales que
|
1 2 |
a ≤ b 0 ≤ c |
entonces
|
1 |
a * c ≤ b * c |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R example (h1 : a ≤ b) (h2 : 0 ≤ c) : 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 |
import algebra.order.ring variables {R : Type*} [ordered_ring R] variables a b c: R -- 1ª demostración -- =============== example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin have h3 : 0 ≤ b - a := sub_nonneg.mpr h1, have h4 : 0 ≤ (b - a) * c := mul_nonneg h3 h2, have h5 : (b - a) * c = b * c - a * c := sub_mul b a c, have h6 : 0 ≤ b * c - a * c := eq.trans_ge h5 h4, show a * c ≤ b * c, by exact sub_nonneg.mp h6, end -- 2ª demostración -- =============== open_locale classical example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := begin by_cases h3 : b ≤ a, { have h3a : a = b := le_antisymm h1 h3, show a * c ≤ b * c, by rw h3a }, { by_cases h4 : c = 0, { calc a * c = a * 0 : by rw h4 ... = 0 : by rw mul_zero ... ≤ 0 : le_refl 0 ... = b * 0 : by rw mul_zero ... = b * c : by {congr ; rw h4}}, { apply le_of_lt, apply mul_lt_mul_of_pos_right, { show a < b, by exact lt_of_le_not_le h1 h3 }, { show 0 < c, by exact lt_of_le_of_ne h2 (ne.symm h4) }}}, end -- 3ª demostración example (h1 : a ≤ b) (h2 : 0 ≤ c) : a * c ≤ b * c := -- by library_search mul_le_mul_of_nonneg_right h1 h2 |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
Referencias
- J. Avigad, K. Buzzard, R.Y. Lewis y P. Massot. Mathematics in Lean, p. 23.