Vestigium

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

Pruebas en Lean de “Un número es par si, y sólo si, lo es su cuadrado”

PorJosé A. Alonso 20 enero 2021

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

Un número es par si, y sólo si, lo es su cuadrado-

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 data.int.parity
open int

variable (n : ℤ)

-- ----------------------------------------------------
-- Ejercicio. Demostrar que un número es par syss lo es
-- su cuadrado.
-- ----------------------------------------------------

-- 1ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    unfold odd,
    intro h,
    cases h with k hk,
    use 2*k*(k+1),
    rw hk,
    ring, },
  { unfold even,
    intro h,
    cases h with k hk,
    use 2*k^2,
    rw hk,
    ring, },
end

-- 2ª demostración
example :
  even (n^2) ↔ even n :=
begin
  split,
  { contrapose,
    rw ← odd_iff_not_even,
    rw ← odd_iff_not_even,
    rintro ⟨k, rfl⟩,
    use 2*k*(k+1),
    ring, },
  { rintro ⟨k, rfl⟩,
    use 2*k^2,
    ring, },
end

-- 3ª demostración
example :
  even (n^2) ↔ even n :=
iff.intro
  ( have h : ¬even n → ¬even (n^2),
      { assume h1 : ¬even n,
        have h2 : odd n,
          from odd_iff_not_even.mpr h1,
        have h3: odd (n^2), from
          exists.elim h2
            ( assume k,
              assume hk : n = 2*k+1,
              have h4 : n^2 = 2*(2*k*(k+1))+1, from
                calc  n^2
                    = (2*k+1)^2       : by rw hk
                ... = 4*k^2+4*k+1     : by ring
                ... = 2*(2*k*(k+1))+1 : by ring,
              show odd (n^2),
                from exists.intro (2*k*(k+1)) h4),
        show ¬even (n^2),
          from odd_iff_not_even.mp h3 },
    show even (n^2) → even n,
      from not_imp_not.mp h )
  ( assume h1 : even n,
    show even (n^2), from
      exists.elim h1
        ( assume k,
          assume hk : n = 2*k ,
          have h2 : n^2 = 2*(2*k^2), from
            calc  n^2
                = (2*k)^2   : by rw hk
            ... = 2*(2*k^2) : by ring,
          show even (n^2),
            from exists.intro (2*k^2) h2 ))

import data.int.parity

open int

variable (n : ℤ)

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

-- Ejercicio. Demostrar que un número es par syss lo es

-- su cuadrado.

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

-- 1ª demostración

example :

even (n^2) ↔ even n :=

begin

split,

{ contrapose,

rw ← odd_iff_not_even,

unfold odd,

intro h,

cases h with k hk,

use 2*k*(k+1),

rw hk,

ring, },

{ unfold even,

intro h,

cases h with k hk,

use 2*k^2,

rw hk,

ring, },

end

-- 2ª demostración

example :

even (n^2) ↔ even n :=

begin

split,

{ contrapose,

rw ← odd_iff_not_even,

rintro ⟨k, rfl⟩,

use 2*k*(k+1),

ring, },

{ rintro ⟨k, rfl⟩,

use 2*k^2,

ring, },

end

-- 3ª demostración

example :

even (n^2) ↔ even n :=

iff.intro

( have h : ¬even n → ¬even (n^2),

{ assume h1 : ¬even n,

have h2 : odd n,

from odd_iff_not_even.mpr h1,

have h3: odd (n^2), from

exists.elim h2

( assume k,

assume hk : n = 2*k+1,

have h4 : n^2 = 2*(2*k*(k+1))+1, from

calc n^2

= (2*k+1)^2 : by rw hk

... = 4*k^2+4*k+1 : by ring

... = 2*(2*k*(k+1))+1 : by ring,

show odd (n^2),

from exists.intro (2*k*(k+1)) h4),

show ¬even (n^2),

from odd_iff_not_even.mp h3 },

show even (n^2) → even n,

from not_imp_not.mp h )

( assume h1 : even n,

show even (n^2), from

exists.elim h1

( assume k,

assume hk : n = 2*k ,

have h2 : n^2 = 2*(2*k^2), from

calc n^2

= (2*k)^2 : by rw hk

... = 2*(2*k^2) : by ring,

show even (n^2),

from exists.intro (2*k^2) h2 ))

Pruebas en Lean de “La relación menor es irreflexiva en los reales”

PorJosé A. Alonso 18 enero 2021

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

La relación menor es irreflexiva en los reales

usando los estilos declarativo, funcional, 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
import tactic

variable {x : ℝ}

