Menu Close

Día: 3 noviembre, 2020

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

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

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

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