CFPTT: [Practico 2] Ejercicio 3.2

Hola estoy trancado en este ejercicio y no me sale:

Definition Irreflexiva := ~exists x:U, (R x x).

Definition Asimetrica := forall x y:U, (R x y) -> ~(R y x).

Lemma e32 : Asimetrica -> Irreflexiva.

Proof.

intro.

unfold not.

Qed.

Creo que esta bien planteado.

Me podrán tirar alguna ayuda de como seguir? No me sale.

Saludos.

Re: [Practico 2] Ejercicio 3.2

de Carlos Luna - sábado, 27 de agosto de 2022, 23:34

Hola Alejandro.

Fijate que para probar que es Irreflexiva la relación tendrías que probar False, sabiendo que es Asimétrica y que existe un elemento z tal que (R z z). La contradicción (False) surge entonces de esto último y de la aplicacion de Asimétrica para z como x e y.

Fijate si con esto te sale y sino volvé a escribir.

Saludos Carlos

Re: [Practico 2] Ejercicio 3.2

de Alejandro Sebastian Flocken Rodriguez - domingo, 28 de agosto de 2022, 11:43

Hola Carlos, no me sale, segun lo que me comentaste hice los siguiente:

Lemma e32 : Asimetrica -> Irreflexiva.
Proof.
intro.
unfold not.
absurd (exists z:U, (R z z)).
unfold not.
intro.
Qed.

Pero sigo con el FALSE, algo me esta faltando ver siempre termino en FALSE.

Se me ocurrió hacer apply (H z z). pero me da el error:

The reference z was not found in the current environment.

Se puede agregar la definición de la variable? Variable z : U.?

Igual no me sale

No se como sacarlo.

Saludos

Re: [Practico 2] Ejercicio 3.2

de Carlos Luna - domingo, 28 de agosto de 2022, 13:31

Hola Alejandro.

Veo que estás siguiendo otro camino de prueba. El error en el apply se debe a que no hiciste la eliminación del existe en la hipótesis, para que puedas usar esta información y aparezca tal elemento de tipo U. El absurd que usás es inncesario. Fijate en:

Lemma e32 : Asimetrica -> Irreflexiva.

Proof.

intro.

unfold not.

intro.

elim H0; intros w Hw. (* acá áplico la eliminación del existe; al elemento lo llamo w *)

apply (H w w); assumption. (* o directamente: exact (H w w Hw Hw). *)

Qed.

Saludos, Carlos