José A. Alonso

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

ForMatUS: Pruebas en Lean de P → (Q → P)

PorJosé A. Alonso 21 septiembre 202020 diciembre 2020

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

P → (Q → P)

1	P → (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

-- Pruebas de P → (Q → P)
-- ======================

-- ----------------------------------------------------
-- Ej. 1. (p. 13) Demostrar
--    P → (Q → P)
-- ----------------------------------------------------

import tactic

variables (P Q : Prop)

-- 1ª demostración
example : P → (Q → P) :=
assume (h1 : P),
show Q → P, from
  ( assume h2 : Q,
    show P, from h1)

-- 2ª demostración
example : P → (Q → P) :=
assume (h1 : P),
show Q → P, from
  ( assume h2 : Q, h1)

-- 3ª demostración
example : P → (Q → P) :=
assume (h1 : P),
show Q → P, from
  (λ h2, h1)

-- 4ª demostración
example : P → (Q → P) :=
assume (h1 : P), (λ h2, h1)

-- 5ª demostración
example : P → (Q → P) :=
λ h1, λ h2, h1

-- 6ª demostración
example : P → (Q → P) :=
λ h1 h2, h1

-- 7ª demostración
example : P → (Q → P) :=
λ h _, h

-- 8ª demostración
example : P → (Q → P) :=
-- by library_search
imp_intro

-- 9ª demostración
example : P → (Q → P) :=
begin
  intro h1,
  intro h2,
  exact h1,
end

-- 10ª demostración
example : P → (Q → P) :=
begin
  intros h1 h2,
  exact h1,
end

-- 11ª demostración
example : P → (Q → P) :=
λ h1 h2, h1

-- 12ª demostración
example : P → (Q → P) :=
-- by hint
by tauto

-- 13ª demostración
example : P → (Q → P) :=
by finish

-- Pruebas de P → (Q → P)

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

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

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

-- P → (Q → P)

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

import tactic

variables (P Q : Prop)

-- 1ª demostración

example : P → (Q → P) :=

assume (h1 : P),

show Q → P, from

( assume h2 : Q,

show P, from h1)

-- 2ª demostración

example : P → (Q → P) :=

assume (h1 : P),

show Q → P, from

( assume h2 : Q, h1)

-- 3ª demostración

example : P → (Q → P) :=

assume (h1 : P),

show Q → P, from

(λ h2, h1)

-- 4ª demostración

example : P → (Q → P) :=

assume (h1 : P), (λ h2, h1)

-- 5ª demostración

example : P → (Q → P) :=

λ h1, λ h2, h1

-- 6ª demostración

example : P → (Q → P) :=

λ h1 h2, h1

-- 7ª demostración

example : P → (Q → P) :=

λ h _, h

-- 8ª demostración

example : P → (Q → P) :=

-- by library_search

imp_intro

-- 9ª demostración

example : P → (Q → P) :=

begin

intro h1,

intro h2,

exact h1,

end

-- 10ª demostración

example : P → (Q → P) :=

begin

intros h1 h2,

exact h1,

end

-- 11ª demostración

example : P → (Q → P) :=

λ h1 h2, h1

-- 12ª demostración

example : P → (Q → P) :=

-- by hint

by tauto

-- 13ª demostración

example : P → (Q → P) :=

by finish

ForMatUS: Pruebas de Q → R ⊢ P ∨ Q → P ∨ R

PorJosé A. Alonso 20 septiembre 202020 diciembre 2020

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

Q → R ⊢ P ∨ Q → P ∨ R

1	Q → R ⊢ P ∨ Q → 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

-- Pruebas de Q → R ⊢ P ∨ Q → P ∨ R
-- ================================

-- ----------------------------------------------------
-- Ej. 1. (p. 12) Demostrar
--    Q → R ⊢ P ∨ Q → P ∨ R
-- ----------------------------------------------------

import tactic

variables (P Q R : Prop)

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

-- 2ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  ( assume h3 : P, or.inl h3 )
  ( assume h4 : Q,
    show P ∨ R,
      from or.inr (h1 h4) )

-- 3ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  ( assume h3 : P, or.inl h3 )
  ( assume h4 : Q, or.inr (h1 h4) )

-- 4ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  (λ h3, or.inl h3)
  (λ h4, or.inr (h1 h4))

-- 5ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  or.inl
  (λ h, or.inr (h1 h) )

-- 6ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, or.elim h2 or.inl (λ h, or.inr (h1 h))

-- 7ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, h2.elim or.inl (λ h, or.inr (h1 h))

-- 8ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, h2.elim or.inl (or.inr ∘ h1)

-- 9ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
-- by library_search
or.imp_right h1

-- 10ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
begin
  intro h2,
  cases h2 with h3 h4,
  { left,
    exact h3, },
  { right,
    exact (h1 h4), },
end

-- 11ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
begin
  rintro (h3 | h4),
  { left,
    exact h3, },
  { right,
    exact (h1 h4), },
end

-- 12ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
begin
  rintro (h3 | h4),
  { exact or.inl h3, },
  { exact or.inr (h1 h4), },
end

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

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

-- Pruebas de Q → R ⊢ P ∨ Q → P ∨ R

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

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

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

-- Q → R ⊢ P ∨ Q → P ∨ R

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

import tactic

variables (P Q R : Prop)

-- 1ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P,

show P ∨ R,

from or.inl h3 )

