[Practico 2] Ejercicio 10.5

[Practico 2] Ejercicio 10.5

de Bruno Rolando Boz -
Número de respuestas: 3

Buenas, 

Haciendo algunos reemplazos en secuencia en este ejercicio. Se me generan múltiples sub-goals que son idénticas.

¿Hay alguna forma de "eliminar" las sub-goals repetidas? 

Por ahora venia encadenando los replace con try reflexivity. Eso me elimina las que se prueban con reflexivity (la mayoría), además, podría encadenar con try symmetry; try apply... De esta manera pruebo todo (salvo 1 sub-goal) pero no parece una manera muy prolija, sin contar que symmetry modifica la única sub-goal que me debería quedar al final. 


Saludos.


En respuesta a Bruno Rolando Boz

Re: [Practico 2] Ejercicio 10.5

de Carlos Luna -

Hola Bruno.

Sugiero razonar primero la idea de la prueba antes de intentar aplicar tácticas, ya que sino pueden llegar a generar casos innecesarios, repetidos o incluso entrar en caminos de prueba medio circulares. Esto es, el objetivo ahora no tendría que ser como eliminar sub-goals repetidos, sino como evitar que se generen sub-goals innecesarios.

En este ejercicico, observar que la prueba es sobre sum, y que sum0 y sumS aportan información cuando está instanciado el segundo argumento; luego una buena idea puede ser empezar la prueba con elim (allNat Y), donde Y:nat es el segundo argumento de sum. El primer caso (donde Y=0) sale fácil y en el segundo se genera un exists; acá hay que usar esta información, hacer reescritura y se puede usar absurd para emplear luego disc.

Saludos, Carlos  


En respuesta a Carlos Luna

Re: [Practico 2] Ejercicio 10.5

de Bruno Rolando Boz -
Intente la demostración sugerida y se me complico. Quizás no la entendí bien. Voy a aprovechar una próxima clase para consultar.

De todos modos, habiendo pensado la prueba de antemano y descubriendo que el m era el mismo para todo n, me resultaba mas intuitivo hacer directamente el exists. Después me quedaba una cadena de remplazos y cada reemplazo me generaba una nueva meta. Termine resolviendo el problema de la creación de sub-metas seleccionando la meta que quería resolver primero. Me quedo una demostración corta (8 líneas) y fácil de seguir.

Edito: En todo momento me refiero al Lemma L10_3 que es el ejercicio 10.5. Aclaro porque me parece (ahora que voy por el ej.7) que la respuesta apuntaba a la resolución del Lemma L10_5 que es el ejercicio 10.7. 

Saludos. 
En respuesta a Bruno Rolando Boz

Re: [Practico 2] Ejercicio 10.5

de Carlos Luna -

Hola.

Tenés razón, yo me refería al lema L10_5 :)

Me alegro que te haya quedado entonces una prueba fácil de seguir. Aquí la clave es la eleccón del testigo del exists, ya que luego (como vos decís) se resuelve esencialmente con reemplazos de prodS, prod0 y sum0.

Saludos, Carlos