Buenas.
Tengo una consulta sobre el tipo list. El ejercicio 4.1 pide definir el tipo genérico, luego el ejercicio 4.4 pide definir una serie de funciones recursivas sobre ese tipo, y más adelante el ejercicio 4.11 parece asumir una cierta definición ya dada (cuyos constructores son nil y cons). Si efectivamente es esta la definición que debe utilizarse, la pregunta es sobre la semántica de cons. Pareciera que tradicionalmente cons construye hacia la izquierda, es decir, [1 2 3] sería entonces (cons 1 (cons 2 (cons 3 nil))), pero parece hacer bastante dificultoso el ejercicio 4.17, que trabaja con posfijos. Para trabajar con posfijos parece más intuitivo trabajar con constructores que anexen hacia la derecha, es decir [1 2 3] siendo (cons 3 (cons 2 (cons 1 nil))). ¿Es libre la elección sobre la semántica de cons en este caso?
Aprovecho para consultar si tenemos permitido modificar sintácticamente el enunciado de algunos de los teoremas que se pide demostrar para utilizar argumentos implícitos, por ejemplo donde se pide:
L4 : forall (A : Set) (l m : list A), length A (append A l m) = sum (length A l) (length A m)
cambiarlo por:
L4 : forall (A : Set) (l m : list A), length (append l m) = sum (length l) (length m)
porque se han definido las funciones con parámetros implícitos.
Finalmente, quería confirmar si las tácticas automáticas sólo podremos utilizarlas cuando se menciona explícitamente (como el ejercicio 4.18 y 4.20) o si ya pueden utilizarse libremente para cualquier demostración.
Saludos.