Resultados de la búsqueda a petición "coq"
Subconjunto inductivo de un conjunto inductivo en Coq
Tengo un conjunto inductivo construido con tres constructores: Inductive MF : Set := | D : MF | cn : MF -> MF -> MF | dn : Z -> MF -> MF.Me gustaría definir de alguna manera un nuevo conjunto inductivo B, de modo que B sea un subconjunto de MF ...
Descomponiendo la igualdad de constructores coq
A menudo en Coq me encuentro haciendo lo siguiente: Tengo el objetivo de la prueba, por ejemplo: some_constructor a c d = some_constructor b c dY realmente solo necesito demostrara = b porque todo lo demás es idéntico de todos modos, así que ...
¿Qué biblioteca de vectores usar en coq?
Me pregunto, ¿hay una biblioteca comúnmente utilizada para vectores en coq, es decir? listas indexadas por su longitud en su tipo. Algunos tutoriales hacen referencia a Bvector, pero no se encuentra cuando intento importarlo. Hay ...
¿Cómo instalar SSReflect y MathComp en Linux?
He instalado correctamente Coq 8.6 y CoqIDE en Linux (Ubuntu 17.04). Sin embargo, no sé si proceder para agregar SSReflect y MathComp a esta instalación. Todas las referencias que he verificado me parecieron muy confusas. ¿Alguien tiene una ...
Cómo llamar a Coq asistente de prueba desde un software externo
¿Cómo llamar al asistente de prueba Coq desde un software externo? ¿Coq tiene alguna API? ¿La interfaz de línea de comandos de Coq es lo suficientemente rica como para pasar argumentos en el archivo y recibir respuesta en el archivo? Estoy ...
¿Por qué los nuevos lenguajes de tipo dependiente no han adoptado el enfoque de SSReflect?
Hay dos convenciones que he encontrado en la extensión SSReflect de Coq que parecen particularmente útiles pero que no he visto ampliamente adoptadas en los nuevos lenguajes de tipo dependiente (Lean, Agda, Idris). En primer lugar, cuando los ...
La mejor manera de realizar una instanciación universal en Coq
Supongamos que tengo una hipótesisH : forall ( x : X ), P x y una variablex : X en el contexto. Quiero realizar una instanciación universal y obtener una nueva hipótesisH' : P x. ¿Cuál es la forma más indolora de hacer esto? Aparentementeapply H ...
¿Cuáles son las fortalezas y debilidades del asistente de pruebas Isabelle en comparación con Coq?
¿El asistente de prueba Isabelle / HOL tiene debilidades y fortalezas en comparación con Coq?
Cómo definir set en coq sin definir set como una lista de elementos
Estoy tratando de definir (1,2,3) como un conjunto de elementos en coq. Puedo definirlo usando list como (1 :: (2 :: (3 :: nil))). ¿Hay alguna manera de definir el conjunto en coq sin usar la lista?