La igualdad de valores es una relación de equivalencia

José A. Alonso

26-06-2024

Sean $X$ e $Y$ dos conjuntos y $f$ una función de $X$ en $Y$ . Se define la relación $\text{R}$ en $X$ de forma que $x$ está relacionado con $y$ si $f(x) = f(y)$ .

Demostrar con Lean4 que $\text{R}$ es una relación de equivalencia.

Para ello, completar la siguiente teoría de Lean4:

import Mathlib.Tactic

variable {X Y : Type _}
variable (f : X → Y)

def R (x y : X) :=
  f x = f y

example : Equivalence (R f) :=
by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que $\text{R}$ es reflexiva, simétrica y transitiva,

Para demostrar que $\text{R}$ es reflexiva, sea $x ∈ X$ . Entonces, $f(x) = f(x)$ y, por tanto $x\text{R}x$ .

Para demostrar que $\text{R}$ es simétrica, sean $x, y ∈ X$ tales que $x\text{R}y$ . Entonces, $f(x) = f(y)$ . Luego, $f(y) = f(x)$ y, por tanto, $y\text{R}x$ .

Para demostrar que $\text{R}$ es transitiva, sean $x, y, z ∈ X$ tales que $x\text{R}y$ y $y\text{R}z$ . Entonces, $f(x) = f(y)$ y $f(y) = f(z)$ . Luego, $f(x) = f(z)$ y, por tanto, $z\text{R}z$ .

2. Demostraciones con Lean4

import Mathlib.Tactic

variable {X Y : Type _}
variable (f : X → Y)

def R (x y : X) :=
  f x = f y

-- 1ª demostración
-- ===============

example : Equivalence (R f) :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : X), R f x x
    intro x
    -- x : X
    -- ⊢ R f x x
    unfold R
    -- ⊢ f x = f x
    exact Eq.refl (f x)
  . -- ⊢ ∀ {x y : X}, R f x y → R f y x
    intros x y hxy
    -- x y : X
    -- hxy : R f x y
    -- ⊢ R f y x
    unfold R at *
    -- hxy : f x = f y
    -- ⊢ f y = f x
    exact Eq.symm hxy
  . -- ⊢ ∀ {x y z : X}, R f x y → R f y z → R f x z
    intros x y z hxy hyz
    -- x y z : X
    -- hxy : R f x y
    -- hyz : R f y z
    -- ⊢ R f x z
    unfold R at *
    -- hxy : f x = f y
    -- hyz : f y = f z
    -- ⊢ f x = f z
    exact Eq.trans hxy hyz

-- 2ª demostración
-- ===============

example : Equivalence (R f) :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : X), R f x x
    intro x
    -- x : X
    -- ⊢ R f x x
    exact Eq.refl (f x)
  . -- ⊢ ∀ {x y : X}, R f x y → R f y x
    intros x y hxy
    -- x y : X
    -- hxy : R f x y
    -- ⊢ R f y x
    exact Eq.symm hxy
  . -- ⊢ ∀ {x y z : X}, R f x y → R f y z → R f x z
    intros x y z hxy hyz
    -- x y z : X
    -- hxy : R f x y
    -- hyz : R f y z
    -- ⊢ R f x z
    exact Eq.trans hxy hyz

-- 3ª demostración
-- ===============

example : Equivalence (R f) :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : X), R f x x
    exact fun x ↦ Eq.refl (f x)
  . -- ⊢ ∀ {x y : X}, R f x y → R f y x
    exact fun hxy ↦ Eq.symm hxy
  . -- ⊢ ∀ {x y z : X}, R f x y → R f y z → R f x z
    exact fun hxy hyz ↦ by exact  Eq.trans hxy hyz

-- 4ª demostración
-- ===============

example : Equivalence (R f) :=
⟨fun x ↦ Eq.refl (f x),
 fun hxy ↦ Eq.symm hxy,
 fun hxy hyz ↦ Eq.trans hxy hyz⟩

-- Lemas usados
-- ============

-- variable (x y z : X)
-- #check (Eq.refl x : x = x)
-- #check (Eq.symm : x = y → y = x)
-- #check (Eq.trans : x = y → y = z → x = z)

Se puede interactuar con las demostraciones anteriores en Lean 4 Web.

3. Demostraciones con Isabelle/HOL

theory La_igualdad_de_valores_es_una_relacion_de_equivalencia
imports Main
begin

definition R :: "('a ⇒ 'b) ⇒ 'a ⇒ 'a ⇒ bool" where
  "R f x y ⟷ (f x = f y)"

(* 1ª demostración *)

lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    have "f x = f x"
      by (rule refl)
    then show "R f x x"
      by (unfold R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then have "f x = f y"
      by (unfold R_def)
    then have "f y = f x"
      by (rule sym)
    then show "R f y x"
      by (unfold R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then have "f x = f y" and "f y = f z"
      by (unfold R_def)
    then have "f x = f z"
      by (rule ssubst)
    then show "R f x z"
      by (unfold R_def)
  qed
qed

(* 2ª demostración *)

lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
  proof (rule reflpI)
    fix x
    show "R f x x"
      by (metis R_def)
  qed
next
  show "symp (R f)"
  proof (rule sympI)
    fix x y
    assume "R f x y"
    then show "R f y x"
      by (metis R_def)
  qed
next
  show "transp (R f)"
  proof (rule transpI)
    fix x y z
    assume "R f x y" and "R f y z"
    then show "R f x z"
      by (metis R_def)
  qed
qed

(* 3ª demostración *)

lemma "equivp (R f)"
proof (rule equivpI)
  show "reflp (R f)"
    by (simp add: R_def reflpI)
next
  show "symp (R f)"
    by (metis R_def sympI)
next
  show "transp (R f)"
    by (metis R_def transpI)
qed

(* 4ª demostración *)

lemma "equivp (R f)"
  by (metis R_def
            equivpI
            reflpI
            sympI
            transpI)

end