septiembre 2020 – Página 4

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

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

PorJosé A. Alonso 15 septiembre 2020

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P → Q ⊢ ¬Q → ¬P en el que se comentan 12 pruebas en Lean de la propiedad

P → Q ⊢ ¬Q → ¬P

A continuación, se muestra el vídeo

y el código de la teoría utilizada

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

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

import tactic

variables (P Q : Prop)

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

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

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

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

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

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

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

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

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

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

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

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

100

101

102

103

104

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

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

-- Ej. 1. Demostrar

-- P → Q ⊢ ¬Q → ¬P

import tactic

variables (P Q : Prop)

-- 1ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

assume h2 : ¬Q,

show ¬P,

from mt h1 h2

-- 2ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

assume h2 : ¬Q, mt h1 h2

-- 3ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

λ h2, mt h1 h2

-- 4ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

mt h1

-- 5ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

begin

intro h2,

exact mt h1 h2,

end

-- 6ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

begin

intro h2,

intro h3,

apply h2,

apply h1,

exact h3,

end

-- 7ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

begin

intro h2,

intro h3,

apply h2,

exact h1 h3,

end

-- 8ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

begin

intro h2,

intro h3,

exact h2 (h1 h3),

end

-- 9ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

begin

intros h2 h3,

exact h2 (h1 h3),

end

-- 10ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

λ h2 h3, h2 (h1 h3)

-- 11ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

by tauto

-- 12ª demostración

example

(h1 : P → Q)

: ¬Q → ¬P :=

by finish

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

PorJosé A. Alonso 15 septiembre 2020

He añadido a la lista Lógica con Lean el vídeo Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R en el que se comentan 5 pruebas en Lean de

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

A continuación, se muestra el vídeo

y el código de la teoría utilizada

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

-- Ej 1. Demostrar que
--    P, P → Q, P → (Q → R) ⊢ R

import tactic

variables (P Q R : Prop)

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

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

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

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

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

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

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

-- Ej 1. Demostrar que

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

import tactic

variables (P Q R : Prop)

-- 1ª demostración

example

(h1 : P)

(h2 : P → Q)

(h3 : P → (Q → R))

: R :=

have h4 : Q,

from h2 h1,

have h5 : Q → R,

from h3 h1,

show R,

from h5 h4

-- 2ª demostración

example

(h1 : P)

(h2 : P → Q)

(h3 : P → (Q → R))

: R :=

have h4 : Q := h2 h1,

have h5 : Q → R := h3 h1,

show R, from h5 h4

-- 3ª demostración

example

(h1 : P)

(h2 : P → Q)

(h3 : P → (Q → R))

: R :=

show R, from (h3 h1) (h2 h1)

-- 4ª demostración

example

(h1 : P)

(h2 : P → Q)

(h3 : P → (Q → R))

: R :=

(h3 h1) (h2 h1)

-- 5ª demostración

example

(h1 : P)

(h2 : P → Q)

(h3 : P → (Q → R))

: R :=

by finish