Údajové štruktúry a polymorfizmus

Úvod do údajových štruktúr

V tejto časti sa zoznámime s niekoľkými základnými údajovými štruktúrami v prostredí Rocq, ktoré sú základom pre reprezentáciu dát a pre logické uvažovanie o programoch.

Budeme postupne preberať:

• Jednoduché štruktúry ako dvojice (pair)
• Dynamické štruktúry ako zoznamy (list)
• Formálne uvažovanie o týchto štruktúrach pomocou logických dôkazov
• Polymorfné verzie, ktoré fungujú pre ľubovoľný typ
• Typ option, ktorý slúži na reprezentáciu čiastočne definovaných funkcií

Potrebné knižnice

Načítame knižnicu reťazcov pre neskorší príklad chybovej správy. Kódové bloky vykonávame postupne v poradí prednášky.

From Stdlib Require Import Strings.String.
Open Scope string_scope.

Dvojica (pair)

Definícia natpair

Začneme s dvojicou prirodzených čísel:

Module natpair.

Inductive natpair : Type :=
  | pair (n m : nat).

natpair je názov induktívneho typu, pair jeho jediný dátový konštruktor. Dvojicu vytvoríme aplikovaním pair na dva argumenty typu nat.

Check (pair 2 8).  
(* pair 2 8 : natpair *)

Projekčné funkcie

Pre extrakciu hodnôt typu natpair potrebujeme dve projekcie: fst (first) a snd (second).

Definition fst (x: natpair) : nat := 
  match x with
  | pair n m => n
  end.

Definition snd (x: natpair) : nat := 
  match x with
  | pair n m => m
  end.

Compute (fst (pair 3 9)).  (* 3 *)
Compute (snd (pair 3 9)).  (* 9 *)
Compute (fst (pair (snd (pair 1 4)) 9)).  (* 4 *)

Notácia pre dvojice

Zavedieme štandardnú notáciu pre dvojicu:

Notation "( x , y )" := (pair x y).

Check (1,8).  (* (1, 8) : natpair *)

Funkcia swap

Funkcia na prehodenie prvkov dvojice:

Definition swap (p : natpair) : natpair :=
  match p with
  | pair m n => pair n m 
  end. 

Compute swap (1,8).  (* (8, 1) *)

Zavedenú notáciu možno použiť aj pri pattern matchingu a pri konštruovaní výsledku:

Definition swap' (p : natpair) : natpair :=
  match p with
  | (m,n) => (n,m) 
  end. 

Compute swap' (1,8).  (* (8, 1) *)

Dvojnásobné prehodenie komponentov vráti pôvodnú dvojicu; túto vlastnosť nazývame involutívnosťou:

Theorem swap_involutive : forall (p : natpair),
  swap (swap p) = p.
Proof.
  intros p.
  destruct p.
  reflexivity.
Qed.

Logické uvažovanie o dvojici čísel

Triviálny dôkaz

Príklad: ak máme n a m, vieme okamžite ukázať, že (n,m) = (fst (n,m), snd (n,m)).

Theorem pair_reconstruction' : forall (n m : nat),
  (n,m) = (fst (n,m), snd (n,m)).
Proof.
  simpl. 
  (* ============================
    forall n m : nat, (n, m) = (n, m) *)

  reflexivity. 
Qed.

Problém s abstraktnou dvojicou

Avšak reflexivity už nestačí, ak tvrdenie napíšeme prirodzenejším spôsobom: p = (fst p, snd p).

Tu sa totiž nedá ďalej redukovať výraz so simpl:

Theorem pair_reconstruction_stuck : forall (p : natpair),
  p = (fst p, snd p).
Proof.
  simpl. 
  (* Každá dvojica vzniká konštruktorom pair, ale pri premennej p
     nepoznáme jej komponenty. Preto fst p a snd p nemožno redukovať.
     ============================
     forall p : natpair, p = (fst p, snd p) *)
Abort.

Riešenie pomocou destruct

