ForMatUS – Página 24

ForMatUS: Regla de eliminación de la disyunción en Lean

PorJosé A. Alonso 20 septiembre 202020 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comenta la regla de eliminación de la disyunción en Lean usando ejemplos con distintos estilos de prueba: declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

variables (P Q R : Prop)

-- ----------------------------------------------------
-- Ej. 1. (p. 11) Demostrar
--    P ∨ Q, P → R, Q → R ⊢ R
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
or.elim h1 h2 h3

-- 2ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
h1.elim h2 h3

-- 3ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
-- by library_search
or.rec h2 h3 h1

-- 4ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
begin
  cases h1 with hP hQ,
  { exact h2 hP, },
  { exact h3 hQ, },
end

-- 5ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
-- by hint
by tauto

-- 6ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
by finish

import tactic

variables (P Q R : Prop)

-- ----------------------------------------------------

-- Ej. 1. (p. 11) Demostrar

-- P ∨ Q, P → R, Q → R ⊢ R

-- ----------------------------------------------------

-- 1ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

or.elim h1 h2 h3

-- 2ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

h1.elim h2 h3

-- 3ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

-- by library_search

or.rec h2 h3 h1

-- 4ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

begin

cases h1 with hP hQ,

{ exact h2 hP, },

{ exact h3 hQ, },

end

-- 5ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

-- by hint

by tauto

-- 6ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

by finish

ForMatUS: Reglas de introducción de la disyunción en Lean

PorJosé A. Alonso 20 septiembre 202020 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan el uso en Lean de las reglas de introducción de la disyunción con ejemplos de pruebas en los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

variables (P Q R : Prop)

-- ----------------------------------------------------
-- Ej. 1. (p. 11) Demostrar
--    P ⊢ P ∨ Q
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : P)
  : P ∨ Q :=
or.intro_left Q h

-- 2ª demostración
example
  (h : P)
  : P ∨ Q :=
-- by library_search
or.inl h

-- 3ª demostración
example
  (h : P)
  : P ∨ Q :=
-- by hint
by tauto

-- 4ª demostración
example
  (h : P)
  : P ∨ Q :=
by finish

-- ----------------------------------------------------
-- Ej. 2. Demostrar
--    P ∧ Q ⊢ P ∨ R
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
have h2 : P,
  from and.elim_left h1,
show P ∨ R,
  from or.inl h2

-- 2ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
have h2 : P,
  from h1.1,
show P ∨ R,
  from or.inl h2

-- 3ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
have h2 : P := h1.1,
show P ∨ R,
  from or.inl h2

-- 4ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
show P ∨ R,
  from or.inl h1.1

-- 5ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
-- by suggest
or.inl h1.1

-- 6ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
-- by hint
by tauto

-- 7ª demostración
example
  (h1 : P ∧ Q)
  : P ∨ R :=
by finish

-- ----------------------------------------------------
-- Ej. 3. Demostrar
--    Q ⊢ P ∨ Q
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : Q)
  : P ∨ Q :=
or.intro_right P h

-- 2ª demostración
example
  (h : Q)
  : P ∨ Q :=
-- by suggest
or.inr h

-- 3ª demostración
example
  (h : Q)
  : P ∨ Q :=
-- by hint
by tauto

-- 4ª demostración
example
  (h : Q)
  : P ∨ Q :=
by finish

-- ----------------------------------------------------
-- Ej. 4. Demostrar
--    P ∧ Q ⊢ R ∨ Q
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
have h2 : Q,
  from and.elim_right h1,
show R ∨ Q,
  from or.inr h2

-- 2ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
have h2 : Q,
  from h1.2,
show R ∨ Q,
  from or.inr h2

-- 3ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
have h2 : Q := h1.2,
show R ∨ Q,
  from or.inr h2

-- 4ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
show R ∨ Q,
  from or.inr h1.2

-- 5ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
-- by suggest
or.inr h1.2

-- 6ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
-- by hint
by tauto

-- 7ª demostración
example
  (h1 : P ∧ Q)
  : R ∨ Q :=
by finish

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

import tactic

variables (P Q R : Prop)

-- ----------------------------------------------------

-- Ej. 1. (p. 11) Demostrar

-- P ⊢ P ∨ Q

-- ----------------------------------------------------

-- 1ª demostración

example

(h : P)

: P ∨ Q :=

or.intro_left Q h

-- 2ª demostración

example

(h : P)

: P ∨ Q :=

-- by library_search

or.inl h

-- 3ª demostración

example

(h : P)

: P ∨ Q :=

-- by hint

by tauto

-- 4ª demostración

example

(h : P)

: P ∨ Q :=

by finish

-- ----------------------------------------------------

-- Ej. 2. Demostrar

-- P ∧ Q ⊢ P ∨ R

-- ----------------------------------------------------

-- 1ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

have h2 : P,

from and.elim_left h1,

show P ∨ R,

from or.inl h2

-- 2ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

have h2 : P,

from h1.1,

show P ∨ R,

from or.inl h2