( assume h4 : Q,

have h5 : R := h1 h4,

show P ∨ R,

from or.inr h5 )

-- 2ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P, or.inl h3 )

( assume h4 : Q,

show P ∨ R,

from or.inr (h1 h4) )

-- 3ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P, or.inl h3 )

( assume h4 : Q, or.inr (h1 h4) )

-- 4ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

(λ h3, or.inl h3)

(λ h4, or.inr (h1 h4))

-- 5ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

or.inl

(λ h, or.inr (h1 h) )

-- 6ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, or.elim h2 or.inl (λ h, or.inr (h1 h))

-- 7ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, h2.elim or.inl (λ h, or.inr (h1 h))

-- 8ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, h2.elim or.inl (or.inr ∘ h1)

-- 9ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

-- by library_search

or.imp_right h1

-- 10ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

intro h2,

cases h2 with h3 h4,

{ left,

exact h3, },

{ right,

exact (h1 h4), },

end

-- 11ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

rintro (h3 | h4),

{ left,

exact h3, },

{ right,

exact (h1 h4), },

end

-- 12ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

rintro (h3 | h4),

{ exact or.inl h3, },

{ exact or.inr (h1 h4), },

end

-- 13ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

-- by hint

by tauto

-- 14ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

by finish

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

PorJosé A. Alonso 20 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 la propiedad conmutativa de la disyunción 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

-- Pruebas de P ∨ Q ⊢ Q ∨ P
-- ========================

import tactic

variables (P Q R : Prop)

-- ----------------------------------------------------
-- Ej. 1. (p. 11) Demostrar
--    P ∨ Q ⊢ Q ∨ P
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
or.elim h1
  ( assume h2 : P,
    show Q ∨ P,
      from or.inr h2 )
  ( assume h3 : Q,
    show Q ∨ P,
      from or.inl h3 )

-- 2ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
or.elim h1
  ( λ h, or.inr h )
  ( λ h, or.inl h )

-- 3ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
or.elim h1 or.inr or.inl

-- 4ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
h1.elim or.inr or.inl

-- 5ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
or.rec or.inr or.inl h1

-- 6ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
-- by library_search
or.swap h1

-- 7ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
begin
  cases h1 with h2 h3,
  { exact or.inr h2, },
  { exact or.inl h3, },
end

-- 7ª demostración
example
  (P ∨ Q)
  : Q ∨ P :=
begin
  cases ‹P ∨ Q›,
  { exact or.inr ‹P›, },
  { exact or.inl ‹Q›, },
end

-- 8ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
begin
  cases h1 with h2 h3,
  { right,
    exact h2, },
  { left,
    exact h3, },
end

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

-- 10ª demostración
example
  (h1 : P ∨ Q)
  : Q ∨ P :=
by finish

-- ----------------------------------------------------
-- Ej. 2 (p. 12). Demostrar
--    Q → R ⊢ P ∨ Q → P ∨ R
-- ----------------------------------------------------

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

-- 2ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  ( assume h3 : P, or.inl h3 )
  ( assume h4 : Q,
    show P ∨ R,
      from or.inr (h1 h4) )

-- 3ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  ( assume h3 : P, or.inl h3 )
  ( assume h4 : Q, or.inr (h1 h4) )

-- 4ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  ( λ h3, or.inl h3 )
  ( λ h4, or.inr (h1 h4) )

-- 5ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
assume h2 : P ∨ Q,
or.elim h2
  or.inl
  (λ h, or.inr (h1 h) )

-- 6ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, or.elim h2 or.inl (λ h, or.inr (h1 h))

-- 7ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, or.elim h2 or.inl (or.inr ∘ h1)

-- 8ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
λ h2, h2.elim or.inl (or.inr ∘ h1)

-- 9ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
-- by library_search
or.imp_right h1

-- 10ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
begin
  intro h2,
  cases h2 with h3 h4,
  { exact or.inl h3, },
  { exact or.inr (h1 h4), },
end

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

-- 12ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
begin
  rintro (h3 | h4),
  { left,
    exact h3, },
  { right,
    exact (h1 h4), },
end

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

-- 14ª demostración
example
  (h1 : Q → R)
  : P ∨ Q → P ∨ R :=
by finish

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

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

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

190

191

192

193

194

195

196

197

198

199

200

201

202

203

204

205

206

207

208

209

210

211

212

213

214

215

216

217

218

219

220

221

222

223

224

225

226

227

228

229

230

231

232

233

234

235

236

237

238

239

240

241

242

243

244

245

246

247

248

249

250

251

252

253

254

255

256

257

258

259

260

261

262

263

264

265

266

267

268

269

270

271

272

273

274

275

276

277

278

279

280

281

282

283

284

285