Riešením je "odkryť štruktúru" dvojice p, aby sa simpl dokázal pozrieť do definícií fst a snd. Pomocou destruct p vykonáme analýzu jediného konštruktora:

Theorem pair_reconstruction : forall (p : natpair),
  p = (fst p, snd p).
Proof.
  intros p.
  (* p : natpair
     ============================
     p = (fst p, snd p) *)

  destruct p. 
  (* Rozloží p na jeho komponenty 

     n, m : nat
     ============================
     (n, m) = (fst (n, m), snd (n, m)) *)

  simpl.
  reflexivity.
Qed.

End natpair.

Zoznam (list)

Definícia natlist

Module natlist.

Inductive natlist : Type :=
| nil
| cons (n: nat) (l:natlist).

Check (nil).  (* nil : natlist *)
Check (cons 1 (cons 3 nil)).  (* cons 1 (cons 3 nil) : natlist *)

Zavedenie štandardnej notácie

Notation "[]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Notation "x :: l" := (cons x l) 
                     (at level 60, right associativity).

Check [].  (* [] : natlist *)
Check [1;2;3].  (* [1; 2; 3] : natlist *)
Check 1::[2;3].  (* [1; 2; 3] : natlist *)

Pravá asociativita

(* right associativity *)
Check (1 :: 2 :: 3 :: nil).
Check (1 :: (2 :: (3 :: nil))).
(* Oba zápisy označujú ten istý term typu natlist. *)

Pravá asociativita je vlastnosť parsovania notácie: 1 :: 2 :: 3 :: nil sa číta ako 1 :: (2 :: (3 :: nil)). Príkaz Check overuje typovú správnosť výrazu a vypisuje jeho typ; nedokazuje pravdivosť rovnosti. Compute výraz redukuje a vypisuje výsledok. Ani jeden príkaz nenahrádza všeobecný dôkaz.

Priorita operátora ::

at level 60 - priorita operátora (nižšie číslo → vyššia priorita)

Napríklad operátory + a - majú level 50, operátor * má level 40

Compute 1+2::5::nil.  (* výsledok je [3; 5] a nie 1 + [2;5] *)

Funkcie pre prácu so zoznamami

Funkcia repeat

Prijíma číslo n a počet count a vracia zoznam dĺžky count, kde každý prvok je n:

Fixpoint repeat (n count :nat) : natlist := 
  match count with
  | 0 => []
  | S m => n :: (repeat n m)
  end.

Compute repeat 1 5.  (* [1; 1; 1; 1; 1] *)

Funkcia length

Počíta počet prvkov v zozname:

Fixpoint length (l:natlist) : nat := 
  match l with 
  | [] => 0
  | head :: tail => 1 + (length tail)
  end.

Compute length [].  (* 0 *)
Compute length [1;2;3;5;9;44;1;1].  (* 8 *)
Compute length nil.  (* 0 *)
Compute length (cons 1 (cons 3 nil)).  (* 2 *)

Funkcia append

Spojí dva zoznamy:

Fixpoint append (l1 l2: natlist) : natlist :=
  match l1 with
  | [] => l2
  | head::tail => head::(append tail l2)
  end.

Compute append [] [1].  (* [1] *)
Compute append [2;5;6] [1;3].  (* [2; 5; 6; 1; 3] *)

Zavedieme aj infixovú notáciu ++. Jej pravá asociativita určuje čítanie l1 ++ l2 ++ l3 ako l1 ++ (l2 ++ l3). Rovnosť s (l1 ++ l2) ++ l3 je samostatná matematická vlastnosť funkcie append, ktorú neskôr dokážeme vetou app_assoc:

Notation "x ++ y" := (append x y) 
                     (at level 60, right associativity). 

Compute [] ++ [1].  (* [1] *)
Compute [2;5;6] ++ [1;3].  (* [2; 5; 6; 1; 3] *)

Funkcie head a tail

