Buenas, estamos trancados en la demostración del lemma, llegamos a tener en las hipótesis MemL x nullL y False como goal, pero no podemos concluir la demostración.
No logramos darnos cuenta de cómo seguir, ¿alguna sugerencia?
Saludos.
Hola.
Si tienen en las hipótesis H: MemL x nullL, entonces inversion H debería probar el goal. N.o hay constructor asociado a Mem para la lista vacía, luego inversion H se comporta como elim False.
Saludos, Carlos
Muchas gracias, en realidad lo que nos pasa es que al hacer inversion quedamos trancados ya que al haber hecho inducción en l para llegar al goal anterior luego nos resta probar con las hipótiesis H : MemL x (deleteAll x (consL a l))
IHl : MemL x (deleteAll x l) -> False
el goal False y es ahí dónde en realida no vemos como seguir.
Saludos.
Hola.
En el caso inductivo va a ser necesario hacer análisis de equal (equal a x), para poder ver los casos y aplicar las definiciones correspondientes. Es útil antes de hacer análisis de casos usar remember (equal a x), para mantener la información en las hipótesis al evaluar cada caso.
Saludos, Carlos