286

287

288

289

290

291

292

293

294

295

296

297

298

299

300

301

302

303

304

305

306

307

308

309

310

311

312

313

314

315

316

317

318

319

320

321

322

323

324

325

326

327

328

329

330

331

332

333

334

335

336

337

338

339

340

341

342

343

344

345

346

347

348

349

350

351

352

353

354

355

356

357

358

359

360

361

362

363

364

365

366

367

368

369

370

371

372

373

374

375

376

377

378

379

380

381

382

383

384

385

386

387

388

389

390

-- Pruebas de P ∨ Q ⊢ Q ∨ P

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

import tactic

variables (P Q R : Prop)

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

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

-- P ∨ Q ⊢ Q ∨ P

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

-- 1ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

or.elim h1

( assume h2 : P,

show Q ∨ P,

from or.inr h2 )

( assume h3 : Q,

show Q ∨ P,

from or.inl h3 )

-- 2ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

or.elim h1

( λ h, or.inr h )

( λ h, or.inl h )

-- 3ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

or.elim h1 or.inr or.inl

-- 4ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

h1.elim or.inr or.inl

-- 5ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

or.rec or.inr or.inl h1

-- 6ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

-- by library_search

or.swap h1

-- 7ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

begin

cases h1 with h2 h3,

{ exact or.inr h2, },

{ exact or.inl h3, },

end

-- 7ª demostración

example

(P ∨ Q)

: Q ∨ P :=

begin

cases ‹P ∨ Q›,

{ exact or.inr ‹P›, },

{ exact or.inl ‹Q›, },

end

-- 8ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

begin

cases h1 with h2 h3,

{ right,

exact h2, },

{ left,

exact h3, },

end

-- 9ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

-- by hint

by tauto

-- 10ª demostración

example

(h1 : P ∨ Q)

: Q ∨ P :=

by finish

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

-- Ej. 2 (p. 12). Demostrar

-- Q → R ⊢ P ∨ Q → P ∨ R

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

-- 1ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P,

show P ∨ R,

from or.inl h3 )

( assume h4 : Q,

have h5 : R := h1 h4,

show P ∨ R,

from or.inr h5 )

-- 2ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P, or.inl h3 )

( assume h4 : Q,

show P ∨ R,

from or.inr (h1 h4) )

-- 3ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( assume h3 : P, or.inl h3 )

( assume h4 : Q, or.inr (h1 h4) )

-- 4ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

( λ h3, or.inl h3 )

( λ h4, or.inr (h1 h4) )

-- 5ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

assume h2 : P ∨ Q,

or.elim h2

or.inl

(λ h, or.inr (h1 h) )

-- 6ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, or.elim h2 or.inl (λ h, or.inr (h1 h))

-- 7ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, or.elim h2 or.inl (or.inr ∘ h1)

-- 8ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

λ h2, h2.elim or.inl (or.inr ∘ h1)

-- 9ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

-- by library_search

or.imp_right h1

-- 10ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

intro h2,

cases h2 with h3 h4,

{ exact or.inl h3, },

{ exact or.inr (h1 h4), },

end

-- 11ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

intro h2,

cases h2 with h3 h4,

{ left,

exact h3, },

{ right,

exact (h1 h4), },

end

-- 12ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

begin

rintro (h3 | h4),

{ left,

exact h3, },

{ right,

exact (h1 h4), },

end

-- 13ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

-- by hint

by tauto

-- 14ª demostración

example

(h1 : Q → R)

: P ∨ Q → P ∨ R :=

by finish

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

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

-- ¬P ∨ Q ⊢ P → Q

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

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

ForMatUS: Regla de eliminación de la disyunción en Lean

PorJosé A. Alonso 20 septiembre 202020 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comenta la regla de eliminación de la disyunción en Lean usando ejemplos con distintos estilos de prueba: 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

variables (P Q R : Prop)

-- ----------------------------------------------------
-- Ej. 1. (p. 11) Demostrar
--    P ∨ Q, P → R, Q → R ⊢ R
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
or.elim h1 h2 h3

-- 2ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
h1.elim h2 h3

-- 3ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
-- by library_search
or.rec h2 h3 h1

-- 4ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
begin
  cases h1 with hP hQ,
  { exact h2 hP, },
  { exact h3 hQ, },
end

-- 5ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
-- by hint
by tauto

-- 6ª demostración
example
  (h1 : P ∨ Q)
  (h2 : P → R)
  (h3 : Q → R)
  : R :=
by finish

import tactic

variables (P Q R : Prop)

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

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

-- P ∨ Q, P → R, Q → R ⊢ R

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

-- 1ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

or.elim h1 h2 h3

-- 2ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

h1.elim h2 h3

-- 3ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

-- by library_search

or.rec h2 h3 h1

-- 4ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

begin

cases h1 with hP hQ,

{ exact h2 hP, },

{ exact h3 hQ, },

end

-- 5ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

-- by hint

by tauto

-- 6ª demostración

example

(h1 : P ∨ Q)

(h2 : P → R)

(h3 : Q → R)

: R :=

by finish