Menu Close

Día: 15 septiembre, 2020

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

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: Pruebas en Lean de P, P → Q, P → (Q → R) ⊢ R

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