Buenas tardes
Realizando el ejercicio 5 del práctico, parte 3c, nos quedamos trancados en la prueba. El lema a demostrar es el que sigue.
forall (e: BoolExpr) (d: Memoria) (w1 w2: Valor), BEval e d w1 /\ BEval e d w2 -> w1 = w2.
Intentamos realizar la prueba haciendo case_eq en e, y logramos demostrar el caso de que e = be_var v (con v : Var) y el caso de que e = be_bool b (con b: bool), donde be_var y be_bool son dos de los constructores de BoolExpr. Nos quedamos trancados en la prueba para el caso del and, intentamos usar inversion pero no nos salio.
Es correcto este enfoque, o hay una forma mas directa de realizar la prueba? Si este es el enfoque correcto, agradecemos alguna ayuda para completar la prueba.
Ademas, nos surgió la duda en la parte d de si lo que se pide demostrar es correcto, creemos que no. Encontramos este link (https://eva.fing.edu.uy/mod/forum/discuss.php?d=129969) en el foro de otro año que plantea lo mismo asi que suponemos que el "no se da que" debe ser ignorado, pero queríamos confirmar.
Gracias y saludos
Eliana y Federico