Gallo (software)

Cazzo Descrizione dell'immagine Rooster logo.png. Descrizione di questa immagine, commentata anche di seguito CoqIDE  : l' ambiente di sviluppo di Coq . Informazione
Sviluppato da INRIA , Paris Diderot University , Polytechnic School , Paris-Sud University , École normale supérieure de Lyon
Prima versione 1984
Ultima versione 8.13.1 (22 febbraio 2021)
Depositare Gallo su GitHub
Stato del progetto In sviluppo attivo In sviluppo attivo
Scritto in OCaml
Sistema operativo Multi piattaforma
Ambiente Cross-platform
Le lingue inglese
genere Assistente di prova
Politica di distribuzione Gratuito e open source
Licenza GNU LGPL 2.1
Sito web http://coq.inria.fr

Coq è un assistente di prova che utilizza il linguaggio Gallina , sviluppato dal team PI.R2 di Inria all'interno del laboratorio PPS del CNRS e in collaborazione con l' École polytechnique , il CNAM , l' Université Paris Diderot e l' Università Paris-Sud (e precedentemente l' École normale supérieure de Lyon ).

Il nome del software (inizialmente CoC ) è particolarmente indicato perché: è francese; si basa sul calcolo delle costruzioni ( CoC abbreviato in inglese) introdotto da Thierry Coquand . Allo stesso modo, la sua lingua è Gallina e Coq ha un wiki dedicato, chiamato Cocorico! .

Coq ha ricevuto il premio ACM SIGPLAN Programming Languages ​​Software 2013 Award.

Storia del progetto

All'inizio degli anni '80, Gérard Huet ha avviato un progetto per produrre un dimostratore di teorema interattivo. Questo è un assistente di prova. Thierry Coquand e Gérard Huet concepiscono la logica di Coq e il calcolo delle costruzioni. Christine Paulin-Mohring estende questa logica con una nuova costruzione, tipi induttivi e un meccanismo di estrazione che ottiene automaticamente un programma zero errori da una dimostrazione.

Funzionalità software

Rooster si basa sulla progettazione di strutture , una teoria dei tipi di ordine superiore e il suo linguaggio di specifica è una forma di lambda calcolo tipizzato. Il calcolo delle costruzioni utilizzato in Coq include direttamente le costruzioni induttive, da cui il nome di calcolo delle costruzioni induttive (CIC).

Coq ha recentemente ricevuto funzionalità di automazione crescenti. Citiamo in particolare la tattica Omega che decide l' aritmetica di Presburger .

Più specificamente, Coq consente:

È un software gratuito distribuito secondo i termini della licenza GNU LGPL .

Tra i grandi successi di Coq, possiamo citare:

Elementi di linguaggio

Rooster usa la corrispondenza Curry-Howard . La prova di una proposizione è vista come un programma il cui tipo è questa proposizione. Per definire un programma o una prova, devi:

È anche possibile utilizzare SSReflect invece di Ltac. Sviluppato in precedenza separatamente, ora è incluso di default in Coq.

Esempi di programmi

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


  • La funzione fattoriale (con 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.

Esempio dimostrativo (con Ltac)

  • Qualsiasi numero naturale è pari o dispari.
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 e riferimenti

  1. "  Versione 8.13.1  " ,22 febbraio 2021(accesso 10 marzo 2021 )
  2. binario , "  Christine Paulin and Zero Defect Software  " , su binario ,24 settembre 2015(accesso 18 marzo 2020 )
  3. L'aritmetica di Presburger, a differenza della solita aritmetica dovuta a Peano , è una teoria completa, cioè per ogni enunciato del suo linguaggio si può decidere se si tratta di un teorema di teoria oppure no (la sua negazione essendo quindi un teorema). Questa aritmetica di Presburger, che non ha assiomi per la moltiplicazione, sfugge quindi all'incompletezza dichiarata dal teorema di incompletezza .
  4. (in) "Il  teorema di Feit-Thompson è stato completamente verificato in Coq  " , Msr-inria.inria.fr,20 settembre 2012(visitato il 25 settembre 2012 ) .

Vedi anche

link esterno