Las reflexivas circulares son simétricas

PorJosé A. Alonso 8 abril 202021 agosto 2021

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

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 con Isabelle/HOL

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

(* 1ª demostración: automática *)
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: estructurada *)
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

(* 3º demostración: detallada *)
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

end

theory Las_reflexivas_circulares_son_simetricas

imports Main

begin

(* 1ª demostración: automática *)

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: estructurada *)

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

(* 3º demostración: detallada *)

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

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

José A. Alonso

6 Comentarios

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 
  have 1: "R(a, a)" 
    using assms(1) by (rule allE)
  show "∀y. R (a, y) ⟶ R (y, a)"
  proof (rule allI) 
    fix b 
    have "∀ y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)" 
      using assms(2) by (rule allE)
    then have "∀ z. R(a, a) ∧ R(a, z) ⟶ R(z, a)" 
      by (rule allE) 
    then have 3: "R(a, a) ∧ R(a, b) ⟶ R(b, a)" 
      by (rule allE) 
    show " R (a, b) ⟶ R (b, a)"
    proof (rule impI) 
      assume 2: "R(a, b)" 
      have "R(a, a) ∧ R(a, b)" 
        using 1 2 by (rule conjI) 
      with 3 show "R(b, a)" 
        by (rule mp) 
    qed
  qed
qed

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

have 1: "R(a, a)"

using assms(1) by (rule allE)

show "∀y. R (a, y) ⟶ R (y, a)"

proof (rule allI)

fix b

have "∀ y z. R(a, y) ∧ R(y, z) ⟶ R(z, a)"

using assms(2) by (rule allE)

then have "∀ z. R(a, a) ∧ R(a, z) ⟶ R(z, a)"

by (rule allE)

then have 3: "R(a, a) ∧ R(a, b) ⟶ R(b, a)"

by (rule allE)

show " R (a, b) ⟶ R (b, a)"

proof (rule impI)

assume 2: "R(a, b)"

have "R(a, a) ∧ R(a, b)"

using 1 2 by (rule conjI)

with 3 show "R(b, a)"

by (rule mp)

qed

Responder

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)"
proof (rule allI)
  fix a
  show "∀y. R(a,y)⟶R(y,a)"
  proof (rule allI)
    fix b
    show "R(a, b) ⟶ R(b, a)"
    proof (rule impI)
      assume 1: "R(a, b)"
      have "R(a, a)" 
        using assms(1) by (rule allE)
      then have 2: "R(a,a) ∧ R(a,b)" 
        using 1 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, a) ∧ R(a, z) ⟶ R(z, a)" 
        by (rule allE)
      then have "R(a, a) ∧ R(a, b)⟶ R(b, a)" 
        by (rule allE)
      then show "R(b, a)" 
        using 2 by (rule mp)
    qed
  qed
qed

end

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)"

proof (rule allI)

fix a

show "∀y. R(a,y)⟶R(y,a)"

proof (rule allI)

fix b

show "R(a, b) ⟶ R(b, a)"

proof (rule impI)

assume 1: "R(a, b)"

have "R(a, a)"

using assms(1) by (rule allE)

then have 2: "R(a,a) ∧ R(a,b)"

using 1 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, a) ∧ R(a, z) ⟶ R(z, a)"

by (rule allE)

then have "R(a, a) ∧ R(a, b)⟶ R(b, a)"

by (rule allE)

then show "R(b, a)"

using 2 by (rule mp)

qed

end

Responder

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)"
proof (rule allI)
  fix a
  show "∀y. R(a, y) ⟶ R(y, a)"
  proof (rule allI)
    fix b
    show "R(a, b) ⟶ R(b, a)"
    proof (rule impI)
      assume "R(a, b)"
      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)
      have "R(b,b)" 
        using assms(1) by (rule allE)
      with ‹R(a,b)› have "R(a, b) ∧ R(b, b)" 
        by (rule conjI)
      with ‹R(a, b) ∧ R(b, b) ⟶ R(b, a)› show "R(b,a)" 
        by (rule mp)
    qed
  qed
qed

lemma
  "⟦∀x. R(x, x);∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)⟧⟹∀x y. R(x, y) ⟶ R(y, x)"
  apply (rule allI)+
  apply (erule allE)+
  apply (rule impI)
  apply (erule mp)
  apply (erule conjI)
  apply assumption
  done

