Menu Close

Mes: septiembre 2020

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 en el que se comentan pruebas en Lean de

¬P → Q, ¬Q ⊢ P

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

-- ----------------------------------------------------
-- Ej. 1. (p. 7) Demostrar
--    ¬P → Q, ¬Q ⊢ P
-- ----------------------------------------------------
 
import tactic
 
variables (P Q : Prop)
 
open_locale classical
 
-- 1ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
have h3 : ¬¬P, from mt h1 h2,
show P,        from not_not.mp h3
 
-- 2ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
not_not.mp (mt h1 h2)
 
-- 3ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
begin
  by_contra h3,
  apply h2,
  exact h1 h3,
end
 
-- 4ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
begin
  by_contra h3,
  exact h2 (h1 h3),
end
 
-- 5ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
by_contra (λ h3, h2 (h1 h3))
 
-- 6ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
by_contra (λ h3, (h2 ∘ h1) h3)
 
-- 7ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
by_contra (h2 ∘ h1)
 
-- 8ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
-- by library_search
not_not.mp (mt h1 h2)
 
-- 9ª demostración
example
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
-- by hint
by tauto
 
-- 10ª demostración
lemma aux
  (h1 : ¬P → Q)
  (h2 : ¬Q)
  : P :=
-- by hint
by finish
 
-- #print axioms aux
Seguir leyendo →

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

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 8 pruebas en Lean de la propiedad en Lean de

P, ¬¬(Q ∧ R) ⊢ ¬¬P ∧ R

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

-- ----------------------------------------------------
-- Ej. 1. (p. 5) Demostrar
--    P, ¬¬(Q ∧ R) ⊢ ¬¬P ∧ R
-- ----------------------------------------------------
 
import tactic
 
variables (P Q R : Prop)
 
open_locale classical
 
-- 1ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
have h3 : ¬¬P,   from not_not_intro h1,
have h4 : Q ∧ R, from not_not.mp h2,
have h5 : R,     from and.elim_right h4,
show ¬¬P ∧ R,    from and.intro h3 h5
 
-- 2ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
have h3 : ¬¬P,   from not_not_intro h1,
have h4 : Q ∧ R, from not_not.mp h2,
have h5 : R,     from and.elim_right h4,
and.intro h3 h5
 
-- 3ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
have h3 : ¬¬P,   from not_not_intro h1,
have h4 : Q ∧ R, from not_not.mp h2,
have h5 : R,     from h4.2,
and.intro h3 h5
 
-- 5ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
and.intro (not_not_intro h1) (not_not.mp h2).2
 
-- 6ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
begin
  split,
  { exact not_not_intro h1, },
  { push_neg at h2,
    exact h2.2, },
end
 
-- 7ª demostración
example
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
-- by hint
by tauto
 
-- 8ª demostración
lemma aux
  (h1 : P)
  (h2 : ¬¬(Q ∧ R))
  : ¬¬P ∧ R :=
by finish
 
-- #print axioms aux
Seguir leyendo →

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

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 13 pruebas en Lean de la propiedad

P → Q ⊢ ¬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

-- ----------------------------------------------------
-- Ej. 1. (p. 24) Demostrar
--    P → Q ⊢ ¬P ∨ Q
-- ----------------------------------------------------
 
import tactic
 
variables (P Q : Prop)
 
open_locale classical
 
-- 1ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( assume h3 : P,
    have h4 : Q,
      from h1 h3,
    show ¬P ∨ Q,
      from or.inr h4)
  ( assume h5 : ¬P,
    show ¬P ∨ Q,
      from or.inl h5)
 
-- 2ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( assume h3 : P,
    have h4 : Q,
      from h1 h3,
    show ¬P ∨ Q,
      from or.inr h4)
  ( assume h5 : ¬P,
    or.inl h5)
 
-- 3ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( assume h3 : P,
    have h4 : Q,
      from h1 h3,
    show ¬P ∨ Q,
      from or.inr h4)
  ( λ h5, or.inl h5)
 
-- 4ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( assume h3 : P,
    have h4 : Q,
      from h1 h3,
    or.inr h4)
  ( λ h5, or.inl h5)
 
-- 5ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( assume h3 : P,
    or.inr (h1 h3))
  ( λ h5, or.inl h5)
 
-- 6ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
have h2 : P ∨ ¬P,
  from em P,
or.elim h2
  ( λ h3, or.inr (h1 h3))
  ( λ h5, or.inl h5)
 
-- 7ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
or.elim (em P)
  ( λ h3, or.inr (h1 h3))
  ( λ h5, or.inl h5)
 
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
(em P).elim
  ( λ h3, or.inr (h1 h3))
  ( λ h5, or.inl h5)
 
