Comment faire la preuve dans des instructions Coq sur des ensembles donnés

Comment peut-on éprouver des instructions comme celle-ci dans COQ.Comment faire la preuve dans des instructions Coq sur des ensembles donnés

Require Import Vector. 
Import VectorNotations. 
Require Import Fin. 

Definition v:=[1;2;3;4;5;6;7;8]. 
Lemma L: forall (x: Fin.t 8), (nth v x) > 0.

Ou, disons que vous avez une liste donnée de chiffres et que vous voulez la preuve que aucun numéro apparaît deux fois dans cette liste.

Peut-être que l'on doit écrire un algorithme avec le lemme comme type. Mais je n'ai aucune idée de comment faire cela.

BTW, ce n'est pas un exercice de devoirs.

Source

2015-12-19 Cryptostasis

Ceci est facile à prouver (en Coq, ou à la main) parce que c'est juste une liste particulière. Votre but ultime est-il de prouver des choses à propos d'une liste générée par quelque chose d'autre? Dans ce cas, vous devrez prouver des choses sur le code/la fonction/la procédure qui génère la liste. C'est là que ça devient intéressant. –

Prouver "à la main" n'est pas possible si la liste devient compliquée. Par exemple, pensez à avoir un modèle COQ qui a besoin d'une grande matrice 1000x1000 en tant que paramètre. Et il doit être assuré que la matrice a un rang complet. Supposons que vous ayez besoin de la propriété full rank pour les preuves des propriétés de votre modèle. Bien sûr, on peut vérifier chaque instance individuelle du modèle avec un système d'algèbre informatique et ajouter la propriété "full rank" comme un axiome au modèle. Mais c'est un peu étrange ... – Cryptostasis

Je pense que le problème est que COQ a quelques limitations avec l'induction des types dépendants. Le site http://homes.cs.washington.edu/~jrw12/dep-destruct.html tente de l'expliquer, mais j'ai quelques difficultés à suivre leurs arguments. – Cryptostasis

Voici une preuve rapide et sale:

Proof. 
Require Import Program. 
dependent destruction x. 
auto. 
dependent destruction x. 
compute. 
auto. 
dependent destruction x. 
compute. 
auto. 
dependent destruction x. 
compute. 
auto. 
dependent destruction x. 
compute. 
auto. 
dependent destruction x. 
compute. 
auto 10. 
dependent destruction x. 
compute. 
auto 10. 
dependent destruction x. 
compute. 
auto 10. 
dependent destruction x. 
Qed.

Nous utilisons la tactique dependent destruction du module Program. Cela repose sur l'axiome JMeq, mais cela ne devrait pas poser de problème.

Source

2015-12-21 13:08:15

Vous pouvez utiliser 'repeat' pour le réduire à' repeat destruction dépendante x; calculer; auto 10. ». – gallais

Permettez-moi de suggérer une solution en utilisant la bibliothèque-maquette mathématique:

From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. 
From mathcomp Require Import fintype tuple. 

Definition v := [tuple of [:: 1;2;3;4;5;6;7;8]]. 

Lemma L : forall x, tnth v x > 0. 
Proof. exact/all_tnthP. Qed.

Le lemme all_tnthP remplacera votre prédicat par sa version calculable, qui à son tour fera Coq vérifier que tous les éléments du tuple sont supérieur à 0, concluant la preuve.

Source

2016-02-26 00:42:52 ejgallego

Comment faire la preuve dans des instructions Coq sur des ensembles donnés

Répondre

Questions connexes