[Práctico 5] Ejercicio 7.8

[Práctico 5] Ejercicio 7.8

de Eliana Rosselli Orrico -
Número de respuestas: 3

Buenos días

Estuvimos intentando hacer el ejercicio 7.8 pero no logramos encarar la prueba por ningún lado. En primer lugar queríamos saber si el enunciado que planteamos para el lema es correcto:

Lemma ej7_8: forall (d d2: Memoria), v1 <> v2 /\ Execute PP_ej7 d d2 -> lookup d2 v2 = false /\ lookup d2 v1 = true.

Si es correcto, no supimos mucho cómo realizar la prueba. Intentamos usando inversión y nos empezó a quedar una prueba re larga que no pudimos terminar en ningún momento. Tienen alguna sugerencia sobre cómo realizar la prueba?

Gracias y saludos

En respuesta a Eliana Rosselli Orrico

Re: [Práctico 5] Ejercicio 7.8

de Carlos Luna -

Hola!

La demostración no es corta y sale esencialmente con inversiones, ya que la prueba gira en torno a la ejecución instanciada sobre  un programa particular. Hay que hacer las inversiones (sucesivas) y reflejar el efecto (las igualdades) donde corresponde (si usás inversion_clear no olvides reflejar las eventuales reescrituras no solo en el goal sino en las hipótesis involucradas; con la variante "in"). Sino pueden usar inversion para conservar las igualdades aunque los contextos crezcan. En alguna parte de la prueba se pueden usar ejercicios previos, como el 6.4 y el 6.5. La prueba seguramente termine con discriminate.

En resumen, con inversion la idea es "ir ejecutando el programa" paso a paso para demostrar la propiedad.

Saludos, Carlos


 

En respuesta a Carlos Luna

Re: [Práctico 5] Ejercicio 7.8

de Eliana Rosselli Orrico -
Gracias Carlos por la respuesta, con inversiones y los lemas del ejercicio 6 salió. Estamos intentando hacer la entrega pero no nos deja subir el archivo, dice que la entrega está retrasada por casi 1 año. 

Saludos