Kohout (software)

Kohout Popis obrázku kohouta logo.png. Popis tohoto obrázku, také komentován níže CoqIDE  : vývojové prostředí společnosti Coq . Informace
Vyvinul INRIA , Paris Diderot University , Polytechnic School , Paris-Sud University , École normale supérieure de Lyon
První verze 1984
Poslední verze 8.13.1 (22. února 2021)
Vklad Kohout na GitHubu
Stav projektu V aktivním vývoji V aktivním vývoji
Napsáno OCaml
Operační systém Multiplatformní
životní prostředí Cross-platform
Jazyky Angličtina
Typ Důkaz asistent
Distribuční politika Zdarma a otevřený zdroj
Licence GNU LGPL 2.1
webová stránka http://coq.inria.fr

Coq je důkazem, asistent pomocí gallina jazyk , vyvinutý PI.R2 týmem z INRIA v PPS laboratoře z CNRS a ve spolupráci s École Polytechnique je CNAM je Université Paris Diderot a Paris-Sud University (a dříve École Normale supérieure de Lyon ).

Název softwaru (původně CoC ) je zvláště vhodný, protože: je francouzský; je založen na výpočtu konstrukcí ( anglicky CoC zkráceně) zavedených Thierry Coquandem . Ve stejném duchu, jeho jazyk je Gallina a Coq má vyhrazený wiki, nazvaný Cocorico! .

Společnost Coq byla oceněna cenou ACM SIGPLAN Programming Languages ​​Software 2013.

Historie projektu

Na začátku 80. let zahájil Gérard Huet projekt výroby interaktivního demonstrátoru vět. Toto je asistent kontroly. Thierry Coquand a Gérard Huet chápou logiku Coq a výpočet konstrukcí. Christine Paulin-Mohring rozšiřuje tuto logiku o novou konstrukci, indukční typy a extrakční mechanismus, který automaticky získá program nulové poruchy z důkazu.

Softwarové funkce

Kohout je založen na návrhu struktur , teorii typů vyššího řádu a jazyk jeho specifikace je formou zadaného počtu lambda kalkulu . Počet konstrukcí použitých v Coq přímo zahrnuje induktivní konstrukce, proto jeho název pro počet indukčních konstrukcí (CIC).

Coq nedávno dostal rostoucí automatizační funkce. Citujme zejména taktiku Omega, která rozhoduje o aritmetice Presburgera .

Coq konkrétněji umožňuje:

Je to bezplatný software distribuovaný za podmínek licence GNU LGPL .

Z velkých úspěchů Coq můžeme zmínit:

Prvky jazyka

Kohout používá korespondenci Curry-Howard . Důkaz o návrhu je považován za program, jehož typem je tento návrh. Chcete-li definovat program nebo důkaz, musíte:

Je také možné použít SSReflect místo Ltac. Dříve vyvinutý samostatně, nyní je ve výchozím nastavení zahrnut do Coq.

Příklady programů

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


  • Faktoriální funkce (s 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.

Demonstrační příklad (s Ltac)

  • Jakékoli přirozené číslo je sudé nebo liché.
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.

Poznámky a odkazy

  1. "  Vydání 8.13.1  " ,22. února 2021(zpřístupněno 10. března 2021 )
  2. binární , „  Christine Paulin and Zero Defect Software  “ , na binární ,24. září 2015(zpřístupněno 18. března 2020 )
  3. Presburgerova aritmetika, na rozdíl od obvyklé aritmetiky způsobené Peanem , je úplnou teorií, tj. Pro jakýkoli výrok jejího jazyka lze rozhodnout, zda jde o teorém teorie nebo ne (její negace je teorém). Tato Presburgerova aritmetika, která nemá žádný axiom pro násobení, proto uniká neúplnosti uvedené v teorému o neúplnosti .
  4. (in) „  Feit-Thompsonova věta byla zcela zkontrolována v Coq  “ , Msr-inria.inria.fr,20. září 2012(zpřístupněno 25. září 2012 ) .

Podívejte se také

externí odkazy