-- 3ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

have h2 : P := h1.1,

show P ∨ R,

from or.inl h2

-- 4ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

show P ∨ R,

from or.inl h1.1

-- 5ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

-- by suggest

or.inl h1.1

-- 6ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

-- by hint

by tauto

-- 7ª demostración

example

(h1 : P ∧ Q)

: P ∨ R :=

by finish

-- ----------------------------------------------------

-- Ej. 3. Demostrar

-- Q ⊢ P ∨ Q

-- ----------------------------------------------------

-- 1ª demostración

example

(h : Q)

: P ∨ Q :=

or.intro_right P h

-- 2ª demostración

example

(h : Q)

: P ∨ Q :=

-- by suggest

or.inr h

-- 3ª demostración

example

(h : Q)

: P ∨ Q :=

-- by hint

by tauto

-- 4ª demostración

example

(h : Q)

: P ∨ Q :=

by finish

-- ----------------------------------------------------

-- Ej. 4. Demostrar

-- P ∧ Q ⊢ R ∨ Q

-- ----------------------------------------------------

-- 1ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

have h2 : Q,

from and.elim_right h1,

show R ∨ Q,

from or.inr h2

-- 2ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

have h2 : Q,

from h1.2,

show R ∨ Q,

from or.inr h2

-- 3ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

have h2 : Q := h1.2,

show R ∨ Q,

from or.inr h2

-- 4ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

show R ∨ Q,

from or.inr h1.2

-- 5ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

-- by suggest

or.inr h1.2

-- 6ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

-- by hint

by tauto

-- 7ª demostración

example

(h1 : P ∧ Q)

: R ∨ Q :=

by finish

ForMatUS: Pruebas en Lean de ¬Q → ¬P ⊢ P → ¬¬Q

PorJosé A. Alonso 17 septiembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 15 pruebas en Lean de

¬Q → ¬P ⊢ P → ¬¬Q

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas de ¬Q → ¬P ⊢ P → ¬¬Q
-- ============================

-- Ej. 1. Demostrar
--    ¬Q → ¬P ⊢ P → ¬¬Q

import tactic

variables (P Q : Prop)

-- 1ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
have h3 : ¬¬P,
  from not_not_intro h2,
show ¬¬Q, 
  from mt h1 h3

-- 2ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
have h3 : ¬¬P := not_not_intro h2,
show ¬¬Q, 
  from mt h1 h3

-- 3ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P,
show ¬¬Q, 
  from mt h1 (not_not_intro h2)

-- 4ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
assume h2 : P, mt h1 (not_not_intro h2)

-- 5ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2, mt h1 (not_not_intro h2)

-- 6ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
imp_not_comm.mp h1

-- 7ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  apply mt h1,
  apply not_not_intro,
  exact h2,
end

-- 8ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  apply mt h1,
  exact not_not_intro h2,
end

-- 9ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  exact mt h1 (not_not_intro h2),
end

-- 10ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2, mt h1 (not_not_intro h2)

-- 11ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intro h2,
  intro h3,
  have h4 : ¬P := h1 h3,
  exact h4 h2,
end

-- 12ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
begin
  intros h2 h3,
  exact (h1 h3) h2,
end

-- 13ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
λ h2 h3, (h1 h3) h2

-- 14ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
by tauto

-- 15ª demostración
example
  (h1 : ¬Q → ¬P)
  : P → ¬¬Q :=
by finish

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

-- Pruebas de ¬Q → ¬P ⊢ P → ¬¬Q

-- ============================

-- Ej. 1. Demostrar

-- ¬Q → ¬P ⊢ P → ¬¬Q

import tactic

variables (P Q : Prop)

-- 1ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

assume h2 : P,

have h3 : ¬¬P,

from not_not_intro h2,

show ¬¬Q,

from mt h1 h3

-- 2ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

assume h2 : P,

have h3 : ¬¬P := not_not_intro h2,

show ¬¬Q,

from mt h1 h3

-- 3ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

assume h2 : P,

show ¬¬Q,

from mt h1 (not_not_intro h2)

-- 4ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

assume h2 : P, mt h1 (not_not_intro h2)

-- 5ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

λ h2, mt h1 (not_not_intro h2)

-- 6ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

imp_not_comm.mp h1

-- 7ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

begin

intro h2,

apply mt h1,

apply not_not_intro,

exact h2,

end

-- 8ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

begin

intro h2,

apply mt h1,

exact not_not_intro h2,

end

-- 9ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

begin

intro h2,

exact mt h1 (not_not_intro h2),

end

-- 10ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

λ h2, mt h1 (not_not_intro h2)

-- 11ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

begin

intro h2,

intro h3,

have h4 : ¬P := h1 h3,

exact h4 h2,

end

-- 12ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

begin

intros h2 h3,

exact (h1 h3) h2,

end

-- 13ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

λ h2 h3, (h1 h3) h2

-- 14ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

by tauto

-- 15ª demostración

example

(h1 : ¬Q → ¬P)

: P → ¬¬Q :=

by finish

