Hola, la verdad que se me complico pila para arrancar con estos ejercicios. No logro que me ande nada en el CoqIde. Busqué en internet pero no logro dar en la tecla, la verdad.
¿Alguien se anima a darme algún ejemplo o algún link con ejemplos que corran bien en el CoqIde sin mayores ajustes para poder comprender bien?
Muchas gracias !
Hola,
Antes que todo importá Classical:
Require Import Classical.
Y probá con este comienzo para el 8.1:
Lemma ej8_1 : forall A, ~~A -> A.
Proof.
intros HnnA.
elim (classic A).
intros HA; assumption.
...
Se puede hacer la prueba en forma más compacta, pero de este manera pienso que te puede ayudar a ver como pueden salir las mismas.
Saludos,
Gustavo
Perdón, el fragmento de prueba tal cual lo mandé queda ok si el goal es
~~A -> A y A: Prop está declarada.
Para forall A, .... usar intros, o intros PA HnnPA.
Saludos,
Gustavo
Hola, una consulta sobre este ejercicio. Las pruebas se tienen que hacer como están en plantilla: Theorem e81: ~~A->A. ? O con forall?
Gracias.
Hola.
Como prefieras. De las dos formas está bien.
Saludos, Carlos
