octubre 2020 – Página 6

ForMatUS: Pruebas en Lean de la transitividad de la igualdad

PorJosé A. Alonso 18 octubre 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 la transitividad de la igualdad 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  (U : Type)
variables (x y z : U)

-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--    x = y, y = z ⊢ x = z
-- ----------------------------------------------------

-- 1ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
eq.subst h2 h1

-- 2ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
h2 ▸ h1

-- 3ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
eq.substr h1 h2

-- 4ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
eq.trans h1 h2

-- 5ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
begin
  rw h1,
  exact h2,
end

-- 6ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
begin
  rw h1,
  assumption,
end

-- 7ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
begin
  rwa h1,
end

-- 8ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
by rwa h1

-- 9ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
begin
  rwa ←h2,
end

-- 10ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
begin
  rwa h2 at h1,
end

-- 11ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
by simp *

-- 12ª demostración
example
  (h1 : x = y)
  (h2 : y = z)
  : x = z :=
-- by hint
by finish

100

101

102

103

104

105

106

import tactic

variable (U : Type)

variables (x y z : U)

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

-- Ej. 1. Demostrar que

-- x = y, y = z ⊢ x = z

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

-- 1ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

eq.subst h2 h1

-- 2ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

h2 ▸ h1

-- 3ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

eq.substr h1 h2

-- 4ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

eq.trans h1 h2

-- 5ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

begin

rw h1,

exact h2,

end

-- 6ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

begin

rw h1,

assumption,

end

-- 7ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

begin

rwa h1,

end

-- 8ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

by rwa h1

-- 9ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

begin

rwa ←h2,

end

-- 10ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

begin

rwa h2 at h1,

end

-- 11ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

by simp *

-- 12ª demostración

example

(h1 : x = y)

(h2 : y = z)

: x = z :=

-- by hint

by finish

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

PorJosé A. Alonso 16 octubre 202020 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 5 pruebas en Lean de un ejemplo que ilustra la regla de eliminación de la igualdad.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

-- #check @eq.subst

-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--      x + 1 = 1 + x
--      x + 1 &gt; 1 → x + 1 &gt; 0
--      ⊢ 1 + x &gt; 1 → 1 + x &gt; 0
-- ----------------------------------------------------

variable (U : Type)
variable (x : U)
variable [has_add U]
variable [has_one U]
variable [has_lt U]
variable [has_zero U]

-- 1ª demostración
example
  (h1 : x + 1 = 1 + x)
  (h2 : x + 1 &gt; 1 → x + 1 &gt; 0)
  : 1 + x &gt; 1 → 1 + x &gt; 0 :=
eq.subst h1 h2


-- 2ª demostración
example
  (h1 : x + 1 = 1 + x)
  (h2 : x + 1 &gt; 1 → x + 1 &gt; 0)
  : 1 + x &gt; 1 → 1 + x &gt; 0 :=
h1 ▸ h2

-- 3ª demostración
example
  (h1 : x + 1 = 1 + x)
  (h2 : x + 1 &gt; 1 → x + 1 &gt; 0)
  : 1 + x &gt; 1 → 1 + x &gt; 0 :=
begin
  rw h1 at h2,
  exact h2,
end

-- 4ª demostración
example
  (h1 : x + 1 = 1 + x)
  (h2 : x + 1 &gt; 1 → x + 1 &gt; 0)
  : 1 + x &gt; 1 → 1 + x &gt; 0 :=
begin
  rw ←h1,
  exact h2,
end

-- 5ª demostración
example
  (h1 : x + 1 = 1 + x)
  (h2 : x + 1 &gt; 1 → x + 1 &gt; 0)
  : 1 + x &gt; 1 → 1 + x &gt; 0 :=
-- by hint
by finish

import tactic

-- #check @eq.subst

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

-- Ej. 1. Demostrar que

-- x + 1 = 1 + x

-- x + 1 > 1 → x + 1 > 0

-- ⊢ 1 + x > 1 → 1 + x > 0

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

variable (U : Type)

variable (x : U)

variable [has_add U]

variable [has_one U]

variable [has_lt U]

variable [has_zero U]

-- 1ª demostración

example

(h1 : x + 1 = 1 + x)

(h2 : x + 1 > 1 → x + 1 > 0)

: 1 + x > 1 → 1 + x > 0 :=

eq.subst h1 h2

-- 2ª demostración

example

(h1 : x + 1 = 1 + x)

