[Practico 5] Ej 5.5

[Practico 5] Ej 5.5

de Geronimo Garcia Koch -
Número de respuestas: 2


Buen día,

Estoy queriendo probar el lemma pedido en la parte 5.5

Lemma e55 : forall (m : Memoria) (e : BoolExpr) (v : Valor),
  beval m e = v <-> BEval m e v.

Comencé la prueba por los distintos lados del iff, en ambos casos haciendo induccion sobre e y en ambos casos me tranco al momento de probar el paso inductivo de e = ~ e.

probando:  beval m e = v -> BEval m e v.

cfppt p5 1


probando: BEval m e v -> beval m e = v.

cfptt p5 2

Alguna idea de como continuar la prueba?

Mi idea es que tengo mal definidio o bien BEval o beval ya que la prueba no parece ser posible con esas hipotesis, adjunto las definiciones de las mismas pero al ser respuestas de practico entiendo si esto es editado luego

BEval not:
  match e with
    ...
  | enott  : forall (e : BoolExpr), BEval m e true ->
      BEval m (Not e) false
  | enotf  : forall (e : BoolExpr), BEval m e false ->
      BEval m (Not e) true.
  end.
beval (m : Memoria) (e: BoolExpr) : Valor :=
   match e with
     ...
   | Not e1    => match (beval m e1) with
                    true  => false
                  | false => true
                  end
   end.

Gracias!

En respuesta a Geronimo Garcia Koch

Re: [Practico 5] Ej 5.5

de Carlos Luna -

Hola.

El lema a probar lo plantearía así (y no como un iff):

Lemma e55 : forall (m : Memoria) (e : BoolExpr), BEval e m (beval m e)

Lo que planteás para la función beval en el caso del negado es correcto. 

En lo que ponés para BEval: "BEval not: match e with ..." no me queda claro el uso del match. Al ser una definición inductiva va un constructor por cada caso pero sin match. 

Saludos, Carlos 


En respuesta a Carlos Luna

Re: [Practico 5] Ej 5.5

de Geronimo Garcia Koch -

Error de formateo al escribir el post, la definicion es

BEval (m : Memoria) : BoolExpr -> Valor -> Prop :=
    evar : ...
  | eboolt : ...
    ...

Los casos del not son los dados arriba, antes de eso estan las demás definiciones dadas en el práctico.

Voy a probar con cambiar el Lemma a lo dado, pero no sería similar lo planteado? (O al menos ser capaz de probar el iff?)


Gracias!

Edit: La demostración del lemma como lo planteaste tu salió, muchas gracias