-
Notifications
You must be signed in to change notification settings - Fork 1
/
Reglas_de_la_conjuncion.lean
96 lines (84 loc) · 1.34 KB
/
Reglas_de_la_conjuncion.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
-- Reglas de la conjunción
-- =======================
-- ----------------------------------------------------
-- Ej. 1 (p. 4). Demostrar que
-- P ∧ Q, R ⊢ Q ∧ R
-- ----------------------------------------------------
import tactic
variables (P Q R : Prop)
-- 1ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
have hQ : Q,
from and.right hPQ,
show Q ∧ R,
from and.intro hQ hR
-- 2ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
have hQ : Q,
from hPQ.right,
show Q ∧ R,
from ⟨hQ, hR⟩
-- 3ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
have hQ : Q,
from hPQ.2,
show Q ∧ R,
from ⟨hQ, hR⟩
-- 4ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
have hQ : Q,
from hPQ.2,
⟨hQ, hR⟩
-- 5ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
⟨hPQ.2, hR⟩
-- 6ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
begin
split,
{ cases hPQ with hP hQ,
exact hQ, },
{ exact hR, },
end
-- 7ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
begin
split,
{ cases hPQ,
assumption, },
{ assumption, },
end
-- 8ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
-- by hint
by tauto
-- 9ª demostración
example
(hPQ : P ∧ Q)
(hR : R)
: Q ∧ R :=
by finish