septiembre 2020 – Página 2

ForMatUS: Pruebas en Lean de la regla de reducción al absurdo

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 6 pruebas en Lean de la regla de reducción al absurdo 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

import tactic

variable (P : Prop)

-- ----------------------------------------------------
-- Ej. 1 (p. 22) Demostrar que
--    ¬P → false ⊢ P
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : ¬P → false)
  : P :=
have h2 : ¬¬P, from
  assume h3 : ¬P,
  show false, from h1 h3,
show P, from not_not.mp h2

-- 2ª demostración
example
  (h1 : ¬P → false)
  : P :=
begin
  apply not_not.mp,
  intro h2,
  exact h1 h2,
end

-- 3ª demostración
example
  (h1 : ¬P → false)
  : P :=
begin
  apply not_not.mp,
  exact λ h2, h1 h2,
end

-- 4ª demostración
example
  (h1 : ¬P → false)
  : P :=
not_not.mp (λ h2, h1 h2)

-- #print axioms not_not

-- 5ª demostración
example
  (h1 : ¬P → false)
  : P :=
-- by library_search
by_contra h1

-- #print axioms by_contra

-- 6ª demostración
lemma RAA
  (h1 : ¬P → false)
  : P :=
-- by hint
by finish

-- #print axioms RAA

import tactic

variable (P : Prop)

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

-- Ej. 1 (p. 22) Demostrar que

-- ¬P → false ⊢ P

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

-- 1ª demostración

example

(h1 : ¬P → false)

: P :=

have h2 : ¬¬P, from

assume h3 : ¬P,

show false, from h1 h3,

show P, from not_not.mp h2

-- 2ª demostración

example

(h1 : ¬P → false)

: P :=

begin

apply not_not.mp,

intro h2,

exact h1 h2,

end

-- 3ª demostración

example

(h1 : ¬P → false)

: P :=

begin

apply not_not.mp,

exact λ h2, h1 h2,

end

-- 4ª demostración

example

(h1 : ¬P → false)

: P :=

not_not.mp (λ h2, h1 h2)

-- #print axioms not_not

-- 5ª demostración

example

(h1 : ¬P → false)

: P :=

-- by library_search

by_contra h1

-- #print axioms by_contra

-- 6ª demostración

lemma RAA

(h1 : ¬P → false)

: P :=

-- by hint

by finish

-- #print axioms RAA

PFH: Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell)

PorJosé A. Alonso 25 septiembre 202020 diciembre 2020

He añadido a la lista Programación funcional con Haskell el vídeo Programas, funciones y dibujos (Introducción a la programación funcional con CodeWorld/Haskell) en el que se explica cómo escribir las funciones de los programas para hacer dibujos. En concreto,

cómo programar dibujos elementales
cómo programar dibujos compuestos
cómo transformar dibujos con traslaciones, rotaciones, escalamiento y
cómo colorear.
cómo programar animaciones

El vídeo es

Los apuntes correspondientes son

ForMatUS: Reglas de eliminación del bicondicional en P ↔ Q, P ∨ Q ⊢ P ∧ Q

PorJosé A. Alonso 23 septiembre 202020 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 9 pruebas en Lean de

P ↔ Q, P ∨ Q ⊢ P ∧ Q

1	P ↔ Q, 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. 18) Demostrar
--     P ↔ Q, P ∨ Q ⊢ P ∧ Q
-- ----------------------------------------------------

import tactic

variables (P Q : Prop)

-- 1ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    have h4 : P → Q,
      from iff.elim_left h1,
    have h5 : Q,
      from h4 h3,
    show P ∧ Q,
      from and.intro h3 h5 )
  ( assume h6 : Q,
    have h7 : Q → P,
      from iff.elim_right h1,
    have h8 : P,
      from h7 h6,
    show P ∧ Q,
      from and.intro h8 h6 )

-- 2ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    have h4 : P → Q := h1.1,
    have h5 : Q := h4 h3,
    show P ∧ Q, from ⟨h3, h5⟩ )
  ( assume h6 : Q,
    have h7 : Q → P := h1.2,
    have h8 : P := h7 h6,
    show P ∧ Q, from ⟨h8, h6⟩ )

-- 3ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  ( assume h3 : P,
    show P ∧ Q, from ⟨h3, (h1.1 h3)⟩ )
  ( assume h6 : Q,
    show P ∧ Q, from ⟨h1.2 h6, h6⟩ )

-- 4ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
or.elim h2
  (λh, ⟨h, (h1.1 h)⟩)
  (λh, ⟨h1.2 h, h⟩)

