PDF de programación - Introducción a Coq - Construcción Formal de Programas en Teoría de Tipos

Construcción Formal de

Programas en Teoría de Tipos

Introducción a Coq

Grupo de Métodos Formales
Grupo de Métodos Formales

www.fing.edu.uy/~mf/

Instituto de Computación

Facultad de Ingeniería

Universidad de la República

Escuela Río 2014, Río Cuarto, Argentina

Motivación

Ejemplo: División
„ 0.

Sean a y b ˛ N, b„
Calculamos a div b y a mod b

simultáneamente haciendo recursión en a:

• 0 divmod b = <0,0>
• 0 divmod b = <0,0>

• (n+1) divmod b = let <q,r> = n divmod b

in

if r < b-1

then <q,r+1>

else <q+1,0>

„
„
División: especificación y prueba

• Especificación: Para todos a,b ˛ N tq. b„

„ 0

existen q y r tq. a=b.q+r y r < b.

• Prueba de que el programa es correcto:

por inducción en a:
por inducción en a:

• 0 divmod b = <0,0>



0 = b.0 + 0 y 0 < b

•

(n+1) divmod b =

let <q,r> = n divmod b

in if r < b-1

then <q,r+1>

else <q+1,0>



supongamos n = b.q+r y r < b
luego, si r < b - 1

entonces n+1 = b.q+(r+1) y r+1<b
sino n+1 = b.(q+1)+0 y 0<b

„
„
Coq

El asistente de pruebas Coq es un entorno que permite trabajar
formalmente con sentencias matemáticas. Permite la definición
de:

- objetos (enteros, listas, árboles, funciones, programas…)
- fórmulas (usando predicados básicos, conectivos y

cuantificadores)
cuantificadores)

- pruebas (lemas, teoremas)

El compilador de Coq automáticamente chequea la corrección
de las definiciones (conjuntos/tipos bien formados, terminación
de las funciones) y de las pruebas.

Coq

El sistema Coq permite trabajar con: bibliotecas, notaciones
avanzadas, desarrollos modulares... También provee un
mecanismo de extracción de programas hacia lenguajes
funcionales (Ocaml, Haskell).
Aplicaciones de Coq incluyen (entre otras):

- formalización de semánticas de lenguajes de programación
- formalización de semánticas de lenguajes de programación
(certificación del compilador de CompCert, certificación a
nivel EAL7 de Java Card);
- diseño de plataformas especiales para la verificación de
software (Certycript);
- formalización de matemáticas (el teorema de los 4 colores);

Más información en: coq.inria.fr

Lenguaje Lógico

“Lógica como herramienta para especificar y

probar corrección de programas”

Cálculo de predicados

Sintaxis

Términos

símbolos de variable

pueden ser variables de individuo, predicado o función
un símbolo de variable tiene asociado un dominio

símbolos de constante
símbolos de función
símbolos de función

Fórmulas

variables de predicados (unarios, binarios, etc)
conectivos:
,
cuantificadores: "

, ~, ^

, «

, fi

, $

Semántica

Noción de verdad: existencia de una prueba
(lógica constructivista)



fi
fi
fi
«
«
«
^
^
^
"
"
"
$
$
$
Conectivos en Coq

• Prop es la familia de proposiciones
• Declaración de variables de proposición:

Variable A B C: Prop

• Conectivos:
• Conectivos:

,

–
– ~ y «
• ~a

, fi

, ^
^ son primitivos (/\, \/,->, False)
son definidos:
:= (a

^ )

:= (a

b )

(b

a )

^
^
a
a
a
a
a
a
fi
fi
fi
fi
^
^
^
"
a
a
a
a
«
«
«
«
b
b
b
b
a
a
a
fi
fi
fi
fi
b
b
b



b
b
b
fi
fi
fi
fi
a
a
a
Cálculo de predicados - orden

• Cálculo de predicados de primer orden:

Cuantificación sobre variables de individuos
únicamente : "

" x˛ nat. x=x

• Cálculo de predicados de orden superior:

Cuantificación sobre variables de individuos, función

y predicados
("
" x. P x fi P (S x)) fi
" P. P 0 fi

" x. P x

f."
" g. ("

" x. f(x) = g(x) fi

f = g)

"
"
"
"
"
"
"
"
"
"
"
"
"
"
"
"
"
"
Cálculo de predicados en Coq

