Oggetti induttivi

In Coq si definiscono nuovi oggetti induttivi usando il comando Inductive:

Inductive <NAME>: <TYPE> :=
  <NAME>: <TYPE>
| <NAME>: <TYPE>
...
| <NAME>: <TYPE>
.

Esempi

Numeri naturali

L'esempio tipico di oggetti induttivi è dato dai numeri naturali. Una rappresentazione possibile è la seguente: 
Inductive nat: Set :=
  O: nat
| S: nat -> nat.
Con tale rappresentazione, 0 è rappresentato come O, 1 è rappresentato come (S O), 2 è rappresentato come (S (S O)) ...

I tipi dei costruttori permettono di assicurarsi che gli oggetti sono costruiti correttamente: 

Check nat.
nat
   : Set

Check O.
O
   : nat

Check S.
S
   : nat -> nat

Check (S O).
(S O)
   : nat

Check (S S).
> Check (S S).
>          ^
Error: The term S has type nat -> nat while it is expected to have type
 nat
Con questo nuovo tipo si possono creare funzioni. Per esempio: 
Definition incr: nat -> nat := [a: nat] (S a).
incr is defined

Booleani

Un altro esempio sono i booleani. Anche se non sono veramente oggetti induttivi, va bene lo stesso: 
Inductive bool: Set :=
  true : bool
| false: bool.

Parità

Il comando Inductive permette non solo di definire nuovi tipi ma anche predicati dando le sue proprietà caratteristiche. Per esempio, la definizione della parità di un numero può essere data induttivamente come segue: 
Inductive Even: nat -> Prop :=
  Even0 : (Even O)
| EvenSS: forall n: nat, (Even n) -> (Even (S (S n))).
Con tale definizione si può provare che 2 è pari, 4 è pari,...: 
Definition Even2: (Even (S (S O))):=
  (EvenSS O Even0).
Even2 is defined

Definition Even4: (Even (S (S (S (S O))))):=
  (EvenSS (S (S O)) Even2).
Even4 is defined

Esercizi

J1. Definire gli oggetti liste con il tipo list.

J2. Definire induttivamente la relazione le fra due numeri naturali che esprime che il primo numero è minore del secondo.

J3. Definire induttivamente la relazione lt fra due numeri naturali che esprime che il primo numero è strettamente minore del secondo.

J4. Definire induttivamente la proprietà Odd che esprime che un numero naturale è dispari.

*J5. Definire induttivamente un tipo btree che rappresenta gli alberi binari le cui foglie sono etichettate con numeri naturali.

*J6. Definire un predicato induttivo checkB di tipo btree->Prop che corrisponde alla proprietà che un oggetto di tipo btree è stato costruito nel seguente modo:
ogni volta che è stato utilizzato il costruttore Node, il costruttore di testa del suo primo parametro è uguale al costruttore di testa del suo secondo parametro.

*J7. Definire induttivamente un tipo bin che rappresenta i numeri binari.

*J8. Definire un predicato induttivo Full che esprime che un numero binario è composto solamente di 1

*J9. Supponendo l'esistenza di un insieme di nodi node 

Parameter node: Set.
supponendo l'esistenza di un predicato Edge che mette in relazione due nodi. (Edge a b) significa che c'è una freccia da a verso b: 
Parameter Edge: node -> node -> Prop.
definire

*J10. Definire una relazione induttiva between fra tre numeri naturali che rappresenta il fatto che il secondo numero è compreso fra il primo e il terzo numero.

Costruzioni per casi

Il comando match permette di fare una discussione sul valore di un oggetto induttivo:

match <EXP> with
  <FILTER> => <EXP>
| <FILTER> => <EXP>
...
| <FILTER> => <EXP>
end

Esempi

Il predicato is_zero indica se un numero è nullo: 
Definition is_zero: nat -> Prop :=
  fun a: nat =>
    match a with
       O    => True
    | (S _) => False
    end.
La funzione notb calcola il complementare di un booleano: 
Definition notb: bool -> bool :=
  fun a: nat =>
    match a with
      true  => false
    | false => true
    end.

Esercizi

J11. Definire la funzione andb che calcola la congiunzione di due booleani.

J12. Definire la funzione orb che calcola la disgiunzione di due booleani.

Funzioni ricorsive

