Práctico 5 - Ejercicio 5.3.c

Práctico 5 - Ejercicio 5.3.c

de Noelia Magali Lencina Alfonso -
Número de respuestas: 2

Hola,

En este ejercicio tengo Lemma e5_3c : forall (m:Memoria) (w1 w2:Valor) (e:BoolExpr), BEval e m w1 -> BEval e m w2 -> w1 = w2 para probar.

Haciendo inducción y luego inversion en cada caso me pasa que para los casos correspondientes a las expresiones con And y las con Not tengo que probar false = true. Automáticamente Coq parece que no se da cuenta de que esto es falso, y para probarlo lo único que se me ocurre es llegar a una contradicción. En las hipótesis tengo dos BEvals de la misma expresión en la misma memoria que evalúan a cosas distintas, y me da la sensación de que eso es algo que debería usar para llegar al absurdo de alguna forma pero no lo logro.

Estoy agarrando por el camino correcto? Alguna ayuda para destrancarme?

Gracias y saludos,

Noelia

En respuesta a Noelia Magali Lencina Alfonso

Re: Práctico 5 - Ejercicio 5.3.c

de German Adolfo Faller Farias -

Te puedo decir que cuando tenes que demostrar true=false, es lo mismo que probar la proposición False. Ahí tenes razón, la única manera de demostrarlo es que tengas una contradicción en las hipótesis, pero ten en cuenta que una contradicción puede ser una hipótesis que no se puede construir (ej. even 1), en ese caso con inversion en la hipótesis probarías cualquier cosa.

Con respecto a ese ejercicio en particular, yo lo demostré de una manera y después revisando el foro encontré un hilo donde lo soluciona, si queres leerlo seria, https://eva.fing.edu.uy/mod/forum/discuss.php?d=111894

 Si no queres leerlo; básicamente es hacer inducción en e é inversion sobre las dos hipótesis (BEval e m w1 Y  BEval e m w2).

Saludos!

G.

En respuesta a German Adolfo Faller Farias

Re: Práctico 5 - Ejercicio 5.3.c

de Carlos Luna -

Hola.

Si, hacer inducción en la expresión es necesario. En cada caso será necesario utilizar la táctica inversion (o inversion_clear) para usar la información de las relaciones inductivas BEval que quedan instanciadas. También es posible usar inversion ... in ... En diferentes casos será útil también rewrite ... in ...

La prueba podría comenzar, por ejemplo, con:

  intros mem exp w1 w2 H1 H2.

  induction exp; inversion H1; inversion H2; auto.

Saludos, Carlos