[Practico1][Ejercicios 7.1 en adelante]

[Practico1][Ejercicios 7.1 en adelante]

de Alejandro Sebastian Flocken Rodriguez -
Número de respuestas: 7

Hola, venia bien, me estaban saliendo todos hasta llegar al 7.1, de ahí en adelante no me sale ninguno.

(* Ej. 7.1 *)Theorem e71: A \/ ~A -> ~~A->A.

¿Podrían ayudarme de alguna manera?

¿Cambio la forma de hacerlos?

En los ejercicios 8.. hay que hacer intro para que se vaya el forall A y aparezca el A0?

Si alguien tiene algún material de donde leer me sirve.

Estoy re perdido.

Saludos


En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: [Practico1][Ejercicios 7.1 en adelante]

de Carlos Luna -

Hola Alejando.

En el ejercicio 7.1 tenés una disyunción como hipótesis luego de hacer un intro (digamos, H : A\/~A). En estos casos tenés que usar la información del \/ para probar el goal (hacer análisis de casos). Esto lo hacés con "eim H", que te va a generar dos obligaciones de prueba, teniendo en cada caso información sobre un lado de la disyunción. 

Por ejemplo, en el primer caso tendrías que probar A con una hipótesis con esto (trivial). 

En el segundo caso, si hacés todos los intros, tendrías que probar A también pero tendrías hipótesis sobre ~~A y ~A. Quizás el caso que se te esté complicando es este último. Hay varias formas de encararlo, por ejemplo usando la táctica cut a partir de estas hipótesis para sacar información intermedia para probar A (por ejempo: cut False). Otra opción interesante sería: "elim (H1 H2)", siendo H1 : ~~A y H2: ~A. Notar que H1 aplicado a H2 es False (teniendo en cuenta lo que comentamos ayer en la clase), asi que se estaría haciendo elim False, que prueba cualquier goal. Hay otras opciones también!

Sobre "En los ejercicios 8.. hay que hacer intro para que se vaya el forall A y aparezca el A0?": SI, es que lo que vimos ayer casi al final de la clase.

Espero que esto te ayude y sino, volvé a escribir.

Saludos, Carlos



En respuesta a Carlos Luna

Re: [Practico1][Ejercicios 7.1 en adelante]

de Alejandro Sebastian Flocken Rodriguez -
Hola Carlos, gracias por la respuesta, me quedaron las siguientes dudas:
Logre resolver el ejercicio de esta manera:

(* Ej 7.1 *)
Theorem e71: A \/ ~A -> ~~A->A.
Proof.
intro.
elim H.
trivial.
intro H1.
intro H2.
elim H2.
assumption.
Qed.


Ahora, vos me dijiste que haga elim(H1 H2) este comando no es válido no? Te referías a "elim H1. elim H2." o hice algo mal?
Otra duda, el elim H1 no me hacía nada así que lo saque. Que se supone que hace el elim H2? porque tengo:

1 goal
A, B, C : Prop
H : A \/ ~ A
H1 : ~ A
H2 : ~ ~ A
______________________________________(1/1)
A

Hago el elim H2 y me queda:

1 goal
A, B, C : Prop
H : A \/ ~ A
H1 : ~ A
H2 : ~ ~ A
______________________________________(1/1)
~ A

No entiendo por qué.

Por otro lado la sugerencia de hacer cut FALSE esta bien de esta forma?
Me quedo asi:

(* Ej 7.1a *)
Theorem e71a: A \/ ~A -> ~~A->A.
Proof.
intro.
elim H.
trivial.
intro H1.
intro H2.
cut False.
intro H3.
elim H3.
absurd (~A).
assumption.
assumption.
Qed.

La tactica absurd se puede sin importar que tenga que demostrar? Yo pensaba que se usaba solo cuando tenia un FALSE como en las diapositivas pero he visto en ejemplos en internet que tipo tienen que demostrar A y hacen absurd(B) y coq te lo toma como valido.

Como si hiciera esto:

1 goal
A, B, C : Prop
H : A \/ ~ A
H1 : ~ A
H2 : ~ ~ A
______________________________________(1/1)
A

(* Ej 7.1a *)
Theorem e71a: A \/ ~A -> ~~A->A.
Proof.
intro.
elim H.
trivial.
intro H1.
intro H2.
absurd (~A).
assumption.
assumption.
cut False.
intro H3.
elim H3.
absurd (~A).
assumption.
assumption.
Qed.

Siempre que no me salte error en coq significa que esta bien la demostracion?
No entiendo como si tengo que demostrar a puedo hacer absurd(Algo) y saltar a demostrar otra cosa.


Me doy cuenta que me falta saber tecnicas, por ejemplo los elim que yo hago son solo en los casos que estan en las diapositivas, la tecnica trivial no sabia de su existencia y cut False no se me habia ocurrido.

Saludos.
En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: [Practico1][Ejercicios 7.1 en adelante]

de Carlos Luna -

Hola.

Trataré de ir en orden, ya que tu mensaje tiene varias cosas.

La primera prueba usa "trivial" que es una táctica de demostración automática que por ahora preferimos no usen (como tatuo o auto).

En la segunda sería "elim (H2 H1)."