In Coq si possono definire funzioni ricorsive. Bisogna fare attenzione nel definire tali funzioni. In Coq, oggetti come 3+4 e 7 sono gli stessi. Dunque una prova di (Prime (3+4)) è anche una prova di (Prime 7). Ciò vuol dire che quando scriviamo 
Definition o: T := P.
per accettare la definizione, Coq deve assicurarsi che il tipo T' di P è equivalente a T. T et T' possono essere sintatticamente diversi come (Prime (3+4)) e (Prime 7). Ma si può valutare T e T' ottenendo le forme normali Tn e Tn'. Adesso per decidere se T e T' sono equivalenti, si verifica semplicemente che Tn e Tn' sono sintatticamente equivalenti.

Nota che l'uguaglianza sintattica non riguarda le variabili legate, ovvero fun A: Set => fun x: A => x è sintatticamente equivalente a fun B: Set => fun y: B => y.

Aggiungere funzioni ricorsive significa introdurre computazioni possibilmente infinite. Tuttavia, tali computazioni non permettono piú al sistema di decidere l'equivalenza dei tipi. Dunque in Coq si possono definire funzioni ricorsive, ma il sistema deve assicurarsi la terminazione di tutte le chiamate possibili della funzione. Per ottenere tale assicurazione, si usa un criterio sintattico. Quando si definisce una funzione, si specifica un argomento particolare della funzione tale che, ad ogni chiamata ricorsiva, il valore di tale argomento deve diminuire strutturalmente.

Il comando per definire una funzione ricorsiva è:

Fixpoint <NAME> (<NAME>: <TYPE>) ... (<NAME>: <TYPE>) {struct <NAME>}: <TYPE> :=
   <EXP>.

La convenzione è che è il nome dopo il struc indica l'argumento che assicura la terminazione.

Esempi

Addizione

L'addizione può essere definita con un Fixpoint prendendo il primo argomento come testimone di terminazione: 
Fixpoint plus (n: nat) (m: nat) {struct n}: nat :=
    match n with
       O     =>  m
    | (S n1) => (S (plus n1 m))
    end.
La funzione termina perché il primo argomento della chiamata ha un S di meno di n.

Per avere la computazione di una funzione dentro Coq, si può usare il comando Eval compute in. Per esempio: 

Eval compute in (plus (S (S O)) (S (S (S O)))). 
     = (S (S (S (S (S O)))))
     : nat
Si può anche definire l'addizione usando il secondo argomento come testimone di terminazione: 
Fixpoint plus (n: nat) (m: nat) {struct m}: nat :=
  match m with
     O     =>  n
  | (S m1) => (S (plus n m1))
  end.

Moltiplicazione

Una volta definita l'addizione, si può definire anche la moltiplicazione come segue: 
Fixpoint mult (n: nat) (m: nat) {struct n}: nat :=
    match n with
       O     =>  O
    | (S n1) => (plus m (mult n1 m))
    end.
o come 
Fixpoint mult (n: nat) (m: nat) {struct m}: nat :=
  match m with
     O     =>  O
  | (S m1) => (plus n (mult n m1))
  end.

Parità

Precedentemente abbiamo definito il predicato di parità usando la costruzione induttiva. Poiché un predicato è in realtà una funzione, per definire la parità si può anche usare una funzione: 
Fixpoint Even (n: nat) {struct n}: Prop :=
  match n with
     O         => True
  | (S O)      => False
  | (S (S n1)) => (Even n1)
  end.
La terminazione è assicurata, poiché n1 ha due S meno di n.

Definire qualcosa tramite una definizione induttiva vuol dire definire una nuova nozione e dare le sue proprietà fondamentali. Usare una funzione è piú diretto. Si vede sulle prove, provare (Even (S (S O))) è piú semplice perché (Even (S (S O))) vale True. Dunque una prova di True è sufficiente. Lo stesso ragionamento vale per (Even (S (S (S (S O))))). 

Parameter I: True.
I is assumed

Definition Even2: (Even (S (S O))) := I.
Even2 is defined

Definition Even4: (Even (S (S (S (S O))))) := I.
Even4 is defined
Se si vuole usare il fatto d'essere pari per definire altri funzioni, occorre definire la funzione pari nel mondo del calcolo (Set) e non in quello delle prove: 
Fixpoint even (n: nat) {struct n}: bool :=
  match n with
    O         => true
  |(S O)      => false
  |(S (S n1)) => (even n1)
  end.
