coq

0La chaleur

1Répondre

Coq - comment nommer une supposition en ligne

Je voudrais avoir un nom pour P dans P-> Q. Le rationnel est d'énoncer un théorème de type P-> Q dans lequel Q dépend de P. Dans l'exemple suivant, j'ai besoin de remplacer le '???'. Je sais que je po

3La chaleur

1Répondre

Retour d'un enregistrement à partir d'une définition dans Coq

Supposons que j'ai un record qui contient deux nats. Record toy := { num1 : nat; num2 : nat }. Je veux construire une définition qui donne deux nats renvoie un record contenant ces deux n

7La chaleur

3Répondre

Types dépendants: Vecteur de vecteurs

Je suis nouveau pour les types dépendants (j'essaie à la fois Idris et Coq, malgré leurs grandes différences). J'essaye d'exprimer le type suivant: donné un type T et une séquence de k nats n1, n2, ..

5La chaleur

1Répondre

Structures canoniques dans ssreflect

J'essaie de traiter des structures canoniques dans ssreflect. Il y a 2 morceaux de code que j'ai pris de here. Je vais apporter des pièces pour le bool et les types d'options. Section BoolFinType.

4La chaleur

2Répondre

Nombre de tests aléatoires générés par QuickChick dans Coq

Chaque fois que j'utilise QuickChick dans Coq, il a une valeur par défaut de 10000 tests. Y at-il un moyen de modifier cette valeur par défaut pour générer un nombre différent de tests?

2La chaleur

2Répondre

Preuve de l'application d'une Substitution sur un terme

J'essaie de prouver que l'application d'une Substitution vide sur un terme est égale au terme donné. Voici le code: Require Import Coq.Strings.String. Require Import Coq.Lists.List. Require Import C

3La chaleur

1Répondre

Comment importer des librairies dans Coq?

Je souhaite utiliser && en tant que forme d'infixe de andb dans Coq. La documentation officielle me dit && est définie dans le module Coq.Init.Datatypes. Je essayé ceci: Import Coq.Init.Datatypes. enc

4La chaleur

2Répondre

Comment appeler proof asistant Coq à partir d'un logiciel externe

Comment appeler proof assistant Coq à partir d'un logiciel externe? Est-ce que Coq a une API? L'interface de ligne de commande Coq est-elle suffisamment riche pour transmettre des arguments dans un fi

1La chaleur

1Répondre

Dans Coq, comment définir un ensemble comme A = {x | f (x) = 0}?

Je suis un débutant dans l'utilisation de Coq. Je veux demander si je veux définir un ensemble comme , comment pourrais-je faire cela? J'écris quelque chose comme: Definition f0 := nat->nat. Definit

2La chaleur

1Répondre

singleton list (`A) dans Coq?

J'essaie de comprendre et de compiler la formalisation logique linéaire en Coq: http://www.cs.nuim.ie/~jpower/Research/LinearLogic/http://www.cs.nuim.ie/~jpower/Research/LinearLogic/ILL.v Voici ce cod