Hacer "elim H2." no es lo más claro, aunque parezca lo más simple. Mejor ir aplicando las tácticas vistas con las opciones propuestas, ya que estas (y otras) tácticas se aplican también en otros casos y realizan acciones más generales/avanzadas.

En la prueba que hiciste con cut podrías reemplazar: "absurd (~A). assumption. assumption." por "apply H2. assumption.", ya que de ello al hacer absurd pasa a ser innecesario el cut. Fijate que con absurd la prueba que estás intentando puede salir (por ejemlo) así:

intro. elim H.

intros. assumption. (* probar A es trivial ya que es una hipótesis en este caso *)

intros. absurd (~A). assumption. assumption. (* absurd (~A) pide probar ~~A y A, que son hipótesis en este caso *) 

Espero que estas respuestas te ayuden. Volvé a escribir si es necesario.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Practico1][Ejercicios 7.1 en adelante]

de Alejandro Sebastian Flocken Rodriguez -
Hola Carlos, aplicando tus recomendaciones me quedaron 3 pruebas distintas del ejercicio.

(* Ej 7.1 con elim (H2 H1) *)
Theorem e71: A \/ ~A -> ~~A->A.
Proof.
intro.
elim H.
intro H1.
intro H2.
assumption.
intro H1.
intro H2.
elim (H2 H1).
Qed.


(* Ej 7.1 con cut *)
Theorem e71b: A \/ ~A -> ~~A->A.
Proof.
intro H.
elim H.
intro H1.
intro H2.
assumption.
intro H3.
intro H4.
cut False.
intro H5.
elim H5.
apply H4.
assumption.
Qed.


(* Ej 7.1 otra profesor *)
Theorem e71c: A \/ ~A -> ~~A->A.
Proof.
intro.
elim H.
intros.
assumption. (* probar A es trivial ya que es una hipótesis en este caso *)
intros.
absurd (~A).
assumption.
assumption. (* absurd (~A) pide probar ~~A y A, que son hipótesis en este caso *)
Qed.

Hasta ahi excelente.

Me quedan 3 dudas:

1) En el primero, cuando voy asi:

1 goal
A, B, C : Prop
H : A \/ ~ A
H1 : ~ A
H2 : ~ ~ A
______________________________________(1/1)
A

Al final le aplico la ultima tactica que le aplico es elim (H2 H1). Como se lee esto? Que es lo que hace no entiendo. Las que estan como ejemplo en las diapositivas las entiendo, elimino la hipotesis y me cambia la prueba en base a la hipotesis que elimine pero esta no entiendo como se lee.

2) En el segundo cuando va:

1 goal
A, B, C : Prop
H : A \/ ~ A
H3 : ~ A
H4 : ~ ~ A
______________________________________(1/1)
False

luego le aplico apply H4. que nuevamente no entiendo eso, nuevamente el ejemplo de las diapos para una Hipotesis de tipo A -> B la entiendo pero esta no.

3) Por ultimo, simpre y cuando el coq me tome la demostracion como valida puedo hacer cualquier cosa?

Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: [Practico1][Ejercicios 7.1 en adelante]

de Carlos Luna -

Hola

1) ~X es X->False. Luego, "elim (H2 H1)" sería hacer el elim del resultado de la aplicación (H2 H1), como si fuera una función H2 aplicada a su argumento H1. Esto es, ~A->False aplicado a ~A es False. En consecuencia, se hace la eliminación de False (que prueba el goal).

2) Sale indirectamente de la expliación anterior. En H4 tenés ~~A. Esto es, ~A->False. Al hacer "apply H4." se hace la eliminación del implica con consecuente False y pide demostrar entonces el antecedente: ~A (que es la hipótesis H3)

3) Cualquier cosa, no :). Si bien Coq valida (chequea) cada paso de una prueba, no recomendamos probar cosas (empezar a combinar tácticas porque si) sin entender lo que están haciendo (más allá que alguna prueba salga), porque así no se aprende ni se escala luego a resolver cosas más interesantes/complejas (pasa lo mismo en la programación...).

Saludos, Carlos 

En respuesta a Carlos Luna

Re: [Practico1][Ejercicios 7.1 en adelante]

de Alejandro Sebastian Flocken Rodriguez -
Excelente Carlos, estoy volviendo a hacer todos los ejercicios pero en papel razonando las reglas.

Me podes explicar estas dos cosas:

1) La Tactica VII

H:False
---------- elim H Probado
A

Como es el razonamiento de esa.

2) Porque el ejercicio 4.6 que es (A \/ B) -> (B \/ A) no se puede resolver con " intro H0. exact(H0) " ? A \/ B no es lo mismo que B \/ A?


Saludos
En respuesta a Alejandro Sebastian Flocken Rodriguez

Re: [Practico1][Ejercicios 7.1 en adelante]

de Carlos Luna -
Hola

1) Viene de la lógica. De False se deduce cualquier cosa. En lógica clásica False->X es lógicamente válido (una tautologia), para todo X.

2) Aquí se está probando la conmutatividad del \/, no la igualdad. Por ejemplo el -> no es conmutativo (algunos conectivos lo son y otros no). El término de prueba para lasdos disyunciones no es el mismo, por eso exact no funciona en este caso.

Saludos