[Práctico 2] Ejercicio 10.7

[Práctico 2] Ejercicio 10.7

de Julian Tricanico Gadea -
Número de respuestas: 6

Buenas,

Para el lema L10_5 podríamos usar el lema L10_4 para la prueba de m = 0 si tuviésemos la conmutatividad de la suma.

Si tuviésemos inducción tendríamos que la prueba de la conmutatividad sería separar en los cuatro casos 0 y sucesor de n y m, y por ejemplo la prueba con n = 0 y m = S m' podría ser:

0 + s m' = s (0 + m') =* s (m' + 0) = s m' = s m' + 0

donde marqué con un asterisco el paso inductivo.

En coq con la definición en particular que tenemos de nat no me estaría saliendo el paso inductivo. Tal vez nunca va a salir así? jeje. Alguna idea?

En respuesta a Julian Tricanico Gadea

Re: [Práctico 2] Ejercicio 10.7

de Carlos Luna -

Hola Julián.

No te apures con esto. El tema 2 lo veremos el martes 16 y no involucra inducción, que incorporaremos recién a partir del tema 3.

Mas allá de esto, en los ejercicios es posible usar otros (por la pregunta del 10 L4 y L5), en general.

Saludos Carlos 

En respuesta a Carlos Luna

Re: [Práctico 2] Ejercicio 10.7

de Julian Tricanico Gadea -

Buenas, sabés que al final nunca pude con este ejercicio así que quería preguntar de nuevo, jeje. Creo que es mejor escribir en este mismo hilo que armar uno nuevo.


Primero, estoy bastante convencido que la conmutatividad en general no la voy a poder probar en la aritmética de Robinson, así que esa primer idea está descartada.


Luego, si trato de probarlo directamente siempre me quedan por probar cosas como:

Sum (S m) n = S (sum m n)

y no tengo idea qué hacer con el sucesor a la izquierda de la suma.

Probé unas cuantas ideas y no parecen funcionar en general. Se trancan en cuestiones similares a la anterior.

Saludos!

En respuesta a Julian Tricanico Gadea

Re: [Práctico 2] Ejercicio 10.7

de Carlos Luna -
Hola Julián.
Teniendo en cuenta la información que tenés para esta prueba (axiomas de la sección 10), una buena idea es comenzar aplicando elim (allNat Y), donde Y:nat sería el segundo parámetro de sum en este ejercicio. Esto se debe a que los axiomas analizan los casos para el segundo argumento de sum. 
El caso cuando Y=0 sale fácil (recordar que rewrite tiene la variante "in" para reescribir en las hipótesis).
En el otro caso, tendrás un existe con información necesaria para esta parte de la prueba. La hipótesis disc será útil acá.
Espero esto ayude y sino volvé a escribir.
Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 2] Ejercicio 10.7

de Julian Tricanico Gadea -
Tremendo, ahí salió, gracias!
Claramente lo estaba empezando mal el ejercicio. Y ahí me quedó mucho más clara la fuerza del casi-paso_inductivo que tiene este sistema.
Saludos!
En respuesta a Julian Tricanico Gadea

Re: [Práctico 2] Ejercicio 10.7

de Carlos Luna -

Me alegro!

El sistema permite trabajar con inducción y recursion, pero esto lo veremos en el módulo 4. Por ahora incluimos algunas definiciones para que vayan aprendiendo la base, antes de pasar a ver y usar otros conceptos.

Saludos Carlos