-- 8ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
-- by library_search
not_or_of_imp h1
 
-- 9ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
if h3 : P then or.inr (h1 h3) else or.inl h3
 
-- 10ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
begin
  by_cases h2 : P,
  { apply or.inr,
    exact h1 h2, },
  { exact or.inl h2, },
end
 
-- 11ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
begin
  by_cases h2 : P,
  { exact or.inr (h1 h2), },
  { exact or.inl h2, },
end
 
-- 12ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
begin
  by_cases h2 : P,
  { right,
    exact h1 h2, },
  { left,
    exact h2, },
end
 
-- 13ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
-- by hint
by tauto
 
-- 14ª demostración
example
  (h1 : P → Q)
  : ¬P ∨ Q :=
-- by hint
by finish
Seguir leyendo →

ForMatUS: Pruebas en Lean del principio del tercio excluso

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 17 pruebas en Lean del principio del tercio excluso 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

-- ----------------------------------------------------
-- Ej. 1. (p. 23) Demostrar que
--    F ∨ ¬F
-- ----------------------------------------------------
 
import tactic
 
variable (F : Prop)
 
open_locale classical
 
-- 1ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      assume h3 : F,
      have h4 : F ∨ ¬F, from or.inl h3,
      show false, from h1 h4,
    have h5 : F ∨ ¬F, from or.inr h2,
    show false, from h1 h5 )
 
-- 2ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      assume h3 : F,
      have h4 : F ∨ ¬F, from or.inl h3,
      show false, from h1 h4,
    have h5 : F ∨ ¬F, from or.inr h2,
    h1 h5 )
 
-- 3ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      assume h3 : F,
      have h4 : F ∨ ¬F, from or.inl h3,
      show false, from h1 h4,
    h1 (or.inr h2) )
 
-- 4ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      assume h3 : F,
      have h4 : F ∨ ¬F, from or.inl h3,
      h1 h4,
    h1 (or.inr h2) )
 
-- 5ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      assume h3 : F,
      h1 (or.inl h3),
    h1 (or.inr h2) )
 
-- 6ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    have h2 : ¬F, from
      λ h3, h1 (or.inl h3),
    h1 (or.inr h2) )
 
-- 7ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( assume h1 : ¬(F ∨ ¬F),
    h1 (or.inr (λ h3, h1 (or.inl h3))) )
 
-- 8ª demostración
example : F ∨ ¬F :=
by_contradiction
  ( λ h1, h1 (or.inr (λ h3, h1 (or.inl h3))) )
 
-- 9ª demostración
example : F ∨ ¬F :=
-- by library_search
em F
 
-- #print axioms em
 
-- 10ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  apply h1,
  right,
  intro h2,
  apply h1,
  left,
  exact h2,
end
 
-- 11ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  apply h1,
  apply or.inr,
  intro h2,
  exact h1 (or.inl h2),
end
 
-- 12ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  apply h1,
  apply or.inr,
  exact λ h2, h1 (or.inl h2),
end
 
-- 13ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  apply h1,
  exact or.inr (λ h2, h1 (or.inl h2)),
end
 
-- 14ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  exact h1 (or.inr (λ h2, h1 (or.inl h2))),
end
 
-- 15ª demostración
example : F ∨ ¬F :=
by_contra (λ h1, h1 (or.inr (λh2, h1 (or.inl h2))))
 
-- 16ª demostración
example : F ∨ ¬F :=
begin
  by_contra h1,
  apply h1,
  right,
  intro h2,
  apply h1,
  left,
  exact h2,
end
 
-- 17ª demostración
example : F ∨ ¬F :=
-- by hint
by tauto
 
-- 18ª demostración
example : F ∨ ¬F :=
by finish
Seguir leyendo →

ForMatUS: Pruebas en Lean de la eliminación de la doble negación

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 7 pruebas de la eliminación de la doble negación en Lean de 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

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--     ¬¬P ⊢ P
-- ----------------------------------------------------
 
import tactic
 
variable (P : Prop)
 
open_locale classical
 
-- 1ª demostración
example
  (h1 : ¬¬P)
  : P :=
by_contra
  ( assume h2 : ¬P,
    show false,
      from h1 h2 )
 
-- 2ª demostración
example
  (h1 : ¬¬P)
  : P :=
by_contra
  ( assume h2 : ¬P,
    h1 h2 )
 
-- 3ª demostración
example
  (h1 : ¬¬P)
  : P :=
by_contra (λ h2, h1 h2)
 
-- 4ª demostración
example
  (h1 : ¬¬P)
  : P :=
-- by library_search
not_not.mp h1
 