Adesso si può fare: 
Definition foo (n: nat): nat :=
  match (even n) with
     true => O
  | false => (S O)
  end.

Esercizi

J13. Usando l'esercizio J1, definire la funzione ricorsiva length che calcola la lunghezza di una lista.

*J14. Definire la funzione max che calcola il maggiore di due numeri naturali.

*J15. Definire la funzione ominus che prende due numeri naturali di tipo nat e restituisce un numero naturale che rappresenta la loro differenza simmetrica, ovvero il valore assoluto della loro differenza. (ominus 7 2) e (ominus 2 7) valgono 5.

*J16. Definire come funzione bmax che prende un oggetto a di tipo btree (come definito nell'esercizio *J5) e restituisce il numero naturalle massimo che compare dentre a.

*J17. Definire come funzione byte che prende un numero binario a di tipo bin (come definito nell'esercizio *J7) e restituisce il suo numero di cifre.

*J18. Definire come funzione bval che prende un numero binario a di tipo bin (come definito nell'esercizio *J7) e restituisce il suo valore. Si prende la convenzione che il binario 110 è rappresentato da destra a sinistra come (zero (one (one end))).

J19. Definire come funzione ricorsiva la relazione le fra due numeri naturali che esprime che il primo numero è minore del secondo.

J20. Definire come funzione ricorsiva la relazione lt fra due numeri naturali che esprime che il primo numero è strettamente minore del secondo.

J21. Definire come funzione ricorsiva la proprietà Odd che esprime che un numero naturale è dispari.

Logica e uguaglianza

Adesso vediamo che in realtà i connettori logici non sono primitivi ma possono essere definiti.

Congiunzione

Una prova di A ∧ B è una coppia di prove data da una prova di A e da una prova di B: 
Inductive and: Prop -> Prop -> Prop :=
  conj: forall A: Prop, forall B: Prop, A ->  B ->  (and A B).
L'introduzione corrisponde a conj, le eliminazioni a and_eliml e and_elimr: 
Definition and_eliml: forall A: Prop, forall B: Prop, (and A B) -> A :=
 fun A: Prop =>
   fun B: Prop =>
     fun H: (and A B) =>
       match H with
         (conj  _ _ H1 _) => H1
       end.

Definition and_elimr: forall A: Prop, forall B: Prop, (and A B) -> B :=
 fun A: Prop =>
   fun B: Prop => 
     fun H: (and A B) =>
       match H with
         (conj _ _ _ H2) => H2
       end.
I due primi argomenti di conj sono solo parametri che non dovrebbero entrare nella discussione. Una variante di Inductive permette di rendere tale fatto esplicito: 
Inductive and (A: Prop) (B: Prop): Prop :=
  conj: A ->  B ->  (and A B).
Gli argomenti dentro le parentesi quadre [] sono comuni a tutti i costruttori.

Tale variante non cambia il tipo di conj ma rende le eliminazioni piú facili da leggere: 

Definition and_eliml: forall A: Prop, forall B: Prop, (and A B) -> A :=
 fun A: Prop =>
   fun B: Prop =>
     fun H: (and A B) =>
       match H  with
         (conj H1 _) => H1
       end.

Definition and_elimr: forall A: Prop, forall B: Prop, (and A B) -> B :=
 fun A: Prop =>
   fun B: Prop =>
     fun H: (and A B) =>
       match H with
         (conj _ H2) => H2
       end.
Nel seguito, (and A B) si scrive A /\ B.

Disgiunzione

Una prova di A ∨ B è o una prova di A o una prova di B: 
Inductive or (A: Prop)(B: Prop): Prop :=
  or_introl: A -> (or A B)
| or_intror: B ->  (or A B).
Le introduzioni corrispondono a or_intro1 e or_intro2, l'eliminazione a or_elim: 
Definition or_elim: forall A: Prop, forall B: Prop, forall C: Prop,
   (or A B) -> (A  ->  C) -> (B -> C) -> C :=
 fun A: Prop =>
   fun B: Prop =>
     fun C: Prop =>
       fun H: (or A B) =>
         fun H1: A -> C =>
           fun H2: B -> C =>
             match H with
               (or_introl H3) => (H1 H3)
             | (or_intror H3) => (H2 H3) 
             end.
Nel seguito, (or A B) si scrive A \/ B.

Verità

La verità è definita come un oggetto che ha una prova I: 
Inductive True: Prop :=
  I: True.

Falsità

La falsità è definita come un oggetto che non ha una prova I: 
Inductive False: Prop := .
L'eliminazione di False è definita cosí: 
Definition false_elim: forall A: Prop, False -> A :=
 fun A: Prop =>
   fun B: False =>
      match B with end.

Negazione

¬A è definita come A ⇒ False, dunque: 
Definition not: Prop -> Prop := fun A: Prop => A -> False.
Nel seguito, (not A) si scrive ~A.

Esistenziale

La quantificazione esistenziale è definita come una coppia data da un elemento che verifica la proprietà e la prova che tale elemento verifica la proprietà: 
Inductive ex (A: Set) (P: (A -> Prop)): Prop :=
  ex_intro: forall x: A, (P x) -> (ex A P).
L'introduzione corrisponde a ex_intro, l'eliminazione a ex_elim (ancora una volta facciamo una discussione dipendente): 
Definition ex_elim: forall A: Set, forall C: Prop, forall P: A -> Prop,
  (ex A P) -> (forall x: A, (P x) -> C) -> C := 
  fun A: Set =>
    fun C: Prop =>
      fun P: A -> Prop =>
        fun H: (ex A P) =>
          fun H1: forall x: A, (P x) -> C =>
            match H with
              (ex_intro x H2)  =>  (H1 x H2)
            end.
Nel seguito, (ex A P) si scrive (exists x: T, (P x)).

Uguaglianza

In Coq l'uguaglianza si scrive come segue: 

Inductive eq (A: Set) (a: A): A -> Prop :=
  refl_equal: (eq A a a).
L'introduzione è la funzione eq. L'eliminazione è definita come: 
Definition eq_elim: forall A: Set, forall P: A -> Prop,
 forall a: A, forall b: A, (eq A a b) -> (P a) -> (P b) :=
 fun A: Set =>
   fun P: A -> Prop =>
     fun a: A =>
       fun b: A =>
         fun H: (eq A a b) =>
           fun H1: (P a) =>
             match H with
               refl_equal => H1
             end.
Nel seguito, (eq A a b) si scrive <A> a=b.

Esercizi

J22. Definire una funzione and_com di tipo forall A: Prop, forall B: Prop, (A /\ B) -> (B /\ A).

J23. Definire una funzione or_com di tipo forall A: Prop, forall B: Prop, (A \/ B) -> (B \/ A).

*J24. Definire una funzione double di tipo forall A: Prop, A -> (A /\ A).

*J25. Definire una funzione triple di tipo forall A: Prop, forall B: Prop, (C: Prop) A -> B -> C -> (A /\ (B /\ C)).

*J26. Definire una funzione mpc di tipo forall A: Prop, forall B: Prop, (A -> B) -> A -> (A /\ B).

*J27. Definire una funzione cumul di tipo forall A: Prop, forall B: Prop, (C: Prop) (A -> B) -> (A -> C) -> A -> (B /\ C).

*J28. Definire una funzione circ di tipo forall A: Prop, forall B: Prop, (A -> B) -> (B -> ~A) -> ~A.

*J29. Definire una funzione nno di tipo forall A: Prop, forall B: Prop, (A -> ~B) -> B -> ~A .

*J30. Definire una funzione mp di tipo forall A: Set, forall a: A, forall P: A -> Prop, forall Q: A -> Prop, (forall x: A, (P x) -> (Q x)) -> (P a) -> (Q a).

*J31. Definire una funzione mpcQ di tipo forall A: Set, forall P: A -> Prop, forall Q: A -> Prop, forall R: A -> Prop, (forall x: A, (P x) -> (Q x)) -> (forall x: A, (P x) -> (R x)) -> (forall x: A, (P x) -> ((Q x) /\ (R x))).

*J32. Definire una funzione cancel2 di tipo forall A: Set, forall P: A -> Prop, forall Q: A -> Prop, forall R: A -> Prop, (forall x: A, (P x) -> (Q x) -> (R x)) -> (forall x: A, (Q x)) -> forall x: A, (P x) -> (R x)).

*J33. Definire una funzione instan di tipo forall A: Set, forall P: A -> Prop, forall Q: A -> A -> Prop, (forall x: A, (P x) -> forall y: A, (Q x y)) -> (forall x: A, (P x)) -> forall x: A, (Q x x).

J34. Con la definitizione seguente 

Definition mconj: Prop -> Prop -> Prop := 
  fun A: Prop => fun B: Prop => forall P: Prop, (A -> B -> P) -> P.
Definire

*J35. Con la definitizione seguente 

Definition mdisj: Prop -> Prop -> Prop :=
  fun A: Prop => fun B: Prop => forall P: Prop, (A -> P) -> (B -> P) -> P.
Definire *J36. Con le definitizioni seguenti 
Definition mfalse: Prop  := forall P: Prop, P.

Definition mneg: Prop -> Prop := fun A: Prop => A -> mfalse.
Definire

Prova per ricorsione

Avendo i numeri naturali, una tecnica di prova usuale in matematica è la prova per ricorsione. Per i numeri naturali tale prova si comporta così: se possiamo provare una proprietà per 0 e se per un numero arbitrario n sappiamo che la proprietà è vera per n e la si può dedurre per n+1, allora sappiamo che tale proprietà è vera per tutti i naturali.

Non solo si può esprimere questo principio come una formula Coq: 

Parameter nat_ind: forall P: nat -> Prop, (P O) -> (forall n: nat, (P n) -> (P (S n))) -> 
forall n: nat, (P n).
ma si può anche provarlo. Il principio è una conseguenza diretta della definizione di nat: 
Fixpoint nat_ind (P: nat -> Prop) (H: (P O)) (H1: forall n: nat, (P n) -> (P (S n))) (n: nat) {struct n}:  (P n) :=
  match n with 
        O  => H
  | (S n1) => (H1 n1 (nat_ind P H H1 n1))
  end.
Un tale principio può essere costruito nello stesso modo per tutte le definizioni induttive. Infatti, ogni volta che si definisce un costruttore induttivo, Coq definisce automaticamente un tale principio, il cui nome è quello del tipo piú il suffisso _ind.

Per esempio, per list abbiamo: 

Check list_ind.
list_ind
     : forall A : Set, forall P : (list A) -> Prop,
       (P nil) ->
       (forall a : A, forall l : (list A), (P l) -> (P (cons a l))) ->
       forall l : (list A), (P l)
Lo stesso si ha per Even: 
Check Even_ind.

Even_ind
     : forall P: nat -> Prop,
        (P O)
        -> (forall n: nat, (Even n) -> (P n) -> (P (S (S n))))
        -> forall n: nat, (Even n) -> (P n)

Esercizi

*J37. Dare il principio d'induzione btree_ind che corrispondente al tipo btree definito all'esercizio *J5.

*J38. Dare il principio d'induzione bin_ind che corrispondente al tipo bin definito all'esercizio *J7.

*J39. Dare il principio d'induzione between_ind che corrispondente alla relazione between definita all'esercizio *J10.

Esercizi

Per tutti gli esercizi seguenti supponiamo di avere un insieme A, una funzione f_le che prende due elementi di A e restituisce un booleano, un predicato ll che rappresenta il fatto per un elemento di A di essere minore di un altro, due assiomi f_le_correct1, f_le_correct2 che assicurano la correttezza di f_le, ed infine il tipo lista di A. In Coq tali dichiarazioni si scrivono come segue: 
Parameter A: Set.
Parameter f_le: A -> A -> bool.
Parameter le: A -> A -> Prop.

Axiom f_le_correct1: forall a: A, forall b: A, (f_le a b) = true ->  (le a b).
Axiom f_le_correct2: forall a: A, forall b: A, (f_le a b) = false -> (le b a).


Inductive list: Set :=
  nil : list
| cons: A -> list -> list.
J40. Scrivere in Coq l'algoritmo d'ordinamento per inserimento isort.

J41. Scrivere in Coq il predicato Ordered_list che esprime che una lista di A è ordinata rispetto al predicato le.

J42. Scrivere in Coq il predicato Permutation che esprime che una lista contiene gli stessi elementi con la stessa molteplicità di un'altra: per esempio, [1;1;2] ha gli stessi elementi di [1;2;1] ma ha un 1 in piú di [1;2].

J43. Scrivere in Coq la formula che esprime che l'algoritmo isort è corretto.

Laurent Théry

Last modified: Tue Jun 4 21:38:21 MEST 2002