Pri definovaní funkcie musíme určiť správanie pre všetky prípustné vstupy vrátane prázdneho zoznamu. V našej implementácii head vraciame pre [] dodatočný argument default. Funkcia tail ho nepotrebuje: chvost prázdneho zoznamu definujeme ako [].

Predvolená hodnota pri head nerozlišuje, či prvok existoval. Neskôr pomocou typu option vyjadríme neprítomnosť výsledku bez náhradnej hodnoty typu nat.

Definition head (l: natlist) (default:nat) : nat := 
  match l with
  | [] => default
  | h::t => h
  end.

Definition tail (l: natlist) : natlist := 
  match l with
  | [] => nil
  | h::t => t
  end.

Compute head [] 999.  (* 999 *)
Compute head [5;6;89] 999.  (* 5 *)
Compute tail [].  (* [] *)
Compute tail [5;6;89].  (* [6; 89] *)

Funkcia reverse

Prehodí poradie prvkov:

Fixpoint reverse l : natlist :=
  match l with
  | [] => []
  | hd :: tl => reverse tl ++ [hd]
  end.

Compute reverse [1;2;3;4].  (* [4; 3; 2; 1] *)

Táto implementácia má pri obvyklom modeli nákladov časovú zložitosť $O(n^2)$: append opakovane prechádza obráteným chvostom, aby pripojil jeden prvok. Jednoduchá definícia je vhodná na demonštráciu rekurzie a dokazovania.

Logické uvažovanie o zozname natlist

Veta: Pripojenie prázdneho zoznamu vľavo

Theorem nil_app_l : forall l, []++l=l.
Proof.
  simpl. reflexivity.
Qed.

Princíp indukcie nad zoznamom

Pri použití induction l Rocq vytvorí dva podciele podľa konštruktorov zoznamu. Pre vlastnosť $P$ rozlišujeme:

• Základný prípad: dokážeme $P([])$.
• Indukčný predpoklad: pre chvost $xs$ predpokladáme $P(xs)$.
• Indukčný cieľ: dokážeme $P(x::xs)$.
• Indukčný krok: pre ľubovoľné $x,xs$ ukážeme $P(xs)\Rightarrow P(x::xs)$.

Základný prípad a indukčný krok tvoria pravidlo indukcie pre $P:\mathsf{natlist}\to\mathsf{Prop}$:

$$ \frac{P([])\qquad \forall x:\mathsf{nat},\;\forall xs:\mathsf{natlist},\; P(xs)\Rightarrow P(x::xs)} {\forall l:\mathsf{natlist},\;P(l)} $$

Podobne ako pri indukcii nad prirodzenými číslami odvodíme vlastnosť väčšej štruktúry z vlastnosti jej rekurzívnej časti; konštruktor cons tu hrá úlohu nasledovníka S. Samotný indukčný predpoklad je $P(xs)$, nie celý indukčný krok.

Veta: Pripojenie prázdneho zoznamu vpravo

V indukčnom kroku je IHl : l ++ [] = l predpoklad pre chvost a (n :: l) ++ [] = n :: l aktuálny cieľ. simpl odkryje rekurzívnu definíciu append; rewrite IHl potom nahradí l ++ [] zoznamom l.

Theorem l_app_nil : forall l, l++[]=l.
Proof.
  intros. induction l.
  - (* ============================
       Subgoal 1/2: Základný prípad l = []

       ============================
       [] ++ [] = [] *)

    reflexivity.
  - (* ============================
       Subgoal 2/2: Indukčný krok pre zoznam n :: l

        n : nat
        l : natlist
        IHl : l ++ [] = l
        ============================
        (n :: l) ++ [] = n :: l *)
       
    simpl. rewrite IHl. reflexivity.
Qed.

Check pred. 
(*Nat.pred : nat -> nat*)

Veta: Dĺžka chvosta zoznamu

Chvost neprázdneho zoznamu má o jeden prvok menej. Veta platí aj pre prázdny zoznam: length [] = 0, length (tail []) = 0 a pred 0 = 0.

