Menu Close

Día: 21 enero, 2021

Pruebas en Lean de la ley de De Morgan: ¬(P ∧ Q) ↔ ¬P ∨ ¬Q

José A. Alonso--

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 12 pruebas en Lean de la ley de De Morgan:

¬(P ∧ Q) ↔ ¬P ∨ ¬Q

usando los estilos declarativo, aplicativo y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic
variables (P Q : Prop)
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que
--    ¬(P ∧ Q) ↔ ¬P ∨ ¬Q
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      apply h,
      split,
      { exact hP, },
      { exact hQ, }},
    { left,
      exact hP, }},
  { intros h h',
    cases h' with hP hQ,
    cases h with hnP hnQ,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end
 
-- 2ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
begin
  split,
  { intro h,
    by_cases hP : P,
    { right,
      intro hQ,
      exact h ⟨hP, hQ⟩, },
    { left,
      exact hP, }},
  { rintros (hnP | hnQ) ⟨hP, hQ⟩,
    { exact hnP hP, },
    { exact hnQ hQ, }},
end
 
-- 3ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        ( assume hnP : ¬P,
          show ¬P ∨ ¬Q,
            from or.inl hnP))
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          ( assume hnQ: ¬Q,
            show false,
              from hnQ (and.right hPQ)))
 
-- 4ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          show ¬P ∨ ¬Q,
            from or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          ( assume hnP: ¬P,
            show false,
              from hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))
 
-- 5ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              have hPQ: P ∧ Q,
                from and.intro hP hQ,
              show false,
                from h hPQ },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      assume hPQ : P ∧ Q,
      show false, from
        or.elim h
          (λ hnP, hnP (and.left hPQ))
          (λ hnQ, hnQ (and.right hPQ)))
 
-- 6ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          have hnQ : ¬Q,
            { assume hQ : Q,
              show false,
                from h (and.intro hP hQ) },
          or.inr hnQ)
        or.inl)
  ( assume h: ¬P ∨ ¬Q,
    show ¬(P ∧ Q), from
      λ hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 7ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        ( assume hP : P,
          or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 8ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  ( assume h : ¬(P ∧ Q),
    show ¬P ∨ ¬Q, from
      or.elim (classical.em P)
        (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
        or.inl)
  ( λ h hPQ, or.elim h (λ hnP, hnP (and.left hPQ))
                       (λ hnQ, hnQ (and.right hPQ)))
 
-- 9ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
iff.intro
  (λ h, or.elim (classical.em P)
          (λ hP, or.inr (λ hQ, h (and.intro hP hQ)))
          or.inl)
  (λ h hPQ, or.elim h
              (λ hnP, hnP (and.left hPQ))
              (λ hnQ, hnQ (and.right hPQ)))
 
-- 10ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
⟨λ h, or.elim (classical.em P) (λ hP, or.inr (λ hQ, h ⟨hP, hQ⟩)) or.inl,
 λ h hPQ, or.elim h (λ hnP, hnP hPQ.1) (λ hnQ, hnQ hPQ.2)⟩
 
-- 11ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by library_search
not_and_distrib
 
-- 12ª demostración
example : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q :=
-- by hint
by finish
Seguir leyendo →