-- 5ª demostración
example
  (h1 : ¬¬P)
  : P :=
begin
  by_contradiction h2,
  exact h1 h2,
end
 
-- 6ª demostración
example
  (h1 : ¬¬P)
  : P :=
-- by hint
by tauto
 
-- 7ª demostración
lemma aux
  (h1 : ¬¬P)
  : P :=
by finish
 
-- #print axioms aux
Seguir leyendo →

ForMatUS: Pruebas en Lean de la regla de reducción al absurdo

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 6 pruebas en Lean de la regla de reducción al absurdo 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

import tactic
 
variable (P : Prop)
 
-- ----------------------------------------------------
-- Ej. 1 (p. 22) Demostrar que
--    ¬P → false ⊢ P
-- ----------------------------------------------------
 
-- 1ª demostración
example
  (h1 : ¬P → false)
  : P :=
have h2 : ¬¬P, from
  assume h3 : ¬P,
  show false, from h1 h3,
show P, from not_not.mp h2
 
-- 2ª demostración
example
  (h1 : ¬P → false)
  : P :=
begin
  apply not_not.mp,
  intro h2,
  exact h1 h2,
end
 
-- 3ª demostración
example
  (h1 : ¬P → false)
  : P :=
begin
  apply not_not.mp,
  exact λ h2, h1 h2,
end
 
-- 4ª demostración
example
  (h1 : ¬P → false)
  : P :=
not_not.mp (λ h2, h1 h2)
 
-- #print axioms not_not
 
-- 5ª demostración
example
  (h1 : ¬P → false)
  : P :=
-- by library_search
by_contra h1
 
-- #print axioms by_contra
 
-- 6ª demostración
lemma RAA
  (h1 : ¬P → false)
  : P :=
-- by hint
by finish
 
-- #print axioms RAA
Seguir leyendo →

PFH: Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell)

José A. Alonso--

He añadido a la lista Programación funcional con Haskell el vídeo Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell) en el que se explica cómo escribir las funciones de los programas para hacer dibujos. En concreto,

  • cómo programar dibujos elementales
  • cómo programar dibujos compuestos
  • cómo transformar dibujos con traslaciones, rotaciones, escalamiento y
  • cómo colorear.
  • cómo programar animaciones

El vídeo es

Los apuntes correspondientes son

Seguir leyendo →

ForMatUS: Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 9 pruebas en Lean de

P ↔ Q, P ∨ Q ⊢ 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

-- ----------------------------------------------------
-- Ej. 1. (p. 18) Demostrar
--     P ↔ Q, P ∨ Q ⊢ P ∧ Q
-- ----------------------------------------------------
 
import tactic
 
variables (P Q : Prop)
 
-- 1ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    have h4 : P → Q,
      from iff.elim_left h1,
    have h5 : Q,
      from h4 h3,
    show P ∧ Q,
      from and.intro h3 h5 )
  ( assume h6 : Q,
    have h7 : Q → P,
      from iff.elim_right h1,
    have h8 : P,
      from h7 h6,
    show P ∧ Q,
      from and.intro h8 h6 )
 
-- 2ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    have h4 : P → Q := h1.1,
    have h5 : Q := h4 h3,
    show P ∧ Q, from ⟨h3, h5⟩ )
  ( assume h6 : Q,
    have h7 : Q → P := h1.2,
    have h8 : P := h7 h6,
    show P ∧ Q, from ⟨h8, h6⟩ )
 
-- 3ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    show P ∧ Q, from ⟨h3, (h1.1 h3)⟩ )
  ( assume h6 : Q,
    show P ∧ Q, from ⟨h1.2 h6, h6⟩ )
 
-- 4ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  (λh, ⟨h, (h1.1 h)⟩)
  (λh, ⟨h1.2 h, h⟩)
 
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
h2.elim
  (λh, ⟨h, (h1.1 h)⟩)
  (λh, ⟨h1.2 h, h⟩)
 
-- 5ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  cases h2 with h3 h4,
  { split,
    { exact h3, },
    { apply h1.mp,
      exact h3, }},
  { split,
    { apply h1.mpr,
      exact h4, },
    { exact h4, }},
end
 
-- 6ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  cases h2 with h3 h4,
  { split,
    { exact h3, },
    { rw ← h1,
      exact h3, }},
  { split,
    { rw h1,
      exact h4, },
    { exact h4, }},
end
 
-- 7ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
-- by hint
by tauto
 
-- 8ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
by finish
 
-- 9ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  simp [h1] at h2 |-,
  assumption,
end
Seguir leyendo →

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 en el que se comentan 13 pruebas en Lean de

