Resultados da pesquisa a pedido "coq"
Decompondo igualdade de construtores coq
Muitas vezes, em Coq, me pego fazendo o seguinte: tenho o objetivo de prova, por exemplo: some_constructor a c d = some_constructor b c dE eu realmente só preciso provara = b porque todo o resto é idêntico, então eu faço: assert (a = b).Então ...
Qual biblioteca de vetores usar no coq?
Gostaria de saber, existe uma biblioteca comumente usada para vetores em coq, ie. listas indexadas pelo tamanho em seu tipo. Alguns tutoriais fazem referência ao Bvector, mas não é encontrado quando tento importá-lo. Há Coq.Vectors.Vectordef, ...
Como instalar o SSReflect e o MathComp no Linux?
Instalei com êxito o Coq 8.6 e o CoqIDE no Linux (Ubuntu 17.04). No entanto, não sei como proceder para adicionar SSReflect e MathComp a esta instalação. Todas as referências que verifiquei me pareciam muito confusas. Alguém tem uma ...
Como chamar Coq asistant à prova de software externo
Como chamar o Coq de assistente de prova de um software externo? Coq tem alguma API? A interface da linha de comandos Coq é rica o suficiente para passar argumentos no arquivo e receber resposta no arquivo? Estou interessado em pontes Java ou C ...
Por que as novas linguagens de tipo dependente não adotaram a abordagem do SSReflect?
Existem duas convenções que encontrei na extensão SSReflect da Coq que parecem particularmente úteis, mas que não vi amplamente adotadas em linguagens de tipo dependente mais recentes (Lean, Agda, Idris). Em primeiro lugar, sempre que possível, ...
Erro na definição de Ackermann na Coq
Eu estou tentando definir a função Ackermann-Peters no Coq, e estou recebendo uma mensagem de erro que não entendo. Como você pode ver, estou empacotando os ...
Melhor maneira de executar instanciação universal no Coq
Suponha que eu tenha uma hipóteseH : forall ( x : X ), P x e uma variávelx : X no contexto. Quero executar instanciação universal e obter uma nova hipóteseH' : P x. Qual é a maneira mais indolor de fazer isso? Pelo vistoapply H in x ...
Quais são os pontos fortes e fracos do assistente de prova de Isabelle em comparação com o Coq?
O assistente de prova de Isabelle / HOL tem alguma fraqueza e força em comparação com a Coq?
Como definir conjunto em coq sem definir conjunto como uma lista de elementos
Eu estou tentando definir (1,2,3) como um conjunto de elementos em coq. Eu posso defini-lo usando list como (1 :: (2 :: (3 :: nil))). Existe alguma maneira de definir conjunto no coq sem usar a lista.
Mantendo informações ao usar indução?
Estou usando o Coq Proof Assistant para implementar um modelo de (pequena) linguagem de programação (estendendo uma implementação do Featherweight Java por Bruno De Fraine, Erik Ernst, Mario Südholt). Uma coisa que continua surgindo ao usar ...