En la pregunta 1 para construir una función sobre (list A) deberíamos de
especificarla formalmente. Por ejemplo, la función append:
 

Inductive espec_append [A:Set]:(list A)->(list A)->(list A)-> Prop:=
espec_append_nil : (m:(list A))(espec_append A (nil A) m m)
| espec_append_cons :(y:A;m,n,p:(list A))(espec_append A m n p) ->
(espec_append A (cons A y m) n (cons A y p)).

Hints Resolve espec_append_nil espec_append_cons .

y a continuación la definimos usando list_rec:
 

Definition append := [X:Set]
(list_rec X
[_:(list X)](list X)->(list X)
[x:(list X)]x
[y:X][_:(list X)][f:(list X)->(list X)][l:(list X)](cons X y (f l))
).

El último paso consistiría en demostrar que la función satisface la especificación. Por ejemplo, en este caso:

Theorem verif: (X:Set)(m,n:(list X))(espec_append X m n (append X m n)).

Induction m.
Simpl; Auto.

Intros.
Simpl; Auto.

verif is defined

Una aproximación a la contestación correcta consiste en referirse a una
función que tenga un nombre familiar (por ejemplo cdr) o no dar una
especificación formal sino una definición menos rigurosa como por ejemplo
"la función que devuelve la cola de una lista". Entonces se utiliza
list_rec para definirla. Esto, aunque no es muy correcto, si está bien
explicado puede servir para aprobar la pregunta pero es fácil cometer
imprecisiones con lo cual, la nota, puede quedar por debajo de 1.25.
 
 
 

La tercera pregunta es la especificación de espec_append dada anteriormante.