Úvod do funkcionálneho programovania v Rocq a prvé dôkazy

Rocq ako nástroj teórie typov

Rocq v predmete Teória typov používame na štúdium vzťahu medzi typovaním, výpočtom a dokazovaním. V tomto cvičení definujeme dátové typy a funkcie, preskúmame typy termov a vyhodnotíme ich aplikácie. Na tieto základy nadviaže formulácia tvrdení a konštrukcia formálnych dôkazov.

Rocq je interaktívny dokazovací systém. Jeho jadro vychádza z Calculus of Inductive Constructions (CIC), teórie typov spájajúcej závislé funkčné typy, induktívne definície a konštruktívne dokazovanie. V Rocqu možno definovať matematické objekty, programy, tvrdenia aj dôkazy. Správnosť formálneho dôkazu napokon kontroluje malé dôveryhodné jadro.

Rocq obsahuje čistý funkcionálny jazyk Gallina, ktorý používame na zápis termov, funkcií, typov a tvrdení. Keď napríklad definujeme funkciu, systém overí, že jej telo má deklarovaný typ. Neskôr budeme rovnakú myšlienku typovej kontroly používať pri dôkazoch.

Vrstvy zápisu v Rocqu

Pri práci s Rocqom sa stretávame s viacerými vrstvami zápisu:

1. Gallina je jazyk termov. Termom môže byť číslo, funkcia, aplikácia funkcie alebo výraz match; zapisujeme ním aj matematické tvrdenia.
2. Vernacular obsahuje príkazy, ktoré menia globálne prostredie alebo sa ho dopytujú. Patria sem Definition, Fixpoint, Inductive, Check, Compute, Print, Lemma a Theorem. Príkaz sa končí bodkou; term môže byť jeho súčasťou.
3. Taktické jazyky, najmä Ltac a Ltac2, slúžia na interaktívne vytváranie dôkazov. Ich kroky spracúvajú aktuálne dôkazové ciele.

Napríklad v príkaze Check 3. je Check príkaz Vernacular a 3 je term Galliny. Rovnako Definition double (n : nat) : nat := n + n. je príkaz, v ktorom je n + n telom funkcie v Galline.

Lemma plus_0_r : forall n : nat, n + 0 = n.
Proof.
  intros n.
  induction n as [| n IHn].
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.

Inštalácia Rocqu

Postup inštalácie pre svoj operačný systém nájdete na oficiálnej stránke Rocqu. Nainštalujte Rocq a pracovné prostredie, v ktorom budete otvárať súbory s príponou .v.

Použiť možno viacero prostredí:

• RocqIDE poskytuje editor, zobrazenie cieľov a správ i interaktívne krokovanie.
• Visual Studio Code s rozšírením VsRocq poskytuje podporu Rocqu; podľa spôsobu inštalácie môže byť potrebný aj zodpovedajúci jazykový server.
• Emacs s rozšírením Proof General je ďalšia možnosť interaktívnej práce.

V rámci tohto cvičenia budeme primárne používať RocqIDE, aby sme mohli sledovať rovnaké okná a postupy. Príklady v súboroch .v možno vykonať aj v inom podporovanom prostredí.

Ovládanie RocqIDE

RocqIDE má editor zdrojového súboru, okno aktuálnych cieľov Goals, okno správ Messages a ovládací panel. V editore píšeme definície, výpočty aj dôkazy. V prvej lekcii bude väčšina príkazov definíciami a dopytmi; okno Goals bude dôležité najmä pri neskoršom dokazovaní.

1. Editor je hlavné textové okno. Príkazy v ňom možno postupne odosielať systému. Na obrázku je editor vľavo.

2. Goals zobrazuje aktuálny dôkazový cieľ a prípadné podciele. Ak práve nedefinujeme dôkaz, nemusí obsahovať nič, čo by bolo potrebné riešiť.