Theorem pred_l_length: forall l, 
  pred (length l) = (length (tail l)).
Proof.
  intros. destruct l.
  - (* ============================
       Subgoal 1/2: Prípad prázdneho zoznamu

       ============================
       Nat.pred (length []) = length (tail []) *)

    simpl. reflexivity.
  - (* ============================
       Subgoal 2/2:  Prípad neprázdneho zoznamu

        n : nat
        l : natlist
        ============================
        Nat.pred (length (n :: l)) = length (tail (n :: l)) *)
        
    simpl. reflexivity.
Qed.

Veta: Funkcia append je asociatívna

Theorem app_assoc: forall l1 l2 l3, 
  (l1++l2)++l3 = l1++(l2++l3).
Proof.
  intros.
  Set Printing Parentheses. 
  (** Slúži iba na zobrazenie úplnej štruktúry výrazov so všetkými zátvorkami.
      Nemá vplyv na samotný dôkaz, používa sa len na lepšie porozumenie a vizualizáciu. **)

  induction l1 as [| n l1' IHl1'].
  - (* ============================
       Subgoal 1/2: Základný prípad

       l2, l3 : natlist
       ============================
       (([] ++ l2) ++ l3) = ([] ++ (l2 ++ l3)) *)

    simpl. reflexivity.
  - (* ============================
       Subgoal 2/2: Indukčný krok

       n : nat
       l1', l2, l3 : natlist
       IHl1' : ((l1' ++ l2) ++ l3) = (l1' ++ (l2 ++ l3))
       ============================
       (((n :: l1') ++ l2) ++ l3) = ((n :: l1') ++ (l2 ++ l3)) *)

    simpl. rewrite IHl1'. reflexivity.
Qed.
Unset Printing Parentheses.

Lema: Dĺžka pri pripojení jedného prvku

Pri dôkaze zachovania dĺžky obráteného zoznamu potrebujeme vedieť, ako sa zmení dĺžka po pripojení jedného prvku na koniec. Túto vlastnosť vyjadruje pomocná lema rev_aux:

Lemma rev_aux: 
  forall l n, S (length l) = length (l ++ [n]).
Proof.
  intros.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite IHl. reflexivity.
Qed.

Veta: Dĺžka obráteného zoznamu

Theorem rev_length: forall l, length l = length (reverse l).
Proof.
  intros.
  induction l.
  - simpl. reflexivity.
  - simpl. rewrite IHl. apply rev_aux.
Qed.

Veta: Obrátenie distribuuje cez spojenie

Ak spojíme dva zoznamy a potom výsledok obrátíme, dostaneme rovnaký zoznam, ako keby sme najprv obrátili každý zoznam osobitne a potom ich spojili v opačnom poradí.

Lemma rev_app_distr : forall l1 l2,
  reverse (l1 ++ l2) = (reverse l2) ++ (reverse l1).
Proof.
  intros l1 l2.
  induction l1 as [| h t IH].
  - (* ============================
       Subgoal 1/2: Základný prípad

       l2 : natlist
       ============================
       reverse ([] ++ l2) = reverse l2 ++ reverse [] *)

    simpl. rewrite l_app_nil. reflexivity.
  - (* ============================
       Subgoal 2/2: Indukčný krok

       h : nat
       t, l2 : natlist
       IH : reverse (t ++ l2) = reverse l2 ++ reverse t
       ============================
       reverse ((h :: t) ++ l2) = reverse l2 ++ reverse (h :: t) *)
    
    simpl.
    rewrite IH.
    rewrite app_assoc.
    reflexivity.
Qed.

Veta: Dvakrát obrátený zoznam

Konkrétny výpočet ukáže výsledok pre jeden zoznam. Veta rev_rev_l dokazuje vlastnosť pre všetky zoznamy a využíva predchádzajúcu lemu rev_app_distr. Rovnosť = vytvára tvrdenie typu Prop, nie booleovskú hodnotu; Compute nad rovnosťou preto nevracia true.

Compute reverse (reverse [1;2;3]).  (* [1; 2; 3] : natlist *)

Theorem rev_rev_l: forall l, reverse (reverse l) = l.
Proof.
  intros.
  induction l.
  - simpl. reflexivity.
  - simpl. 
    (* n : nat
       l : natlist
       IHl : reverse (reverse l) = l
       ============================
       reverse (reverse l ++ [n]) = n :: l *)

    rewrite rev_app_distr. 
    (* n : nat
       l : natlist
       IHl : reverse (reverse l) = l
       ============================
       reverse [n] ++ reverse (reverse l) = n :: l *)

    rewrite IHl. simpl. reflexivity.
Qed.

Typ option a čiastočné funkcie

Vo výpočtovom fragmente Rocq definujeme úplné funkcie a rekurzívne definície podliehajú kontrole ukončenia. Čiastočnú matematickú funkciu však môžeme reprezentovať úplnou funkciou s vhodným návratovým typom, napríklad option.

Príklad: Výber prvku zoznamu

Zoznamy indexujeme od nuly: index 0 označuje prvý prvok. Najprv použijeme náhradnú hodnotu 0 pre index mimo rozsahu.

Fixpoint nth_bad (l:natlist) (n:nat) : nat :=
  match l with 
  | [] => 0   (* zvolím nejakú predvolenú hodnotu *)
  | hd::tl => match n with
             | 0 => hd
             | S m => nth_bad tl m 
             end
  end.

Compute nth_bad [] 4.  (* 0 *)
Compute nth_bad [10;12;0] 1.  (* 12 *)
Compute nth_bad [10;12;0] 2.  (* 0 *)

Problém: Ako viem, či 0 bol n-ty prvok, alebo som zvolil hodnotu mimo rozsahu zoznamu?

Namiesto nerozlíšiteľnej náhradnej hodnoty zvolíme návratový typ, ktorý explicitne zachytí neprítomnosť prvku.

Riešenie: typ option

Zmeníme návratový typ funkcie nth_bad tak, aby obsahoval aj možnosť chyby. Tento typ nazveme natoption:

Inductive natoption : Type := 
| None
| Some (n:nat).

Funkcia nth_error

Teraz je možné zmeniť pôvodnú definíciu funkcie nth_bad tak, aby vrátila None, keď je zoznam príliš krátky, a Some m, keď má zoznam dostatok prvkov a m sa nachádza na pozícii n. Túto novú funkciu nazveme nth_error, aby sme naznačili, že môže skončiť chybou.

Fixpoint nth_error (l:natlist) (n:nat) : natoption := 
  match l with
  | [] => None
  | hd::tl => match n with
             | 0 => Some hd
             | S m => nth_error tl m 
             end
  end.

Compute nth_error [] 4.  (* None *)
Compute nth_error [10;12;0] 1.  (* Some 12 *)
Compute nth_error [10;12;0] 2.  (* Some 0 *)

Some 0 znamená, že prvok existuje a jeho hodnota je 0. None znamená, že požadovaný prvok neexistuje. Funkcia nth_error je úplná: pre každý zoznam a index vráti jednu z týchto možností.

Option s chybovou hláškou

Inductive natoptionerror : Type := 
| None' (s:string)
| Some' (n:nat).

Fixpoint nth_error' (l:natlist) (n:nat) : natoptionerror := 
  match l with
  | [] => None' "mimo rozsahu zoznamu"
  | hd::tl => match n with
             | 0 => Some' hd
             | S m => nth_error' tl m 
             end
  end.

Compute nth_error' [] 4.  (* None' "mimo rozsahu zoznamu" *)
Compute nth_error' [10;12;0] 1.  (* Some' 12 *)
Compute nth_error' [10;12;0] 2.  (* Some' 0 *)

