Vestigium

Resumen de lecturas compartidas durante diciembre de 2020

PorJosé A. Alonso 1 enero 202130 agosto 2021

Esta entrada es una recopilación de lecturas compartidas, durante diciembre de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante diciembre de 2020”

Resumen de lecturas compartidas durante noviembre de 2020

PorJosé A. Alonso 1 diciembre 202030 agosto 2021

Esta entrada es una recopilación de lecturas compartidas, durante noviembre de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante noviembre de 2020”

ForMatUS: Pruebas en Lean de propiedades de la composición de funciones (elemento neutro y asociatividad)

PorJosé A. Alonso 3 noviembre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de propiedades de la composición de funciones:

la función identidad es el elemento neutro de la composición y
la composición es asociativa.

En las pruebas se usan los estilos aplicativos y declarativos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import tactic

open function

variables {X Y Z W : Type}

-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--    id ∘ f = f
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  calc (id ∘ f) x = id (f x) : by rw comp_app
       ...        = f x      : by rw id.def,
end

-- 2ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  rw comp_app,
  rw id.def,
end

-- 3ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  rw [comp_app, id.def],
end

-- 4ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
begin
  ext,
  calc (id ∘ f) x = id (f x) : rfl
       ...        = f x      : rfl,
end

-- 5ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
rfl

-- 6ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
-- by library_search
left_id f

-- 7ª demostración
example
  (f : X → Y)
  : id ∘ f = f :=
comp.left_id f

-- ----------------------------------------------------
-- Ej. 2. Demostrar que
--    f ∘ id = f
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  calc (f ∘ id) x = f (id x) : by rw comp_app
       ...        = f x      : by rw id.def,
end

-- 2ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  rw comp_app,
  rw id.def,
end

-- 3ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  rw [comp_app, id.def],
end

-- 4ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
begin
  ext,
  calc (f ∘ id) x = f (id x) : rfl
       ...        = f x      : rfl,
end

-- 5ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
rfl

-- 6ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
-- by library_search
right_id f

-- 7ª demostración
example
  (f : X → Y)
  : f ∘ id = f :=
comp.right_id f

-- ----------------------------------------------------
-- Ej. 3. Demostrar que
--    (f ∘ g) ∘ h = f ∘ (g ∘ h)
-- ----------------------------------------------------

-- 1ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  calc ((f ∘ g) ∘ h) x
           = (f ∘ g) (h x)   : by rw comp_app
       ... = f (g (h x))     : by rw comp_app
       ... = f ((g ∘ h) x)   : by rw comp_app
       ... = (f ∘ (g ∘ h)) x : by rw comp_app
end

-- 2ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  rw comp_app,
end

-- 3ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
begin
  ext,
  calc ((f ∘ g) ∘ h) x
           = (f ∘ g) (h x)   : rfl
       ... = f (g (h x))     : rfl
       ... = f ((g ∘ h) x)   : rfl
       ... = (f ∘ (g ∘ h)) x : rfl
end

-- 4ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
rfl

-- 5ª demostración
example
  (f : Z → W)
  (g : Y → Z)
  (h : X → Y)
  : (f ∘ g) ∘ h = f ∘ (g ∘ h) :=
comp.assoc f g h

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

import tactic

open function

variables {X Y Z W : Type}

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

-- Ej. 1. Demostrar que

-- id ∘ f = f

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

-- 1ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

calc (id ∘ f) x = id (f x) : by rw comp_app

... = f x : by rw id.def,

end

-- 2ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

rw comp_app,

rw id.def,

end

-- 3ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

rw [comp_app, id.def],

end

-- 4ª demostración

example

(f : X → Y)

: id ∘ f = f :=

begin

ext,

calc (id ∘ f) x = id (f x) : rfl

... = f x : rfl,

end

-- 5ª demostración

example

(f : X → Y)

: id ∘ f = f :=

rfl

-- 6ª demostración

example

(f : X → Y)

: id ∘ f = f :=

-- by library_search

left_id f

-- 7ª demostración

example

(f : X → Y)

: id ∘ f = f :=