3. Messages zobrazuje výsledky príkazov Check, Print a Compute, ako aj upozornenia a chybové hlásenia.

Ovládací panel umožňuje vykonať ďalší príkaz (Next), vrátiť sa o krok (Previous), vrátiť spracovanie na začiatok (Reset) alebo skontrolovať zvyšok súboru (Run to end). Krokovanie sa vzťahuje na príkazy v súbore, nielen na dôkazové taktiky. Klávesové skratky sa môžu líšiť podľa verzie RocqIDE a operačného systému; aktuálne priradenie si overte v ponuke aplikácie.

Prvý term, typ a výpočet

Do nového súboru .v vložte tieto príkazy a vykonávajte ich po jednom:

Check 3.
Compute 2 + 3.

Definition double (n : nat) : nat :=
  n + n.

Check double.
Compute double 4.
Print double.

Výstupy príkazov v poradí, v akom sa vykonajú:

3 : nat
= 5
: nat
double : nat -> nat
= 8
: nat

Skrátený výstup Print double.:

double = fun n : nat => n + n
     : nat -> nat

Ďalšie pomocné riadky výpisu Print sa môžu medzi verziami líšiť.

Číslo 3 je term typu nat, čo zistí Check 3.. Compute 2 + 3. vyhodnotí term a zobrazí výsledok 5. Príkaz Definition zavedie meno double pre funkciu, ktorá svoj vstup sčíta so sebou. Check double. vypíše funkčný typ nat -> nat; Compute double 4. vypíše 8. Print double. zobrazí uloženú definíciu a jej typ.

Výsledky príkazov sa zobrazujú v Messages. Check zisťuje typ, Compute vykonáva výpočet a Print ukazuje definíciu. Funkčný typ nat -> nat hovorí, že double prijíma prirodzené číslo a vracia prirodzené číslo.

Termy a funkcie v Galline

Funkcionálne programovanie stavia výpočty na tvorbe a aplikácii funkcií. Gallina je čistý funkcionálny jazyk používaný v Rocqu na zápis termov, funkcií, dátových typov a matematických objektov. Pri štúdiu teórie typov nám umožní sledovať, aký typ má každý term a ako sa jeho vyhodnotenie viaže na typové pravidlá.

• Nemennosť: Definované meno označuje term; jeho hodnotu nemeníme priradením ako pri meniteľnej premennej. Nový lokálny názov možno zaviesť pomocou let.
• Čisté funkcie: Výsledok funkcie závisí od vstupov a jej vyhodnotenie nemení vonkajší stav programu.
• Funkcie ako hodnoty: Funkcie v Galline môžu byť argumentmi iných funkcií aj ich výsledkami. Toto je jedna z vlastností funkcionálneho programovania, nie jeho jediná definícia.

Komentáre

Komentár je uzatvorený medzi (* a *). Môže zaberať jeden riadok alebo viac riadkov; samostatný symbol pre jednoriadkový komentár sa nepoužíva. Napríklad:

(* Nasledujúci príkaz vypočíta súčet. *)
Compute 1 + 1. (* Výsledok je 2. *)

Definície a základné príkazy Vernacular

Príkaz Definition zavedie globálne meno pre term. Nasledujúca definícia nepredstavuje priradenie do meniteľnej programovej premennej:

Definition x : nat := 10.
Check x.
Print x.
Compute x + 2.

Výstup Check x. a Compute x + 2.:

x : nat
= 12
: nat

Skrátený výstup Print x.:

x = 10
  : nat

Meno x označuje term 10. Check x. zistí typ nat, Print x. vypíše definíciu a Compute x + 2. vypočíta 12. Ak je typ z termu jednoznačný, Rocq ho často dokáže odvodiť; explicitná anotácia : nat je pri výklade užitočná.

Rovnaký príkaz môže definovať funkciu:

Definition increment (n : nat) : nat := n + 1.
Check increment.
Print increment.
Compute increment 4.

