Las clases de equivalencia de elementos relacionados son iguales

Demostrar que las clases de equivalencia de elementos relacionados son iguales.

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

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
sorry

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

sorry

[expand title=»Soluciones con Lean»]

import tactic

variable  {X : Type}
variables {x y: X}
variable  {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=
  {y : X | R x y}

-- En la demostración se usará el siguiente lema del que se presentan
-- varias demostraciones.

-- 1ª demostración del lema auxiliar
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
begin
  intros z hz,
  have hyz : R y z := hz,
  have htrans : transitive R := h.2.2,
  have hxz : R x z := htrans hxy hyz,
  exact hxz,
end

-- 2ª demostración del lema auxiliar
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
begin
  intros z hz,
  exact h.2.2 hxy hz,
end

-- 3ª demostración del lema auxiliar
lemma aux
  (h : equivalence R)
  (hxy : R x y)
  : clase R y ⊆ clase R x :=
λ z hz, h.2.2 hxy hz

-- A continuación se presentan varias demostraciones del ejercicio
-- usando el lema auxiliar

-- 1ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
begin
  apply le_antisymm,
  { have hs : symmetric R := h.2.1,
    have hyx : R y x := hs hxy,
    exact aux h hyx, },
  { exact aux h hxy, },
end

-- 2ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
begin
  apply le_antisymm,
  { exact aux h (h.2.1 hxy), },
  { exact aux h hxy, },
end

-- 3ª demostración
example
  (h : equivalence R)
  (hxy : R x y)
  : clase R x = clase R y :=
le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

import tactic

variable {X : Type}

variables {x y: X}

variable {R : X → X → Prop}

def clase (R : X → X → Prop) (x : X) :=

{y : X | R x y}

-- En la demostración se usará el siguiente lema del que se presentan

-- varias demostraciones.

-- 1ª demostración del lema auxiliar

example

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

begin

intros z hz,

have hyz : R y z := hz,

have htrans : transitive R := h.2.2,

have hxz : R x z := htrans hxy hyz,

exact hxz,

end

-- 2ª demostración del lema auxiliar

example

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

begin

intros z hz,

exact h.2.2 hxy hz,

end

-- 3ª demostración del lema auxiliar

lemma aux

(h : equivalence R)

(hxy : R x y)

: clase R y ⊆ clase R x :=

λ z hz, h.2.2 hxy hz

-- A continuación se presentan varias demostraciones del ejercicio

-- usando el lema auxiliar

-- 1ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

begin

apply le_antisymm,

{ have hs : symmetric R := h.2.1,

have hyx : R y x := hs hxy,

exact aux h hyx, },

{ exact aux h hxy, },

end

-- 2ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

begin

apply le_antisymm,

{ exact aux h (h.2.1 hxy), },

{ exact aux h hxy, },

end

-- 3ª demostración

example

(h : equivalence R)

(hxy : R x y)

: clase R x = clase R y :=

le_antisymm (aux h (h.2.1 hxy)) (aux h hxy)

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 Las_clases_de_equivalencia_de_elementos_relacionados_son_iguales
imports Main
begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"
  where "clase R x = {y. R x y}"

(* En la demostración se usará el siguiente lema del que se presentan
   varias demostraciones. *)

(* 1ª demostración del lema auxiliar *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
proof (rule subsetI)
  fix z
  assume "z ∈ clase R y"
  then have "R y z"
    by (simp add: clase_def)
  have "transp R"
    using assms(1) by (rule equivp_imp_transp)
  then have "R x z"
    using ‹R x y› ‹R y z› by (rule transpD)
  then show "z ∈ clase R x"
    by (simp add: clase_def)
qed

(* 2ª demostración del lema auxiliar *)
lemma aux :
  assumes "equivp R"
          "R x y"
  shows "clase R y ⊆ clase R x"
  using assms
  by (metis clase_def eq_refl equivp_def)

(* A continuación se presentan demostraciones del ejercicio *)

(* 1ª demostración *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
proof (rule equalityI)
  show "clase R y ⊆ clase R x"
    using assms by (rule aux)
next
  show "clase R x ⊆ clase R y"
  proof -
    have "symp R"
      using assms(1) equivpE by blast
    have "R y x"
      using ‹R x y› by (simp add: ‹symp R› sympD)
    with assms(1) show "clase R x ⊆ clase R y"
       by (rule aux)
  qed
qed

(* 2ª demostración *)
lemma
  assumes "equivp R"
          "R x y"
  shows "clase R y = clase R x"
  using assms
  by (metis clase_def equivp_def)

end

theory Las_clases_de_equivalencia_de_elementos_relacionados_son_iguales

imports Main

begin

definition clase :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a set"

where "clase R x = {y. R x y}"

(* En la demostración se usará el siguiente lema del que se presentan

varias demostraciones. *)

(* 1ª demostración del lema auxiliar *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y ⊆ clase R x"

proof (rule subsetI)

fix z

assume "z ∈ clase R y"

then have "R y z"

by (simp add: clase_def)

have "transp R"

using assms(1) by (rule equivp_imp_transp)

then have "R x z"

using ‹R x y› ‹R y z› by (rule transpD)

then show "z ∈ clase R x"

by (simp add: clase_def)

qed

(* 2ª demostración del lema auxiliar *)

lemma aux :

assumes "equivp R"

"R x y"

shows "clase R y ⊆ clase R x"

using assms

by (metis clase_def eq_refl equivp_def)

(* A continuación se presentan demostraciones del ejercicio *)

(* 1ª demostración *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y = clase R x"

proof (rule equalityI)

show "clase R y ⊆ clase R x"

using assms by (rule aux)

show "clase R x ⊆ clase R y"

proof -

have "symp R"

using assms(1) equivpE by blast

have "R y x"

using ‹R x y› by (simp add: ‹symp R› sympD)

with assms(1) show "clase R x ⊆ clase R y"

by (rule aux)

qed

(* 2ª demostración *)

lemma

assumes "equivp R"

"R x y"

shows "clase R y = clase R x"

using assms

by (metis clase_def equivp_def)

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