(h2 : x + 1 > 1 → x + 1 > 0)

: 1 + x > 1 → 1 + x > 0 :=

h1 ▸ h2

-- 3ª demostración

example

(h1 : x + 1 = 1 + x)

(h2 : x + 1 > 1 → x + 1 > 0)

: 1 + x > 1 → 1 + x > 0 :=

begin

rw h1 at h2,

exact h2,

end

-- 4ª demostración

example

(h1 : x + 1 = 1 + x)

(h2 : x + 1 > 1 → x + 1 > 0)

: 1 + x > 1 → 1 + x > 0 :=

begin

rw ←h1,

exact h2,

end

-- 5ª demostración

example

(h1 : x + 1 = 1 + x)

(h2 : x + 1 > 1 → x + 1 > 0)

: 1 + x > 1 → 1 + x > 0 :=

-- by hint

by finish

ForMatUS: Pruebas en Lean de ∃x∃y P(x,y) ↔ ∃y∃x P(x,y)

PorJosé A. Alonso 8 octubre 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 la propiedad

∃x∃y P(x,y) ↔ ∃y∃x P(x,y)

1	∃x∃y P(x,y) ↔ ∃y∃x P(x,y)

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

section

variable {U : Type}
variable {P : U -&gt; U -&gt; Prop}

-- ------------------------------------------------------
-- Ej. 1. Demostrar que
--    ∃x∃yP(x,y) → ∃y∃xP(x,y)
-- ------------------------------------------------------

-- 1ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
assume h1 : ∃ x, ∃ y, P x y,
exists.elim h1
  ( assume x₀ (h2 : ∃ y, P x₀ y),
    exists.elim h2
      ( assume y₀ (h3 : P x₀ y₀),
        have h4 : ∃ x, P x y₀, from exists.intro x₀ h3,
        show ∃ y, ∃ x, P x y,  from exists.intro y₀ h4))

-- 2ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,
have h2 : ∃ x, P x y₀, from ⟨x₀, h1⟩,
show (∃ y, ∃ x, P x y), from ⟨y₀, h2⟩

-- 3ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,
show (∃ y, ∃ x, P x y), from ⟨y₀, ⟨x₀, h1⟩⟩

-- 4ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,
show (∃ y, ∃ x, P x y), from ⟨y₀, x₀, h1⟩

-- 5ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,
⟨y₀, x₀, h1⟩

-- 6ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
λ ⟨x₀, y₀, h1⟩, ⟨y₀, x₀, h1⟩

-- 7ª demostración
example :
  (∃ x y, P x y) → (∃ y x, P x y) :=
-- by library_search
exists_comm.mp

-- 8ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
begin
  intro h1,
  cases h1 with x₀ h2,
  cases h2 with y₀ h3,
  use y₀,
  use x₀,
  exact h3,
end

-- 9ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
begin
  intro h1,
  cases h1 with x₀ h2,
  cases h2 with y₀ h3,
  use [y₀, x₀],
  exact h3,
end

-- 10ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
begin
  intro h1,
  rcases h1 with ⟨x₀, y₀, h2⟩,
  use [y₀, x₀],
  exact h2,
end

-- 11ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
begin
  intro h1,
  rcases h1 with ⟨x₀, y₀, h2⟩,
  exact ⟨y₀, x₀, h2⟩,
end

-- 12ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
begin
  rintro ⟨x₀, y₀, h2⟩,
  exact ⟨y₀, x₀, h2⟩,
end

-- 13ª demostración
example :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
-- by hint
by tauto