Výstup Check increment. a Compute increment 4.:

increment : nat -> nat
= 5
: nat

Skrátený výstup Print increment.:

increment = fun n : nat => n + 1
          : nat -> nat

Funkcia increment má typ nat -> nat. V zobrazení Print ju možno vidieť aj ako anonymnú funkciu fun n : nat => n + 1; presný formát ďalších riadkov výpisu sa môže medzi verziami Rocqu líšiť.

Ďalšie dopytovacie príkazy

Pri prvých príkladoch používajte najmä Check, Compute a Print. Na skúmanie existujúcich objektov sú užitočné aj tieto príkazy:

About Nat.add.
Search Nat.add.
Locate "+".
Print Scope nat_scope.

Skrátený výstup:

Nat.add : nat -> nat -> nat
Notation "x + y" := (Nat.add x y) : nat_scope

Search môže nájsť viac objektov a úplný výpis závisí od aktuálne načítaných knižníc. Uvedená notácia je podstatná časť výstupu Locate "+". a Print Scope nat_scope..

About poskytuje informácie o objekte, Search vyhľadáva podľa zadaného termu alebo tvaru a Locate zisťuje, ku ktorým definíciám sa môže viazať notácia +. Symbol + môže v rôznych kontextoch označovať rôzne operácie. Rozsah notácie (scope) pomáha určiť jeho interpretáciu; Print Scope nat_scope. ukáže notácie v rozsahu prirodzených čísel. Vlastné notácie zavedie samostatná časť nižšie.

Základné typy a hierarchia typov

Každý term má typ. Aj typy sú v Rocqu termami: napríklad true má typ bool a samotný bool má typ Set. Nasledujúca tabuľka odlišuje dátové typy od univerz, do ktorých tieto typy patria.

Zápis $Type_i : Type_{i+1}$ vyjadruje hierarchiu univerz: univerzum na úrovni i patrí do vyššieho univerza. Je to matematický opis, nie doslovná syntax príkazu Rocqu. Pri dopyte Check Type. sa môže zobraziť Type : Type, pretože Rocq v bežnom výstupe konkrétne úrovne skrýva. Neznamená to, že ide o ten istý typ na tej istej úrovni.

Check Set.
Check Prop.
Check Type.

Typický výstup:

Set : Type
Prop : Type
Type : Type

Pri základných dátových typoch a ich hodnotách:

Check bool.
Check true.
Check false.
Check nat.
Check O.
Check (S O).
Check unit.
Check tt.
Check Empty_set.

Výstup (Rocq môže zobrazovať O ako 0 a S O ako 1):

bool : Set
true : bool
false : bool
nat : Set
0 : nat
1 : nat
unit : Set
tt : unit
Empty_set : Set

Typ list očakáva parameter, ktorý určí typ prvkov zoznamu. Po dosadení nat dostaneme dátový typ list nat:

Check list.
Check (list nat).
Check (nil : list nat).
Check (cons 1 nil).

Výstup:

list : Type -> Type
list nat : Set
nil : list nat
(1 :: nil)%list : list nat

Zápis cons 1 nil môže Rocq vo výstupe zobraziť pomocou notácie ::. Napokon príklady tvrdení:

Check True.
Check False.
Check (3 = 4).
Check (forall n, n + 0 = n).

Výstup:

True : Prop
False : Prop
3 = 4 : Prop
forall n : nat, n + 0 = n : Prop

True a False sú tvrdenia, nie booleovské hodnoty true a false. Tvrdenie 3 = 4 je dobre typované ako objekt v Prop, hoci nie je pravdivé.

Anonymná funkcia a súvis s λ-kalkulom

Gallina zapisuje anonymnú funkciu v tvare fun x => t. Ide o obdobu λ-abstrakcie $\lambda x.t$ z prednášky o λ-kalkule. Identickú funkciu na prirodzených číslach môžeme definovať takto:

Definition id_nat : nat -> nat :=
  fun n => n.
Check id_nat.
Compute id_nat 3.

Výstup:

id_nat : nat -> nat
= 3
: nat

Term fun n => n zodpovedá $\lambda n.n$. Anotácia nat -> nat určuje, že vstup aj výstup majú typ nat. Pri aplikácii id_nat 3 sa argument dosadí za parameter funkcie.

Funkcie vyššieho rádu a čiastočná aplikácia

Funkcia je hodnotou, a preto môže prijímať inú funkciu alebo ju vrátiť ako výsledok. Funkcie viacerých argumentov sa v Galline zapisujú ako postupnosť funkcií jedného argumentu. Preto aj aplikácia len na časť argumentov môže vrátiť funkciu.

Definition plus (a b : nat) : nat := a + b.
Definition plus2 := plus 2.
Check plus.
Check plus2.
Compute plus2 3.

Výstup:

plus : nat -> nat -> nat
plus2 : nat -> nat
= 5
: nat

Check plus. zobrazí nat -> nat -> nat. Šípka funkčného typu sa združuje sprava, takže ide o nat -> (nat -> nat): po prijatí prvého čísla zostáva funkcia z nat do nat. Výraz plus 2 má preto typ nat -> nat; Compute plus2 3. vráti 5. Tento spôsob reprezentácie viacargumentových funkcií sa nazýva currying.

Funkcia vyššieho rádu môže prijať funkciu ako argument:

Definition apply_twice (f : nat -> nat) (n : nat) : nat :=
  f (f n).
Check apply_twice.
Compute apply_twice increment 3.

Výstup:

apply_twice : (nat -> nat) -> nat -> nat
= 5
: nat

Tu je prvým argumentom f funkcia nat -> nat; výsledok posledného výpočtu je 5.

Lokálne meno pomocou let ... in

Konštrukcia let zavedie lokálne meno iba v rámci daného termu. Nejde o meniteľnú premennú ani o novú globálnu definíciu:

Definition add_xy : nat :=
  let a := 10 in
  let b := 20 in
  a + b.
Compute add_xy.

Výstup:

= 30
: nat

Výsledkom je 30. Mená a a b nie sú po skončení definície dostupné v globálnom prostredí.

Induktívne typy, analýza prípadov a rekurzia

Doteraz sme používali štandardné typy nat a bool. Teraz uvidíme, ako konštruktory vytvárajú hodnoty induktívneho typu, ako ich rozlišuje match a prečo pri rekurzii sledujeme štruktúru vstupu.

Induktívny typ a jeho konštruktory

Príkaz Inductive zavádza nový typ a jeho konštruktory. Jednoduchý nerekurzívny príklad predstavujú dni v týždni:

Inductive day : Type :=
| Monday
| Tuesday
| Wednesday
| Thursday
| Friday
| Saturday
| Sunday.
Check day.
Check Monday.

day je typ. Monday až Sunday sú jeho konštruktory; každý z nich vytvorí jednu hodnotu typu day. Konštruktory iných induktívnych typov môžu prijímať argumenty. V tomto príklade ich nemajú.

Všeobecný zápis má tvar Inductive MenoTypu : Type := ..., kde za := nasledujú konkrétne konštruktory a ich typy. Tri bodky tu vyjadrujú opis formátu, nie spustiteľný príkaz Rocqu. Typ konštruktorov závisí od definovaného typu; preto sa učíme prednostne z úplných príkladov.

Type označuje univerzum typov. Pri logických tvrdeniach sa neskôr stretneme aj s Prop. Podrobné rozlíšenie univerzov teraz nepotrebujeme.

Analýza podľa konštruktora: match

Výraz match vyberie vetvu podľa konštruktora spracúvanej hodnoty. V prípade typu day môžeme definovať nasledujúci kalendárny deň:

Definition next_day (d : day) : day :=
  match d with
  | Monday    => Tuesday
  | Tuesday   => Wednesday
  | Wednesday => Thursday
  | Thursday  => Friday
  | Friday    => Saturday
  | Saturday  => Sunday
  | Sunday    => Monday
  end.
Compute next_day Friday.

Výstup:

= Saturday
: day

Výsledok next_day Friday je Saturday. Názov next_day zodpovedá tomu, že príklad počíta aj s víkendom.

Pri štandardnom type bool sú konštruktory true a false. Obe možnosti možno rozlíšiť priamo:

Print bool.
Definition negb_ok (b : bool) : bool :=
  match b with
  | true => false
  | false => true
  end.
Compute negb_ok true.

Výstup:

= false
: bool

Podobne pri type nat symbol 0 reprezentuje konštruktor O a vzor _ znamená „ľubovoľný iný prípad“:

Definition is_zero (n : nat) : bool :=
  match n with
  | 0 => true
  | _ => false
  end.
Compute is_zero 0.
Compute is_zero 3.

Výstupy:

= true
: bool
= false
: bool

Podčiarkovník _ nepomenuje zachytenú hodnotu, preto je vhodný vtedy, keď ju vetva nepotrebuje. V druhej vetve is_zero pokrýva všetky nenulové prirodzené čísla.

Úplnosť analýzy prípadov

Rocq vyžaduje, aby match pokryl všetky možné konštruktory spracúvaného typu. Nasledujúci príkaz ukazuje zámerne neúspešný pokus; predpona Fail potvrdí, že vnútornú definíciu Rocq odmietol, a umožní pokračovať vo vykonávaní súboru:

Fail Definition negb_bad (b : bool) : bool :=
  match b with
  | true => false
  end.

Typ bool má aj konštruktor false, pre ktorý chýba vetva. Opravená definícia negb_ok vyššie pokrýva oba prípady. Toto je problém úplnosti vzorov; nesúvisí s termináciou rekurzie.

Bežné programovacie jazyky ako OCaml alebo Haskell môžu neúplný pattern matching akceptovať, často s upozornením. Ak počas behu nastane nepokrytý prípad, výpočet môže skončiť chybou. Rocq takúto definíciu funkcie neprijme.

Prirodzené čísla ako rekurzívny induktívny typ

Základnú myšlienku štandardnej definície nat možno znázorniť takto:

Inductive nat : Type :=
| O
| S (n : nat).

Tento zápis je zjednodušená ukážka, ktorú teraz nevykonávame: štandardný typ nat je už v prostredí zavedený. Konštruktor O predstavuje nulu, S n nasledovníka čísla n. Na rozdiel od day sa nat vyskytuje v type argumentu vlastného konštruktora S, preto je rekurzívny. Jeho skutočnú definíciu si môžete pozrieť príkazmi:

Print nat.
Check O.
Check S.
Compute S (S O).

Štruktúra O alebo S n nám dáva dve vetvy pre match a zároveň spôsob, ako pri rekurzii prejsť k menšiemu podtermu n.

Rekurzívne funkcie pomocou Fixpoint

Rekurzívna funkcia sa definuje príkazom Fixpoint. Pre faktoriál platí:

$$ \mathit{factorial}(n)= \begin{cases} 1, & n=0,\\ n\cdot\mathit{factorial}(n-1), & n>0. \end{cases} $$

Pri prirodzenom čísle tvaru S k platí n = S k. Rekurzívne volanie vykonáme na podterme k:

Fixpoint factorial (n : nat) : nat :=
  match n with
  | 0 => 1
  | S k => n * factorial k
  end.
Check factorial.
Compute factorial 5.

Výstup:

factorial : nat -> nat
= 120
: nat

Check factorial. vráti nat -> nat a Compute factorial 5. vráti 120. V druhej vetve je k štrukturálne menší podterm pôvodného argumentu S k; preto Rocq túto rekurziu akceptuje. Samotný fakt, že v tele vidíme menšie číslo, nestačí: kontrola sleduje vhodný štrukturálny vzťah medzi argumentmi.

