Coq é um provador de teoremas interativo baseado no Cálculo de Construções Indutivas.
Estou aprendendo sozinho os provedores de teoremas automatizados / solucionadores de SMT / assistentes de prova e postar uma série de perguntas sobre o processo, começando aqui. Observe que esses tópicos não são facilmente digeridos sem um histórico em lógicas (matemáticas). Se você tiver...
A Wikipedia e outras fontes que eu encontrei listam o voidtipo de C como um tipo de unidade, em vez de um tipo vazio. Acho isso confuso, pois me parece que voidmelhor se ajusta à definição de um tipo vazio / inferior. Nenhum valor habita void, até onde eu sei. Uma função com um tipo de retorno de...
Eu estava assistindo as " Cinco etapas da aceitação da matemática construtiva ", de Andrej Bauer, e ele diz que existem dois tipos de provas por contradição (ou duas coisas que os matemáticos chamam de prova por contradição): Suponha que seja falso ... blá blá blá, contradição. Portanto, é...
Considere um tipo indutivo que possui algumas ocorrências recursivas em um local aninhado, mas estritamente positivo. Por exemplo, árvores com ramificação finita com nós usando uma estrutura de dados de lista genérica para armazenar os filhos. Inductive LTree : Set := Node : list LTree ->...
Alguém já escreveu um sistema (software ou explicação detalhada no papel, com exemplos simples) que gera programas de computador? Eu introduzo e ele cria um programa que lista os números primos menores que 10. é simplesmente definido como professores dizem que podem, mas ninguém dá exemplos...
Sou programador com domínio de autômatos, mas não de lógica. Li nos jornais que os dois estão muito relacionados. Autômatos finitos determinísticos (DFA), autômatos em árvore e autômatos visivelmente pushdown estão todos relacionados à lógica monádica de segunda ordem (MSO). Embora eu entenda que...
Fechadas. Esta questão está fora de tópico . No momento, não está aceitando respostas. Deseja melhorar esta pergunta? Atualize a pergunta para que ela esteja no tópico do Computer Science Stack Exchange. Fechado há 2 anos . Os tipos AFAIU podem ser a...
Atualmente, tenho que aprender Coq e não sei como lidar com or: Como exemplo, por mais simples que seja, não vejo como provar: Theorem T0: x \/ ~x. Eu realmente aprecio isso, se alguém puder me ajudar. Para referência, eu uso esta folha de dicas . Também um exemplo de uma prova que tenho em...
Estou curioso. Eu tenho trabalhado nesse tipo de dados no OCaml : type 'a exptree = | Epsilon | Delta of 'a exptree * 'a exptree | Omicron of 'a | Iota of 'a exptree exptree Que pode ser manipulado usando funções recursivas de tipo explícito (um recurso que foi adicionado recentemente)....
fundo Estou aprendendo assistência, Coq, sozinho. Até agora, concluí a leitura Coq apressado de Yves Bertot . Agora, meu objetivo é provar alguns resultados básicos relativos aos números naturais, culminando com o chamado algoritmo de divisão. No entanto, encontrei alguns contratempos no meu...
Números naturais são definidos indutivamente como (usando a sintaxe Coq como exemplo) Inductive nat: Set := | O: nat | S: nat -> nat. Existe uma maneira padrão de definir números inteiros (e talvez outros conjuntos como racionais e reais)
Sou relativamente novo em teoria de tipos e programação dependente. Eu estudei o cálculo de construções (CoC) e outros sistemas de tipo puro. Estou particularmente interessado em usá-lo como uma representação intermediária de preservação de prova para um sistema de compilador. Entendo que os tipos...
Coq inclui let-expression em sua linguagem principal. Podemos traduzir expressões let para aplicativos como este: let x : t = v in b ~> (\(x:t). b) v Entendo que isso nem sempre funciona porque o valor vnão estaria disponível ao digitar b. No entanto, isso pode ser facilmente corrigido através...
Estou no seguinte exercício no Software Foundations : (** **** Exercise: 2 stars (baz_num_elts) *) (** Consider the following inductive definition: *) Inductive baz : Type := | x : baz -> baz | y : baz -> bool -> baz. (** How _many_ elements does the type [baz] have? (* FILL IN HERE...
O COQ é um provador de teoremas interativo que usa o cálculo de construções indutivas, ou seja, depende muito de tipos indutivos. Usando isso, estruturas discretas como números naturais, números racionais, gráficos, gramáticas, semânticas etc. são representadas de forma muito concisa. No entanto,...
Sou totalmente iniciante na Coq e estou tentando implementar algumas coisas da teoria das categorias como um exercício. Naveguei um pouco entre os repositórios git das muitas implementações disponíveis (HoTT, companhia de Awodey's Coq etc.), parece que todo projeto implementa algo assim Record...
Tenho a seguinte prova inacabada de um lema: Goal forall (P : Type -> Prop) (Q : Prop), ((forall x, (P x)) -> Q) -> (exists x, P x -> Q). Proof. intros. eapply ex_intro. intros. apply H. intros. eapply H0. O problema é a última eapplyfalha, com a mensagem Error: In environment P...
Estou aprendendo sobre metateoria da linguagem e sistemas de tipos e estou usando coq para formalizar meu estudo. Uma das coisas que eu gostaria de fazer é examinar os sistemas de tipos que incluem tipos dependentes , o que eu entendo estar muito envolvido: poder confiar no coq seria...