-- 14ª demostración
lemma aux :
  (∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=
by finish

-- ------------------------------------------------------
-- Ej. 2. Demostrar que
--    ∃x∃yP(x,y) ↔ ∃y∃xP(x,y)
-- ------------------------------------------------------

-- 1ª demostración
example :
  (∃ x y, P x y) ↔ (∃ y x, P x y) :=
iff.intro aux aux

-- 2ª demostración
example :
  (∃ x y, P x y) ↔ (∃ y x, P x y) :=
⟨aux, aux⟩

-- 3ª demostración
example :
  (∃ x y, P x y) ↔ (∃ y x, P x y) :=
-- by library_search
exists_comm

-- 4ª demostración
example :
  (∃ x y, P x y) ↔ (∃ y x, P x y) :=
-- by hint
by tauto

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

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

import tactic

section

variable {U : Type}

variable {P : U -> U -> Prop}

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

-- Ej. 1. Demostrar que

-- ∃x∃yP(x,y) → ∃y∃xP(x,y)

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

-- 1ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

assume h1 : ∃ x, ∃ y, P x y,

exists.elim h1

( assume x₀ (h2 : ∃ y, P x₀ y),

exists.elim h2

( assume y₀ (h3 : P x₀ y₀),

have h4 : ∃ x, P x y₀, from exists.intro x₀ h3,

show ∃ y, ∃ x, P x y, from exists.intro y₀ h4))

-- 2ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,

have h2 : ∃ x, P x y₀, from ⟨x₀, h1⟩,

show (∃ y, ∃ x, P x y), from ⟨y₀, h2⟩

-- 3ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,

show (∃ y, ∃ x, P x y), from ⟨y₀, ⟨x₀, h1⟩⟩

-- 4ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,

show (∃ y, ∃ x, P x y), from ⟨y₀, x₀, h1⟩

-- 5ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

assume ⟨x₀, y₀, (h1 : P x₀ y₀)⟩,

⟨y₀, x₀, h1⟩

-- 6ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

λ ⟨x₀, y₀, h1⟩, ⟨y₀, x₀, h1⟩

-- 7ª demostración

example :

(∃ x y, P x y) → (∃ y x, P x y) :=

-- by library_search

exists_comm.mp

-- 8ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

begin

intro h1,

cases h1 with x₀ h2,

cases h2 with y₀ h3,

use y₀,

use x₀,

exact h3,

end

-- 9ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

begin

intro h1,

cases h1 with x₀ h2,

cases h2 with y₀ h3,

use [y₀, x₀],

exact h3,

end

-- 10ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

begin

intro h1,

rcases h1 with ⟨x₀, y₀, h2⟩,

use [y₀, x₀],

exact h2,

end

-- 11ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

begin

intro h1,

rcases h1 with ⟨x₀, y₀, h2⟩,

exact ⟨y₀, x₀, h2⟩,

end

-- 12ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

begin

rintro ⟨x₀, y₀, h2⟩,

exact ⟨y₀, x₀, h2⟩,

end

-- 13ª demostración

example :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

-- by hint

by tauto

-- 14ª demostración

lemma aux :

(∃ x, ∃ y, P x y) → (∃ y, ∃ x, P x y) :=

by finish

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

-- Ej. 2. Demostrar que

-- ∃x∃yP(x,y) ↔ ∃y∃xP(x,y)

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

-- 1ª demostración

example :

(∃ x y, P x y) ↔ (∃ y x, P x y) :=

iff.intro aux aux

-- 2ª demostración

example :

(∃ x y, P x y) ↔ (∃ y x, P x y) :=

⟨aux, aux⟩

-- 3ª demostración

example :

(∃ x y, P x y) ↔ (∃ y x, P x y) :=

-- by library_search

exists_comm

-- 4ª demostración

example :

(∃ x y, P x y) ↔ (∃ y x, P x y) :=

-- by hint

by tauto

end

ForMatUS: Pruebas en Lean de ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)

PorJosé A. Alonso 5 octubre 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 la propiedad distributiva del existencial sobre la disyunción

∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)

1	∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)

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

section

variable  {U : Type}
variables {P Q : U -&gt; Prop}

-- -----------------------------------------------------
-- Ej. 1. Demostrar
--    ∃x (P(x) ∨ Q(x)) ⊢ ∃x P(x) ∨ ∃x Q(x)
-- -----------------------------------------------------

-- 1ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  ( assume x₀ (h2 : P x₀ ∨ Q x₀),
    or.elim h2
    ( assume h3 : P x₀,
      have h4 : ∃x, P x,          from exists.intro x₀ h3,
      show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )
    ( assume h6 : Q x₀,
      have h7 : ∃x, Q x,          from exists.intro x₀ h6,
      show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))

-- 2ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  ( assume x₀ (h2 : P x₀ ∨ Q x₀),
    or.elim h2
    ( assume h3 : P x₀,
      have h4 : ∃x, P x,          from ⟨x₀, h3⟩,
      show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )
    ( assume h6 : Q x₀,
      have h7 : ∃x, Q x,          from ⟨x₀, h6⟩,
      show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))