example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
h2.elim
  (λh, ⟨h, (h1.1 h)⟩)
  (λh, ⟨h1.2 h, h⟩)

-- 5ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  cases h2 with h3 h4,
  { split,
    { exact h3, },
    { apply h1.mp,
      exact h3, }},
  { split,
    { apply h1.mpr,
      exact h4, },
    { exact h4, }},
end

-- 6ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  cases h2 with h3 h4,
  { split,
    { exact h3, },
    { rw ← h1,
      exact h3, }},
  { split,
    { rw h1,
      exact h4, },
    { exact h4, }},
end

-- 7ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
-- by hint
by tauto

-- 8ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
by finish

-- 9ª demostración
example
  (h1 : P ↔ Q)
  (h2 : P ∨ Q)
  : P ∧ Q :=
begin
  simp [h1] at h2 |-,
  assumption,
end

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

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

-- Ej. 1. (p. 18) Demostrar

-- P ↔ Q, P ∨ Q ⊢ P ∧ Q

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

import tactic

variables (P Q : Prop)

-- 1ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

or.elim h2

( assume h3 : P,

have h4 : P → Q,

from iff.elim_left h1,

have h5 : Q,

from h4 h3,

show P ∧ Q,

from and.intro h3 h5 )

( assume h6 : Q,

have h7 : Q → P,

from iff.elim_right h1,

have h8 : P,

from h7 h6,

show P ∧ Q,

from and.intro h8 h6 )

-- 2ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

or.elim h2

( assume h3 : P,

have h4 : P → Q := h1.1,

have h5 : Q := h4 h3,

show P ∧ Q, from ⟨h3, h5⟩ )

( assume h6 : Q,

have h7 : Q → P := h1.2,

have h8 : P := h7 h6,

show P ∧ Q, from ⟨h8, h6⟩ )

-- 3ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

or.elim h2

( assume h3 : P,

show P ∧ Q, from ⟨h3, (h1.1 h3)⟩ )

( assume h6 : Q,

show P ∧ Q, from ⟨h1.2 h6, h6⟩ )

-- 4ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

or.elim h2

(λh, ⟨h, (h1.1 h)⟩)

(λh, ⟨h1.2 h, h⟩)

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

h2.elim

(λh, ⟨h, (h1.1 h)⟩)

(λh, ⟨h1.2 h, h⟩)

-- 5ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

begin

cases h2 with h3 h4,

{ split,

{ exact h3, },

{ apply h1.mp,

exact h3, }},

{ split,

{ apply h1.mpr,

exact h4, },

{ exact h4, }},

end

-- 6ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

begin

cases h2 with h3 h4,

{ split,

{ exact h3, },

{ rw ← h1,

exact h3, }},

{ split,

{ rw h1,

exact h4, },

{ exact h4, }},

end

-- 7ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

-- by hint

by tauto

-- 8ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

by finish

-- 9ª demostración

example

(h1 : P ↔ Q)

(h2 : P ∨ Q)

: P ∧ Q :=

begin

simp [h1] at h2 |-,

assumption,

end

ForMatUS: Pruebas en Lean de P ∧ Q ↔ Q ∧ P

PorJosé A. Alonso 22 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

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. 17) Demostrar
--    P ∧ Q ↔ Q ∧ P
-- ----------------------------------------------------

import tactic

variables (P Q : Prop)

-- 1ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P,
      from and.elim_left h1,
    have h3 : Q,
      from and.elim_right h1,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q,
      from and.elim_left h4,
    have h6 : P,
      from and.elim_right h4,
    show P ∧ Q,
      from and.intro h6 h5)

-- 2ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P,
      from h1.1,
    have h3 : Q,
      from h1.2,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q,
      from h4.1,
    have h6 : P,
      from h4.2,
    show P ∧ Q,
      from and.intro h6 h5)

-- 3ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    have h2 : P := h1.1,
    have h3 : Q := h1.2,
    show Q ∧ P,
      from and.intro h3 h2)
  ( assume h4 : Q ∧ P,
    have h5 : Q := h4.1,
    have h6 : P := h4.2,
    show P ∧ Q,
      from and.intro h6 h5)

-- 4ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q,
    show Q ∧ P,
      from and.intro h1.2 h1.1)
  ( assume h4 : Q ∧ P,
    show P ∧ Q,
      from and.intro h4.2 h4.1)

-- 5ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q, and.intro h1.2 h1.1)
  ( assume h4 : Q ∧ P, and.intro h4.2 h4.1)

