Buenas, tengo un par de dudas con respecto a esta parte.
Lo planteé de la siguiente manera:
Lemma ej53d : forall (mem: Memoria) (e1 e2: Valor), BEval mem (boolExpr e1) false -> ~ BEval mem (Not (And (boolExpr e1 (boolExpr e2))) true.
Esta bien asi? o se deberia probar tambien el caso en el que fueran expresiones generales del tipo BoolExpr (var,And,Not)?
La otra duda que tengo es sobre como probarlo, ya que al hacer intros tengo para probar False, y no veo como hacerlo.
Gracias, saludos.
Hola.
e1 y e2 deberían ser expresiones.
Lemma ej53d: forall (m: Memoria) (e1 e2: BoolExpr), BEval m e1 false -> ~ (BEval m (Not (And e1 e2)) true).
Para la prueba, luego de hacer intros te sugiero hacer inversiones en las hipótesis que corresponden a BEval ... Es importante que veas conceptualmente de donde sale la contracción para probar False.
La parte c) podría ser últil en la prueba.
Saludos, Carlos
Buenas,
En la clase de teorico de ayer le consulte a gustavo por este ejercicio y nos dimos cuenta que esta mal planteado ya que si BEval m e1 false entonces BEval m (Not (And e1 e2)) true.
Lo plantee de la siguiente manera y pude llegar a una prueba:
Lemma ej53d: forall (m: Memoria) (e1 e2: BoolExpr), BEval m e1 false -> (BEval m (Not (And e1 e2)) true).
Es correcto el planteo?
Gracias, saludos
