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: SetEssere 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
La notazione matematica usuale di fun x: T => P: forall x: T, C è λx. P: ∀x: T. C.
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
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.
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
Check and. and : Prop -> Prop -> PropMa (and A B) si può scrivere come A /\ B.
La disgiunzione è definita in Coq con la funzione or.
Check or. or : Prop -> Prop -> PropMa (or A B) si può scrivere come A \/ B.
La negazione è definita in Coq con la funzione not.
Check not. not : Prop -> PropMa (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) -> PropMa (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 è:
La regola d'eliminazione è:
a=a
e corrisponde alla riscrittura.
a=b (P a)
(P b)
L'uguaglianza è definita in Coq con la funzione eq.
Check eq. eq : exists A: Set, A -> A -> PropMa (eq T A B) si può scrivere come <T> A = B o semplicemente A = B se dal contesto si può capire il tipo T.
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
I2. Definire una relazione lt fra due numeri naturali che esprime che il primo numero è strettamente minore del secondo.