End natlist.

Polymorfné verzie zoznamu, dvojice a typu option

V predchádzajúcej časti sme definovali typy dvojice, zoznamu a option pre prirodzené čísla. Ak by sme ich potrebovali pre iný typ, museli by sme definície typov aj príslušných funkcií prepísať.

Rocq podporuje polymorfizmus; využijeme ho na definíciu dvojice, zoznamu a typu option parametrizovaných typmi ich prvkov.

Polymorfný zoznam

Definícia

natlist : Type je konkrétny typ zoznamov prirodzených čísel. Naproti tomu list : Type -> Type bude typový konštruktor: z typu prvkov vytvorí typ zoznamu. list nat : Type a list bool : Type sú dva konkrétne typy vytvorené tou istou polymorfnou definíciou.

Vlastné polymorfné zoznamy umiestnime do modulu PolymorphicList; dvojice a didaktický typ option budú mať samostatné moduly.

Module PolymorphicList.

Inductive list (X:Type) : Type :=
| nil 
| cons (x : X) (l: list X).

Implicitné argumenty a notácia zoznamu

Typový parameter X konštruktorov nil a cons necháme pri bežnom použití odvodiť z kontextu. Príkaz Arguments mení spôsob zadávania argumentov, nie definíciu ani typ konštruktorov. Polymorfizmus umožňuje pracovať s rôznymi typmi, inferencia dopĺňa chýbajúce typové informácie a implicitnosť dovoľuje typový argument pri volaní vynechať. Hneď potom zavedieme notáciu zoznamu, ktorú budeme používať v ďalších príkladoch:

