La congruencia módulo 2 es una relación de equivalencia

José A. Alonso

04-06-2024

Se define la relación \(R\) entre los números enteros de forma que \(x\) está relacionado con \(y\) si \(x-y\) es divisible por 2.

Demostrar con Lean4 que \(R\) es una relación de equivalencia.

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

import Mathlib.Data.Int.Basic
import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

example : Equivalence R :=
by sorry

1. Demostración en lenguaje natural

Tenemos que demostrar que \(\mathrel{R}\) es reflexiva, simétrica y transitiva.

Para demostrar que \(\mathrel{R}\) es reflexiva, sea \(x ∈ ℤ\). Entonces, \(x - x = 0\) que es divisible por 2. Luego, \(x\mathrel{R}x\).

Para demostrar que \(\mathrel{R}\) es simétrica, sean \(x, y ∈ ℤ\) tales que \(x\mathrel{R}y\). Entonces, \(x - y\) es divisible por 2. Luego, existe un \(a ∈ ℤ\) tal que \[ x - y = 2·a \] Por tanto, \[ y - x = 2·(-a) \] Por lo que \(y - x\) es divisible por 2 y \(y\mathrel{R}x\).

Para demostrar que \(\mathrel{R}\) es transitiva, sean \(x, y, z ∈ ℤ\) tales que \(x\mathrel{R}y\) y \(y\mathrel{R}z\). Entonces, tanto \(x - y\) como \(y - z\) son divibles por 2. Luego, existen \(a, b ∈ ℤ\) tales que \begin{align} x - y &= 2·a \newline y - z &= 2·b \end{align} Por tanto, \[ x - z = 2·(a + b) \] Por lo que \(x - z\) es divisible por 2 y \(x\mathrel{R}z\).

2. Demostraciones con Lean4

import Mathlib.Data.Int.Basic
import Mathlib.Tactic

def R (m n : ℤ) := 2 ∣ (m - n)

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

example : Equivalence R :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : ℤ), R x x
    intro x
    -- x : ℤ
    -- ⊢ R x x
    unfold R
    -- ⊢ 2 ∣ x - x
    rw [sub_self]
    -- ⊢ 2 ∣ 0
    exact dvd_zero 2
  . -- ⊢ ∀ {x y : ℤ}, R x y → R y x
    intros x y hxy
    -- x y : ℤ
    -- hxy : R x y
    -- ⊢ R y x
    unfold R at *
    -- hxy : 2 ∣ x - y
    -- ⊢ 2 ∣ y - x
    cases' hxy with a ha
    -- a : ℤ
    -- ha : x - y = 2 * a
    use -a
    -- ⊢ y - x = 2 * -a
    calc y - x
         = -(x - y) := (neg_sub x y).symm
       _ = -(2 * a) := by rw [ha]
       _ = 2 * -a   := neg_mul_eq_mul_neg 2 a
  . -- ⊢ ∀ {x y z : ℤ}, R x y → R y z → R x z
    intros x y z hxy hyz
    -- x y z : ℤ
    -- hxy : R x y
    -- hyz : R y z
    -- ⊢ R x z
    cases' hxy with a ha
    -- a : ℤ
    -- ha : x - y = 2 * a
    cases' hyz with b hb
    -- b : ℤ
    -- hb : y - z = 2 * b
    use a + b
    -- ⊢ x - z = 2 * (a + b)
    calc x - z
         = (x - y) + (y - z) := (sub_add_sub_cancel x y z).symm
       _ = 2 * a + 2 * b     := congrArg₂ (. + .) ha hb
       _ = 2 * (a + b)       := (mul_add 2 a b).symm

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

example : Equivalence R :=
by
  repeat' constructor
  . -- ⊢ ∀ (x : ℤ), R x x
    intro x
    -- x : ℤ
    -- ⊢ R x x
    simp [R]
  . -- ⊢ ∀ {x y : ℤ}, R x y → R y x
    rintro x y ⟨a, ha⟩
    -- x y a : ℤ
    -- ha : x - y = 2 * a
    -- ⊢ R y x
    use -a
    -- ⊢ y - x = 2 * -a
    linarith
  . -- ⊢ ∀ {x y z : ℤ}, R x y → R y z → R x z
    rintro x y z ⟨a, ha⟩ ⟨b, hb⟩
    -- x y z a : ℤ
    -- ha : x - y = 2 * a
    -- b : ℤ
    -- hb : y - z = 2 * b
    -- ⊢ R x z
    use a + b
    -- ⊢ x - z = 2 * (a + b)
    linarith

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

-- variable (a b c x y x' y' : ℤ)
-- #check (congrArg₂  (. + .) : x = x' → y = y' → x + y = x' + y')
-- #check (dvd_zero a : a ∣ 0)
-- #check (mul_add a b c : a * (b + c) = a * b + a * c)
-- #check (neg_mul_eq_mul_neg a b : -(a * b) = a * -b)
-- #check (neg_sub a b : -(a - b) = b - a)
-- #check (sub_add_sub_cancel a b c : a - b + (b - c) = a - c)
-- #check (sub_self a : a - a = 0)

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

