Menu Close

Negación del existencial en Lean: Caracterización de números no pares

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 15 pruebas en Lean de la propiedad

¬(∃ k, n = 2k) ↔ ∀ k, n ≠ 2k

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
 
variable (n : )
 
-- ----------------------------------------------------
-- Ejercicio. Demostrar que si n es un número entero,
-- entonces
--    ¬(∃ k, n = 2*k) ↔ ∀ k, n ≠ 2*k
-- ----------------------------------------------------
 
-- 1ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
begin
  split,
  { intro h,
    intro k,
    intro hk,
    apply h,
    use k,
    exact hk, },
  { intro h1,
    intro h2,
    cases h2 with k hk,
    apply h1 k,
    exact hk, },
end
 
-- 2ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
begin
  split,
  { intros h k hk,
    exact h ⟨k, hk⟩ },
  { rintros h ⟨k, rfl⟩,
    apply h k,
    refl, },
end
 
-- 3ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
begin
  split,
  { intros h k hk,
    exact h ⟨k, hk⟩ },
  { rintros h ⟨k, rfl⟩,
    exact h k rfl },
end
 
-- 4ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
begin
  push_neg,
end
 
-- 5ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
by push_neg
 
-- 6ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  ( assume h1 : ¬( k, n = 2*k),
    show  k, n  2*k, from
      assume k,
      show n  2*k, from
        assume h2 : n = 2*k,
        have h3 :  k, n = 2*k,
          from exists.intro k h2,
        show false,
          from h1 h3)
  ( assume h1 :  k, n  2*k,
    show ¬( k, n = 2*k), from
      assume h2 :  k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            have h3 : n  2*k,
              from h1 k,
            show false,
              from h3 hk))
 
-- 7ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  ( assume h1 : ¬( k, n = 2*k),
    show  k, n  2*k, from
      assume k,
      show n  2*k, from
        assume h2 : n = 2*k,
        have h3 :  k, n = 2*k,
          from exists.intro k h2,
        h1 h3)
  ( assume h1 :  k, n  2*k,
    show ¬( k, n = 2*k), from
      assume h2 :  k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            have h3 : n  2*k,
              from h1 k,
            h3 hk))
 
-- 8ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  ( assume h1 : ¬( k, n = 2*k),
    show  k, n  2*k, from
      assume k,
      show n  2*k, from
        assume h2 : n = 2*k,
        h1 (exists.intro k h2))
  ( assume h1 :  k, n  2*k,
    show ¬( k, n = 2*k), from
      assume h2 :  k, n = 2*k,
      show false, from
        exists.elim h2
          ( assume k,
            assume hk : n = 2*k,
            (h1 k) hk))
 
-- 9ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  ( assume h1 : ¬( k, n = 2*k),
    show  k, n  2*k, from
      assume k,
      λ h2, h1 (exists.intro k h2))
  ( assume h1 :  k, n  2*k,
    show ¬( k, n = 2*k), from
      assume h2 :  k, n = 2*k,
      show false, from
        exists.elim h2
          (λ k hk, (h1 k) hk))
 
-- 10ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  ( assume h1 : ¬( k, n = 2*k),
    λ k, λ h2, h1 (exists.intro k h2))
  ( assume h1 :  k, n  2*k,
    show ¬( k, n = 2*k), from
      assume h2 :  k, n = 2*k,
      exists.elim h2 (λ k hk, (h1 k) hk))
 
-- 11ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
iff.intro
  (λ h1 k h2, h1 (exists.intro k h2))
  (λ h1 h2, exists.elim h2 (λ k hk, (h1 k) hk))
 
-- 12ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=λ h1 k h2, h1 ⟨k, h2⟩,
 λ h1 h2, exists.elim h2 (λ k hk, (h1 k) hk)⟩
 
-- 13ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
-- by hint
by simp
 
-- 14ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
by finish
 
-- 15ª demostración
example : ¬( k, n = 2*k)   k, n  2*k :=
by norm_num
ForMatUS