[Práctico 4] Ejercicio 17.3.3 - error

[Práctico 4] Ejercicio 17.3.3 - error

de Julian Tricanico Gadea -
Número de respuestas: 3
Buenas,

Me está sucediendo lo siguiente y busco en google y tampoco logro entender qué está pasando.

Tengo de hipótesis 
H1 : exists ys' : List X, ys = ys' ++' xs
y si hago elim H1 obtengo el error
Cannot find the elimination combinator ex_rec, the elimination of the inductive definition ex on sort Set is probably not allowed.
Y si hago destruct H1 as [ys' H1] obtengo
Case analysis on sort Set is not allowed for inductive definition ex.
Por si acaso lo que está en el goal es
xs << zs
Alguna idea? Siento que estuve en esta misma situación un montón de veces ya. No veo qué tiene de diferente esta vez.
Saludos!
En respuesta a Julian Tricanico Gadea

Re: [Práctico 4] Ejercicio 17.3.3 - error

de Carlos Luna -

Hola Julian.

No puedo identificar el error, al menos en la versión de Coq que tengo instalada (no es la última). 

Pasame el archivo a cluna@fing.edu.uy y lo veo con todas tus definiciones.

Saludos, Carlos

En respuesta a Carlos Luna

Re: [Práctico 4] Ejercicio 17.3.3 - error

de Julian Tricanico Gadea -
Ahora después de haber leído tu mensaje le di un intento más y encontré la solución.

El problema estaba en que había definido posfijo con codominio en Set en lugar de Prop:
Inductive posfijo (X : Set) : List X -> List X -> Set := ...
Honestamente tiré a embocar. Me supera un poco la diferencia, jajaja. (Con Type me tira el mismo error.)

Si se puede comentar algo al respecto, agradezco.
Saludos!
En respuesta a Julian Tricanico Gadea

Re: [Práctico 4] Ejercicio 17.3.3 - error

de Carlos Luna -
Hola.
Posfijo es un predicado (una relación); es razonable que sea un Prop.
En general, en Set se ponen los tipos de datos y elementos con información computacional, y en Prop se formalizan predicados y relaciones que permiten especificar comportamiento.
Saludos