Ejercicio 7

Ejercicio 7

de Pablo Palou Singlet -
Número de respuestas: 2

Buenas! 

En este ejercicio se pide que apliquemos tacticals para resolver los problemas en una linea. En el 7.1 con el uso de ; no tuve problemas. En el caso 7.2 y 7.3, se me genera el mismo incoveniente. El mismo es que tengo dos subgoals, las cuales necesitan pasos distintos para poder probarse, por lo que aplicar simplemente ; no funcionaria. En una de las subgoals necesito hacer left y en la otra right. Si yo quisiera hacer left || right, esto no funcionaria porque en ambas subgoals no falla hacer left. 

Luego los pasos son identicos en ambas, por lo que no deberia haber problemas. Como puedo hacer para resolver este incoveniente de en una linea hacer pruebas distintas segun la subgoal? 

Obviamente que al hacerlo en muchas lineas no hay ningun tipo de problemas. 

Segun vi en internet las tacticals son (;, or, all, repeat y try), quizas me este faltando alguna.

Saludos, Pablo Palou. 

En respuesta a Pablo Palou Singlet

Re: Ejercicio 7

de Pablo Palou Singlet -
Ya encontre como resolverlo. Adjunto link por si a alguno le pasa lo mismo https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#tacticals .
En respuesta a Pablo Palou Singlet

Re: Ejercicio 7

de Carlos Luna -

Ok Pablo.

Tener presente entonces que el ";" permite hacer la composición de tácticas. Por ejemplo, t1;t2 aplica t2 a cada subgoal generado luego de aplicar t1. Ahora, supongamos que al aplicar t1 al goal actual se generan dos subgoals; si se pone t1;[t2|t3];t4 el efecto que es que luego de aplicar t1 se aplica t2 al primer subgoal generado y t3 al segundo. En ambos casos se aplicaría t4 al final.  

Saludos, Carlos