Arguments nil {X}.
Arguments cons {X}.

Notation "x :: y" := (cons x y)
                     (at level 60, right associativity).
Notation "[ ]" := nil.
Notation "[ x ; .. ; y ]" := (cons x .. (cons y []) ..).

Čo je polymorfný zoznam?

list prijíma typový parameter X a vytvára typ list X. Konštruktory nil a cons potom vytvárajú hodnoty tohto typu; typový konštruktor odlišujeme od dátových konštruktorov.

Pre ľubovoľný konkrétny typ X je typ list X induktívne definovaná množina zoznamov, ktorých prvky sú typu X.

Check list.  
(* list : Type -> Type *)

Polymorfné konštruktory

Parameter X v definícii list sa stáva aj parametrom konštruktorov nil a cons. Ich úplný polymorfný typ zobrazíme pomocou @:

Pri bežnom použití už typový argument nepíšeme; napríklad prázdny zoznam opatrený typom a zoznam dvoch čísel zapíšeme takto:

Check @nil.   (* forall X : Type, list X *)
Check @cons.  (* forall X : Type, X -> list X -> list X *)

Check ([] : list nat).  (* [] : list nat *)
Check [1;2].           (* [1; 2] : list nat *)

Polymorfná funkcia repeat

repeat demonštruje polymorfizmus: tá istá definícia je parametrizovaná typom X a vytvára zoznam jeho prvkov. Pri definícii je X explicitný; po deklarácii Arguments repeat {X} ho pri volaní odvodí Rocq.

Fixpoint repeat (X:Type) (a:X) (count : nat): list X :=
  match count with
  | 0 => []
  | S m => a :: repeat X a m
  end.

Arguments repeat {X}.

Compute repeat true 5.  (* [true; true; true; true; true] : list bool *)
Compute repeat 1 5.     (* [1; 1; 1; 1; 1] : list nat *)

Odvodenie typovej anotácie

Definícia bez explicitnej typovej anotácie

Inferencia typov dopĺňa chýbajúce typové informácie. V repeat' Rocq odvodí typy parametrov X, a a count z návratového typu a tela; polymorfizmus zostáva rovnaký ako pri repeat.

Fixpoint repeat' X a count: list X :=
  match count with
  | 0 => []
  | S m => a :: repeat' X a m
  end.

Check repeat'.  (* forall X : Type, X -> nat -> list X *)

Automatické odvodzovanie pomocou _

V repeat'' používame _ na miestach typových argumentov. Keďže typové argumenty konštruktorov sú už implicitné, pomocou @ ich v definícii dočasne sprístupníme; Rocq ich potom doplní z kontextu. Aj v type list _ určí typ prvkov podľa vytvoreného zoznamu.