-- 3ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  ( assume x₀ (h2 : P x₀ ∨ Q x₀),
    or.elim h2
    ( assume h3 : P x₀,
      have h4 : ∃x, P x,          from ⟨x₀, h3⟩,
      or.inl h4 )
    ( assume h6 : Q x₀,
      have h7 : ∃x, Q x,          from ⟨x₀, h6⟩,
      or.inr h7 ))

-- 4ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  ( assume x₀ (h2 : P x₀ ∨ Q x₀),
    or.elim h2
    ( assume h3 : P x₀,
      or.inl ⟨x₀, h3⟩ )
    ( assume h6 : Q x₀,
      or.inr ⟨x₀, h6⟩ ))

-- 5ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  ( assume x₀ (h2 : P x₀ ∨ Q x₀),
    or.elim h2
    ( λ h3, or.inl ⟨x₀, h3⟩ )
    ( λ h6, or.inr ⟨x₀, h6⟩ ))

-- 6ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
exists.elim h1
  (λ x₀ h2, h2.elim (λ h3, or.inl ⟨x₀, h3⟩)
                    (λ h6, or.inr ⟨x₀, h6⟩))

-- 7ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
-- by library_search
exists_or_distrib.mp h1

-- 8ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
match h1 with ⟨x₀, (h2 : P x₀ ∨ Q x₀)⟩ :=
  ( or.elim h2
    ( assume h3 : P x₀,
      have h4 : ∃x, P x,          from exists.intro x₀ h3,
      show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )
    ( assume h6 : Q x₀,
      have h7 : ∃x, Q x,          from exists.intro x₀ h6,
      show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))
end

-- 9ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
begin
  cases h1 with x₀ h3,
  cases h3 with hp hq,
  { left,
    use x₀,
    exact hp, },
  { right,
    use x₀,
    exact hq, },
end

-- 10ª demostración
example
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
begin
  rcases h1 with ⟨x₀, hp | hq⟩,
  { left,
    use x₀,
    exact hp, },
  { right,
    use x₀,
    exact hq, },
end

-- 11ª demostración
lemma aux1
  (h1 : ∃x, P x  ∨ Q x)
  : (∃x, P x) ∨ (∃x, Q x) :=
-- by hint
by finish

-- -----------------------------------------------------
-- Ej. 2. Demostrar
--    ∃x P(x) ∨ ∃x Q(x) ⊢ ∃x (P(x) ∨ Q(x))
-- -----------------------------------------------------

-- 1ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
or.elim h1
  ( assume h2 : ∃x, P x,
    exists.elim h2
      ( assume x₀ (h3 : P x₀),
        have h4 : P x₀ ∨ Q x₀, from or.inl h3,
        show ∃x, P x  ∨ Q x,   from exists.intro x₀ h4 ))
  ( assume h2 : ∃x, Q x,
    exists.elim h2
      ( assume x₀ (h3 : Q x₀),
        have h4 : P x₀ ∨ Q x₀, from or.inr h3,
        show ∃x, P x  ∨ Q x,   from exists.intro x₀ h4 ))

-- 2ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
h1.elim
  ( assume ⟨x₀, (h3 : P x₀)⟩,
    have h4 : P x₀ ∨ Q x₀, from or.inl h3,
    show ∃x, P x  ∨ Q x,   from ⟨x₀, h4⟩ )
  ( assume ⟨x₀, (h3 : Q x₀)⟩,
    have h4 : P x₀ ∨ Q x₀, from or.inr h3,
    show ∃x, P x  ∨ Q x,   from ⟨x₀, h4⟩ )

-- 3ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
h1.elim
  ( assume ⟨x₀, (h3 : P x₀)⟩,
    have h4 : P x₀ ∨ Q x₀, from or.inl h3,
    ⟨x₀, h4⟩ )
  ( assume ⟨x₀, (h3 : Q x₀)⟩,
    have h4 : P x₀ ∨ Q x₀, from or.inr h3,
    ⟨x₀, h4⟩ )

-- 4ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
h1.elim
  ( assume ⟨x₀, (h3 : P x₀)⟩,
    ⟨x₀, or.inl h3⟩ )
  ( assume ⟨x₀, (h3 : Q x₀)⟩,
    ⟨x₀, or.inr h3⟩ )

-- 5ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
h1.elim
  (λ ⟨x₀, h3⟩, ⟨x₀, or.inl h3⟩)
  (λ ⟨x₀, h3⟩, ⟨x₀, or.inr h3⟩)

