Buenas, estoy usando los libros de Software Foundations para aprender Coq.
No consigo importar módulos como por ejemplo, en la parte de Simple imperative programs (Imp) From LF Require Import Maps.
Como consecuencia, no puedo definir algo tan simple como variables:
"Definition W : string := “W”. "
¡Muchas gracias!
Hola Cristina, ¿puedes incluir el mensaje de error que obtienes al intentar importar el módulo Maps?
La causa más probable que se me ocurre a ojo de buen cubero es que el módulo que estás importando no esté compilado, que es una condición necesaria para su uso en otros módulos.
Este es el error que me da al definir las variables : Error: No interpretation for string “W”.
Y si, creo que estoy importando mal el módulo pero es que creo que no sé ni hacerlo.
Directemente me pone “Error: Cannot find library Maps in loadpath”
Gracias por vuestro tiempo.
En general, puede ser una de dos cosas: o bien el módulo Maps no está compilado, o bien el path es incorrecto. Sería bueno saber qué versión de Coq tienes instalada y qué editor y sistema operativo utilizas. También puedes comprobar si puedes reproducir los siguientes pasos.
Acabo de bajar una copia de la versión actual (5.6) del volumen 1 de Software Foundations. Con la version 8.8.2 de Coq instalada (y es de suponer que igualmente con la versión 8.8.1, que es la indicada en la portada del volumen), puedo ejecutar make en el directorio de extracción y compilar todos los ficheros sin problemas. Una vez hecho eso, puedo abrir Imp.v en mi editor (Proof General) e importar el módulo Maps sin problemas.
Hola Cristina, y enhorabuena por estrenar la sección de ¡Coq en Español!
¿Que versión de Coq estás utilizando? ¿Sistema operativo? Como te comenta @robblanco lo más probable es que el módulo map no haya sido compilado.
Ya estoy usando la versión que me has dicho @robblanco pero ahora, al poner “From LF Require Import Maps.” me dice “Unable to locate library Maps with prefix LF.”.
Supongo que LF será el nombre de la carpeta donde tenga Maps.v .
Siento ser tan pesada 
En absoluto, @Cristina, es un placer. ¿Has tenido problemas compilando e importando los módulos anteriores de Software Foundations?
El error que obtienes apunta a algún problema con las rutas durante la compilación. El comienzo del capítulo sobre inducción en Software Foundations (aquí) explica bastante bien la relación entre las librerías, su compilación y los espacios de nombres.
En Linux he podido compilar e importar todo sin problemas a partir de una copia nueva de Software Foundations, tanto con Proof General como con CoqIDE. Si las indicaciones de arriba no son suficientes, sería bueno tener más detalles de tu sistema operativo y configuración, como dice @ejgallego.