Buenas noches!
Estamos trancados con esta prueba.
Va contexto de lo que tenemos hasta ahora.
Para llegar a esto hicimos inducción en n2 (aunque también probamos en n1), luego de probar el paso base, aplicamos inversión en la hipótesis H0 probando trivialmente el caso base.
Cómo podemos seguir?
Gracias
Hola.
No te conviene hacer inducción en n2 por como tenés las definiciones; si en n1.
La idea sería hacer induction n1 al comienzo, haciendo que la hipótesis inductiva quede generalizada (cuantificada sobre n2). Por ejemplo, pueden arrancar la prueba así:
induction n1; simpl; intros.
Luego, cuando n1 es 0 la prueba es simple, haciendo inversion en la hipótesis que tiene a repeatI con 0.
El caso donde tener sucesor (S), tenés que hacer también inversion para sacar información de la hipótesis que vincula al repeatI. Finalmente, los pases clave en esta parte de la prueba serán la aplicación del constructor correspondiente de la definición del repeatI (para el caso S) y la aplicación de la hipótesis inductiva con los parámetros adecuados.
Saludos, Carlos
Buenas!
Gracias por la respuesta. La prueba salió siguiendo esto.
De todos modos, ya habíamos intentado exactamente esto antes y el problema era que las memorias de la hipótesis inductiva quedaban fijas entonces no nos servía.
Esto lo solucionamos cambiando de lugar las variables ligadas al cuantificador (en el el enunciado del teorema) poniendo las memorias después de los naturales de modo que estas queden como variables cuantificadas al aplicar induction n1 y podamos sustituirlas para al aplicar la hipótesis.
Gracias nuevamente