comp.left_id f

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

-- Ej. 2. Demostrar que

-- f ∘ id = f

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

-- 1ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

calc (f ∘ id) x = f (id x) : by rw comp_app

... = f x : by rw id.def,

end

-- 2ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

rw comp_app,

rw id.def,

end

-- 3ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

rw [comp_app, id.def],

end

-- 4ª demostración

example

(f : X → Y)

: f ∘ id = f :=

begin

ext,

calc (f ∘ id) x = f (id x) : rfl

... = f x : rfl,

end

-- 5ª demostración

example

(f : X → Y)

: f ∘ id = f :=

rfl

-- 6ª demostración

example

(f : X → Y)

: f ∘ id = f :=

-- by library_search

right_id f

-- 7ª demostración

example

(f : X → Y)

: f ∘ id = f :=

comp.right_id f

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

-- Ej. 3. Demostrar que

-- (f ∘ g) ∘ h = f ∘ (g ∘ h)

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

-- 1ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

calc ((f ∘ g) ∘ h) x

= (f ∘ g) (h x) : by rw comp_app

... = f (g (h x)) : by rw comp_app

... = f ((g ∘ h) x) : by rw comp_app

... = (f ∘ (g ∘ h)) x : by rw comp_app

end

-- 2ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

rw comp_app,

end

-- 3ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

begin

ext,

calc ((f ∘ g) ∘ h) x

= (f ∘ g) (h x) : rfl

... = f (g (h x)) : rfl

... = f ((g ∘ h) x) : rfl

... = (f ∘ (g ∘ h)) x : rfl

end

-- 4ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

rfl

-- 5ª demostración

example

(f : Z → W)

(g : Y → Z)

(h : X → Y)

: (f ∘ g) ∘ h = f ∘ (g ∘ h) :=

comp.assoc f g h

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

PorJosé A. Alonso 3 noviembre 202022 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que la identidad es biyectiva 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

open function

variables {X : Type}

-- #print injective
-- #print surjective
-- #print bijective

-- ----------------------------------------------------
-- Ej. 1. Demostrar que la identidad es inyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : injective (@id X) :=
begin
  intros x₁ x₂ h,
  exact h,
end

-- 2ª demostración
example : injective (@id X) :=
λ x₁ x₂ h, h

-- 3ª demostración
example : injective (@id X) :=
λ x₁ x₂, id

-- 4ª demostración
example : injective (@id X) :=
assume x₁ x₂,
assume h : id x₁ = id x₂,
show x₁ = x₂, from h

-- 5ª demostración
example : injective (@id X) :=
--by library_search
injective_id

-- 6ª demostración
example : injective (@id X) :=
-- by hint
by tauto

-- 7ª demostración
example : injective (@id X) :=
-- by hint
by finish

-- ----------------------------------------------------
-- Ej. 2. Demostrar que la identidad es suprayectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : surjective (@id X) :=
begin
  intro x,
  use x,
  exact rfl,
end

-- 2ª demostración
example : surjective (@id X) :=
begin
  intro x,
  exact ⟨x, rfl⟩,
end

-- 3ª demostración
example : surjective (@id X) :=
λ x, ⟨x, rfl⟩

-- 4ª demostración
example : surjective (@id X) :=
assume y,
show ∃ x, id x = y, from exists.intro y rfl

-- 5ª demostración
example : surjective (@id X) :=
-- by library_search
surjective_id

-- 6ª demostración
example : surjective (@id X) :=
-- by hint
by tauto

-- ----------------------------------------------------
-- Ej. 3. Demostrar que la identidad es biyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : bijective (@id X) :=
and.intro injective_id surjective_id

-- 2ª demostración
example : bijective (@id X) :=
⟨injective_id, surjective_id⟩

-- 3ª demostración
example : bijective (@id X) :=
-- by library_search
bijective_id

100

101

102

103

104

import tactic

open function

variables {X : Type}

-- #print injective

-- #print surjective

-- #print bijective

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

-- Ej. 1. Demostrar que la identidad es inyectiva.

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

-- 1ª demostración