Fixpoint repeat'' X a count: list X :=
  match count with
  | 0 => @nil _
  | S m => @cons _ a (repeat'' _ a m)
  end.

Check repeat''. (* forall X : Type, X -> nat -> list X *)

Definition list123' : list _ :=
  [1;2;3].

Check list123'.
(* list123' : list nat *)

Definition list123'' := 1 :: [2;3].

Alternatívna syntax s implicitnými argumentmi

Alternatívne môžeme deklarovať argument ako implicitný priamo pri definícii funkcie, tým že ho uzavrieme do zložených zátvoriek namiesto zátvoriek obyčajných:

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0 => []
  | S count' => x :: repeat''' x count'
  end.

Compute repeat''' true 5.        (* [true; true; true; true; true] : list bool *)
Compute @repeat''' bool true 5.  (* rovnaký zoznam : list bool *)

Problém s implicitnými argumentami

Po Arguments nil {X} je X implicitný. Zápis nil nat sa preto pokúša aplikovať už vytvorený zoznam ako funkciu na nat; nejde iba o nedostatok informácií na inferenciu. Typová anotácia určí očakávaný typ a @nil nat poskytne parameter explicitne:

Fail Definition mynil := nil nat.  (* Chyba! *)
(* The command has indeed failed with message:
   Illegal application (Non-functional construction): 
   The expression "nil" of type
   "list ?X"
   cannot be applied to the term
   "nat" : "Set" *)

(* Riešenia: *)
Definition mynil : list nat := nil.
Definition mynil' := @nil nat.

Skutočný nedostatok informácií nastane pri samotnom nil bez očakávaného typu: nie je určený typ prvkov. Preto používame jednu z uvedených anotovaných definícií.

Polymorfné spájanie zoznamov

Notáciu ++ môžeme zaviesť až po definícii funkcie append, na ktorú sa odvoláva.

Fixpoint append {X:Type} (l1 l2: list X) : list X := 
  match l1 with
  | [] => l2
  | x :: xs => x :: append xs l2
  end.

Notation "x ++ y" := (append x y)
                     (at level 60, right associativity).

Compute append [2] [1].       (* [2; 1] : list nat *)
Check [1].                    (* [1] : list nat *)
Compute [1;2] ++ [3;5;6].     (* [1; 2; 3; 5; 6] : list nat *)

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

End PolymorphicList.
Import PolymorphicList.

Import sprístupní definície a notácie zoznamov pre nasledujúce príklady; ich kvalifikované názvy, napríklad PolymorphicList.list, zostávajú dostupné.

Polymorfná dvojica

Definícia

Typový konštruktor product vytvorí typ dvojice z typov jej dvoch komponentov. Aj tu najprv nastavíme implicitné typové argumenty a zavedieme notáciu, až potom použijeme príklady.

Module PolymorphicPair.

Inductive product (X:Type) (Y:Type): Type :=
| pair (m:X) (n:Y).

Arguments pair {X} {Y}.

(* Notácia pre dvojicu *)
Notation "( x , y )" := (pair x y).

(* Vlastný rozsah predíde prepísaniu knižničnej notácie súčinu. *)
Declare Scope polymorphic_pair_scope.
Delimit Scope polymorphic_pair_scope with ppair.
Notation "X * Y" := (product X Y) : polymorphic_pair_scope.
Open Scope polymorphic_pair_scope.

Príklady polymorfnej dvojice

Check product.  (* product : Type -> Type -> Type *)
Check @pair.    (* forall X Y : Type, X -> Y -> (X * Y)%ppair *)
Check ((3, true) : (nat * bool)%ppair).
Check pair 3.
(* pair 3 : ?Y -> (nat * ?Y)%ppair
   where ?Y : [ |- Type] *)
Check (3, true).  (* (3, true) : (nat * bool)%ppair *)

pair 3 je čiastočná aplikácia konštruktora: prvá komponenta už je 3, druhú ešte treba dodať. Tento neúplný výraz nemožno zapísať notáciou (x, y). Jeho typ ?Y je zatiaľ neurčená metavariabla, nie univerzálne kvantifikovaný parameter. Pri dvojici (3, true) sa druhý typ určí ako bool. Zápis súčinového typu používame vo vlastnom rozsahu; prípona %ppair v typových anotáciách vyberá náš product namiesto knižničného prod.

Polymorfné projekčné funkcie

Definition fst {X Y : Type} (p : (X * Y)%ppair) : X :=
  match p with
  | (x, y) => x
  end.

Definition snd {X Y : Type} (p : (X * Y)%ppair) : Y :=
  match p with
  | (x, y) => y
  end.

Compute (fst (1,true)).  (* 1 *)
Compute (snd (1,true)).  (* true *)
Compute (fst ((false,5),true)).  (* (false, 5) *)

Polymorfná funkcia swap

Polymorfná dvojica môže obsahovať hodnoty dvoch rôznych typov. product : Type -> Type -> Type z typov X a Y vytvorí súčinový typ X * Y; prehodenie komponentov preto vracia Y * X.

Definition swap {X Y : Type} (p : (X * Y)%ppair) : (Y * X)%ppair :=
  match p with 
  | (x,y) => (y,x)
  end.

Veta o dvojnásobnom prehodení dvojice

Tak ako pri nepolymorfnom swap, dvojnásobné prehodenie vráti pôvodnú dvojicu. Vlastnosť teraz platí pre ľubovoľné typy komponentov.

Theorem swap_swap_p:
  forall {X Y: Type} (p : (X * Y)%ppair), p = swap (swap p).
Proof.
  intros.
  destruct p.
  simpl.
  reflexivity.
Qed.

End PolymorphicPair.

Polymorfná verzia option

Posledným polymorfným typom bude option, ktorý zovšeobecňuje natoption z predchádzajúcej časti.

Module PolymorphicOption.

  (* Polymorfná definícia option *)
  Inductive option (X: Type) : Type :=
    | Some (x : X)
    | None.

  (* Nastavenie implicitného argumentu *)
  Arguments Some {X}.
  Arguments None {X}.

End PolymorphicOption.

Polymorfná verzia funkcie nth_error

Prázdny zoznam ani index neurčujú typ prvkov. Pri jeho výpočte preto uvedieme anotáciu list nat. Indexovanie opäť začína od nuly.

Fixpoint nth_error {X:Type} (l:list X) (n:nat): option X := 
  match l with
  | [] => None
  | hd::tl => match n with
             | 0 => Some hd
             | S m => nth_error tl m 
             end
  end.

Compute (nth_error ([] : list nat) 4).  (* None : option nat *)
Compute nth_error [10;12;0] 1.  (* Some 12 *)
Compute nth_error [10;12;0] 2.  (* Some 0 *)

Zhrnutie

V tejto prednáške sme sa naučili:

1. Základné údajové štruktúry

   • Dvojica (pair) - reprezentácia dvoch hodnôt
   • Zoznam (list) - dynamická kolekcia prvkov
   • Option - rozlíšenie existujúceho výsledku od jeho neprítomnosti

2. Logické uvažovanie o štruktúrach

   • Dôkazy vlastností pomocou destruct a induction
   • Vety o append, reverse a ďalších operáciách

3. Polymorfizmus

   • Definície parametrizované typom prvkov
   • Inferencia dopĺňa chýbajúce typové informácie
   • Implicitné argumenty menia spôsob zadania argumentov
   • Notácie pre prirodzenú syntax

4. Úplnosť funkcií

   • Úplné funkcie a kontrola ukončenia rekurzie
   • Typ option reprezentuje neprítomnosť výsledku čiastočnej matematickej funkcie

Tieto koncepty tvoria základ pre prácu s komplexnejšími dátovými štruktúrami a formálne uvažovanie o programoch v Rocq.