Menu Close

Mes: noviembre 2020

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

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 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
Seguir leyendo →

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
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las relaciones reflexivas y euclídeas son de equivalencia

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 si una relación es reflexiva y euclídea, entonces es de equivalencia. Se usan los estilos declarativos, aplicativos y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Una relación binaria (≈) es euclídea si
--    ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c
--
-- El objetivo de esta teoría es demostrar que si una
-- relación es reflexiva y euclídea, entonces es de
-- equivalencia.
-- ----------------------------------------------------
 
import tactic
 
section
 
parameter {A : Type}
parameter (R : A → A → Prop)
 
local infix ≈ := R
 
parameter reflexivaR : reflexive (≈)
parameter euclideaR : ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c
 
include reflexivaR euclideaR
 
-- ----------------------------------------------------
-- Ej. 1. Demostrar que las relaciones reflexivas y
-- y euclídeas son simétricas.
-- ----------------------------------------------------
 
-- 1ª demostración
example : symmetric (≈) :=
begin
  intros a b h,
  exact euclideaR (reflexivaR b) h,
end
 
-- 2ª demostración
example : symmetric (≈) :=
λ a b h, euclideaR (reflexivaR b) h
 
-- 3ª demostración
lemma simetricaR : symmetric (≈) :=
assume a b (h1 : a ≈ b),
have h2 : b ≈ b, from (reflexivaR b),
show b ≈ a, from euclideaR h2 h1
 
-- ----------------------------------------------------
-- Ej. 2. Demostrar que las relaciones reflexivas y
-- y euclídeas son transitivas.
-- ----------------------------------------------------
 
-- 1ª demostración
example : transitive (≈) :=
begin
  rintros a b c h1 h2,
  apply euclideaR h1,
  exact euclideaR (reflexivaR c) h2,
end
 
-- 2ª demostración
lemma transitivaR : transitive (≈) :=
λ a b c h1 h2, (euclideaR h1) (euclideaR (reflexivaR c) h2)
 
-- 3ª demostración
example : transitive (≈) :=
assume a b c (h1 : a ≈ b) (h2 : b ≈ c),
have h3 : c ≈ b, from euclideaR (reflexivaR c) h2,
show a ≈ c, from euclideaR h1 h3
 
-- ----------------------------------------------------
-- Ej. 3. Demostrar que las relaciones reflexivas y
-- y euclídeas son de equivalencia.
-- ----------------------------------------------------
 
-- 1ª demostración
example : equivalence (≈) :=
begin
  unfold equivalence,
  exact ⟨reflexivaR, simetricaR, transitivaR⟩,
end
 
-- 2ª demostración
example : equivalence (≈) :=
⟨reflexivaR, simetricaR, transitivaR⟩
 
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las equivalencias son los preórdenes simétricos

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 5 pruebas en Lean de que las equivalencias son los preórdenes simétricos, 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

-- ----------------------------------------------------
-- Ej. 1. Un preorden es una relación reflexiva y
-- transitiva.
--
-- Demostrar que las relaciones de equivalencias son
-- los prórdenes simétricos.
-- ----------------------------------------------------
 
import tactic
 
variable {A : Type}
variable R : A → A → Prop
 
def preorden (R : A → A → Prop) : Prop :=
  reflexive R ∧ transitive R
 
-- #print equivalence
-- #print symmetric
 
-- 1ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
begin
  split,
  { rintros ⟨h1, h2, h3⟩,
    exact ⟨⟨h1, h3⟩, h2⟩, },
  { rintros ⟨⟨h1, h3⟩, h2⟩,
    exact ⟨h1, h2, h3⟩, },
end
 
-- 2ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
⟨λ ⟨h1, h2, h3⟩, ⟨⟨h1, h3⟩, h2⟩,
 λ ⟨⟨h1, h3⟩, h2⟩, ⟨h1, h2, h3⟩⟩
 
-- 3ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
iff.intro
  ( assume h1 : equivalence R,
    have h2 : reflexive R, from and.left h1,
    have h3 : symmetric R, from and.left (and.right h1),
    have h4 : transitive R, from and.right (and.right h1),
    show preorden R ∧ symmetric R,
      from and.intro (and.intro h2 h4) h3)
  ( assume h1 : preorden R ∧ symmetric R,
    have h2 : preorden R, from and.left h1,
    show equivalence R,
      from and.intro (and.left h2)
             (and.intro (and.right h1) (and.right h2)))
 
-- 4ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
begin
  unfold equivalence preorden,
  tauto,
end
 
-- 5ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
by finish [preorden]
Seguir leyendo →

ForMatUS: Pruebas en Lean de una desigualdad entre números naturales

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 8 pruebas en Lean de una desigualdad entre números naturales, 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

-- ----------------------------------------------------
-- Ej. 1. Demostrar que si n y m son números naturales
-- tales que n + 1 ≤ m, entonces n < m + 1.
-- ----------------------------------------------------
 
import tactic
 
variables n m : ℕ
 
-- 1ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
calc
  n   < n + 1 : lt_add_one n
  ... ≤ m     : h
  ... < m + 1 : lt_add_one m
 
-- 2ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
have h1 : n < n + 1, from lt_add_one n,
have h2 : n < m,     from lt_of_lt_of_le h1 h,
have h3 : m < m + 1, from lt_add_one m,
show n < m + 1,      from lt.trans h2 h3
 
-- 3ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
begin
  apply lt_trans (lt_add_one n),
  apply lt_of_le_of_lt h (lt_add_one m),
end
 
-- 4ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
lt_trans (lt_add_one n) (lt_of_le_of_lt h (lt_add_one m))
 
-- 5ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
-- by suggest
nat.lt.step h
 
-- 6ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
-- by hint
by omega
 
-- 7ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
by linarith
 
-- 8ª demostración
example
  (h : n + 1 ≤ m)
  : n < m + 1 :=
by nlinarith
Seguir leyendo →