¿Cuál es el uso del comando ‘Prueba’ en Coq?

El comando Teorema se usa para indicar que uno quiere probar un teorema,
indicando el nombre de este teorema y su declaración. Este comando puede
ir seguido de un comando de prueba opcional, que puede ayudar a hacer que la sesión
guión más legible. Se crea un objetivo inicial, que combina el actual
contexto y la declaración del teorema. Este objetivo se muestra dando
primero el contexto y luego el enunciado, separados por una línea horizontal. En
En nuestro ejemplo, elegimos nombrar nuestro teorema imp_trans.
Un buen uso requiere que los comandos Teorema o Lema sean
seguido por el comando Prueba (generalmente sin argumento); esto hace que el
los documentos de prueba son más legibles, pero no afectan el comportamiento de Coq
sistema.
De coq art.
Por lo tanto, no tiene ningún efecto, excepto generar documentos.