[Práctico 5] Ej 5.3c

[Práctico 5] Ej 5.3c

de Andres Fulloni Papaleo -
Número de respuestas: 5

Buenas, este ejercicio lo planteé de la siguiente forma:

Lemma ej53c : forall (mem: Memoria) (e: BoolExpr) (w1 w2: Valor), BEval mem e w1 /\ BEval mem e w2 -> w1 = w2.

Para probarlo hice intros y luego inversion en H0. Luego, coq me exige una prueba para cada posible forma de e, o sea para e = varExp, e = boolExp, etc. El problema es que no he podido realizar la prueba para e = And e1 e2.

Llego a lo siguiente:

H : BEval mem e w1 /\ BEval mem e w2
H0 : BEval mem e w1
H1 : BEval mem e w2
e1, e2 : BoolExpr
H2 : BEval mem e1 false
H3 : And e1 e2 = e
H4 : false = w1
______________________________________(1/5)
false = w2


Alguna sugerencia de como seguir?

Gracias.

En respuesta a Andres Fulloni Papaleo

Re: [Práctico 5] Ej 5.3c

de Carlos Luna -

Hola.

La prueba no sale por inversion desde el inicio (recordar que inversion no sustituye a induction). La táctica inversion se usa cuando hay un predicado inductivo instanciado con constructores, esencialmente. Su efecto es generar las condiciones necesarias para la hipótesis sobre la cual se hace la inversion.

La prueba recomiendo iniciarla por inducción en la expresión e. Luego, en cada caso la táctica inversion será útil.

Un detalle en la formalización del lema. En vez de:

BEval mem e w1 /\ BEval mem e w2 -> w1 = w2.

Sugiero (que es equivalente):

BEval mem e w1 -> BEval mem e w2 -> w1 = w2.

De esta manera al hacer intros se tienen las hipótesis sobre BEval separadas.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 5] Ej 5.3c

de Andres Fulloni Papaleo -

Gracias Carlos, ahora me encaminé mejor. Aún así sigo teniendo problemas cuando me aparece (And e1 e2). No sólo en este ejercicio sino que en otros también. Por ejemplo si llego a algo asi: BEval mem (And e1 e2) w1, lo corrector seria hacer induction en w1 no?.

También me pasa en el ejercicio 5.5, llego a lo siguiente:

mem : Memoria
e1, e2 : BoolExpr
IHe1 : BEval mem e1 (beval mem e1)
IHe2 : BEval mem e2 (beval mem e2)
______________________________________(1/2)
BEval mem (And e1 e2) (beval mem (And e1 e2))

Probé hacer case_eq (beval mem (And e1 e2)) pero luego no veo como usar las hipótesis para probar los casos que se me generan.

Gracias.

En respuesta a Andres Fulloni Papaleo

Re: [Práctico 5] Ej 5.3c

de Carlos Luna -

Hola.

Dado que tenés un predicado inductivo (BEval) instanciado con un  constructor (And), podés hacer inversion y va a generar los casos. Si elegís la variante inversion_clear tenés que tener cuidado de instanciar las hipótesis que estén involucradas (usando la variante inversion_clear H in Hi Hj...). Si usás inversion como las igualdades quedan en el ambiente, luego podés hacer reescrituras.

En el segundo caso quizás te convenga hacer case_eq (beval mem e1) y eventualmente también para e2.

Saludos, Carlos


En respuesta a Carlos Luna

Re: [Práctico 5] Ej 5.3c

de Damian Augusto Langone Fusari -

Buenas, en el ejercicio 5.3.c (Lemma ej53c : forall (mem: Memoria) (e: BoolExpr) (w1 w2: Valor), BEval mem e w1 -> BEval mem e w2 -> w1 = w2.) llego a lo siguiente:

3 subgoals

mem : Memoria

e1, e2 : BoolExpr

IHe1 : forall w1 w2 : Valor, BEval mem e1 w1 -> BEval mem e1 w2 -> w1 = w2

IHe2 : forall w1 w2 : Valor, BEval mem e2 w1 -> BEval mem e2 w2 -> w1 = w2

w2 : Valor

H : BEval mem (And e1 e2) false

H0 : BEval mem (And e1 e2) w2

e0, e3 : BoolExpr

H2 : BEval mem e2 false

H1 : e0 = e1

H3 : e3 = e2

______________________________________(1/3)

BEval mem e1 false

______________________________________(2/3)

BEval mem e1 w2

______________________________________(3/3)

w1 = w2


Me parece que los pasos anteriores que hice son correctos, por lo que no veo como poder probar BEval mem e1 false con las hipotesis que tengo. Con las hipotesis H y H2 tengo que el en la memoria, el And de e1 y e2 es false y e2 es false tambien por lo que el valor de la memoria en e1 podria ser true o false, eso es correcto?


Gracias

En respuesta a Damian Augusto Langone Fusari

Re: [Práctico 5] Ej 5.3c

de Carlos Luna -

Hola.

En el contexo en el que estás no es demostrable el goal. Algo está mal o perdiste información en el camino...

Si están bien definidas las cosas una prueba como la que sigue debería andar:


Lemma parteC: forall (m: Memoria)(e: BoolExpr)(w1 w2: Valor), BEval m e w1 -> BEval m e w2 -> w1 = w2.

Proof.

induction e.

induction b; intros; inversion H; inversion H0; auto. (* expresiones booleanas *)

intros; inversion H; inversion H0; auto.  (* expresiones que son variables *)

intros; inversion H; inversion H0; auto.  (* expresiones And *)

intros; inversion H; inversion H0; auto.  (* expresiones Not *)

Qed.


Si no te sale, enviame todo lo que tenés definido para hacer esta parte y veo si hay algún error.  


Saludos, Carlos