5 octubre 2020 – Vestigium

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