CFPTT: [Práctico 5] Código del ejercicio 1 no compila

Buenos días,

Estoy haciendo el ejercicio 1 del práctico 5 y el código provisto en la letra no me compila:

Inductive Mem (A : Set) (a : A) : list A -> Prop :=
 | here : forall x : list A, Mem A a (cons A a x)
 | there : forall x : list A, Mem A a x ->
forall b : A, Mem A a (cons A b x).

En particular, me dice el error "The term "a" has type "A" while it is expected to have type "list Set"." en la expresión (cons A a x). Si a los dos cons le saco el tipo (dejando (cons a x) y (cons b x)) ahí si compila.
Es correcto hacer esto? Tampoco me queda del todo claro por qué funciona haciendo esto.

Gracias y saludos

Re: [Práctico 5] Código del ejercicio 1 no compila

de Carlos Luna - sábado, 30 de octubre de 2021, 11:20

Hola Eliana.

Si, es correcto hacer lo que decís.

Otra alternativa es declarar antes (por ejemplo al inicio de la sección de este ejercicio):

Variable A : Set.

En este caso el parámetro del Set en MemL podría ser omitido; así:

Variable A: Set.

Inductive MemL (a : A) : list A -> Prop :=

| here : forall l : list A, MemL a (cons a l)

| there : forall l : list A, MemL a l -> forall b : A, MemL a (cons b l).

Al cerrar luego la sección del ejercicio, Coq generaliza las definiciones considerando las variables definidas (que son globales a la sección).

Pueden elegir la opción que prefieran, ya que a partir del práctico 4 no hay plantillas predefinidas.

Saludos, Carlos