Kontrola terminácie

Gallina povoľuje rekurzívnu definíciu iba vtedy, keď Rocq dokáže overiť jej termináciu. Bežnú neobmedzenú všeobecnú rekurziu preto priamo nepovoľuje. Nasledujúce volanie používa ten istý argument n, takže nespĺňa požiadavku štrukturálneho zmenšovania:

Fail Fixpoint loop (n : nat) : nat :=
  loop n.

Fail opäť označuje zámerne odmietnutý pokus. Kontrastuje s factorial, kde volanie pracuje s podtermom k. Kontrola terminácie súvisí s logickými vlastnosťami systému a s výpočtami, ktoré Rocq používa pri kontrole typov. Zložitejšie spôsoby definovania terminujúcich funkcií budeme študovať neskôr.

Moduly a vlastný typ nat

Modul vytvorí priestor mien. Objekt definovaný v module možno zvonka pomenovať kvalifikovaným názvom, napríklad NatPlayground.plus. Vlastnú verziu prirodzených čísel preto uzavrieme do modulu:

Module NatPlayground.

Inductive nat : Type :=
| O
| S (n : nat).

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S k => S (plus k m)
  end.

Fixpoint mult (n m : nat) : nat :=
  match n with
  | O => O
  | S k => plus m (mult k m)
  end.

Compute plus (S O) (S O).
Compute mult (S (S O)) (S (S O)).

End NatPlayground.

Výstupy oboch výpočtov v module zobrazujú hodnoty zostavené z jeho vlastných konštruktorov:

= S (S O)
: nat
= S (S (S (S O)))
: nat

Vnútri modulu sa meno nat vzťahuje na NatPlayground.nat; pri výpise po uzavretí modulu Rocq môže použiť kvalifikované názvy.

V definícii plus sa prvý argument postupne mení z S k na k. V definícii mult sa ten istý menší podterm používa pri rekurzívnom volaní mult k m. V oboch prípadoch ide o štrukturálnu rekurziu. Po uzavretí modulu sú vlastné objekty dostupné napríklad takto:

Check NatPlayground.nat.
Check NatPlayground.plus.
Compute NatPlayground.plus
  (NatPlayground.S NatPlayground.O)
  (NatPlayground.S NatPlayground.O).

Výstup posledného výpočtu:

= NatPlayground.S (NatPlayground.S NatPlayground.O)
: NatPlayground.nat

Typy NatPlayground.nat a štandardný nat sú rôzne. Modul bráni kolízii mien pri písaní príkladov; pri odkazoch na objekty používame ich kvalifikované názvy. Nie je presné povedať, že vlastná definícia automaticky zmení definíciu štandardnej knižnice.

Notácie a rozsahy notácií

Notácia nemení význam funkcie; poskytuje alternatívny syntaktický zápis termu. Napríklad 3 + 4 je zápis aplikácie funkcie sčítania na dva argumenty:

Compute Nat.add 3 4.
Compute 3 + 4.
Locate "+".

Rocq môže viazať ten istý symbol na rôzne funkcie podľa rozsahu notácie (scope). Notácia pre prirodzené čísla je v nat_scope; medzi ďalšie používané rozsahy patria bool_scope, list_scope a type_scope. Niektoré rozsahy sa otvárajú podľa očakávaného typu, iné môžeme vybrať explicitne. Príkaz Locate ukazuje možné interpretácie symbolu a Print Scope nat_scope. vypíše notácie daného rozsahu.

Vlastnú notáciu môžeme bezpečne zaviesť v novom rozsahu. Nasledujúci samostatný modul pokračuje v práci s vlastným typom nat:

Module NatNotation.
Import NatPlayground.

