Menu Close

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

José A. Alonso--

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