-- 6ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  ( assume h1 : P ∧ Q, ⟨h1.2, h1.1⟩)
  ( assume h4 : Q ∧ P, ⟨h4.2, h4.1⟩)

-- 7ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  (λ h, ⟨h.2, h.1⟩)
  (λ h, ⟨h.2, h.1⟩)

-- 8ª demostración
example : P ∧ Q ↔ Q ∧ P :=
iff.intro
  (λ ⟨hP, hQ⟩, ⟨hQ, hP⟩)
  (λ ⟨hQ, hP⟩, ⟨hP, hQ⟩)

-- 9ª demostración
lemma aux :
  P ∧ Q → Q ∧ P :=
λ h, ⟨h.2, h.1⟩

example : P ∧ Q ↔ Q ∧ P :=
iff.intro (aux P Q) (aux Q P)

-- 10ª demostración
example : P ∧ Q ↔ Q ∧ P :=
-- by library_search
and.comm

-- 11ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  split,
  { intro h1,
    cases h1 with h2 h3,
    split,
    { exact h3, },
    { exact h2, }},
  { intro h4,
    cases h4 with h5 h6,
    split,
    { exact h6, },
    { exact h5, }},
end

-- 12ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  split,
  { rintro ⟨h2, h3⟩,
    split,
    { exact h3, },
    { exact h2, }},
  { rintro ⟨h5, h6⟩,
    split,
    { exact h6, },
    { exact h5, }},
end

-- 13ª demostración
example : P ∧ Q ↔ Q ∧ P :=
begin
  constructor,
  { rintro ⟨h2, h3⟩,
    constructor,
    { exact h3, },
    { exact h2, }},
  { rintro ⟨h5, h6⟩,
    constructor,
    { exact h6, },
    { exact h5, }},
end

-- 14ª demostración
example : P ∧ Q ↔ Q ∧ P :=
-- by hint
by tauto

-- 15ª demostración
example : P ∧ Q ↔ Q ∧ P :=
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. 17) Demostrar

-- P ∧ Q ↔ Q ∧ P

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

import tactic

variables (P Q : Prop)

-- 1ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q,

have h2 : P,

from and.elim_left h1,

have h3 : Q,

from and.elim_right h1,

show Q ∧ P,

from and.intro h3 h2)

( assume h4 : Q ∧ P,

have h5 : Q,

from and.elim_left h4,

have h6 : P,

from and.elim_right h4,

show P ∧ Q,

from and.intro h6 h5)

-- 2ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q,

have h2 : P,

from h1.1,

have h3 : Q,

from h1.2,

show Q ∧ P,

from and.intro h3 h2)

( assume h4 : Q ∧ P,

have h5 : Q,

from h4.1,

have h6 : P,

from h4.2,

show P ∧ Q,

from and.intro h6 h5)

-- 3ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q,

have h2 : P := h1.1,

have h3 : Q := h1.2,

show Q ∧ P,

from and.intro h3 h2)

( assume h4 : Q ∧ P,

have h5 : Q := h4.1,

have h6 : P := h4.2,

show P ∧ Q,

from and.intro h6 h5)

-- 4ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q,

show Q ∧ P,

from and.intro h1.2 h1.1)

( assume h4 : Q ∧ P,

show P ∧ Q,

from and.intro h4.2 h4.1)

-- 5ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q, and.intro h1.2 h1.1)

( assume h4 : Q ∧ P, and.intro h4.2 h4.1)

-- 6ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

( assume h1 : P ∧ Q, ⟨h1.2, h1.1⟩)

( assume h4 : Q ∧ P, ⟨h4.2, h4.1⟩)

-- 7ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

(λ h, ⟨h.2, h.1⟩)

-- 8ª demostración

example : P ∧ Q ↔ Q ∧ P :=

iff.intro

(λ ⟨hP, hQ⟩, ⟨hQ, hP⟩)

(λ ⟨hQ, hP⟩, ⟨hP, hQ⟩)

-- 9ª demostración

lemma aux :

P ∧ Q → Q ∧ P :=

λ h, ⟨h.2, h.1⟩

example : P ∧ Q ↔ Q ∧ P :=

iff.intro (aux P Q) (aux Q P)

-- 10ª demostración

example : P ∧ Q ↔ Q ∧ P :=

-- by library_search

and.comm

-- 11ª demostración

example : P ∧ Q ↔ Q ∧ P :=

begin

split,

{ intro h1,

cases h1 with h2 h3,

split,

{ exact h3, },

{ exact h2, }},

{ intro h4,

cases h4 with h5 h6,

split,

{ exact h6, },

{ exact h5, }},

end

-- 12ª demostración

