Menu Close

Día: 2 noviembre, 2020

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

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

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

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]