Menu Close

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

José A. Alonso--

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
ForMatUS