Lean_Prover – Vestigium

Reseña: Formalising Lie algebras in Lean

PorJosé A. Alonso 27 diciembre 202127 diciembre 2021

Se ha publicado un artículo de razonamiento formalizado en Lean sobre álgebras de Lie titulado Formalising Lie algebras.

Su autor es Oliver Nash (Imperial College in London, U.K.).

Su resumen es

Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean’s Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory.

Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.

In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.

El código de las correspondientes teorías se encuentra aquí.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

Pruebas en Lean de “La función identidad no está acotada superiormente”

PorJosé A. Alonso 27 enero 20212 marzo 2021

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

La función identidad no está acotada superiormente

usando los estilos aplicativo, declarativo, y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    acotada_superiormente : (ℝ → ℝ) → Prop
-- tal que (acotada_superiormente f) expresa que la
-- función f está acotada superiormente.
-- ----------------------------------------------------

def acotada_superiormente : (ℝ → ℝ) → Prop
| f := ∃ M, ∀ x, f x ≤ M

-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que la función identidad no
-- está acotada superiormente.
-- ----------------------------------------------------

-- 1ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente,
  unfold id,
  by_contradiction h,
  cases h with M hM,
  specialize hM (M+1),
  contrapose hM,
  simp only [not_le],
  exact lt_add_one M,
end

-- 2ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente id,
  push_neg,
  intro M,
  use M + 1,
  linarith,
end

-- 3ª demostración
example : ¬acotada_superiormente id :=
begin
  unfold acotada_superiormente id,
  push_neg,
  exact no_top,
end

-- 4ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      have h4 : ¬(M < M + 1),
        from not_lt.mpr h3,
      have h5 : M < M + 1,
        from lt_add_one M,
      show false,
        from h4 h5)

-- 5ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      have h4 : ¬(M < M + 1),
        from not_lt.mpr h3,
      have h5 : M < M + 1,
        from lt_add_one M,
      h4 h5)

-- 6ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      have h3 : M + 1 ≤ M,
        from hM (M+1),
      (not_lt.mpr h3) (lt_add_one M))

