Menu Close

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

José A. Alonso--

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
ForMatUS