(* Ej 7.3 *)
Theorem e73: (A \/ ~A) -> ~(A /\ B) -> ~A \/ ~B.
Alguien me puede dar una mano con esto?
O me falta algo muy importante o cometo un error muy obvio.
Empiezo haciendo unfold not.
y luego hago intros y elim... pero nunca alcanzo goal.
Alguna pista???
Hola Pablo.
El unfold y los intros para agregar hipótesis al contexto están bien.
el elim entiendo que es de la hipótesis con A\/~A. De aquí se generan dos obligaciones de prueba: una con hipótesis A y otra con ~A.
En el primer caso (teniendo A) para probar el or deberías tratar de probar ~B (esto es, elegir right). Al hacer unfold de ~B y luego intro la situación es que deberías probar False, pero vas a tener como hipótesis tanto A como B. Acordate que tenés la hipótesis con ~(A /\ B). Esto es: (A /\ B) -> False. Te dejo a vos el resto de la prueba en este caso.
En el segundo caso (teniendo ~A) para probar el or del goal es muy simple!
Espero que te sirva, sino volvé a escribir.
Saludos, Carlos
Hola Pablo.
El unfold y los intros para agregar hipótesis al contexto están bien.
el elim entiendo que es de la hipótesis con A\/~A. De aquí se generan dos obligaciones de prueba: una con hipótesis A y otra con ~A.
En el primer caso (teniendo A) para probar el or deberías tratar de probar ~B (esto es, elegir right). Al hacer unfold de ~B y luego intro la situación es que deberías probar False, pero vas a tener como hipótesis tanto A como B. Acordate que tenés la hipótesis con ~(A /\ B). Esto es: (A /\ B) -> False. Te dejo a vos el resto de la prueba en este caso.
En el segundo caso (teniendo ~A) para probar el or del goal es muy simple!
Espero que te sirva, sino volvé a escribir.
Saludos, Carlos
