CFPTT: Dudas sobre el lenguaje de tácticas

Hola, tengo algunas dudas sobre el lenguaje de tácticas, agradezco si me pueden responder.

Con respecto al constructor de expresiones expr := [> expr_1 | .. | expr_n]

->En la referencia (https://coq.inria.fr/refman/proof-engine/ltac.html?highlight=repeat#local-application-of-tactics) dice que aplica expr_i al Goal_i. Con Goal_i se refiere al i-ésimo Goal que figura en el momento previo a ejecutar el comando no?

->Cual es la diferencia con el constructor [expr_1 | .. | expr_n]?

-> Con respecto a repeat expr dice:

expr is evaluated to v. If v denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the tactic is applied recursively to all the generated subgoals until it eventually fails. The recursion stops in a subgoal when the tactic has failed to make progress. The tactic repeat expr itself never fails.

Que serían los focused goals? Con hacer progreso se refiere a que la táctica aplique al caso no?, es decir, que el compilador no se queje. No?

Saludos

Damián

Re: Dudas sobre el lenguaje de tácticas

de Carlos Luna - lunes, 26 de agosto de 2019, 18:03

Hola Damian.

Supongo que algo de esto verán en las clases teóricas.

Trato de responder tus consultas:

1) ->En la referencia (https://coq.inria.fr/refman/proof-engine/ltac.html?highlight=repeat#local-application-of-tactics) dice que aplica expr_i al Goal_i. Con Goal_i se refiere al i-ésimo Goal que figura en el momento previo a ejecutar el comando no?

2) ->Cual es la diferencia con el constructor [expr_1 | .. | expr_n]?
Supongamos que al aplicar una táctica t1 al goal actual se general 2 subgoals. Si se pone t1 ; [ t2 | t3 ] el efecto que es que luego de aplicar t1, se aplica t2 al primer subgoal generado y t2 al segundo.

3) Que serían los focused goals? Con hacer progreso se refiere a que la táctica aplique al caso no?, es decir, que el compilador no se queje. No?

Por defecto el el primer subgoal, aunque es posible extender el alcance. El progreso refiera a que aplique y genere un resultado diferente al inicial.

Saludos, Carlos

Re: Dudas sobre el lenguaje de tácticas

de Damian Ferencz - martes, 27 de agosto de 2019, 00:27

Hola Carlos,

Gracias por las respuestas.

Solo para asegurarme:

->Cuando decís ... se aplica t2 al primer subgoal generado y t2 al segundo. , quisiste poner ... y t3 al segundo?

-> t1 ; [ t2 | t3 ] es lo mismo que [t1 | t2 | t3 ]?

Saludos

Damián

Re: Dudas sobre el lenguaje de tácticas

de Carlos Luna - martes, 27 de agosto de 2019, 07:00

Hola.

Si, perdón, quise decir t3 al segundo:

Si se pones t1 ; [ t2 | t3 ] el efecto que es que luego de aplicar t1 al goal actual, se aplica t2 al primer subgoal generado y t3 al segundo.

Saludos, Carlos

Re: Dudas sobre el lenguaje de tácticas

de Damian Ferencz - martes, 27 de agosto de 2019, 18:48

Ahora entendí. Si hicieras t1; t2 se aplicaría t2 a los dos subgoals generados. t1; [t2 | t3] es la manera de generar estrategias distintas para los dos subgoals. Mi mayor obstáculo se debía a que pensaba que [t2 | t3] era una expresión por sí sola.

Voy con otra: En el ejercicio 'Lemma L10_2: forall n :nat, ~(O=n /\ (exists m :nat, n = (S m))).' quiero aplicar la reescritura S n = S m teniendo n = m en el contexto, es decir, transformar mi goal G(S n) en G(S m). Me vi forzado a usar la regla 'cut S n = S m' . Es la mejor forma? O hay algun atajo?

Saludos Damián

Re: Dudas sobre el lenguaje de tácticas

de Carlos Luna - miércoles, 28 de agosto de 2019, 22:56

Hola Damián.

No entiendo en qué contexto tenés n=m para esta prueba. No obstante, según lo que describís, si en tu goal aparece G(S n) y tenés en tus hipótesis n=m, aplicas rewrite.

Si querés enviame tu prueba y veo bien lo que decís, ya que quizás te referís al axioma inj, que no se precisa en este ejercicio.

No obstante, no está mal usar cut, generando pasos/resultados intermedios en una prueba.

Saludos, Carlos