-- 6ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
-- by library_search
exists_or_distrib.mpr h1

-- 7ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
begin
  cases h1 with hp hq,
  { cases hp with x₀ hx₀,
    use x₀,
    left,
    exact hx₀, },
  { cases hq with x₁ hx₁,
    use x₁,
    right,
    exact hx₁, },
end

-- 8ª demostración
example
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
begin
  rcases h1 with ⟨x₀, hx₀⟩ | ⟨x₁, hx₁⟩,
  { use x₀,
    left,
    exact hx₀, },
  { use x₁,
    right,
    exact hx₁, },
end

-- 9ª demostración
lemma aux2
  (h1 : (∃x, P x) ∨ (∃x, Q x))
  : ∃x, P x  ∨ Q x :=
-- by hint
by finish

-- -----------------------------------------------------
-- Ej. 3. Demostrar
--    ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)
-- -----------------------------------------------------

-- 1ª demostración
example :
  (∃x, P x  ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=
iff.intro aux1 aux2

-- 2ª demostración
example :
  (∃x, P x  ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=
⟨aux1, aux2⟩

-- 3ª demostración
example :
  (∃x, P x  ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=
-- by library_search
exists_or_distrib

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

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

import tactic

section

variable {U : Type}

variables {P Q : U -> Prop}

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

-- Ej. 1. Demostrar

-- ∃x (P(x) ∨ Q(x)) ⊢ ∃x P(x) ∨ ∃x Q(x)

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

-- 1ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

( assume x₀ (h2 : P x₀ ∨ Q x₀),

or.elim h2

( assume h3 : P x₀,

have h4 : ∃x, P x, from exists.intro x₀ h3,

show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )

( assume h6 : Q x₀,

have h7 : ∃x, Q x, from exists.intro x₀ h6,

show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))

-- 2ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

( assume x₀ (h2 : P x₀ ∨ Q x₀),

or.elim h2

( assume h3 : P x₀,

have h4 : ∃x, P x, from ⟨x₀, h3⟩,

show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )

( assume h6 : Q x₀,

have h7 : ∃x, Q x, from ⟨x₀, h6⟩,

show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))

-- 3ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

( assume x₀ (h2 : P x₀ ∨ Q x₀),

or.elim h2

( assume h3 : P x₀,

have h4 : ∃x, P x, from ⟨x₀, h3⟩,

or.inl h4 )

( assume h6 : Q x₀,

have h7 : ∃x, Q x, from ⟨x₀, h6⟩,

or.inr h7 ))

-- 4ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

( assume x₀ (h2 : P x₀ ∨ Q x₀),

or.elim h2

( assume h3 : P x₀,

or.inl ⟨x₀, h3⟩ )

( assume h6 : Q x₀,

or.inr ⟨x₀, h6⟩ ))

-- 5ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

( assume x₀ (h2 : P x₀ ∨ Q x₀),

or.elim h2

( λ h3, or.inl ⟨x₀, h3⟩ )

( λ h6, or.inr ⟨x₀, h6⟩ ))

-- 6ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

exists.elim h1

(λ x₀ h2, h2.elim (λ h3, or.inl ⟨x₀, h3⟩)

(λ h6, or.inr ⟨x₀, h6⟩))

-- 7ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

-- by library_search

exists_or_distrib.mp h1

-- 8ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

match h1 with ⟨x₀, (h2 : P x₀ ∨ Q x₀)⟩ :=

( or.elim h2

( assume h3 : P x₀,

have h4 : ∃x, P x, from exists.intro x₀ h3,

show (∃x, P x) ∨ (∃x, Q x), from or.inl h4 )

( assume h6 : Q x₀,

have h7 : ∃x, Q x, from exists.intro x₀ h6,

show (∃x, P x) ∨ (∃x, Q x), from or.inr h7 ))

end

-- 9ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

begin

cases h1 with x₀ h3,

cases h3 with hp hq,

{ left,

use x₀,

exact hp, },

{ right,

use x₀,

exact hq, },

end

-- 10ª demostración

example

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

begin

rcases h1 with ⟨x₀, hp | hq⟩,

{ left,

use x₀,

exact hp, },

{ right,

use x₀,

exact hq, },

end

-- 11ª demostración

lemma aux1

(h1 : ∃x, P x ∨ Q x)

: (∃x, P x) ∨ (∃x, Q x) :=

-- by hint

by finish

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

-- Ej. 2. Demostrar

-- ∃x P(x) ∨ ∃x Q(x) ⊢ ∃x (P(x) ∨ Q(x))

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

-- 1ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

or.elim h1

( assume h2 : ∃x, P x,

exists.elim h2

( assume x₀ (h3 : P x₀),

have h4 : P x₀ ∨ Q x₀, from or.inl h3,

show ∃x, P x ∨ Q x, from exists.intro x₀ h4 ))

( assume h2 : ∃x, Q x,

exists.elim h2

( assume x₀ (h3 : Q x₀),

have h4 : P x₀ ∨ Q x₀, from or.inr h3,

show ∃x, P x ∨ Q x, from exists.intro x₀ h4 ))

-- 2ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

h1.elim

( assume ⟨x₀, (h3 : P x₀)⟩,

have h4 : P x₀ ∨ Q x₀, from or.inl h3,

show ∃x, P x ∨ Q x, from ⟨x₀, h4⟩ )

( assume ⟨x₀, (h3 : Q x₀)⟩,

have h4 : P x₀ ∨ Q x₀, from or.inr h3,

show ∃x, P x ∨ Q x, from ⟨x₀, h4⟩ )

-- 3ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

h1.elim

( assume ⟨x₀, (h3 : P x₀)⟩,

have h4 : P x₀ ∨ Q x₀, from or.inl h3,

⟨x₀, h4⟩ )

( assume ⟨x₀, (h3 : Q x₀)⟩,

have h4 : P x₀ ∨ Q x₀, from or.inr h3,

⟨x₀, h4⟩ )

-- 4ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

h1.elim

( assume ⟨x₀, (h3 : P x₀)⟩,

⟨x₀, or.inl h3⟩ )

( assume ⟨x₀, (h3 : Q x₀)⟩,

⟨x₀, or.inr h3⟩ )

-- 5ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

h1.elim

(λ ⟨x₀, h3⟩, ⟨x₀, or.inl h3⟩)

(λ ⟨x₀, h3⟩, ⟨x₀, or.inr h3⟩)

-- 6ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

-- by library_search

exists_or_distrib.mpr h1

-- 7ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

begin

cases h1 with hp hq,

{ cases hp with x₀ hx₀,

use x₀,

left,

exact hx₀, },

{ cases hq with x₁ hx₁,

use x₁,

right,

exact hx₁, },

end

-- 8ª demostración

example

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

begin

rcases h1 with ⟨x₀, hx₀⟩ | ⟨x₁, hx₁⟩,

{ use x₀,

left,

exact hx₀, },

{ use x₁,

right,

exact hx₁, },

end

-- 9ª demostración

lemma aux2

(h1 : (∃x, P x) ∨ (∃x, Q x))

: ∃x, P x ∨ Q x :=

-- by hint

by finish

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

-- Ej. 3. Demostrar

-- ∃x (P(x) ∨ Q(x)) ↔ ∃x P(x) ∨ ∃x Q(x)

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

-- 1ª demostración

example :

(∃x, P x ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=

iff.intro aux1 aux2

-- 2ª demostración

example :

(∃x, P x ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=

⟨aux1, aux2⟩

-- 3ª demostración

example :

(∃x, P x ∨ Q x) ↔ (∃x, P x) ∨ (∃x, Q x) :=

-- by library_search

exists_or_distrib

end

ForMatUS: Pruebas en Lean de ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)

PorJosé A. Alonso 3 octubre 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 la propiedad

∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)

1	∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)

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

section

variable  {U : Type}
variables {P Q : U -&gt; Prop}

-- ------------------------------------------------------
-- Ej. 1. Demostrar
--    ∀x (P(x) ∧ Q(x)) ⊢ ∀x P(x) ∧ ∀x Q(x)
-- ------------------------------------------------------

-- 1ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    assume x₀,
    have h3 : P x₀ ∧ Q x₀,  from h1 x₀,
    show P x₀,              from and.elim_left h3,
have h9 : ∀x, Q x, from
    assume x₁,
    have h7 : P x₁ ∧ Q x₁,  from h1 x₁,
    show Q x₁,              from and.elim_right h7,
show (∀x, P x) ∧ (∀x, Q x), from and.intro h5 h9

-- 2ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    assume x₀,
    have h3 : P x₀ ∧ Q x₀,  from h1 x₀,
    show P x₀,              from h3.left,
have h9 : ∀x, Q x, from
    assume x₁,
    have h7 : P x₁ ∧ Q x₁,  from h1 x₁,
    show Q x₁,              from h7.right,
show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 3ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    assume x₀,
    have h3 : P x₀ ∧ Q x₀,  from h1 x₀,
    h3.left,
have h9 : ∀x, Q x, from
    assume x₁,
    have h7 : P x₁ ∧ Q x₁,  from h1 x₁,
    h7.right,
show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 4ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    assume x₀,
    (h1 x₀).left,
have h9 : ∀x, Q x, from
    assume x₁,
    (h1 x₁).right,
show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 5ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    λ x₀, (h1 x₀).left,
have h9 : ∀x, Q x, from
    λ x₁, (h1 x₁).right,
show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 6ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
have h5 : ∀x, P x, from
    λ x₀, (h1 x₀).left,
have h9 : ∀x, Q x, from
    λ x₁, (h1 x₁).right,
⟨h5, h9⟩

-- 7ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
⟨λ x₀, (h1 x₀).left, λ x₁, (h1 x₁).right⟩

-- 8ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
-- by library_search
forall_and_distrib.mp h1

-- 9ª demostración
example
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
begin
  split,
  { intro x₀,
    specialize h1 x₀,
    exact h1.left, },
  { intro x₁,
    specialize h1 x₁,
    exact h1.right, },
end

-- 9ª demostración
lemma aux1
  (h1 : ∀x, P x ∧ Q x)
  : (∀x, P x) ∧ (∀x, Q x) :=
-- by hint
by finish

-- ------------------------------------------------------
-- Ej. 2. Demostrar
--    ∀x P(x) ∧ ∀x Q(x) ⊢ ∀x (P(x) ∧ Q(x))
-- ------------------------------------------------------

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

-- 2ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
have h3 : ∀x, P x, from h1.left,
have h4 : P x₀,    from h3 x₀,
have h5 : ∀x, Q x, from h1.right,
have h6 : Q x₀,    from h5 x₀,
show P x₀ ∧ Q x₀,  from ⟨h4, h6⟩

-- 3ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
have h3 : ∀x, P x, from h1.left,
have h4 : P x₀,    from h3 x₀,
have h5 : ∀x, Q x, from h1.right,
have h6 : Q x₀,    from h5 x₀,
⟨h4, h6⟩

-- 4ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
have h3 : ∀x, P x, from h1.left,
have h4 : P x₀,    from h3 x₀,
have h5 : ∀x, Q x, from h1.right,
⟨h4, h5 x₀⟩

-- 5ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
have h3 : ∀x, P x, from h1.left,
have h4 : P x₀,    from h3 x₀,
⟨h4, h1.right x₀⟩

-- 6ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
have h3 : ∀x, P x, from h1.left,
⟨h3 x₀, h1.right x₀⟩

-- 7ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
assume x₀,
⟨h1.left x₀, h1.right x₀⟩

-- 8ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
λ x₀, ⟨h1.left x₀, h1.right x₀⟩

-- 9ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
-- by library_search
forall_and_distrib.mpr h1

-- 10ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
begin
  cases h1 with h2 h3,
  intro x₀,
  split,
  { apply h2, },
  { apply h3, },
end

-- 11ª demostración
example
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
-- by hint
by tauto

-- 12ª demostración
lemma aux2
  (h1 : (∀x, P x) ∧ (∀x, Q x))
  : ∀x, P x ∧ Q x :=
by finish

-- ------------------------------------------------------
-- Ej. 3. Demostrar
--    ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)
-- ------------------------------------------------------

-- 1ª demostración
example :
  (∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=
iff.intro aux1 aux2

-- 2ª demostración
example :
  (∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=
-- by library_search
forall_and_distrib

-- 3ª demostración
example :
  (∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=
-- by hint
by finish

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

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

import tactic

section

variable {U : Type}

variables {P Q : U -> Prop}

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

-- Ej. 1. Demostrar

-- ∀x (P(x) ∧ Q(x)) ⊢ ∀x P(x) ∧ ∀x Q(x)

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

-- 1ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

assume x₀,

have h3 : P x₀ ∧ Q x₀, from h1 x₀,

show P x₀, from and.elim_left h3,

have h9 : ∀x, Q x, from

assume x₁,

have h7 : P x₁ ∧ Q x₁, from h1 x₁,

show Q x₁, from and.elim_right h7,

show (∀x, P x) ∧ (∀x, Q x), from and.intro h5 h9

-- 2ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

assume x₀,

have h3 : P x₀ ∧ Q x₀, from h1 x₀,

show P x₀, from h3.left,

have h9 : ∀x, Q x, from

assume x₁,

have h7 : P x₁ ∧ Q x₁, from h1 x₁,

show Q x₁, from h7.right,

show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 3ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

assume x₀,

have h3 : P x₀ ∧ Q x₀, from h1 x₀,

h3.left,

have h9 : ∀x, Q x, from

assume x₁,

have h7 : P x₁ ∧ Q x₁, from h1 x₁,

h7.right,

show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 4ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

assume x₀,

(h1 x₀).left,

have h9 : ∀x, Q x, from

assume x₁,

(h1 x₁).right,

show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 5ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

λ x₀, (h1 x₀).left,

have h9 : ∀x, Q x, from

λ x₁, (h1 x₁).right,

show (∀x, P x) ∧ (∀x, Q x), from ⟨h5, h9⟩

-- 6ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

have h5 : ∀x, P x, from

λ x₀, (h1 x₀).left,

have h9 : ∀x, Q x, from

λ x₁, (h1 x₁).right,

⟨h5, h9⟩

-- 7ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

⟨λ x₀, (h1 x₀).left, λ x₁, (h1 x₁).right⟩

-- 8ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

-- by library_search

forall_and_distrib.mp h1

-- 9ª demostración

example

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

begin

split,

{ intro x₀,

specialize h1 x₀,

exact h1.left, },

{ intro x₁,

specialize h1 x₁,

exact h1.right, },

end

-- 9ª demostración

lemma aux1

(h1 : ∀x, P x ∧ Q x)

: (∀x, P x) ∧ (∀x, Q x) :=

-- by hint

by finish

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

-- Ej. 2. Demostrar

-- ∀x P(x) ∧ ∀x Q(x) ⊢ ∀x (P(x) ∧ Q(x))

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

-- 1ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from and.elim_left h1,

have h4 : P x₀, from h3 x₀,

have h5 : ∀x, Q x, from and.elim_right h1,

have h6 : Q x₀, from h5 x₀,

show P x₀ ∧ Q x₀, from and.intro h4 h6

-- 2ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from h1.left,

have h4 : P x₀, from h3 x₀,

have h5 : ∀x, Q x, from h1.right,

have h6 : Q x₀, from h5 x₀,

show P x₀ ∧ Q x₀, from ⟨h4, h6⟩

-- 3ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from h1.left,

have h4 : P x₀, from h3 x₀,

have h5 : ∀x, Q x, from h1.right,

have h6 : Q x₀, from h5 x₀,

⟨h4, h6⟩

-- 4ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from h1.left,

have h4 : P x₀, from h3 x₀,

have h5 : ∀x, Q x, from h1.right,

⟨h4, h5 x₀⟩

-- 5ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from h1.left,

have h4 : P x₀, from h3 x₀,

⟨h4, h1.right x₀⟩

-- 6ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

have h3 : ∀x, P x, from h1.left,

⟨h3 x₀, h1.right x₀⟩

-- 7ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

assume x₀,

⟨h1.left x₀, h1.right x₀⟩

-- 8ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

λ x₀, ⟨h1.left x₀, h1.right x₀⟩

-- 9ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

-- by library_search

forall_and_distrib.mpr h1

-- 10ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

begin

cases h1 with h2 h3,

intro x₀,

split,

{ apply h2, },

{ apply h3, },

end

-- 11ª demostración

example

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

-- by hint

by tauto

-- 12ª demostración

lemma aux2

(h1 : (∀x, P x) ∧ (∀x, Q x))

: ∀x, P x ∧ Q x :=

by finish

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

-- Ej. 3. Demostrar

-- ∀x (P(x) ∧ Q(x)) ↔ ∀x P(x) ∧ ∀x Q(x)

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

-- 1ª demostración

example :

(∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=

iff.intro aux1 aux2

-- 2ª demostración

example :

(∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=

-- by library_search

forall_and_distrib

-- 3ª demostración

example :

(∀x, P x ∧ Q x) ↔ (∀x, P x) ∧ (∀x, Q x) :=

-- by hint

by finish

end