Hola,
Estamos probando esta parte y no sabemos como continuar luego de llegar a tener que probar exists l3 : list A, append A m p = append A l3 l1, sabiendo que posfijo A l1 p.
Sabemos que el testigo es (m++p)--l1, pero no tenemos una resta.
Podemos utilizar la parte 3 y 4 para definir una resta, y luego dar un testigo, o esto es más complejo?
Muchas gracias.
Saludos.
Hola.
Si, pueden hacerlo. No obstante, se están complicando mucho.
Recuerden que al hacer inducción no solo se puede razonar sobre una lista en este caso, sino también sobre (posfijo A l1 l2), que es un objeto inductivo. Mi consejo es que prueben hacer inducción en la hipótesis referida (luego de hacer intros).
El caso base sale fácil y para el caso inductivo tengan presente que van a tener que probar un existe pero la hipótesis inductiva es también un existe. En este caso tienen primero que usar (eliminar) la hipótesis inductiva antes de proponer el testigo para el goal. La prueba sale fácil, sin ser necesario usar lemas auxiliares.
Saludos, Carlos