end

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)"

proof (rule allI)

fix a

show "∀y. R(a, y) ⟶ R(y, a)"

proof (rule allI)

fix b

show "R(a, b) ⟶ R(b, a)"

proof (rule impI)

assume "R(a, b)"

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)

have "R(b,b)"

using assms(1) by (rule allE)

with ‹R(a,b)› have "R(a, b) ∧ R(b, b)"

by (rule conjI)

with ‹R(a, b) ∧ R(b, b) ⟶ R(b, a)› show "R(b,a)"

by (rule mp)

qed

lemma

"⟦∀x. R(x, x);∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)⟧⟹∀x y. R(x, y) ⟶ R(y, x)"

apply (rule allI)+

apply (erule allE)+

apply (rule impI)

apply (erule mp)

apply (erule conjI)

apply assumption

done

end

Responder

theory Las_reflexivas_circulares_son_simetricas
imports Main
begin

lemma
  assumes reflexiva: "∀x. R(x, x)" and
          circular:  "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"
  shows   "∀x y. R(x, y) ⟶ R(y, x)"
proof (intro allI)
  fix a b
  show "R(a, b) ⟶ R(b, a)"
  proof (rule impI)
    assume "R(a, b)"
    have "R(b, b)" 
      using reflexiva by (rule allE)
    with `R(a,b)` have "R(a,b) ∧ R(b,b)" 
      by (rule conjI)
    from circular have "R(a, b) ∧ R(b, b) ⟶ R(b, a)" 
      by (erule_tac x="a" in allE,
          erule_tac x="b" in allE,
          erule_tac x="b" in allE) 
    then show "R(b,a)" 
      using `R(a,b) ∧ R(b,b)` by (rule mp)
  qed
qed

end

theory Las_reflexivas_circulares_son_simetricas

imports Main

begin

lemma

assumes reflexiva: "∀x. R(x, x)" and

circular: "∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)"

shows "∀x y. R(x, y) ⟶ R(y, x)"

proof (intro allI)

fix a b

show "R(a, b) ⟶ R(b, a)"

proof (rule impI)

assume "R(a, b)"

have "R(b, b)"

using reflexiva by (rule allE)

with `R(a,b)` have "R(a,b) ∧ R(b,b)"

by (rule conjI)

from circular have "R(a, b) ∧ R(b, b) ⟶ R(b, a)"

by (erule_tac x="a" in allE,

erule_tac x="b" in allE,

erule_tac x="b" in allE)

then show "R(b,a)"

using `R(a,b) ∧ R(b,b)` by (rule mp)

qed

end

Responder

lemma 
  "∀x. R(x, x)
   ⟹ ∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x) 
   ⟹ ∀x y. R(x, y) ⟶ R(y, x)"
  apply(rule allI)+
  apply(erule allE)+
  apply (rule impI)
  apply(erule mp)
  apply(rule conjI)
   apply assumption+
  done

lemma

"∀x. R(x, x)

⟹ ∀x y z. R(x, y) ∧ R(y, z) ⟶ R(z, x)

⟹ ∀x y. R(x, y) ⟶ R(y, x)"

apply(rule allI)+

apply(erule allE)+

apply (rule impI)

apply(erule mp)

apply(rule conjI)

apply assumption+

done

Responder

Solución en Lean:

variables (α : Type) (r : α → α → Prop)

theorem las_reflexivas_circulares_son_simetricas
   (refl : ∀ x, r x x)
   (circ : ∀ x y z, (r x y) ∧ (r y z) → (r z x))
   : (∀ x y, r x y → r y x) :=
assume x y,
assume h : r x y,
show r y x, from circ x y y (and.intro h (refl y))

variables (α : Type) (r : α → α → Prop)

theorem las_reflexivas_circulares_son_simetricas

(refl : ∀ x, r x x)

(circ : ∀ x y z, (r x y) ∧ (r y z) → (r z x))

: (∀ x y, r x y → r y x) :=

assume x y,

assume h : r x y,

show r y x, from circ x y y (and.intro h (refl y))

Responder

Soluciones con Isabelle/HOL

Otras soluciones

Share this:

6 Comentarios

Escribe un comentarioCancel reply