Introducción a Coq

Introducción a Coq#

Funciones y parámetros#

  • En Coq se utiliza la noción de función de modo más formal que en otros lenguajes.

  • Estamos acostumbrados a tener funciones que toman varios parámetros, como int suma(int a, b).

  • En Coq las funciones toman un parámetro y devuelven un parámetro.

  • Estas funciones se trabajan mediante el uso de funciones parciales y la técnica denominada “currying”.

  • Una función como suma, en Coq, toma un número natural, devuelve una función que toma un sólo número natural, le suma el anterior, y devuelve el resultado, que es otro natural.

  • A las funciones que toman o devuelven otras funciones como parámetros se las denomina funciones de orden superior.

  • Simplemente, add es una función que, a efectos prácticos, toma dos naturales y nos devuelve otro, mediante una función intermedia de orden superior.

Ejemplo sobre el cómputo de funciones#

Compute Nat.add 2 3.
(* = 5 : nat *)

¿Qué nos presenta el anterior ejemplo?

  • add se aplica sobre el parámetro 2 y retorna otra función que se aplica sobre 3 para retornarnos el valor 5.

  • Adicionalmente nos indica el tipo del valor de retorno, un natural.

¿Pero qué es un tipo en Coq?

  • Función de primera clase (se puede tratar como otro valor del lenguaje).

  • Se construye de manera inductiva.

Ejemplo sobre definición inductiva en Coq#

Print nat.
(* Inductive nat : Set := O : nat | S : nat -> nat *)

¿Qué nos presenta el anterior ejemplo?

  • nat es un tipo inductivo (perteneciente a Set (conjunto)) que se puede formar mediante dos constructores:

    1. O que representa el cero.

    2. Una función S (función sucesor) que toma un nat y devuelve otro nat.

Ejemplo de verificación de tipo de sucesor#

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

¿Qué aprendemos del ejemplo anterior?

  • 3 es simplemente azúcar sintáctico para S (S (S O)).

  • Es la codificación de Peano que vimos previamente.

  • Utiliza un sólo dígito y aunque es poco eficiente permite realizar pruebas inductivas con mayor facilidad.

Ejemplo de verificación de tipo de add#

Print Nat.add.
(*
Nat.add =
fix add (n m : nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (add p m)
  end
     : nat -> nat -> nat
*)

Explicación de Nat.add

  • fix es un operador para definir funciones recursivas (se llama a sí misma).

  • (n m : nat) {struct n} : nat indica que toma 2 parámetros, n y m, de tipo nat.

  • struct n indica que la recursión es estructural en n, es decir, que cuando add se llama a sí misma, n va a ser siempre inferior.

  • Esto garantiza que add siempre devuelva un resultado en tiempo finito.

  • El último nat es el tipo del valor de retorno de la función.

  • Decimos que toma dos parámetros porque el currying es automático.

Definiendo funciones recursivas en Coq#

Ejemplo: Definir la función factorial en Coq#

Fixpoint factorial (n:nat) : nat :=
match n with
| O => (S O)
| S p => (S p) * (factorial p)
end.

Ejemplo: Definir la multiplicación de dos números n y m en Coq#

Fixpoint multiplicar (n m:nat) : nat :=
match n with
| O => O
| S p => m + (multiplicar p m)
end.
Contents