septiembre 2020 – Vestigium

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

PorJosé A. Alonso 30 septiembre 202020 diciembre 2020

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

1	¬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

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

-- 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

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

PorJosé A. Alonso 30 septiembre 202020 diciembre 2020

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

1	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

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

-- 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

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

PorJosé A. Alonso 30 septiembre 202020 diciembre 2020

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

1	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

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

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

-- 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

ForMatUS: Pruebas en Lean del principio del tercio excluso

PorJosé A. Alonso 29 septiembre 202020 diciembre 2020

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

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

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

-- 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

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

PorJosé A. Alonso 29 septiembre 202020 diciembre 2020

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

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

-- 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