P ∧ Q ↔ Q ∧ P

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

-- ----------------------------------------------------
-- Ej. 1. (p. 17) Demostrar
--    P ∧ Q ↔ Q ∧ P
-- ----------------------------------------------------
 
import tactic
 
variables (P Q : Prop)
 
-- 1ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P,
      from and.elim_left h1,
    have h3 : Q,
      from and.elim_right h1,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q,
      from and.elim_left h4,
    have h6 : P,
      from and.elim_right h4,
    show P ∧ Q,
      from and.intro h6 h5)
 
-- 2ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P,
      from h1.1,
    have h3 : Q,
      from h1.2,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q,
      from h4.1,
    have h6 : P,
      from h4.2,
    show P ∧ Q,
      from and.intro h6 h5)
 
-- 3ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P := h1.1,
    have h3 : Q := h1.2,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q := h4.1,
    have h6 : P := h4.2,
    show P ∧ Q,
      from and.intro h6 h5)
 
-- 4ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    show Q ∧ P,
      from and.intro h1.2 h1.1)
  ( assume h4 : Q ∧ P,
    show P ∧ Q,
      from and.intro h4.2 h4.1)
 
-- 5ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q, and.intro h1.2 h1.1)
  ( assume h4 : Q ∧ P, and.intro h4.2 h4.1)
 
-- 6ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q, ⟨h1.2, h1.1⟩)
  ( assume h4 : Q ∧ P, ⟨h4.2, h4.1⟩)
 
-- 7ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  (λ h, ⟨h.2, h.1⟩)
  (λ h, ⟨h.2, h.1⟩)
 
-- 8ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  (λ ⟨hP, hQ⟩, ⟨hQ, hP⟩)
  (λ ⟨hQ, hP⟩, ⟨hP, hQ⟩)
 
-- 9ª demostración
lemma aux :
  P ∧ Q → Q ∧ P :=
λ h, ⟨h.2, h.1⟩
 
example : P ∧ Q ↔ Q ∧ P :=
iff.intro (aux P Q) (aux Q P)
 
-- 10ª demostración
example : P ∧ Q ↔ Q ∧ P :=
-- by library_search
and.comm
 
-- 11ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  split,
  { intro h1,
    cases h1 with h2 h3,
    split,
    { exact h3, },
    { exact h2, }},
  { intro h4,
    cases h4 with h5 h6,
    split,
    { exact h6, },
    { exact h5, }},
end
 
-- 12ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  split,
  { rintro ⟨h2, h3⟩,
    split,
    { exact h3, },
    { exact h2, }},
  { rintro ⟨h5, h6⟩,
    split,
    { exact h6, },
    { exact h5, }},
end
 
-- 13ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  constructor,
  { rintro ⟨h2, h3⟩,
    constructor,
    { exact h3, },
    { exact h2, }},
  { rintro ⟨h5, h6⟩,
    constructor,
    { exact h6, },
    { exact h5, }},
end
 
-- 14ª demostración
example : P ∧ Q ↔ Q ∧ P :=
-- by hint
by tauto
 
-- 15ª demostración
example : P ∧ Q ↔ Q ∧ P :=
by finish
Seguir leyendo →

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

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 13 pruebas en Lean de

¬P ∨ Q ⊢ 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

-- Prueba de ¬P ∨ Q ⊢ P → Q
-- ========================
 
-- ----------------------------------------------------
-- Ej. 1. (p. 15) Demostrar
--    ¬P ∨ Q ⊢ P → Q
-- ----------------------------------------------------
 
import tactic
 
variables (P Q : Prop)
 
-- 1ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( assume h5 : Q,
    show Q, from h5)
 
-- 2ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( assume h5 : Q, h5)
 
-- 3ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( λ h5, h5)
 
-- 4ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  id
 
-- 5ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    show Q,
      from false.elim (h3 h2))
  id
 
-- 6ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P, false.elim (h3 h2))
  id
 
-- 7ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( λ h3, false.elim (h3 h2))
  id
 
-- 8ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, or.elim h1 (λ h3, false.elim (h3 h2)) id
 
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, h1.elim (λ h3, false.elim (h3 h2)) id
 
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, h1.elim (λ h3, (h3 h2).elim) id
 
-- 9ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
-- by library_search
imp_iff_not_or.mpr h1
 
-- 10ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { apply false.rec,
    exact h3 h2, },
  { exact h4, },
end
 
-- 11ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { exact false.elim (h3 h2), },
  { exact h4, },
end
 
-- 12ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { exfalso,
    exact h3 h2, },
  { exact h4, },
end
 
-- 13ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
-- by hint
by tauto
 
-- 14ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
by finish
Seguir leyendo →