-- ----------------------------------------------------
-- Ejercicio. Demostrar que la relación menor es
-- irreflexiva en los reales.
-- ----------------------------------------------------

-- 1ª demostración
example : ¬ x < x :=
begin
  intro h1,
  rw lt_iff_le_and_ne at h1,
  cases h1 with h2 h3,
  -- clear h2,
  -- change x = x → false at h3,
  apply h3,
  refl,
end

-- 2ª demostración
example : ¬ x < x :=
begin
  intro h1,
  rw lt_iff_le_and_ne at h1,
  cases h1 with h2 h3,
  apply h3,
  refl,
end

-- 3ª demostración
example : ¬ x < x :=
begin
  intro h1,
  cases (lt_iff_le_and_ne.mp h1) with h2 h3,
  apply h3,
  refl,
end

-- 4ª demostración
example : ¬ x < x :=
begin
  intro h1,
  apply (lt_iff_le_and_ne.mp h1).2,
  refl,
end

-- 5ª demostración
example : ¬ x < x :=
begin
  intro h1,
  exact absurd rfl (lt_iff_le_and_ne.mp h1).2,
end

-- 6ª demostración
example : ¬ x < x :=
λ h, absurd rfl (lt_iff_le_and_ne.mp h).2

-- 7ª demostración
example : ¬ x < x :=
assume h1 : x < x,
have h2 : x ≤ x ∧ x ≠ x,
  from lt_iff_le_and_ne.mp h1,
have h3 : x ≠ x,
  from and.right h2,
have h4 : x = x,
  from rfl,
show false,
  from absurd h4 h3

-- 8ª demostración
example : ¬ x < x :=
assume h1 : x < x,
have h2 : x ≤ x ∧ x ≠ x,
  from lt_iff_le_and_ne.mp h1,
absurd rfl (and.right h2)

-- 9ª demostración
example : ¬ x < x :=
assume h1 : x < x,
absurd rfl (and.right (lt_iff_le_and_ne.mp h1))

-- 10ª demostración
example : ¬ x < x :=
assume h1 : x < x,
absurd rfl (lt_iff_le_and_ne.mp h1).2

-- 11ª demostración
example : ¬ x < x :=
λ h, absurd rfl (lt_iff_le_and_ne.mp h).2

-- 12ª demostración
example : ¬ x < x :=
-- by library_search
irrefl x

-- 12ª demostración
example : ¬ x < x :=
-- by hint
by simp

-- 13ª demostración
example : ¬ x < x :=
by finish

-- 14ª demostración
example : ¬ x < x :=
by norm_num

-- 15ª demostración
example : ¬ x < x :=
by linarith

-- 16ª demostración
example : ¬ x < x :=
by nlinarith

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

import data.real.basic

import tactic

variable {x : ℝ}

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

-- Ejercicio. Demostrar que la relación menor es

-- irreflexiva en los reales.

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

-- 1ª demostración

example : ¬ x < x :=

begin

intro h1,

rw lt_iff_le_and_ne at h1,

cases h1 with h2 h3,

-- clear h2,

-- change x = x → false at h3,

apply h3,

refl,

end

-- 2ª demostración

example : ¬ x < x :=

begin

intro h1,

rw lt_iff_le_and_ne at h1,

cases h1 with h2 h3,

apply h3,

refl,

end

-- 3ª demostración

example : ¬ x < x :=

begin

intro h1,

cases (lt_iff_le_and_ne.mp h1) with h2 h3,

apply h3,

refl,

end

-- 4ª demostración

example : ¬ x < x :=

begin

intro h1,

apply (lt_iff_le_and_ne.mp h1).2,

refl,

end

-- 5ª demostración

example : ¬ x < x :=

begin

intro h1,

exact absurd rfl (lt_iff_le_and_ne.mp h1).2,

end

-- 6ª demostración

example : ¬ x < x :=

λ h, absurd rfl (lt_iff_le_and_ne.mp h).2

-- 7ª demostración

example : ¬ x < x :=

assume h1 : x < x,

have h2 : x ≤ x ∧ x ≠ x,

from lt_iff_le_and_ne.mp h1,

have h3 : x ≠ x,

from and.right h2,

have h4 : x = x,

from rfl,

show false,

from absurd h4 h3

-- 8ª demostración

example : ¬ x < x :=

assume h1 : x < x,

have h2 : x ≤ x ∧ x ≠ x,

from lt_iff_le_and_ne.mp h1,

absurd rfl (and.right h2)

-- 9ª demostración

example : ¬ x < x :=

assume h1 : x < x,

absurd rfl (and.right (lt_iff_le_and_ne.mp h1))

-- 10ª demostración

