Lezione 1

  • Coq: un linguaggio di programmazione funzionale
    • funzioni anonime e non
    • valutazione di funzioni
    • tipi di dato algebrici
    • pattern matching
    • ricorsione
    • tipi di dato polimorfi
    • ordine superiore
    • calcolo simbolico

  • Esercizi

Funzioni

Prendiamo come esempio la definizione di una semplice funzione aritmetica f:

$$ f = x \mapsto x + 1 $$ $$ f : \mathcal{N} \to \mathcal{N} $$

e traduciamola in Coq.

Nota: anche se nat, +, * e 1 sono concetti definibili in Coq, l'ambiente iniziale non è vuoto ma contiene alcuni declarazioni utili a fare esempi come i numeri naturali e le operazioni di addizione e moltiplicazione

Concetti:

  • funzione anonima fun
  • definizione con nome Definition
  • sintassi per l'applicazione
  • comando Check per chiedere il tipo di un termine

Valutazione di funzioni (calcolo, esecuzione)

In Coq funzione = programma, ovvero le funzioni definite vengono calcolate (eseguite) quando il loro input è noto.

Chiediamo a Coq di calcolare la forma canonica dei termini seguenti:

Esempio di XXX\betaXXX-riduzione (sostituzione di x con l'argomento)

In questi due esempi f e g (nomi) sono sostituiti con i propri valori

Concetti:

  • esecuzione di programmi Eval compute in

Tipi di dato algebrici

Facciamo finta che i numeri naturali che abbiamo usato finora non siano disponibili e definiamoli noi. Lo facciamo dentro un Module, una specie di contenitore per evitare che Coq faccia confusione tra i concetti già esistenti e quelli che stiamo definendo.

true e false si chiamano costruttori, e corrispondono alle regole XXXTipo-I_nXXX nelle note del corso

I numeri naturali à la Peano

Nota: O è una o maiuscola, non la cifra zero

Nota: esistono varie sintassi alternative per la dichiarazione di tipi di dato.

Quella che abbiamo utilizzato è la più simile a quella usata nelle note del corso (e anche nei linguaggi di programmazione). Se chiediamo a Coq di stampare una dichiarazione di tipo con:

otteniamo la stampa in una sintassi alternativa.

Ora torniamo a utilizzare la dichiarazione standard di nat in quanto il sistema li stampa/parsa meglio (notazione decimale).

Concetti:

  • dichiarazione tipo induttivo Inductive
  • comando per stampare una dichiarazione induttiva Print
  • notazioni decimali per nat, e.g. 1 = S O

Pattern matching

  • In Coq l'eliminatore (chiamato XXXElXXX nelle note del corso) è fornito in kit:
    • il costrutto match fornisce l'analisi per casi
    • il costrutto Fixpoint (in seguito) fornisce l'ipotesi induttiva
  • Inoltre le regole computazionali dell'eliminatore sono date dalla combinazione di match e Fixpoint

Definiamo ora il predecessore

Esempio di esecuzione: 

   match S (S O) with
   | O => O
   | S p => p
   end

   O    ==?== S (S O)  no, proviamo la prossima clausola
   S p  ==?== S (S O)  sì, p lega (S O)

Note:

  • Ogni clausola del pattern matching è della forma | pattern => corpo dove pattern è un costruttore applicato a un numero di variabili appropriato
  • Tutti i costruttori del tipo di dato devono essere trattati da un pattern (eg anche il caso O per pred)
  • p è una variabile legata dal pattern matching e può essere utilizzata nel corpo della clausola
  • il termine a cui il match è applicato viene messo in forma canonica. In altre parole i casi del match parlano della forma canonica.

Concetti:

  • pattern matching match .. with .. end
  • forma delle clausole K x => v dove K è un costruttore
  • calcolo di una funzione definita via pattern matching

    • Ricorsione

    Definiamo l'addizione sui numeri naturali.

    $$ 0 + m = m $$ $$ S~p + m = S (p + m) $$

    Esempio di esecuzione: 

      addn 2 
  addn (S (S O)) 4
  S (addn (S O) 4)
  S (S (addn O 4))
  S (S 4)
  6

    Non tutti i programmi ricorsivi sono accettati!

    Concetti:

    • programmi ricorsivi Fixpoint
    • terminazione

    Tipi di dato polimorfi

    I tipi di dato polimorfi sono, in genere, dei contenitori per aggregare vari termini. Inoltre vogliamo spesso riutilizzare tali contenitori per aggregare termini di tipo di volta in volta diverso.

    Esempi classici:

    • La coppia XXX(a,b)XXX dove XXXa : AXXX e XXXb : BXXX
    • La lista XXXx_1 :: \ldots :: x_nXXX dove XXXx_i : AXXX

    forall A B : Type, ci indica che pair è polimorfo, ovvero A e B possono essere rimpiazzati per tipi di dato a piacere

    Come assegnare il tipo a una applicazione 

          addn : nat -> nat -> nat
      addn 3 : nat -> nat
      addn 3 4 : nat

    Se il tipo è quantificato, allora il valore dell'argomento sostituisce la variabile in ciò che rimane 

          pair : forall A, forall B, A -> B -> prod A B
      pair nat : forall B, nat -> B -> prod nat B
      pair nat bool : nat -> bool -> prod nat bool
      pair nat bool 3 : bool -> prod nat bool
      pair nat bool 3 false : prod nat bool

    Concetti:

    • polimorfismo e quantificazione forall A : Type
    • tipaggio dell'applicazione in presenza di forall
    • pattern matching e parametri di tipo

    Argomenti impliciti (inferiti da Coq)

    I termini costruiti in precedenza, come pair nat bool 3 false sono molto verbosi e contengono informazione ridondante.

    Concetti:

    • argomenti impliciti (inferenza)

    Liste (omogenee) e notazione

    Concetti:

    • liste
    • notazioni infisse
    • parametri tra {} sono impliciti

    Ordine superiore e calcolo simbolico

    Le funzioni possono essere passate ad altre funzioni come argumenti

    iter f 3 x = f (f (f x))

    Incomincia il mal di testa ...

    L'ordine superiore è comodo per definire iteratori su tipi di dato polimorfi

    fold f (a :: b :: c) x = f c (f b (f a x))

    Ora chiediamo a Coq di considerare addn come un simbolo privo di corpo

    Coq è in grado di calcolare in modo simbolico (addn è momentaneament un simbolo). Ciò significa che il comportamento di fold non dipende da f e che, nella lezione 3, potremo dimostrare proprietà di fold valide per ogni f

    Concetti:

    • ordine superiore
    • calcolo simbolico

    Wrap up

    • funzioni anonime: fun x : nat => x + 1
    • tipi di dato: Inductive nat := O | S (n : nat)
    • pattern matching: match x with O => .. | S p => ..
    • ricorsione: Fixpoint addn n m := ...
    • polymorfismo: Inductive pair (A B : Type) := ..
    • argomenti impliciti: Check pair 2 3
    • funzioni di ordine superiore e calcolo simbolico

    Esercizi

    1: Scrivere la funzione anonima $$ x \mapsto \mathrm{notb}(\mathrm{notb}~x) $$ $$ \mathcal{B} \to \mathcal{B} $$ e verificarne il tipo. 

    Check (fun (b : bool) => notb (notb b)).
    2: Dare il nome neg2 alla funzione precedente e calcolarla con input true e poi con input false. 

    Definition neg2 := (fun (b : bool) => notb (notb b)).
Eval compute in neg2 true.
Eval compute in neg2 false.
    3: Definire il tipo di dato bussola con costruttori Nord, Sud, Est, Ovest. 

    Inductive bussola := Nord | Sud | Est | Ovest.
    4: Definire la funzione isNord che data una bussola restituisce il booleano true se e solo se la direzione è nord 

    Definition isNord b := match b with Nord => true | _ => false end.
    Nota: [_ => ..] significa "in tutti gli altri casi.."
    5: Definire la funzione xorb che dati due booleani restituisce true se e solo se uno dei due è true. Eseguire la funzione con input true true e false true 

    Definition xorb b1 b2 :=
  match b1 with
  | false => b2
  | true => notb b2 end.
Eval compute in xorb true true.
Eval compute in xorb false true.

    6: Scrivere la funzione ricorsiva eqn che prende due numeri di tipo nat e restituisce true se e solo se i due numeri sono uguali. Testare la funzione. 

    Fixpoint eqn n1 n2 := 
  match n1 with
  | O => match n2 with O => true | S _ => false end
  | S p1 => match n2 with O => false | S p2 => eqn p1 p2 end end.
Eval compute in eqn 3 4.
Eval compute in eqn 3 3.

    7: Scrivere la funzione ricorsiva leqn che prende due numeri di tipo nat e restituisce true se e solo se il primo numero è minore o uguale al secondo. Testare la funzione. 

    Fixpoint leqn n1 n2 := 
  match n1 with
  | O => true
  | S p1 => match n2 with O => false | S p2 => leqn p1 p2 end end.
Eval compute in leqn 3 4.
Eval compute in leqn 4 3.

    8: Definire la funzione odd che restituisce true se e solo se il numero naturale in input è dispari. 

    Fixpoint odd n := 
  match n with
  | O => false
  | S O => true
  | S (S p) => odd p end.
Eval compute in odd 3.
Eval compute in odd 4.
    Nota: la sintassi concreta di Coq permette di scrivere pattern-match profondi. Non è altro che una notazione. Nel caso predente è espansa in 
    Fixpoint odd n := 
  match n with
  | O => false
  | S q =>
    match q with
    | O => true
    | S p => odd p end end.

    8bis: Definire la funzione swap che prende una coppia (di tipo prod A B) e restituisce la coppia dove gli argomenti sono invertiti (di tipo prod B A. 

    Definition swap {A B} (x : prod A B) := 
   match x with
   | pair a b => pair b a
   end.

    9: Definire la funzione filter che prende una lista (di tipo A) una funzione di tipo (A -> bool) e restituisce la lista degli elementi sui quali la funzione restituisce true. Testare filter odd (1 :: 2 :: 3 :: nil). 

    Fixpoint filter {A} (f : A -> bool) l := 
  match l with
  | nil => nil
  |  x :: xs =>
      let ys := filter f xs in
      match f x with
      | true =>  x :: ys
      | false => ys end end.
Eval compute in filter odd (1 :: 2 :: 3 :: nil).
    Nota: la sintassi [let nome := espressione in ..] permette di dare un nome a una espression al fine di non dovere ripetere l'espressione (potenzialmente grande) in quanto segue.

    10: Definire la funzione ricorsiva rev che prende una lista l (di tipo A) e restituisce la lista degli elementi di l in ordine inverso. Nota: è possibile definire una funzione ausiliaria. Testare la funzione. 

    Fixpoint rev_aux {A} (l : list A) (acc : list A) := 
  match l with
   | nil => acc
   | x :: xs => rev_aux xs (x :: acc) end.
Definition rev {A} (l : list A) := rev_aux l nil.
Eval compute in rev (1 :: 2 :: 3 :: nil).

    11: Definire la funzione rev usando fold. (Questa volta chiamiamola rev2). Dichiarare che il primo argomento di rev2 (il tipo A) è implicito. Testare la funzione. 

    Definition rev2 {A} (l : list A) := fold cons l nil.
Eval compute in rev2 (1 :: 2 :: 3 :: nil).