[Practico 6] Ej 3.1

[Practico 6] Ej 3.1

de Damian Augusto Langone Fusari -
Número de respuestas: 7

Buenas,

En esta parte uso de testigo (beval1 e) pero me tranco cuando hay que probar (band e1 e2 true). Aplico constructor y se  me generan dos goals para probar, BEval e1 true y BEval e2 true. Para el primero la prueba sale, pero para el segundo las hipotesis no me alcanzan para probarlo. Me queda lo siguiente:

5 subgoals

e1, e2 : BoolExpr

e3 : beval1 e1 = true

e4 : beval2 e2 = true

IHv : BEval e1 (beval1 e1)

______________________________________(1/5)

BEval e2 true

Es correcto llegar a este punto? 

Gracias

En respuesta a Damian Augusto Langone Fusari

Re: [Practico 6] Ej 3.1

de Carlos Luna -

Hola.

No parece ser un punto adecuado para probar el goal.

Cómo estás realizando la prueba?

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Practico 6] Ej 3.1

de Damian Augusto Langone Fusari -
Hola

Hago lo siguiente:

Intros.

Exists (beval1 e).

Functional induction (beval1 e).

Constructor.

Constructor.

Rewrite e3 in IHv.

Assumption.


Lo pude probar pero sin usar el testigo beval1 e, no veo como empezar de otra manera utilizandolo.

En respuesta a Damian Augusto Langone Fusari

Re: [Practico 6] Ej 3.1

de Carlos Luna -

Hola

No entiendo el comentario "Lo pude probar pero sin usar el testigo beval1 e". Lo estás usando! Estás probando el existencial, dando como testigo en cada caso al resultado de beval1, con: exists (beval1 e).

Luego al hacer la prueba usando la información (inductiva) de la función la función (con: functional induction (beval1 e)), vas probando cada caso siguiendo el flujo de la función, usando en cada caso las hipótesis que se generan. Al poner los constructores de BEval en Hint se logra que algunos casos se generan, se prueben automáticamente al usar auto.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Practico 6] Ej 3.1

de Damian Augusto Langone Fusari -

Hola Carlos,

Con las tacticas que puse en el mensaje anterior, llego a lo que puse en el primer mensaje, que no lo logro probar. Para probarlo me estaria faltando una hipotesis de la forma :

BEval e2 (beval2 e2)


Lo que dije que pude probar sin usar el testigo (beval1 e) es porque lo hice de esta manera:

intros.

induction e.

induction b.

exists true.

constructor.

exists false.

constructor.

inversion IHe1.

inversion IHe2.

case x in H.

case x0 in H0.

exists true.

constructor; assumption.

exists false.

constructor 3; assumption.

exists false.

constructor; assumption.

inversion IHe.

case x in H.

exists false.

constructor.

assumption.

exists true.

constructor.

assumption.

Pero la letra pide utilizando como testigo (beval1 e), por lo tanto no seria correcto.

Saludos

En respuesta a Damian Augusto Langone Fusari

Re: [Practico 6] Ej 3.1

de Carlos Luna -

Hola.

A ver si podemos aclarar las cosas...

En este ejercicio se piden dos pruebas de corrección, una de beval1 y otra de beval2. Se pide ver que ambos programas satisface la relación (especificación) BEval.

Lemma beval1C : forall e:BoolExpr, {b:Value | (BEval e b)}.

Lemma beval2C : forall e:BoolExpr, {b:Value | (BEval e b)}.

En el primer lema la idea es usar beval1 y en el segundo beval2. Para ello se sugiere usar exists (bevali e) al inicio y luego functional induction sobre dicha función (donde bevali es beval1 o bevial2, según el lema). Ver un mail mio previo sobre cómo probar usar functional induction.

Saludos, Carlos


 

En respuesta a Carlos Luna

Re: [Practico 6] Ej 3.1

de Andres Fulloni Papaleo -

Hola Carlos,

Entendemos lo que decis, y hemos seguido esos pasos. De hecho la prueba para (beval2 e) salió usando rewrite con las hipótesis. Pero el problema con la prueba que usa exists (beval1 e) es que nos falta la hipótesis BEval e2 (beval1 e2) para resolver el goal BEval e2 true.

Viendo la letra, se define beval1 de la siguiente forma:

Fixpoint beval1 (e : BoolExpr) : Value :=
                                                           match e with
                                                             | bbool b => b
                                                             | band e1 e2 =>
                                                                                     match beval1 e1, beval2 e2 with
                                                                                         | true, true => true
                                                                                         | _, _ => false
                                                                                     end
                                                              | bnot e1 => if beval1 e1 then false else true
                                                            end

Puede ser que en el segundo match, en vez de decir beval2 e2 tendría que decir beval1 e2? Porque de esa forma sí aparece la hipótesis faltante y sale la prueba.

Gracias.