Las particiones definen relaciones transitivas

José A. Alonso

08-07-2024

Cada familia de conjuntos \(P\) define una relación de forma que dos elementos están relacionados si algún conjunto de \(P\) contiene a ambos elementos. Se puede definir en Lean4 por

   def relacion (P : set (set X)) (x y : X) :=
     ∃ A ∈ P, x ∈ A ∧ y ∈ A

Una familia \(P\) de subconjuntos de \(X\) es una partición de \(X\) si cada elemento de \(X\) pertenece a un único conjunto de \(P\) y todos los elementos de \(P\) son no vacíos. Se puede definir en Lean por

   def particion (P : set (set X)) : Prop :=
     (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

Demostrar con Lean4 que si \(P\) es una partición de \(X\), entonces la relación definida por \(P\) es transitiva.

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

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

example
  (h : particion P)
  : Transitive (relacion P) :=
by sorry

1. Demostración en lenguaje natural

Sea \(R\) la relación definida por \(P\) y \(x, y, z ∈ X\) tales que \(xRy\) e \(yRz\). Entonces, existen \(B_1\) y \(B_2\) tales que \begin{align} &B_1 ∈ P ∧ x ∈ B_1 ∧ y ∈ B_1 \tag{1} \newline &B_2 ∈ P ∧ y ∈ B_2 ∧ z ∈ B_2 \tag{2} \end{align} Si demostramos que \(B_1 = B_2\), se tiene que \[ B_1 ∈ P ∧ x ∈ B_1 ∧ z ∈ B_1 \] y, por tanto, \(xRz\).

Para demostrar que \(B_1 = B_2\), se observa que, por ser \(P\) una partición de \(X\), se tiene \[ (∀ x ∈ X)(∃ B ∈ P)(∀ C ∈ P)[x ∈ C → B = C] \] por tanto, existe un \(B ∈ P\) tal que \[ (∀ C ∈ P)[y ∈ C → B = C] \tag{3} \] Entonces, \begin{align} B_1 &= B &&\text{[de (3) y (1)]} \newline &= B_2 &&\text{[de (3) y (2)]} \end{align}

2. Demostraciones con Lean4

import Mathlib.Tactic

variable {X : Type}
variable (P : Set (Set X))

def relacion (P : Set (Set X)) (x y : X) :=
  ∃ A ∈ P, x ∈ A ∧ y ∈ A

def particion (P : Set (Set X)) : Prop :=
  (∀ x, (∃ B ∈ P, x ∈ B ∧ ∀ C ∈ P, x ∈ C → B = C)) ∧ ∅ ∉ P

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

example
  (h : particion P)
  : Transitive (relacion P) :=
by
  rintro x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩
  -- x y z : X
  -- B1 : Set X
  -- hB1P : B1 ∈ P
  -- hxB1 : x ∈ B1
  -- hyB1 : y ∈ B1
  -- B2 : Set X
  -- hB2P : B2 ∈ P
  -- hyB2 : y ∈ B2
  -- hzB2 : z ∈ B2
  -- ⊢ relacion P x z
  have h1 : B1 = B2 := by
    rcases (h.1 y) with ⟨B, -, -, hB⟩
    -- B : Set X
    -- hB : ∀ (C : Set X), C ∈ P → y ∈ C → B = C
    calc B1 = B  := by exact (hB B1 hB1P hyB1).symm
          _ = B2 := hB B2 hB2P hyB2
  repeat' constructor
  . -- ⊢ B1 ∈ P
    exact hB1P
  . -- ⊢ x ∈ B1
    exact hxB1
  . -- ⊢ z ∈ B1
    rw [h1]
    -- ⊢ z ∈ B2
    exact hzB2

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

example
  (h : particion P)
  : Transitive (relacion P) :=
by
  unfold Transitive
  -- ⊢ ∀ ⦃x y z : X⦄, relacion P x y → relacion P y z → relacion P x z
  intros x y z h1 h2
  -- x y z : X
  -- h1 : relacion P x y
  -- h2 : relacion P y z
  -- ⊢ relacion P x z
  unfold relacion at *
  -- h1 : ∃ A, A ∈ P ∧ x ∈ A ∧ y ∈ A
  -- h2 : ∃ A, A ∈ P ∧ y ∈ A ∧ z ∈ A
  -- ⊢ ∃ A, A ∈ P ∧ x ∈ A ∧ z ∈ A
  rcases h1 with ⟨B1, hB1P, hxB1, hyB1⟩
  -- B1 : Set X
  -- hB1P : B1 ∈ P
  -- hxB1 : x ∈ B1
  -- hyB1 : y ∈ B1
  rcases h2 with ⟨B2, hB2P, hyB2, hzB2⟩
  -- B2 : Set X
  -- hB2P : B2 ∈ P
  -- hyB2 : y ∈ B2
  -- hzB2 : z ∈ B2
  use B1
  -- ⊢ B1 ∈ P ∧ x ∈ B1 ∧ z ∈ B1
  repeat' constructor
  . -- ⊢ B1 ∈ P
    exact hB1P
  . -- ⊢ x ∈ B1
    exact hxB1
  . -- ⊢ z ∈ B1
    convert hzB2
    -- ⊢ B1 = B2
    rcases (h.1 y) with ⟨B, -, -, hB⟩
    -- B : Set X
    -- hB : ∀ (C : Set X), C ∈ P → y ∈ C → B = C
    have hBB1 : B = B1 := hB B1 hB1P hyB1
    have hBB2 : B = B2 := hB B2 hB2P hyB2
    exact Eq.trans hBB1.symm hBB2

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

example
  (h : particion P)
  : Transitive (relacion P) :=
by
  rintro x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩
  -- x y z : X
  -- B1 : Set X
  -- hB1P : B1 ∈ P
  -- hxB1 : x ∈ B1
  -- hyB1 : y ∈ B1
  -- B2 : Set X
  -- hB2P : B2 ∈ P
  -- hyB2 : y ∈ B2
  -- hzB2 : z ∈ B2
  -- ⊢ relacion P x z
  use B1
  -- ⊢ B1 ∈ P ∧ x ∈ B1 ∧ z ∈ B1
  repeat' constructor
  . -- ⊢ B1 ∈ P
    exact hB1P
  . -- ⊢ x ∈ B1
    exact hxB1
  . -- ⊢ z ∈ B1
    convert hzB2
    -- ⊢ B1 = B2
    rcases (h.1 y) with ⟨B, -, -, hB⟩
    -- B : Set X
    -- hB : ∀ (C : Set X), C ∈ P → y ∈ C → B = C
    exact Eq.trans (hB B1 hB1P hyB1).symm (hB B2 hB2P hyB2)

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

example
  (h : particion P)
  : Transitive (relacion P) :=
by
  rintro x y z ⟨B1,hB1P,hxB1,hyB1⟩ ⟨B2,hB2P,hyB2,hzB2⟩
  -- x y z : X
  -- B1 : Set X
  -- hB1P : B1 ∈ P
  -- hxB1 : x ∈ B1
  -- hyB1 : y ∈ B1
  -- B2 : Set X
  -- hB2P : B2 ∈ P
  -- hyB2 : y ∈ B2
  -- hzB2 : z ∈ B2
  -- ⊢ relacion P x z
  exact ⟨B1, ⟨hB1P,
              hxB1,
              by { convert hzB2
                   rcases (h.1 y) with ⟨B, -, -, hB⟩
                   exact Eq.trans (hB B1 hB1P hyB1).symm
                                  (hB B2 hB2P hyB2) }⟩⟩

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

-- variable (x y z : 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 Las_particiones_definen_relaciones_transitivas
imports Main
begin

definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where
  "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"

definition particion :: "('a set) set ⇒ bool" where
  "particion P ⟷ (∀x. (∃B∈P. x ∈ B ∧ (∀C∈P. x ∈ C ⟶ B = C))) ∧ {} ∉ P"

(* 1ª demostración *)

lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  have "∃A∈P. x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (simp only: relacion_def)
  then obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    by (rule bexE)
  have "∃B∈P. y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (simp only: relacion_def)
  then obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    by (rule bexE)
  have "A = B"
  proof -
    have "∃C ∈ P. y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms
      by (simp only: particion_def)
    then obtain C where "C ∈ P"
                    and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      by (rule bexE)
    have hC' : "∀D∈P. y ∈ D ⟶ C = D"
      using hC by (rule conjunct2)
    have "C = A"
      using ‹A ∈ P› hA hC' by simp
    moreover have "C = B"
      using ‹B ∈ P› hB hC by simp
    ultimately show "A = B"
      by (rule subst)
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by simp
  then have "∃A∈P. x ∈ A ∧ z ∈ A"
    using ‹A ∈ P› by (rule bexI)
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P›
    by (unfold relacion_def)
qed

(* 2ª demostración *)

lemma
  assumes "particion P"
  shows   "transp (relacion P)"
proof (rule transpI)
  fix x y z
  assume "relacion P x y" and "relacion P y z"
  obtain A where "A ∈ P" and hA : "x ∈ A ∧ y ∈ A"
    using ‹relacion P x y›
    by (meson relacion_def)
  obtain B where "B ∈ P" and hB : "y ∈ B ∧ z ∈ B"
    using ‹relacion P y z›
    by (meson relacion_def)
  have "A = B"
  proof -
    obtain C where "C ∈ P" and hC : "y ∈ C ∧ (∀D∈P. y ∈ D ⟶ C = D)"
      using assms particion_def
      by metis
    have "C = A"
      using ‹A ∈ P› hA hC by auto
    moreover have "C = B"
      using ‹B ∈ P› hB hC by auto
    ultimately show "A = B"
      by simp
  qed
  then have "x ∈ A ∧ z ∈ A"
    using hA hB by auto
  then show "relacion P x z"
    using ‹A = B› ‹A ∈ P› relacion_def
    by metis
qed

(* 3ª demostración *)

lemma
  assumes "particion P"
  shows   "transp (relacion P)"
  using assms particion_def relacion_def
  by (smt (verit) transpI)

end