Buenas. Estoy trancado con esta prueba.
Buscan en el foro encontre que se debia iniciar con induccion en e. Haciendo eso pude probar los casos base var y bool, pero quede trancado en los casos and y not.
Esta es la situacion en la que estoy.
Alguna ayuda?
De paso quería consultar sobre el 5.3.d, ese también sale con induccion?
gracias
saludos
Hola Agustin.
Luego de hacer intros H1 H2 tendrías que hacer inversión en H1 y H2, ya que BEval se define inductivamente y está instanciada en contructores (be_and). Una forma simplificada sería:
inversion_clear H1 in IHe1 IHe2; inversion_clear H2 in IHe1 IHe2; auto.
Notar que hago "in IHe1 IHe2" ya que al instanciarse w1 y w2 con la inversión, los valores se reescriben en estas hipótesis, donde aparecen. Una alternativa es no usar "in ..." pero luego será necesario hacer las reescrituras a mano y en este caso no deberías usar la variante inversion_clear, ya que no deja las igualdades en el contexto (usar en este caso inversion). La táctica auto realiza el trabajo simple restante; podrías sacar auto para ver los casos que se generan y tratar de probarlos a mano también.
El caso del not es similar pero más simple, asi que te lo dejo a vos.
Saludos, Carlos
Si aplicaste todo lo que puse tal cual (incluido el "auto"), estas obligaciones de prueba se deberían haber probado a partir de las hipótesis induuctivas. Sino, deberían salir de las hipótesis inductivas que tendrían que tener instanciados los valores booleanos w1 y w2.
Sino, poné por acá todas las tácticas que aplicaste en el caso del and, y el contexto que te aparece para probar estas obligaciones de prueba.
Saludos, Carlos
Hola.
La diferencia que veo es que tenés cuantificadas w1 y w2 en las hipótesis inductivas; por eso no se instancian al hacer lo que te dije. Tendría que ver el archivo para ayudarte, si con esta observación no lográs sacarlo vos. Si no te sale mandame el ejercicio a cluna@fing.edu.uy.
Saludos, Carlos