-
Notifications
You must be signed in to change notification settings - Fork 0
/
Cancelativa_izquierda.lean
123 lines (104 loc) · 3.13 KB
/
Cancelativa_izquierda.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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
-- Cancelativa_izquierda.lean
-- Si R es un anillo y a, b, c ∈ R tales que a+b=a+c, entonces b=c
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 1-agosto-2023
-- ---------------------------------------------------------------------
-- ---------------------------------------------------------------------
-- Demostrar que si R es un anillo y a, b, c ∈ R tales que
-- a + b = a + c
-- entonces
-- b = c
-- ----------------------------------------------------------------------
-- Demostraciones en lenguaje natural (LN)
-- ======================================
-- 1ª demostración en LN
-- =====================
-- Por la siguiente cadena de igualdades
-- b = 0 + b [por suma con cero]
-- = (-a + a) + b [por suma con opuesto]
-- = -a + (a + b) [por asociativa]
-- = -a + (a + c) [por hipótesis]
-- = (-a + a) + c [por asociativa]
-- = 0 + c [por suma con opuesto]
-- = c [por suma con cero]
-- 2ª demostración en LN
-- =====================
-- Por la siguiente cadena de implicaciones
-- a + b = a + c
-- ==> -a + (a + b) = -a + (a + c) [sumando -a]
-- ==> (-a + a) + b = (-a + a) + c [por la asociativa]
-- ==> 0 + b = 0 + b [suma con opuesto]
-- ==> b = c [suma con cero]
-- 3ª demostración en LN
-- =====================
-- Por la siguiente cadena de igualdades
-- b = -a + (a + b)
-- = -a + (a + c) [por la hipótesis]
-- = c
-- Demostraciones con Lean4
-- ========================
import Mathlib.Algebra.Ring.Defs
import Mathlib.Tactic
variable {R : Type _} [Ring R]
variable {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 [neg_add_cancel]
_ = -a + (a + b) := by rw [add_assoc]
_ = -a + (a + c) := by rw [h]
_ = (-a + a) + c := by rw [←add_assoc]
_ = 0 + c := by rw [neg_add_cancel]
_ = c := by rw [zero_add]
-- 2ª demostración
example
(h : a + b = a + c)
: b = c :=
by
have h1 : -a + (a + b) = -a + (a + c) :=
congrArg (HAdd.hAdd (-a)) h
clear h
rw [← add_assoc] at h1
rw [neg_add_cancel] at h1
rw [zero_add] at h1
rw [← add_assoc] at h1
rw [neg_add_cancel] at h1
rw [zero_add] at h1
exact h1
-- 3ª demostración
example
(h : a + b = a + c)
: b = c :=
calc
b = -a + (a + b) := by rw [neg_add_cancel_left a b]
_ = -a + (a + c) := by rw [h]
_ = c := by rw [neg_add_cancel_left]
-- 4ª demostración
example
(h : a + b = a + c)
: b = c :=
by
rw [← neg_add_cancel_left a b]
rw [h]
rw [neg_add_cancel_left]
-- 5ª demostración
example
(h : a + b = a + c)
: b = c :=
by
rw [← neg_add_cancel_left a b, h, neg_add_cancel_left]
-- 6ª demostración
example
(h : a + b = a + c)
: b = c :=
add_left_cancel h
-- Lemas usados
-- ============
-- #check (add_assoc a b c : (a + b) + c = a + (b + c))
-- #check (add_left_cancel : a + b = a + c → b = c)
-- #check (neg_add_cancel a : -a + a = 0)
-- #check (neg_add_cancel_left a b : -a + (a + b) = b)
-- #check (zero_add a : 0 + a = a)