2 noviembre 2020 – Vestigium

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

PorJosé A. Alonso 2 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 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

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

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

PorJosé A. Alonso 2 noviembre 202021 diciembre 2020

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]

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

-- 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]