-Variables-

Cada símbolo de variable o constante tiene asociado su

dominio y Set es la clase de todos los dominios

nat : Set
Z : Set
Z : Set
0 : nat
f : natfi nat (f es una función unaria de naturales

(nat es dominio)
(Z es un dominio)
(Z es un dominio)
(0 es un elemento del dominio nat)

en naturales)

g : natfi

natfi

nat (g es una función binaria entre

naturales – “currificación”)

Cálculo de predicados en Coq

-Predicados-

• Un predicado se representa como una función

proposicional sobre cierto dominio

• La aridad del predicado está dada por la

cantidad de argumentos de la función
P : natfi Prop

(P es un predicado unario sobre naturales)

Q : nat fi

(natfi

nat)fi

Prop

(Q es un predicado binario entre naturales y

funciones de naturales en naturales)

Cálculo de predicados en Coq

-Cuantificadores-

Notación:

("
" x˛ U) a se escribe en Coq forall x:U, a
($
$ x˛ U) a se escribe en Coq exists x:U, a

Ejemplos:
Ejemplos:
forall P: natfi Prop,

P 0 fi

(forall x:nat, P x fi

P (S x)) fi

forall x:nat, P x

forall f g: natfi nat, (forall x:nat, f x = g x) fi

f = g

"
"
a
a
a
$
$
a
a
a
Más ejemplos

Considerando las declaraciones:

0 : nat
S : natfi nat
Le : nat fi
Min : nat fi

natfi
(natfi

Prop

nat) fi

Prop

Algunas fórmulas del cálculo de predicados:

Le 0 (S 0) ~(Le (S 0) 0)
exists x:nat, Min x S
forall (f:natfi nat)(m x : nat), Le m (f x) fi Min m f

Construcción de pruebas en Coq

Para comenzar:

– Queremos probar cierta fórmula objetivo

(goal)
(goal)

– Para ello, utilizaremos diferentes tácticas que

transforman al objetivo original e introducen
hipótesis adicionales

Desarrollo de pruebas lógicas

Situación general:

– existen varios objetivos a probar, cada uno a

partir de ciertas hipótesis:

donde:

1
1

1

...
...

2
2

2

n
n

n

secuentes
secuentes

– cada G
de la forma:

i es un conjunto de fórmulas (hipótesis)
g 0, H1: g

g 1,... Hk: g

g k.

H0: g
i es una fórmula

– a
– cada a

i debe ser probada a partir de G

i

G
G
G
G
G
G
G
G
G
G
G
G
a
a
a
a
a
a
a
a
a
a
a
a
G
G
G
g
g
g
g
g
g
a
a
a
a
a
a
G
G
G
Tácticas = Reglas de inferencia

Una táctica transforma un secuente de la

forma:

i

i

en cero o más secuentes:

i1
i1

...

i2

i2

in

in

tales que probar los últimos es suficiente
para construir una prueba del secuente
original.

G
G
G
G
a
a
a
a
G
G
G
G
G
G
G
G
G
G
G
G
G
G
G
G
a
a
a
a
G
G
G
G
a
a
a
a
G
G
G
G
a
a
a
a
Prueba completa = Árbol

Goal inicial

1a

1
1

2a

2
2

Subgoals

11

11

…

12

12

1n

1n

21

21

... ... ... ... ... ...

a
a
a
a
G
G
G
G
a
a
a
G
G
G
G
a
a
a
a
a
a
a
a
a
a
a
G
G
G
G
a
a
a
a
G
G
G
G
a
a
a
a
G
G
G
G
a
a
a
a
G
G
G
G
a
a
a
a
Tácticas

caso trivial

H: a
a a a a

assumption

Probado!

G
G
G
G
a
a
a
Tácticas

Reglas de introducción

introducción fi

intro H

H: a
b b b b
b b b b

• variantes: intros, intros H1...Hn

G
G
G
G
a
fi
b
a
fi
b
a
fi
b
a
fi
b
G
G
G
G
a
a
a
fi
fi
fi
Tácticas

Cuantificador universal

introducción "

intro x

x: a

forall x:a

, b

• el identificador x es opcional
• variantes: intros, intros x1,...xn

"
"
"
G
G
b
b
Tácticas

Reglas de eliminación

apply H

H: a
a a a a

eliminación fi

H: a
b b b b

en general:

a 1fi

H: a
b b b b

a 2fi

... fi

apply H

H: ...
a 1111

H: ...
a 2222

...

G
G
G
G
fi
a
fi
a
fi
a
fi
b
b
b
b
G
G
G
G
fi
a
fi
a
fi
a
fi
b
b
b
b
fi
fi
fi
G
G
G
G
a
a
fi
fi
fi
a
a
a
fi
fi
fi
fi
fi
fi
b
b
b
b
G
G
G
G
a
a
a
G
G
G
G
a
a
a
Tácticas

Cuantificador universal

eliminación "

H: forall x:a

, g

apply H

Probado!

Si existe a:a a

a a tal que b

b = g[g[g[g[ x:=a]

G
b
"
"
"
b
b
Tácticas

Cuantificador existencial

introducción $

exists x:U, a

(x)

exists t

eliminación $

H: exists x:U, a (x)

(t)

donde t:U
donde t:U
(witness)

elim H

H: exists x:U, a
(x)
forall y: U, a (y) fi
donde y es una variable
nueva que no ocurre en b

G
$
$
$
G
a
$
$
$
G
b
G
b
b
b
b
Ejemplo 1

Variable A B: Prop.

Lemma L1: A -> B -> A.
Proof.

intros H1 H2.
assumption.

Qed.

Ejemplo 2

Variable U: Set.
Variable P Q: U -> Prop.

Lemma L2 : (forall x:U, P x -> Q x) -> (forall y:U, P y) ->

forall z:U, Q z.

Proof.

intros H1 H2 z.
apply H1.
apply H2.

Qed.

Lenguaje de Programación
Cálculo de Construcciones

Cálculo l

l simplemente tipado

Sintaxis

Términos

e ::= x | l x.e | (e1 e2) | c

Tipos
Tipos

::= t | a 1fi

2

Contextos

G

::= x1:a 1... xn:a n (n‡ 0)

x˛ Var
c˛ Const

t˛ TConst

l
l
a
a
Sistema de tipos

Juicios de la forma: G
“la expresión e tiene tipo a bajo el contexto G ”

|- e: a

Reglas:

x:a
x:a
|- x:a
G

ctx

|- e: b

G, x:a
|- l x.e: a fi

G

abs

|- e1:a fi
G

|- e2: a

b G
|- (e1 e2): b

app

G
G
G
a
a
a
˛
G
b
G
˛
G
Cálculo l

l simplemente tipado en Coq

• Constantes de tipo: nat, bool, etc.

• Las abstracciones se escriben con:

fun ... => ...
El tipo de las variables aparece en las
El tipo de las variables aparece en las
abstracciones:
– fun x: nat => x : nat fi
– fun x: bool => x : bool fi
– fun (f:natfi bool)(x:nat) => f x : bool
– fun (g:natfi natfi bool)(n:nat) => g n : nat fi

bool

nat

bool

l
l
Polimorfismo paramétrico

• En los lenguajes funcionales (ML, Haskell)

escribimos: l x. x : a

Variable de tipo!!

• En Coq, abstraemos el tipo. Los tipos de datos
pertenecen a la clase Set:

fun (X:Set)(x:X) => x : forall X:Set, X fi X
Abstrayendo en la clase Set se obtiene polimorfismo
paramétrico

fi
a
Tipos dependientes

• Polimorfismo paramétrico = abstraer variables

de tipo (de Set).

• En forma más general: podemos abstraer

variables de cualquier tipo
variables de cualquier tipo
cualquier tipo.
cualquier tipo.

Tipos dependientes
Tipos dependientes: un tipo puede depender
no solo de otro tipo, sino también de un objeto
de cierto tipo.

Tipos dependientes

Ejemplo

Array: Set fi

nat fi Set

– (Array bool 3)
– zip: forall (A B:Set)(k:nat),

(Array A k) fi

(Array B k) fi

fi Array (A*B) k

fi
fi
fi
fi
fi
Lenguaje de Programación de Coq

• Es un lambda cálculo tipado con las

siguientes características:
– es de orden superior
– permite definir funciones paramétricas
– tiene tipos dependientes
– tiene tipos dependientes
– permite definir tipos inductivos
– permite definir tipos coinductivos

CC

CCI
CCI

Cálculo de Construcciones (CC)
Cálculo d