Menu Close

Día: 17 septiembre, 2020

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

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

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

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