-- 7ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    ( assume M,
      assume hM : ∀ x, id x ≤ M,
      (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 8ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
show false, from
  exists.elim h2
    (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 9ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
have h2 : ∃ M, ∀ x, id x ≤ M,
  from h1,
exists.elim h2
  (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 10ª demostración
example : ¬acotada_superiormente id :=
assume h1 : acotada_superiormente id,
exists.elim h1
  (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 11ª demostración
example : ¬acotada_superiormente id :=
λ h1, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

import data.real.basic

-- ----------------------------------------------------

-- Ejercicio 1. Definir la función

-- acotada_superiormente : (ℝ → ℝ) → Prop

-- tal que (acotada_superiormente f) expresa que la

-- función f está acotada superiormente.

-- ----------------------------------------------------

def acotada_superiormente : (ℝ → ℝ) → Prop

| f := ∃ M, ∀ x, f x ≤ M

-- ----------------------------------------------------

-- Ejercicio 2. Demostrar que la función identidad no

-- está acotada superiormente.

-- ----------------------------------------------------

-- 1ª demostración

example : ¬acotada_superiormente id :=

begin

unfold acotada_superiormente,

unfold id,

by_contradiction h,

cases h with M hM,

specialize hM (M+1),

contrapose hM,

simp only [not_le],

exact lt_add_one M,

end

-- 2ª demostración

example : ¬acotada_superiormente id :=

begin

unfold acotada_superiormente id,

push_neg,

intro M,

use M + 1,

linarith,

end

-- 3ª demostración

example : ¬acotada_superiormente id :=

begin

unfold acotada_superiormente id,

push_neg,

exact no_top,

end

-- 4ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

show false, from

exists.elim h2

( assume M,

assume hM : ∀ x, id x ≤ M,

have h3 : M + 1 ≤ M,

from hM (M+1),

have h4 : ¬(M < M + 1),

from not_lt.mpr h3,

have h5 : M < M + 1,

from lt_add_one M,

show false,

from h4 h5)

-- 5ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

show false, from

exists.elim h2

( assume M,

assume hM : ∀ x, id x ≤ M,

have h3 : M + 1 ≤ M,

from hM (M+1),

have h4 : ¬(M < M + 1),

from not_lt.mpr h3,

have h5 : M < M + 1,

from lt_add_one M,

h4 h5)

-- 6ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

show false, from

exists.elim h2

( assume M,

assume hM : ∀ x, id x ≤ M,

have h3 : M + 1 ≤ M,

from hM (M+1),

(not_lt.mpr h3) (lt_add_one M))

-- 7ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

show false, from

exists.elim h2

( assume M,

assume hM : ∀ x, id x ≤ M,

(not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 8ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

show false, from

exists.elim h2

(λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 9ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

have h2 : ∃ M, ∀ x, id x ≤ M,

from h1,

exists.elim h2

(λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 10ª demostración

example : ¬acotada_superiormente id :=

assume h1 : acotada_superiormente id,

exists.elim h1

(λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

-- 11ª demostración

example : ¬acotada_superiormente id :=

λ h1, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M))

Negación del universal en Lean: Caracterización de funciones no pares

PorJosé A. Alonso 23 enero 2021

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

¬par f ↔ ∃ x, f (-x) ≠ f x

usando los estilos declarativo, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variable (f : ℝ → ℝ)

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    par : (ℝ → ℝ) → Prop
-- tal que (par f) expresa que f es par.
-- ----------------------------------------------------

def par : (ℝ → ℝ) → Prop
| f := ∀ x, f (-x) = f x

-- ----------------------------------------------------
-- Ejercicio 2. Demostrar que
--    ¬par f ↔ ∃ x, f (-x) ≠ f x
-- ----------------------------------------------------

-- 1ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  split,
  { contrapose,
    intro h1,
    rw not_not,
    unfold par,
    intro x,
    by_contradiction h2,
    apply h1,
    use x, },
  { intro h1,
    intro h2,
    unfold par at h2,
    cases h1 with x hx,
    apply hx,
    exact h2 x, },
end

-- 2ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  split,
  { contrapose,
    intro h1,
    rw not_not,
    intro x,
    by_contradiction h2,
    apply h1,
    use x, },
  { rintros ⟨x, hx⟩ h',
    exact hx (h' x) },
end

-- 3ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
begin
  unfold par,
  push_neg,
end

-- 4ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
iff.intro
  ( have h1 : ¬(∃ x, f (-x) ≠ f x) → ¬¬par f,
      { assume h2 : ¬(∃ x, f (-x) ≠ f x),
        have h3 : par f,
          { assume x,
            have h4 : ¬(f (-x) ≠ f x),
              { assume h5 : f (-x) ≠ f x,
                have h6 : ∃ x, f (-x) ≠ f x,
                  from exists.intro x h5,
                show false,
                  from h2 h6, },
            show f (-x) = f x,
              from not_not.mp h4},
        show ¬¬par f,
          from not_not.mpr h3 },
    show ¬par f → (∃ x, f (-x) ≠ f x),
      from not_imp_not.mp h1)
  ( assume h1 : ∃ x, f (-x) ≠ f x,
    show ¬par f,
      { assume h2 : par f,
        show false, from
          exists.elim h1
            ( assume x,
              assume hx : f (-x) ≠ f x,
              have h3 : f (-x) = f x,
                from h2 x,
              show false,
                from hx h3)})

-- 5ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
-- by suggest
not_forall

-- 6ª demostración
example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=
-- by hint
by simp [par]

100

import data.real.basic

variable (f : ℝ → ℝ)

-- ----------------------------------------------------

-- Ejercicio 1. Definir la función

-- par : (ℝ → ℝ) → Prop

-- tal que (par f) expresa que f es par.

-- ----------------------------------------------------

def par : (ℝ → ℝ) → Prop

| f := ∀ x, f (-x) = f x

-- ----------------------------------------------------

-- Ejercicio 2. Demostrar que

-- ¬par f ↔ ∃ x, f (-x) ≠ f x

-- ----------------------------------------------------

-- 1ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

begin

split,

{ contrapose,

intro h1,

rw not_not,

unfold par,

intro x,

by_contradiction h2,

apply h1,

use x, },

{ intro h1,

intro h2,

unfold par at h2,

cases h1 with x hx,

apply hx,

exact h2 x, },

end

-- 2ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

begin

split,

{ contrapose,

intro h1,

rw not_not,

intro x,

by_contradiction h2,

apply h1,

use x, },

{ rintros ⟨x, hx⟩ h',

exact hx (h' x) },

end

-- 3ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

begin

unfold par,

push_neg,

end

-- 4ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

iff.intro

( have h1 : ¬(∃ x, f (-x) ≠ f x) → ¬¬par f,

{ assume h2 : ¬(∃ x, f (-x) ≠ f x),

have h3 : par f,

{ assume x,

have h4 : ¬(f (-x) ≠ f x),

{ assume h5 : f (-x) ≠ f x,

have h6 : ∃ x, f (-x) ≠ f x,

from exists.intro x h5,

show false,

from h2 h6, },

show f (-x) = f x,

from not_not.mp h4},

show ¬¬par f,

from not_not.mpr h3 },

show ¬par f → (∃ x, f (-x) ≠ f x),

from not_imp_not.mp h1)

( assume h1 : ∃ x, f (-x) ≠ f x,

show ¬par f,

{ assume h2 : par f,

show false, from

exists.elim h1

( assume x,

assume hx : f (-x) ≠ f x,

have h3 : f (-x) = f x,

from h2 x,

show false,

from hx h3)})

-- 5ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

-- by suggest

not_forall

-- 6ª demostración

example : ¬par f ↔ ∃ x, f (-x) ≠ f x :=

-- by hint

by simp [par]

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

PorJosé A. Alonso 22 enero 2021

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

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

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

PorJosé A. Alonso 21 enero 2021

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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

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