[Práctico 4] Ejercicio 17

[Práctico 4] Ejercicio 17

de Marco Nicolas Rodriguez Alvariza -
Número de respuestas: 4

Hola,

Tres dudas sobre este ejercicio.

Para probar que l1 << l2 /\ l2 << l1 -> l1 = l2, tuve que usar un resultado que se pide demostrar después (l1 << l2 /\ l2 << l3 -> l1 << l3). A los efectos de la entrega, ¿se puede hacer esto?

Luego, hice inducción en l1 << l2. Para el caso inductivo me aparecían dos hipótesis contradictorias

H1 : l1 << l2
H2 : cons A a l2 << l1

Tuve que definirme tres lemas auxiliares para llegar a un absurdo sobre los largos de las listas. La segunda duda es si hay un camino más sencillo para la prueba.

La última duda es sobre la parte de demostrar que "ultimo l << l". Lo único que se me ocurre es una prueba por inducción en l, pero en el caso inductivo hay que probar "ultimo (cons a l) << cons a l" a partir de "utlimo l << l" y ahí me quedé sin ideas. ¿Hay algún otro camino?

Saludos,

Nicolás

En respuesta a Marco Nicolas Rodriguez Alvariza

Re: [Práctico 4] Ejercicio 17

de Carlos Luna -

Hola Nicolás.

Voy en orden sobre tus preguntas.

Si, se puede. Sobre si hay un camino alternativo más corto, si también. En casos como este suele ser últil hacer inducción sobre hipótesis que tengan relaciones inductivas (posfijo), en vez de hacer inducción sobre los argumentos (listas). Por ejemplo, posfijo es una relación entre listas; si se hace inducción en una hipótesis de tipo posfijo se restringe la prueba a listas que exclusivamente estén en la relación, algo que sería diferente si se hace inducción en las listas que intervienen (supongo que esto lo vieron con Gustavo en el teórico). En este ejercicio se usan otros lemas del práctico (como por ejemplo el L10) y pueden definirse lemas auxiliares también. No hay una manera única de hacer la prueba.

Respecto a la consulta sobre el ejercicio que vincula a la función ultimo, el encare que seguiste es adecuado. Donde te quedaste sin ideas deberías mirar como está definida la función ultimo, ya que seguramente hacés un análisis de casos sobre l. Si es así, en la prueba deberías seguir una lógica similar (destruct, por ejemplo), para poder analizar los diferentes casos de la función y de esa manera poder demostrar la propiedad.

Saludos, Carlos   

 

En respuesta a Carlos Luna

Re: [Práctico 4] Ejercicio 17

de Marco Nicolas Rodriguez Alvariza -
Perfecto.

Sobre el último punto, no puedo utilizar la hipótesis inductiva.  Primero separo en casos según la lista. En el caso de lista no vacía, tengo el goal:

ultimo A (cons A a l) << cons A a l

Luego hago inducción en l. En el caso inductivo llego a

IHl : ultimo A (cons A a0 l) << cons A a0 l
______________________________________(1/1)
ultimo A (cons A a (cons A a0 l)) << cons A a0 l

Luego utilizo "simpl", buscando reducir "ultimo A (cons A a (cons A a0 l))" a "ultimo A (cons A a0 l)" (porque así definí la función "ultimo" para el caso "(cons A a (cons A a0 l))". De ese modo, aplicaría la hipótesis inductiva y terminaría la demostración.

Pero ocurre que "simpl" aplica dos betas reducciones y transforma el goal a

match l with
| nil _ => cons A a0 (nil A)
| cons _ _ _ => ultimo A l
end << cons A a0 l

En el manual no encontré una forma de hacer una sola beta reducción.

Saludos,
Nicolás
En respuesta a Marco Nicolas Rodriguez Alvariza

Re: [Práctico 4] Ejercicio 17

de Marco Nicolas Rodriguez Alvariza -

Pude resolverlo.

La idea fue demostrar el resultado siguiendo el esquema de la definición de la función "ultimo".

Primero hice inducción en la lista y luego en el caso inductivo (demostrar el lema para (cons A a l0) asumiendo que se cumple para l0) hice un análisis de casos para la lista l0.

En el medio tuve que demostrar que

ultimo A (cons A a (cons A a0 l1)) = ultimo A (cons A a0 l1)

para poder utilizar la hipótesis inductiva.

Saludos,

Nicolás