example : ¬ x < x :=

assume h1 : x < x,

absurd rfl (lt_iff_le_and_ne.mp h1).2

-- 11ª demostración

example : ¬ x < x :=

λ h, absurd rfl (lt_iff_le_and_ne.mp h).2

-- 12ª demostración

example : ¬ x < x :=

-- by library_search

irrefl x

-- 12ª demostración

example : ¬ x < x :=

-- by hint

by simp

-- 13ª demostración

example : ¬ x < x :=

by finish

-- 14ª demostración

example : ¬ x < x :=

by norm_num

-- 15ª demostración

example : ¬ x < x :=

by linarith

-- 16ª demostración

example : ¬ x < x :=

by nlinarith

Pruebas en Lean de “Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u”

PorJosé A. Alonso 16 enero 2021

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

Si u es una sucesión de Cauchy y a es un punto de acumulación de u, entonces a es el límite de u.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variable  {u : ℕ → ℝ}
variables {a : ℝ}
variable  {φ : ℕ → ℕ}

-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=
λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

def extraccion : (ℕ → ℕ) → Prop
| φ := ∀ n m, n < m → φ n < φ m

lemma id_mne_extraccion
  (h : extraccion φ)
  : ∀ n, n ≤ φ n :=
begin
  intros n,
  induction n with m HI,
  { linarith },
  { exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },
end

lemma extraccion_mye
  (h : extraccion φ)
  : ∀ N N', ∃ n ≥ N', φ n ≥ N :=
