Proposizione e insieme

Coq è un dimostratore basato sull'isomorfismo di Curry-Howard, che usa un linguaggio funzionale tipato chiamato Calcolo delle costruzioni induttive per definire calcolo e prova.

Il fatto che si può calcolare e provare dentro Coq si vede perché ci sono due tipi Prop e Set. Il primo corrisponde al tipo delle proposizioni, dunque appartiene al mondo delle prove. Il secondo corrisponde agli oggetti sui quali possiamo calcolare. Per esempio abbiamo:

False: Prop
nat: Set
Essere in un linguaggio tipato vuole dire che anche Prop e Set hanno un tipo Type. Si finisce qui perché Type ha per tipo se stesso.

Per sapere il tipo di un oggetto dentro Coq si usa il comando Check. Ogni comando in Coq comincia con una maiuscola e termina con un punto. Per esempio,O rappresenta il numero 0 in Coq e si può avere l'interazione seguente in Coq (l'input e l'output):

Check O.
0
  : nat

Check nat.
nat
     : Set

Check Set.
Set
     : Type

Funzioni

Il costruttore di base di Coq è la funzione. Si scrive fun x:T => P. Il suo tipo è forall x: T, C dove C è il tipo di P. Se il tipo non è dipendente, cioé x non compare dentro C, una variante del tipo è T -> C.

La notazione matematica usuale di fun x: T => P: forall x: T, C è λx. P: ∀x: T. C.

Parameter

Il comando per introdurre un parametro è:
Parameter <NAME>: <TYPE>.

Esempi

Parameter A: Set.
A is assumed

Parameter B: Prop.
B is assumed

Parameter a: A.
a is assumed

Parameter b: B.
b is assumed

Parameter f: A ->  A.
f is assumed

Parameter g: B ->  B.
g is assumed

Parameter  P: A -> Prop.
P is assumed

Parameter  Q: A ->  A ->  Prop.
Q is assumed

Parameter  id: forall A: Set, A ->  A.
id is assumed

Parameter  Id: forall A: Prop, A ->  A.
Id is assumed

A è un insieme d'oggetti.
B è una proposizione.
a è un elemento di A.
b è una prova di B.
f è una funzione da A in A.
g è una prova di B ⇒ B.
P è un predicato: una proprietà degli elementi di A.
Q è un predicato: una relazione fra due elementi di A.
id è una funzione che prende un insieme A e un elemento di questo insieme e restituisce un elemento di A.
Id è una prova della formula ∀A: Prop. A ⇒ A.

Quando si vuole definire un parametro che è una proposizione, invece di Parameter, si può usare la parola chiave Axiom:

Axiom b: B.
Axiom Id: forall A: Prop, A ->  A.

Polimorfismo

I tipi dipendenti forniscono direttamente il polimorfismo:
Check (id nat).
(id nat)
     : nat -> nat

Check (id bool).
(id bool)
     : bool -> bool

Check (Id False).
(Id False)
     : False -> False

Check (Id True).
(Id True)
     : True -> True

Logica e uguaglianza

La congiunzione è definita in Coq con la funzione and.
Check and.
and
    : Prop -> Prop -> Prop
Ma (and A B) si può scrivere come A /\ B.

La disgiunzione è definita in Coq con la funzione or.

Check or.
or
    : Prop -> Prop -> Prop
Ma (or A B) si può scrivere come A \/ B.

La negazione è definita in Coq con la funzione not.

Check not.
not
    : Prop -> Prop
Ma (not A) si può scrivere come ~A.

La costante vera è definita in Coq con la funzione True.

Check True.
True
    : Prop

La costante falsa è definita in Coq con l'oggetto False.

Check False.
False
    : Prop

Il quantificatore esistenziale è definito in Coq con la funzione ex.

Check ex.
ex
    : forall A: Set,  (A -> Prop) -> Prop
Ma (ex T P) si può scrivere come (exists x: T, (P T)).

In Coq due oggetti sono uguali se sono esattamente gli stessi. Tale uguaglianza è detta intensionale o uguaglianza di Leibniz. La regola d'introduzione è:

a=a
La regola d'eliminazione è:

a=b         (P a)
(P b)
e corrisponde alla riscrittura.

L'uguaglianza è definita in Coq con la funzione eq.

Check eq.
eq
    : exists A: Set,  A -> A -> Prop
Ma (eq T A B) si può scrivere come <T> A = B o semplicemente A = B se dal contesto si può capire il tipo T.

Definizioni

I parametri permettono d'assumere l'esistenza di oggetti. In Coq si possono ovviamente definire nuovi oggetti in termini di altri oggetti.
Definition <NAME>: <TYPE> := <EXP>.

Esempi

Supponiamo di avere i numeri naturali, l'addizione, la moltiplicazione e la relazione d'uguaglianza. Tale ambiente può essere descritto con i parametri:
Parameter nat: Set.
Parameter plus: nat -> nat -> nat.
Parameter mult: nat -> nat -> nat.
Parameter eq: nat -> nat -> Prop.
Dentro tale ambiente si può definire una relazione divide fra due numeri naturali che esprime che il primo numero divide l'altro:
Definition divide: nat -> nat -> Prop :=
  fun a: nat =>
    fun b: nat =>
       exists c: nat, (eq b (mult a c)).
divide is defined

Si può definire una relazione is_gcd fra tre numeri naturali che esprime che il terzo numero è il massimo comun divisore dei primi due:

Definition is_gcd: nat -> nat -> nat -> Prop :=
  fun a: nat =>
    fun b: nat =>
      fun c: nat =>
        (divide c a) /\
        (divide c b) /\
        (forall d: nat, ((divide d a) /\ (divide d b)) -> (divide d c)).
is_gcd is defined

Esercizi

I1. Definire una relazione le fra due numeri naturali che esprime che il primo numero è minore del secondo.

I2. Definire una relazione lt fra due numeri naturali che esprime che il primo numero è strettamente minore del secondo.


Laurent Théry

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