Declare Scope playground_nat_scope.
Delimit Scope playground_nat_scope with pnat.
Notation "a + b" := (plus a b)
  (at level 50, left associativity) : playground_nat_scope.
Notation "a * b" := (mult a b)
  (at level 40, left associativity) : playground_nat_scope.

Compute ((S O) + (S O))%pnat.
Print Scope playground_nat_scope.

End NatNotation.

Parameter at level určuje prioritu: v bežnom rozsahu úrovní má nižšie číslo vyššiu prioritu, takže násobenie na úrovni 40 sa zoskupí skôr než sčítanie na úrovni 50. left associativity určuje zoskupovanie operátorov rovnakej priority zľava. Sufix %pnat vyberie vlastný rozsah; tým sa vyhneme zámene so štandardným + a *.

Polymorfizmus a implicitné argumenty

id_nat funguje iba na hodnotách typu nat. Polymorfná identická funkcia prijíma typ A a hodnotu tohto typu; výsledok má opäť typ A:

Definition id_poly (A : Type) (value : A) : A := value.
Definition id_poly2 : forall A : Type, A -> A :=
  fun A value => value.
Check id_poly.
Compute id_poly nat 3.
Compute id_poly _ 3.

Výstup Check id_poly. a oboch výpočtov:

id_poly : forall A : Type, A -> A
= 3
: nat
= 3
: nat

Argument A určuje typ ďalšieho argumentu. V poslednom výpočte podčiarkovník žiada Rocq, aby A odvodil z typu hodnoty 3. Zápis forall A : Type, A -> A vyjadruje, že funkcia funguje pre každý typ A.

Ak parameter uzavrieme do zložených zátvoriek, stane sa implicitným argumentom. Bežne ho potom pri aplikácii vynechávame:

Definition id_poly3 {A : Type} (value : A) : A := value.
Compute id_poly3 3.
Compute @id_poly3 nat 3.
Compute id_poly3 (A := nat) 3.

Všetky tri výpočty vrátia:

= 3
: nat

Symbol @ vypne v danom použití implicitnosť, takže typ nat zapíšeme explicitne. Pomenovaný argument (A := nat) je druhý spôsob, ako typ uviesť bez zmeny ostatných argumentov. Tieto možnosti sa budú hodiť pri typovo všeobecných definíciách v ďalších lekciách.

Vzájomná rekurzia

Dve funkcie sa môžu volať navzájom. Príkaz with spája ich definície do jednej vzájomne rekurzívnej skupiny. Nasledujúce funkcie zisťujú paritu čísla:

Fixpoint is_even (n : nat) : bool :=
  match n with
  | 0 => true
  | S k => is_odd k
  end
with is_odd (n : nat) : bool :=
  match n with
  | 0 => false
  | S k => is_even k
  end.

Compute is_even 4.
Compute is_odd 5.

Výstupy oboch volaní:

= true
: bool
= true
: bool

Každé rekurzívne volanie pracuje s podtermom k čísla S k. Rocq teda môže overiť termináciu celej skupiny.

Extrakcia kódu

Z výpočtového obsahu definovaného v Galline možno generovať kód pre bežné funkcionálne jazyky, napríklad OCaml. Pri faktoriáli stačí načítať podporu extrakcie a určiť výstupný súbor:

From Corelib Require Extraction.
Extraction Language OCaml.
Extraction "factorial.ml" factorial.

Posledný príkaz vytvorí súbor factorial.ml v pracovnom adresári procesu Rocq. Extrakcia je samostatný ďalší krok po definovaní a typovej kontrole funkcie; výsledný súbor je vhodné osobitne skompilovať a otestovať. Rocq podporuje aj extrakciu do ďalších funkcionálnych jazykov.

Programovanie v Rocqu

Compute (! false &&& false).                (* false *)
Compute (true ||| true &&& false).          (* true *)
Compute (false &&& true ---> false).        (* true *)
Compute (false ---> true ---> false).       (* true *)