λ N N',
  ⟨max N N', le_max_right N N',
             le_trans (le_max_left N N')
             (id_mne_extraccion h (max N N'))⟩

def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop
| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

lemma cerca_acumulacion
  (h : punto_acumulacion u a)
  : ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=
begin
  intros ε hε N,
  rcases h with ⟨φ, hφ1, hφ2⟩,
  cases hφ2 ε hε with N' hN',
  rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,
  exact ⟨φ m, hm', hN' _ hm⟩,
end

def sucesion_de_Cauchy : (ℕ → ℝ) → Prop
| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

-- ----------------------------------------------------
-- Ejercicio. Demostrar que si u es una sucesión de
-- Cauchy y a es un punto de acumulación de u, entonces
-- a es el límite de u.
-- ----------------------------------------------------

-- 1ª demostración
example
  (hu : sucesion_de_Cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  -- unfold limite,
  intros ε hε,
  -- unfold sucesion_de_Cauchy at hu,
  cases hu (ε/2) (half_pos hε) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,
    apply cerca_acumulacion ha (ε/2) (half_pos hε),
  cases ha' with N' h,
  cases h with hNN' hN',
  intros n hn,
  calc   |u n - a|
       = |(u n - u N') + (u N' - a)| : by ring
   ... ≤ |u n - u N'| + |u N' - a|   : abs_add (u n - u N') (u N' - a)
   ... ≤ ε/2 + |u N' - a|            : add_le_add_right (hN n N' hn hNN') _
   ... ≤ ε/2 + ε/2                   : add_le_add_left hN' (ε / 2)
   ... = ε                           : add_halves ε
end

-- 2ª demostración
example
  (hu : sucesion_de_Cauchy u)
  (ha : punto_acumulacion u a)
  : limite u a :=
begin
  intros ε hε,
  cases hu (ε/2) (by linarith) with N hN,
  use N,
  have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,
    apply cerca_acumulacion ha (ε/2) (by linarith),
  rcases ha' with ⟨N', hNN', hN'⟩,
  intros n hn,
  calc  |u n - a|
      = |(u n - u N') + (u N' - a)| : by ring
  ... ≤ |u n - u N'| + |u N' - a|   : by simp [abs_add]
  ... ≤ ε                           : by linarith [hN n N' hn hNN'],
end

100

101

102

import data.real.basic

variable {u : ℕ → ℝ}

variables {a : ℝ}

variable {φ : ℕ → ℕ}

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

-- Nota. Usaremos los siguientes conceptos estudiados

-- anteriormente.

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

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

def extraccion : (ℕ → ℕ) → Prop

| φ := ∀ n m, n < m → φ n < φ m

lemma id_mne_extraccion

(h : extraccion φ)

: ∀ n, n ≤ φ n :=

begin

intros n,

induction n with m HI,

{ linarith },

{ exact nat.succ_le_of_lt (by linarith [h m (m+1) (by linarith)]) },

end

lemma extraccion_mye

(h : extraccion φ)

: ∀ N N', ∃ n ≥ N', φ n ≥ N :=

λ N N',

⟨max N N', le_max_right N N',

le_trans (le_max_left N N')

(id_mne_extraccion h (max N N'))⟩

def punto_acumulacion : (ℕ → ℝ) → ℝ → Prop

| u a := ∃ φ, extraccion φ ∧ limite (u ∘ φ) a

lemma cerca_acumulacion

(h : punto_acumulacion u a)

: ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε :=

begin

intros ε hε N,

rcases h with ⟨φ, hφ1, hφ2⟩,

cases hφ2 ε hε with N' hN',

rcases extraccion_mye hφ1 N N' with ⟨m, hm, hm'⟩,

exact ⟨φ m, hm', hN' _ hm⟩,

end

def sucesion_de_Cauchy : (ℕ → ℝ) → Prop

| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

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

-- Ejercicio. Demostrar que si u es una sucesión de

-- Cauchy y a es un punto de acumulación de u, entonces

-- a es el límite de u.

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

-- 1ª demostración

example

(hu : sucesion_de_Cauchy u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

-- unfold limite,

intros ε hε,

-- unfold sucesion_de_Cauchy at hu,

cases hu (ε/2) (half_pos hε) with N hN,

use N,

have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,

apply cerca_acumulacion ha (ε/2) (half_pos hε),

cases ha' with N' h,

cases h with hNN' hN',

intros n hn,

calc |u n - a|

= |(u n - u N') + (u N' - a)| : by ring

... ≤ |u n - u N'| + |u N' - a| : abs_add (u n - u N') (u N' - a)

... ≤ ε/2 + |u N' - a| : add_le_add_right (hN n N' hn hNN') _

... ≤ ε/2 + ε/2 : add_le_add_left hN' (ε / 2)

... = ε : add_halves ε

end

-- 2ª demostración

example

(hu : sucesion_de_Cauchy u)

(ha : punto_acumulacion u a)

: limite u a :=

begin

intros ε hε,

cases hu (ε/2) (by linarith) with N hN,

use N,

have ha' : ∃ N' ≥ N, |u N' - a| ≤ ε/2,

apply cerca_acumulacion ha (ε/2) (by linarith),

rcases ha' with ⟨N', hNN', hN'⟩,

intros n hn,

calc |u n - a|

= |(u n - u N') + (u N' - a)| : by ring

... ≤ |u n - u N'| + |u N' - a| : by simp [abs_add]

... ≤ ε : by linarith [hN n N' hn hNN'],

end

Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”

PorJosé A. Alonso 15 enero 2021

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

Toda sucesión convergente es una sucesión de Cauchy

usando los estilos aplicativo y declarativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.real.basic

variable {u : ℕ → ℝ}

-- ----------------------------------------------------
-- Nota. Usaremos los siguientes conceptos estudiados
-- anteriormente.
-- ----------------------------------------------------

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=
λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

-- ----------------------------------------------------
-- Ejercicio 1. Definir la función
--    sucesion_convergente : (ℕ → ℝ) → Prop
-- tal que (sucesion_convergente u) expresa que la
-- sucesión u es convergente.
-- ----------------------------------------------------

def sucesion_convergente : (ℕ → ℝ) → Prop
| u := ∃ a, limite u a

-- ----------------------------------------------------
-- Ejercicio 2. Definir la función
--    sucesion_de_Cauchy : (ℕ → ℝ) → Prop
-- tal que (sucesion_de_Cauchy u) expresa que la
-- sucesión u es una sucesión de Cauchy.
-- ----------------------------------------------------

def sucesion_de_Cauchy : (ℕ → ℝ) → Prop
| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

-- ----------------------------------------------------
-- Ejercicio 3. Demostrar que toda sucesión convergente
-- es una sucesión de Cauchy.
-- ----------------------------------------------------

-- 1ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
begin
  -- unfold sucesion_convergente at h,
  cases h with a ha,
  -- unfold sucesion_de_Cauchy,
  intros ε hε,
  -- unfold limite at ha,
  cases ha (ε/2) (half_pos hε) with N hN,
  use N,
  intros p q hp hq,
  calc  |u p - u q|
      = |(u p - a) + (a - u q)| : by ring
  ... ≤ |u p - a| + |a - u q|   : by apply abs_add
  ... = |u p - a| + |u q - a|   : by rw abs_sub (u q) a
  ... ≤ ε/2 + |u q - a|         : add_le_add_right (hN p hp) _
  ... ≤ ε/2 + ε/2               : add_le_add_left (hN q hq) (ε/2)
  ... = ε                       : add_halves ε
end

-- 2ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
begin
  cases h with a ha,
  intros ε hε,
  cases ha (ε/2) (by linarith) with N hN,
  use N,
  intros p q hp hq,
  calc  |u p - u q|
      = |(u p - a) + (a - u q)| : by ring
  ... ≤ |u p - a| + |a - u q|   : by simp only [abs_add]
  ... = |u p - a| + |u q - a|   : by simp only [abs_add, abs_sub]
  ... ≤ ε                       : by linarith [hN p hp, hN q hq],
end

-- 3ª demostración
example
  (h : sucesion_convergente u)
  : sucesion_de_Cauchy u :=
exists.elim h
  (assume a,
   assume ha : limite u a,
   show sucesion_de_Cauchy u, from
     (assume ε,
      assume hε : ε > 0,
      exists.elim (ha (ε/2) (by linarith))
        (assume N,
         assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε/2,
         show ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε,
           from exists.intro N
             (assume p q,
              assume hp: p ≥ N,
              assume hq: q ≥ N,
              show |u p - u q| ≤ ε, from
                calc  |u p - u q|
                    = |(u p - a) + (a - u q)| : by ring
                ... ≤ |u p - a| + |a - u q|   : by simp only [abs_add]
                ... = |u p - a| + |u q - a|   : by simp only [abs_add, abs_sub]
                ... ≤ ε                       : by linarith [hN p hp, hN q hq]))))

100

101

102

import data.real.basic

variable {u : ℕ → ℝ}

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

-- Nota. Usaremos los siguientes conceptos estudiados

-- anteriormente.

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

notation `|`x`|` := abs x

def limite : (ℕ → ℝ) → ℝ → Prop :=

λ u c, ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

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

-- Ejercicio 1. Definir la función

-- sucesion_convergente : (ℕ → ℝ) → Prop

-- tal que (sucesion_convergente u) expresa que la

-- sucesión u es convergente.

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

def sucesion_convergente : (ℕ → ℝ) → Prop

| u := ∃ a, limite u a

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

-- Ejercicio 2. Definir la función

-- sucesion_de_Cauchy : (ℕ → ℝ) → Prop

-- tal que (sucesion_de_Cauchy u) expresa que la

-- sucesión u es una sucesión de Cauchy.

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

def sucesion_de_Cauchy : (ℕ → ℝ) → Prop

| u := ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε

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

-- Ejercicio 3. Demostrar que toda sucesión convergente

-- es una sucesión de Cauchy.

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

-- 1ª demostración

example

(h : sucesion_convergente u)

: sucesion_de_Cauchy u :=

begin

-- unfold sucesion_convergente at h,

cases h with a ha,

-- unfold sucesion_de_Cauchy,

intros ε hε,

-- unfold limite at ha,

cases ha (ε/2) (half_pos hε) with N hN,

use N,

intros p q hp hq,

calc |u p - u q|

= |(u p - a) + (a - u q)| : by ring

... ≤ |u p - a| + |a - u q| : by apply abs_add

... = |u p - a| + |u q - a| : by rw abs_sub (u q) a

... ≤ ε/2 + |u q - a| : add_le_add_right (hN p hp) _

... ≤ ε/2 + ε/2 : add_le_add_left (hN q hq) (ε/2)

... = ε : add_halves ε

end

-- 2ª demostración

example

(h : sucesion_convergente u)

: sucesion_de_Cauchy u :=

begin

cases h with a ha,

intros ε hε,

cases ha (ε/2) (by linarith) with N hN,

use N,

intros p q hp hq,

calc |u p - u q|

= |(u p - a) + (a - u q)| : by ring

... ≤ |u p - a| + |a - u q| : by simp only [abs_add]

... = |u p - a| + |u q - a| : by simp only [abs_add, abs_sub]

... ≤ ε : by linarith [hN p hp, hN q hq],

end

-- 3ª demostración

example

(h : sucesion_convergente u)

: sucesion_de_Cauchy u :=

exists.elim h

(assume a,

assume ha : limite u a,

show sucesion_de_Cauchy u, from

(assume ε,

assume hε : ε > 0,

exists.elim (ha (ε/2) (by linarith))

(assume N,

assume hN : ∀ n, n ≥ N → |u n - a| ≤ ε/2,

show ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε,

from exists.intro N

(assume p q,

assume hp: p ≥ N,

assume hq: q ≥ N,

show |u p - u q| ≤ ε, from

calc |u p - u q|

= |(u p - a) + (a - u q)| : by ring

... ≤ |u p - a| + |a - u q| : by simp only [abs_add]

... = |u p - a| + |u q - a| : by simp only [abs_add, abs_sub]

... ≤ ε : by linarith [hN p hp, hN q hq]))))