ForMatUS: Pruebas en Lean de P → (Q → R), P, ¬R ⊢ ¬Q

PorJosé A. Alonso 17 septiembre 2020

He añadido a la lista Lógica con Lean un vídeo en el que se se comentan 9 prueba en Lean de

P → (Q → R), P, ¬R ⊢ ¬Q

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q
-- ==================================

-- Ej. 1. Demostrar
--    Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q 

import tactic

variables (P Q R : Prop)

-- 1ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
have h4 : Q → R,
  from h1 h2,
show ¬Q,
  from mt h4 h3  

-- 2ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
have h4 : Q → R := h1 h2,
show ¬Q,
  from mt h4 h3  

-- 3ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
show ¬Q,
  from mt (h1 h2) h3  

-- 4ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
mt (h1 h2) h3

-- 5ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  apply h3,
  apply (h1 h2),
  exact h4,
end

-- 6ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  apply h3,
  exact (h1 h2) h4,
end

-- 7ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
begin
  intro h4,
  exact h3 ((h1 h2) h4),
end

-- 8ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
λ h4, h3 ((h1 h2) h4)

-- 9ª demostración
example 
  (h1 : P → (Q → R)) 
  (h2 : P)
  (h3 : ¬R)
  : ¬Q :=
by finish

-- Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q

-- ==================================

-- Ej. 1. Demostrar

-- Pruebas de P → (Q → R), P, ¬R ⊢ ¬Q

import tactic

variables (P Q R : Prop)

-- 1ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

have h4 : Q → R,

from h1 h2,

show ¬Q,

from mt h4 h3

-- 2ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

have h4 : Q → R := h1 h2,

show ¬Q,

from mt h4 h3

-- 3ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

show ¬Q,

from mt (h1 h2) h3

-- 4ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

mt (h1 h2) h3

-- 5ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

begin

intro h4,

apply h3,

apply (h1 h2),

exact h4,

end

-- 6ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

begin

intro h4,

apply h3,

exact (h1 h2) h4,

end

-- 7ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

begin

intro h4,

exact h3 ((h1 h2) h4),

end

-- 8ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

λ h4, h3 ((h1 h2) h4)

-- 9ª demostración

example

(h1 : P → (Q → R))

(h2 : P)

(h3 : ¬R)

: ¬Q :=

by finish

ForMatUS: Pruebas en Lean de la regla de introducción de la doble negación

PorJosé A. Alonso 16 septiembre 2020

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de la regla de introducción de la doble negación

P ⊢ ¬¬P

en el que se comentan 9 pruebas en Lean de la regla de introducción de la doble negación usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- Regla de introducción de la doble negación
-- ==========================================

-- Ej. 1. Demostrar
--    P ⊢ ¬¬P

import tactic
variable (P : Prop)

-- 1ª demostración
example
  (h1 : P)
  : ¬¬P :=
not.intro 
  ( assume h2: ¬P,
    show false, 
      from h2 h1)
  
-- 2ª demostración
example
  (h1 : P)
  : ¬¬P :=
assume h2: ¬P,
show false,
  from h2 h1

-- 3ª demostración
example
  (h1 : P)
  : ¬¬P :=
assume h2: ¬P, h2 h1

-- 4ª demostración
example
  (h1 : P)
  : ¬¬P :=
λ h2, h2 h1

-- 5ª demostración
example
  (h1 : P)
  : ¬¬P :=
not_not.mpr h1

-- 6ª demostración
example
  (h1 : P)
  : ¬¬P :=
not_not_intro h1

-- 7ª demostración
example
  (h1 : P)
  : ¬¬P :=
begin
  intro h2,
  exact h2 h1,
end

-- 8ª demostración
example
  (h1 : P)
  : ¬¬P :=
by tauto

-- 9ª demostración
example
  (h1 : P)
  : ¬¬P :=
by finish

-- Regla de introducción de la doble negación

-- ==========================================

-- Ej. 1. Demostrar

-- P ⊢ ¬¬P

import tactic

variable (P : Prop)

-- 1ª demostración

example

(h1 : P)

: ¬¬P :=

not.intro

( assume h2: ¬P,

show false,

from h2 h1)

-- 2ª demostración

example

(h1 : P)

: ¬¬P :=

assume h2: ¬P,

show false,

from h2 h1

-- 3ª demostración

example

(h1 : P)

: ¬¬P :=

assume h2: ¬P, h2 h1

-- 4ª demostración

example

(h1 : P)

: ¬¬P :=

λ h2, h2 h1

-- 5ª demostración

example

(h1 : P)

: ¬¬P :=

not_not.mpr h1

-- 6ª demostración

example

(h1 : P)

: ¬¬P :=

not_not_intro h1

-- 7ª demostración

example

(h1 : P)

: ¬¬P :=

begin

intro h2,

exact h2 h1,

end

-- 8ª demostración

example

(h1 : P)

: ¬¬P :=

by tauto

-- 9ª demostración

example

(h1 : P)

: ¬¬P :=

by finish