La igualdad de valores es una relación de equivalencia

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

Demostrar que R es una relación de equivalencia.

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

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

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

example : equivalence (R f) :=
sorry

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

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

example : equivalence (R f) :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

universe u
variables {X Y : Type u}
variable  (f : X → Y)

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

-- 1ª demostración
example : equivalence (R f) :=
begin
  unfold equivalence,
  repeat { split },
  { unfold reflexive,
    intro x,
    unfold R, },
  { unfold symmetric,
    intros x y hxy,
    unfold R,
    exact symm hxy, },
  { unfold transitive,
    unfold R,
    intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 2ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { intro x,
    exact rfl, },
  { intros x y hxy,
    exact eq.symm hxy, },
  { intros x y z hxy hyz,
    exact eq.trans hxy hyz, },
end

-- 3ª demostración
example : equivalence (R f) :=
begin
  repeat { split },
  { exact λ x, rfl, },
  { exact λ x y hxy, eq.symm hxy, },
  { exact λ x y z hxy hyz, eq.trans hxy hyz, },
end

-- 4ª demostración
example : equivalence (R f) :=
⟨λ x, rfl,
 λ x y hxy, eq.symm hxy,
 λ x y z hxy hyz, eq.trans hxy hyz⟩

import tactic

universe u

variables {X Y : Type u}

variable (f : X → Y)

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

-- 1ª demostración

example : equivalence (R f) :=

begin

unfold equivalence,

repeat { split },

{ unfold reflexive,

intro x,

unfold R, },

{ unfold symmetric,

intros x y hxy,

unfold R,

exact symm hxy, },

{ unfold transitive,

unfold R,

intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 2ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ intro x,

exact rfl, },

{ intros x y hxy,

exact eq.symm hxy, },

{ intros x y z hxy hyz,

exact eq.trans hxy hyz, },

end

-- 3ª demostración

example : equivalence (R f) :=

begin

repeat { split },

{ exact λ x, rfl, },

{ exact λ x y hxy, eq.symm hxy, },

{ exact λ x y z hxy hyz, eq.trans hxy hyz, },

end

-- 4ª demostración

example : equivalence (R f) :=

⟨λ x, rfl,

λ x y hxy, eq.symm hxy,

λ x y z hxy hyz, eq.trans hxy hyz⟩

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]

[expand title=»Soluciones 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

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

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

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

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

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

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

(* 3ª demostración *)

lemma "equivp (R f)"

proof (rule equivpI)

show "reflp (R f)"

by (simp add: R_def reflpI)

show "symp (R f)"

by (metis R_def sympI)

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

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]

Share this:

Escribe un comentarioCancel reply