Cocos (software)

Cocoş Descrierea imaginii Rooster logo.png. Descrierea acestei imagini, comentată și mai jos CoqIDE  : mediul de dezvoltare al Coq . informație
Dezvoltat de INRIA , Diderot Universitatea din Paris , Școala Politehnică , Universitatea Paris-Sud , École Normale Supérieure de Lyon
Prima versiune 1984
Ultima versiune 8.13.1 (22 februarie 2021)
Depozit Cocos pe GitHub
Starea proiectului În dezvoltarea activă În dezvoltarea activă
Scris in OCaml
Sistem de operare Multiplatform
Mediu inconjurator Cross-platform
Limbi Engleză
Tip Asistent de dovadă
Politica de distribuție Free și open source
Licență GNU LGPL 2.1
Site-ul web http://coq.inria.fr

Coq este un asistent de probă care utilizează limbajul Gallina , dezvoltat de echipa PI.R2 din Inria în cadrul laboratorului PPS al CNRS și în parteneriat cu École Polytechnique , CNAM , Université Paris Diderot și Universitatea Paris-Sud (și anterior the École normale supérieure de Lyon ).

Numele software-ului (inițial CoC ) este deosebit de potrivit deoarece: este francez; se bazează pe calculul construcțiilor ( CoC prescurtat în limba engleză) introdus de Thierry Coquand . În același sens, limbajul său este Gallina și Coq are un wiki dedicat, numit Cocorico! .

Coq a primit premiul ACM SIGPLAN Programming Languages ​​Software 2013 Award.

Istoria proiectului

La începutul anilor 1980, Gérard Huet a inițiat un proiect pentru fabricarea unui demonstrator de teoreme interactive. Acesta este un asistent de probă. Thierry Coquand și Gérard Huet concep logica lui Coq și calculul construcțiilor. Christine Paulin-Mohring extinde această logică cu o construcție nouă, tipuri inductive și un mecanism de extracție care obține automat un program de eroare zero dintr-o dovadă.

Caracteristici software

Cocoșul se bazează pe proiectarea structurilor , o teorie a tipului de ordin superior , iar limbajul său de specificații este o formă de calcul lambda . Calculul construcțiilor utilizate în Coq include direct construcții inductive, de unde și numele său de calcul al construcțiilor inductive (CIC).

Coq a primit recent funcții de automatizare în creștere. Să cităm în special tactica Omega care decide aritmetica lui Presburger .

Mai precis, Coq permite:

Este un software gratuit distribuit în condițiile licenței GNU LGPL .

Printre marile succese ale Coq, putem menționa:

Elemente de limbaj

Cocoșul folosește corespondența Curry-Howard . Dovada unei propuneri este văzută ca un program al cărui tip este această propunere. Pentru a defini un program sau o dovadă, trebuie să:

De asemenea, este posibil să utilizați SSReflect în loc de Ltac. Fost dezvoltat separat, acum este inclus în mod implicit în Coq.

Exemple de programe

Require Import Arith List Bool. Fixpoint factorielle (x : nat) : nat := match x with 0 => 1 | S p => x * factorielle( p ) end.


  • Funcția factorială (cu Ltac):
Require Import Arith List Bool. Definition factorielle: forall n:nat, nat. (* on nomme l'argument *) intro n. (* on fait une définition par récurrence*) induction n. * (* si l'argument est 0, on retourne 1*) apply 1%nat. * (* si l'argument de la forme (S n), on retourne un produit *) apply Nat.mul. - (* 1er facteur du produit: valeur de factorielle en n *) apply IHn. - (* 2e facteur du produit: le successeur de n *) apply S. + apply n. (*On indique que la définition est terminée et que l'on souhaite pouvoir calculer cette fonction. *) Defined.

Exemplu demonstrativ (cu Ltac)

  • Orice număr natural este par sau impar.
Require Import Omega. Lemma odd_or_ind: forall n : nat, (exists p:nat, n=2*p) \/ (exists p:nat, n = 1 + 2 * p). Proof. induction n. - (* cas 0 *) left. exists 0. trivial. - (* cas (n + 1) *) destruct IHn as [[p Hpair] | [p Himpair]]. + (* n pair *) right. exists p. omega. + (* n impair *) left. exists (p + 1). omega. (* On indique que la preuve est terminée et qu'elle ne sera pas utilisée comme un programme.*) Qed.

Note și referințe

  1. „  Versiunea 8.13.1  ” ,22 februarie 2021(accesat pe 10 martie 2021 )
  2. binar , „  Christine Paulin și Zero Defect Software  ” , pe binar ,24 septembrie 2015(accesat la 18 martie 2020 )
  3. Aritmetica lui Presburger, spre deosebire de aritmetica obișnuită datorată lui Peano , este o teorie completă, adică pentru orice afirmație a limbajului său se poate decide dacă este sau nu o teoremă a teoriei (negarea sa fiind atunci o teoremă). Această aritmetică Presburger, care nu are nicio axiomă pentru multiplicare, scapă, prin urmare, de incompletitudinea afirmată de teorema incompletitudinii .
  4. (în) „  Teorema Feit-Thompson a fost complet verificată în Coq  ” , Msr-inria.inria.fr,20 septembrie 2012(accesat la 25 septembrie 2012 ) .

Vezi și tu

linkuri externe