example : P ∧ Q ↔ Q ∧ P :=

begin

split,

{ rintro ⟨h2, h3⟩,

split,

{ exact h3, },

{ exact h2, }},

{ rintro ⟨h5, h6⟩,

split,

{ exact h6, },

{ exact h5, }},

end

-- 13ª demostración

example : P ∧ Q ↔ Q ∧ P :=

begin

constructor,

{ rintro ⟨h2, h3⟩,

constructor,

{ exact h3, },

{ exact h2, }},

{ rintro ⟨h5, h6⟩,

constructor,

{ exact h6, },

{ exact h5, }},

end

-- 14ª demostración

example : P ∧ Q ↔ Q ∧ P :=

-- by hint

by tauto

-- 15ª demostración

example : P ∧ Q ↔ Q ∧ P :=

by finish

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

PorJosé A. Alonso 22 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

¬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

-- Prueba de ¬P ∨ Q ⊢ P → Q
-- ========================

-- ----------------------------------------------------
-- Ej. 1. (p. 15) Demostrar
--    ¬P ∨ Q ⊢ P → Q
-- ----------------------------------------------------

import tactic

variables (P Q : Prop)

-- 1ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( assume h5 : Q,
    show Q, from h5)

-- 2ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( assume h5 : Q, h5)

-- 3ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  ( λ h5, h5)

-- 4ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    have h4 : false,
      from h3 h2,
    show Q,
      from false.elim h4)
  id

-- 5ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P,
    show Q,
      from false.elim (h3 h2))
  id

-- 6ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( assume h3 : ¬P, false.elim (h3 h2))
  id

-- 7ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
assume h2 : P,
or.elim h1
  ( λ h3, false.elim (h3 h2))
  id

-- 8ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, or.elim h1 (λ h3, false.elim (h3 h2)) id

example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, h1.elim (λ h3, false.elim (h3 h2)) id

example
  (h1 : ¬P ∨ Q)
  : P → Q :=
λ h2, h1.elim (λ h3, (h3 h2).elim) id

-- 9ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
-- by library_search
imp_iff_not_or.mpr h1

-- 10ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { apply false.rec,
    exact h3 h2, },
  { exact h4, },
end

-- 11ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { exact false.elim (h3 h2), },
  { exact h4, },
end

-- 12ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
begin
  intro h2,
  cases h1 with h3 h4,
  { exfalso,
    exact h3 h2, },
  { exact h4, },
end

-- 13ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
-- by hint
by tauto

-- 14ª demostración
example
  (h1 : ¬P ∨ Q)
  : P → Q :=
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

-- Prueba de ¬P ∨ Q ⊢ P → Q

-- ========================

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

-- Ej. 1. (p. 15) Demostrar

-- ¬P ∨ Q ⊢ P → Q

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

import tactic

variables (P Q : Prop)

-- 1ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P,

have h4 : false,

from h3 h2,

show Q,

from false.elim h4)

( assume h5 : Q,

show Q, from h5)

-- 2ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P,

have h4 : false,

from h3 h2,

show Q,

from false.elim h4)

( assume h5 : Q, h5)

-- 3ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P,

have h4 : false,

from h3 h2,

show Q,

from false.elim h4)

( λ h5, h5)

-- 4ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P,

have h4 : false,

from h3 h2,

show Q,

from false.elim h4)

-- 5ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P,

show Q,

from false.elim (h3 h2))

-- 6ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( assume h3 : ¬P, false.elim (h3 h2))

-- 7ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

assume h2 : P,

or.elim h1

( λ h3, false.elim (h3 h2))

-- 8ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

λ h2, or.elim h1 (λ h3, false.elim (h3 h2)) id

example

(h1 : ¬P ∨ Q)

: P → Q :=

λ h2, h1.elim (λ h3, false.elim (h3 h2)) id

example

(h1 : ¬P ∨ Q)

: P → Q :=

λ h2, h1.elim (λ h3, (h3 h2).elim) id

-- 9ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

-- by library_search

imp_iff_not_or.mpr h1

-- 10ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

begin

intro h2,

cases h1 with h3 h4,

{ apply false.rec,

exact h3 h2, },

{ exact h4, },

end

-- 11ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

begin

intro h2,

cases h1 with h3 h4,

{ exact false.elim (h3 h2), },

{ exact h4, },

end

-- 12ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

begin

intro h2,

cases h1 with h3 h4,

{ exfalso,

exact h3 h2, },

{ exact h4, },

end

-- 13ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

-- by hint

by tauto

-- 14ª demostración

example

(h1 : ¬P ∨ Q)

: P → Q :=

by finish