CFPTT: [Práctico 2] Ejercicios para entregar

El enlace al práctico 2 indica que hay que entregar los ejercicios 2.2, 2.3, 2.5, 2.7, 2.8 y 2.10.

La plantilla contiene los ejercicios 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.9, 2.10 y 2.11.

Es decir, si nos guíamos por la instrucción del enlace, en la plantilla "sobran" los ejercicios 2.1, 2.4, 2.6, 2.9, y 2.11, y estaría faltando el ejercicio 2.8.

¿O a lo mejor está mal la indicación? ¿Cuáles son los ejercicios que hay que entregar?

Ya aprovecho el espacio para hacer una consulta sobre el ejercicio de tácticas. Dice que hay que demostrar en una sola linea, pero por ejemplo tomando una prueba cualquier y reemplazando todos los puntos por punto y coma se consigue una prueba igual pero que se hace "de una". En fin, quería algún detalle más sobre los requerimientos, o qué se espera en la resolución de ese ejercicio.

Saludos.

Re: [Práctico 2] Ejercicios para entregar

de Carlos Luna - martes, 27 de agosto de 2019, 10:56

Hola Juan Manuel.

En la plantilla hay más ejercicios que los que se piden entregar (2.2, 2.3, 2.5, 2.7, 2.8 y 2.10). Si quieren pueden sacar los que no entreguen en el momento del envío. Respecto al 2.8, la idea es que ustedes los agreguen a la plantilla, ya que hay elementos a formalizar. La pregunta referida a 8.3 pueden responderla como un comentario en el archivo: (*...*)

Sobre la consulta de tácticas: si, en algunos casos podés reemplazar ";" por ".". La idea es que en estas pruebas haya solo un "." al final (a esto refiere en realidad el demostrar en una línea). Hay que tener presente que algunas tácticas generan más de un subgoal y en estos casos habría que usar, por ejemplo, el patrón: t1 ; [ t2 | t3 ], si al aplicar t1 se generan dos subgoals y sobre cada uno de ellos se quieren aplicar tácticas distintas (t2 y t3 en este caso). Si al aplicar t1 se generaran dos o más subgoals y sobre todos ellos se quisiera aplicar una misma táctica t2, entonces simplemente se escribiría t1;t2.

Saludos, Carlos

Re: [Práctico 2] Ejercicios para entregar

de Juan Manuel Rivara De Leon - domingo, 1 de septiembre de 2019, 15:48

Hola, tengo otra consulta. Cuando uno tiene el objetivo f(x) = f(y) y quiere probarlo a partir de x = y, uno puede usar apply f_equal para transformar el objetivo f(x) = f(y) en x = y. No he visto esta funcionalidad en las notas, la consulta es si esta táctica está permitida o hay otra forma de tratar de deducir la igualdad de aplicaciones de predicados o funciones a partir de la igualdad del predicado o función y los argumentos.

Saludos.

Re: [Práctico 2] Ejercicios para entregar

de Carlos Luna - domingo, 1 de septiembre de 2019, 20:02

Hola Juan Manuel.

Si, pueden usar ésta y otras tácticas de Coq. En el curso vemos solo algunas que alcanzan para desarrollar determinados temas, pero pueden ir más allá de esto y aplicar otras tácticas de Coq. En el caso de tácticas automáticas (como auto), pueden usarlas en los ejercicios en los que está permitido. En los siguientes prácticos podrán usarlas, una vez que entiendan bien/mejor qué es lo que hacen y cómo se puede hacer una prueba sin ellas.

En el caso de la igualdad, si H: x=y, el goal también se prueba con rewrite H; reflexivity.

Saludos, Carlos