coq

19El calor

3Respuesta

¿Qué significa `true = false` en Coq?

[no estoy seguro de que esto es apropiado para el desbordamiento de pila, pero hay muchas otras preguntas Coq aquí, así que tal vez alguien puede ayudar.] estoy trabajando a través de las siguientes o

7El calor

1Respuesta

ejemplificación existencial y generalización en coq

¿Puede alguien darme por favor un ejemplo simple de instanciación existencial y generalización existencial en Coq? Cuando quiero probar exists x, P, donde P es Prop que usa x, a menudo quiero nombrar

6El calor

1Respuesta

cómo nombrar la suposición al recordar una expresión?

La documentación de Coq contiene la advertencia general no para confiar en el mecanismo de nomenclatura incorporado, pero seleccione los nombres propios, para que los cambios en el mecanismo de nomenc

9El calor

1Respuesta

invertir recursivamente las hipótesis en coq

Tengo problemas para definir una táctica para invertir recursivamente las hipótesis en un contexto de prueba. Por ejemplo, supongamos que tengo un contexto prueba que contiene una hipótesis como: H1 :

26El calor

1Respuesta

Diferencia entre Z3 y coq

Me pregunto si alguien me puede decir la diferencia entre Z3 y CoQ? Me parece que coq es un asistente de pruebas ya que requiere que el usuario complete los pasos de prueba, mientras que Z3 no tiene e

5El calor

1Respuesta

Comportamiento incoherente de Coq con respecto a los parámetros implícitos de las definiciones de Let

He encontrado algún tipo de comportamiento incoherente de Coq con respecto a los parámetros implícitos. Section foo. Let id1 {t : Set} (x : t) := x. Let id2 {t : Set} (x : t) : t. assumption

9El calor

1Respuesta

Glifos Unicode para palabras clave y operadores en Coq/Proof General bajo Emacs

Esta pregunta tiene que ver con la configuración del modo Coq dentro de Proof General, en Emacs. Estoy intentando que Emacs reemplace automáticamente las palabras clave y la notación en Coq con los gl

8El calor

3Respuesta

Error al definir Ackermann en Coq

Estoy intentando definir la función de Ackermann-Peters en Coq, y aparece un mensaje de error que no entiendo. Como puede ver, estoy empaquetando los argumentos a, b de Ackermann en un par ab; Proporc

9El calor

1Respuesta

No se puede encontrar una instancia para la variable

Contexto: Estoy trabajando en ejercicios en Software Foundations. Theorem neg_move : forall x y : bool, x = negb y -> negb x = y. Proof. Admitted. Theorem evenb_n__oddb_Sn : forall n : nat,

16El calor

2Respuesta

LTAC-camente abstracción sobre un subtérmino del tipo de objetivo

Como un fondo áspero y sin instrucción, en HoTT, se deduce a los diablos de tipo inductivo definido Inductive paths {X : Type } : X -> X -> Type := | idpath : forall x: X, paths x x. que permite la