Las relaciones reflexivas y circulares son simétricas

José A. Alonso

08-04-2020

Se dice que la relación binaria \(R\) es

reflexiva si \((∀x)R(x, x)\)
circular si \((∀x, y, z)[R(x, y) ∧ R(y, z) ⟶ R(z, x)]\)
simétrica si \((∀x, y)[R(x, y) ⟶ R(y, x)]\)

Demostrar que las relaciones reflexivas y circulares son simétricas. Para ello, completar la siguiente teoría de Isabelle/HOL:

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
  oops

end

Soluciones

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

(* 1ª demostración *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
  using assms
  by blast

(* 2ª demostración *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
proof (rule allI)+
  fix a b
  show "R (a, b) ⟶ R (b, a)"
  proof (rule impI)
    assume "R(a , b)"
    have "R(b, b)" using assms(1) ..
    with `R(a, b)` have "R(a, b) ∧ R(b, b)" ..
    have  "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" using assms(2) ..
    then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)" ..
    then have "R(a, b) ∧ R(b, b) ⟶R(b, a)" ..
    then show "R(b, a)" using `R(a, b) ∧ R(b, b)` ..
  qed
qed

(* 3º demostración *)
lemma
  assumes "∀x. R(x, x)"
          "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
proof (rule allI)+
  fix a b
  show "R (a, b) ⟶ R (b, a)"
  proof (rule impI)
    assume "R(a, b)"
    have "R(b, b)"
      using assms(1) by (rule allE)
    with `R(a, b)` have "R(a, b) ∧ R(b, b)"
      by (rule conjI)
    have  "∀y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)"
      using assms(2) by (rule allE)
    then have "∀z. R(a, b) ∧ R(b, z) ⟶R(z, a)"
      by (rule allE)
    then have "R(a, b) ∧ R(b, b) ⟶R(b, a)"
      by (rule allE)
    then show "R(b, a)" using `R(a, b) ∧ R(b, b)`
      by (rule mp)
  qed
qed

end