3. Demostraciones con Isabelle/HOL

theory La_congruencia_modulo_2_es_una_relacion_de_equivalencia
imports Main
begin

definition R :: "(int × int) set" where
  "R = {(m, n). even (m - n)}"

lemma R_iff [simp]:
  "((x, y) ∈ R) = even (x - y)"
by (simp add: R_def)

(* 1ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show "R ⊆ UNIV × UNIV"
    proof -
      have "R ⊆ UNIV"
        by (rule top.extremum)
      also have "… = UNIV × UNIV"
        by (rule Product_Type.UNIV_Times_UNIV[symmetric])
      finally show "R ⊆ UNIV × UNIV"
        by this
    qed
  next
    show "∀x∈UNIV. (x, x) ∈ R"
    proof
      fix x :: int
      assume "x ∈ UNIV"
      have "even 0" by (rule even_zero)
      then have "even (x - x)" by (simp only: diff_self)
      then show "(x, x) ∈ R"
        by (simp only: R_iff)
    qed
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y :: int
    assume "(x, y) ∈ R"
    then have "even (x - y)"
      by (simp only: R_iff)
    then show "(y, x) ∈ R"
    proof (rule evenE)
      fix a :: int
      assume ha : "x - y = 2 * a"
      have "y - x = -(x - y)"
        by (rule minus_diff_eq[symmetric])
      also have "… = -(2 * a)"
        by (simp only: ha)
      also have "… = 2 * (-a)"
        by (rule mult_minus_right[symmetric])
      finally have "y - x = 2 * (-a)"
        by this
      then have "even (y - x)"
        by (rule dvdI)
      then show "(y, x) ∈ R"
        by (simp only: R_iff)
    qed
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume hxy : "(x, y) ∈ R" and hyz : "(y, z) ∈ R"
    have "even (x - y)"
      using hxy by (simp only: R_iff)
    then obtain a where ha : "x - y = 2 * a"
      by (rule dvdE)
    have "even (y - z)"
      using hyz by (simp only: R_iff)
    then obtain b where hb : "y - z = 2 * b"
      by (rule dvdE)
    have "x - z = (x - y) + (y - z)"
      by simp
    also have "… = (2 * a) + (2 * b)"
      by (simp only: ha hb)
    also have "… = 2 * (a + b)"
      by (simp only: distrib_left)
    finally have "x - z = 2 * (a + b)"
      by this
    then have "even (x - z)"
      by (rule dvdI)
    then show "(x, z) ∈ R"
      by (simp only: R_iff)
  qed
qed

(* 2ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show "R ⊆ UNIV × UNIV" by simp
  next
    show "∀x∈UNIV. (x, x) ∈ R"
    proof
      fix x :: int
      assume "x ∈ UNIV"
      have "x - x = 2 * 0"
        by simp
      then show "(x, x) ∈ R"
        by simp
    qed
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y :: int
    assume "(x, y) ∈ R"
    then have "even (x - y)"
      by simp
    then obtain a where ha : "x - y = 2 * a"
      by blast
    then have "y - x = 2 *(-a)"
      by simp
    then show "(y, x) ∈ R"
      by simp
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume hxy : "(x, y) ∈ R" and hyz : "(y, z) ∈ R"
    have "even (x - y)"
      using hxy by simp
    then obtain a where ha : "x - y = 2 * a"
      by blast
    have "even (y - z)"
      using hyz by simp
    then obtain b where hb : "y - z = 2 * b"
      by blast
    have "x - z = 2 * (a + b)"
      using ha hb by auto
    then show "(x, z) ∈ R"
      by simp
  qed
qed

(* 3ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
  proof (unfold refl_on_def; intro conjI)
    show " R ⊆ UNIV × UNIV"
      by simp
  next
    show "∀x∈UNIV. (x, x) ∈ R"
      by simp
  qed
next
  show "sym R"
  proof (unfold sym_def; intro allI impI)
    fix x y
    assume "(x, y) ∈ R"
    then show "(y, x) ∈ R"
      by simp
  qed
next
  show "trans R"
  proof (unfold trans_def; intro allI impI)
    fix x y z
    assume "(x, y) ∈ R" and "(y, z) ∈ R"
    then show "(x, z) ∈ R"
      by simp
  qed
qed

(* 4ª demostración *)

lemma "equiv UNIV R"
proof (rule equivI)
  show "refl R"
    unfolding refl_on_def by simp
next
  show "sym R"
    unfolding sym_def by simp
next
  show "trans R"
    unfolding trans_def by simp
qed

(* 5ª demostración *)

lemma "equiv UNIV R"
  unfolding equiv_def refl_on_def sym_def trans_def
  by simp

(* 6ª demostración *)

lemma "equiv UNIV R"
  by (simp add: equiv_def refl_on_def sym_def trans_def)

end