Tema 1
De Seminario de Lógica Computacional (2018)
Revisión del 10:39 27 feb 2018 de Jalonso (discusión | contribuciones)
(* T1: Programación funcional en Coq *)
Definition admit {T: Type} : T. Admitted.
(* =====================================================================
§ Datos y funciones
================================================================== *)
(* =====================================================================
§§ Tipos enumerados
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo day cuyos constructores sean los días de
la semana.
------------------------------------------------------------------ *)
Inductive day : Type :=
| monday : day
| tuesday : day
| wednesday : day
| thursday : day
| friday : day
| saturday : day
| sunday : day.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
next_weekday :: day -> day
tal que (next_weekday d) es el día laboral siguiente a d.
------------------------------------------------------------------ *)
Definition next_weekday (d:day) : day :=
match d with
| monday => tuesday
| tuesday => wednesday
| wednesday => thursday
| thursday => friday
| friday => monday
| saturday => monday
| sunday => monday
end.
(* ---------------------------------------------------------------------
Ejemplo. Calcular el valor de las siguientes expresiones
+ (next_weekday friday)
+ (next_weekday (next_weekday saturday))
------------------------------------------------------------------ *)
Compute (next_weekday friday).
(* ==> monday : day *)
Compute (next_weekday (next_weekday saturday)).
(* ==> tuesday : day *)
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
(next_weekday (next_weekday saturday)) = tuesday
------------------------------------------------------------------ *)
Example test_next_weekday:
(next_weekday (next_weekday saturday)) = tuesday.
Proof. simpl. reflexivity. Qed.
(* =====================================================================
§§ Booleanos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo bool cuyos constructores son true y false.
------------------------------------------------------------------ *)
Inductive bool : Type :=
| true : bool
| false : bool.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
negb :: bool -> bool
tal que (negb b) es la negación de b.
------------------------------------------------------------------ *)
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
andb :: bool -> bool -> bool
tal que (andb b1 b2) es la conjunción de b1 y b2.
------------------------------------------------------------------ *)
Definition andb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => b2
| false => false
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
orb :: bool -> bool -> bool
tal que (orb b1 b2) es la disyunción de b1 y b2.
------------------------------------------------------------------ *)
Definition orb (b1:bool) (b2:bool) : bool :=
match b1 with
| true => true
| false => b2
end.
(* ---------------------------------------------------------------------
Ejemplo. Demostrar las siguientes propiedades
(orb true false) = true.
(orb false false) = false.
(orb false true) = true.
(orb true true) = true.
------------------------------------------------------------------ *)
Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb2: (orb false false) = false.
Proof. simpl. reflexivity. Qed.
Example test_orb3: (orb false true) = true.
Proof. simpl. reflexivity. Qed.
Example test_orb4: (orb true true) = true.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Definir los operadores (&&) y (||) como abreviaturas de las
funciones andb y orb.
------------------------------------------------------------------ *)
Notation "x && y" := (andb x y).
Notation "x || y" := (orb x y).
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
false || false || true = true.
------------------------------------------------------------------ *)
Example test_orb5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejercicio 1. Definir la función
nandb :: bool -> bool -> bool
tal que (nanb x y) se verifica si x e y no son verdaderos.
Demostrar las siguientes propiedades de nand
(nandb true false) = true.
(nandb false false) = true.
(nandb false true) = true.
(nandb true true) = false.
------------------------------------------------------------------ *)
Definition nandb (b1:bool) (b2:bool) : bool :=
admit.
Example prop_nandb1: (nandb true false) = true.
Admitted.
Example prop_nandb2: (nandb false false) = true.
Admitted.
Example prop_nandb3: (nandb false true) = true.
Admitted.
Example prop_nandb4: (nandb true true) = false.
Admitted.
(* ---------------------------------------------------------------------
Ejercicio 2. Definir la función
andb3 :: bool -> bool -> bool -> bool
tal que (andb3 x y z) se verifica si x, y y z son verdaderos.
Demostrar las siguientes propiedades de andb3
(andb3 true true true) = true.
(andb3 false true true) = false.
(andb3 true false true) = false.
(andb3 true true false) = false.
------------------------------------------------------------------ *)
Definition andb3 (x:bool) (y:bool) (z:bool) : bool :=
admit.
Example prop_andb31: (andb3 true true true) = true.
Admitted.
Example prop_andb32: (andb3 false true true) = false.
Admitted.
Example prop_andb33: (andb3 true false true) = false.
Admitted.
Example prop_andb34: (andb3 true true false) = false.
Admitted.
(* =====================================================================
§§ Tipos de las funciones
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Calcular el tipo de las siguientes expresiones
+ true
+ (negb true)
+ negb
------------------------------------------------------------------ *)
Check true.
(* ===> true : bool *)
Check (negb true).
(* ===> negb true : bool *)
Check negb.
(* ===> negb : bool -> bool *)
(* =====================================================================
§ Tipos compuestos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo rgb cuyos constructores son red, green y
blue.
------------------------------------------------------------------ *)
Inductive rgb : Type :=
| red : rgb
| green : rgb
| blue : rgb.
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo color cuyos constructores son black, white y
primary, donde primary es una función de rgb en color.
------------------------------------------------------------------ *)
Inductive color : Type :=
| black : color
| white : color
| primary : rgb -> color.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
monochrome :: color -> bool
tal que (monochrome c) se verifica si c es monocromático.
------------------------------------------------------------------ *)
Definition monochrome (c : color) : bool :=
match c with
| black => true
| white => true
| primary p => false
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
isred :: color -> bool
tal que (isred c) se verifica si c es rojo.
------------------------------------------------------------------ *)
Definition isred (c : color) : bool :=
match c with
| black => false
| white => false
| primary red => true
| primary _ => false
end.
(* =====================================================================
§§ Módulos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Iniciar el módulo NatPlayground.
------------------------------------------------------------------ *)
Module NatPlayground.
(* =====================================================================
§§ Números naturales
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo. Definir el tipo nat de los números naturales con los
constructores 0 (para el 0) y S (para el siguiente).
------------------------------------------------------------------ *)
Inductive nat : Type :=
| O : nat
| S : nat -> nat.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
pred :: nat -> nat
tal que (pred n) es el predecesor de n.
------------------------------------------------------------------ *)
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Finaliz el módulo NatPlayground.
------------------------------------------------------------------ *)
End NatPlayground.
(* ---------------------------------------------------------------------
Ejemplo. Calcular el tipo y valor de la expresión (S (S (S (S O)))).
------------------------------------------------------------------ *)
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
minustwo :: nat -> nat
tal que (minustwo n) es n-2.
------------------------------------------------------------------ *)
Definition minustwo (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Evaluar la expresión (minustwo 4).
------------------------------------------------------------------ *)
Compute (minustwo 4).
(* ===> 2 : nat *)
(* ---------------------------------------------------------------------
Ejemplo. Calcular et tipo de las funcionse S, pred y minustwo.
------------------------------------------------------------------ *)
Check S.
Check pred.
Check minustwo.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
evenb :: nat -> bool
tal que (evenb n) se verifica si n es par.
------------------------------------------------------------------ *)
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
oddb :: nat -> bool
tal que (oddb n) se verifica si n es impar.
------------------------------------------------------------------ *)
Definition oddb (n:nat) : bool := negb (evenb n).
(* ---------------------------------------------------------------------
Ejemplo. Demostrar que
+ oddb 1 = true.
+ oddb 4 = false.
------------------------------------------------------------------ *)
Example test_oddb1: oddb 1 = true.
Proof. simpl. reflexivity. Qed.
Example test_oddb2: oddb 4 = false.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Iniciar el módulo NatPlayground2.
------------------------------------------------------------------ *)
Module NatPlayground2.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
plus :: nat -> nat -> nat
tal que (plus n m) es la suma de n y m. Por ejemplo,
plus 3 2 = 5
------------------------------------------------------------------ *)
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.
Compute (plus 3 2).
(* ===> 5: nat *)
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
mult :: nat -> nat -> nat
tal que (mult n m) es el producto de n y m. Por ejemplo,
mult 3 2 = 6
------------------------------------------------------------------ *)
Fixpoint mult (n m : nat) : nat :=
match n with
| O => O
| S n' => plus m (mult n' m)
end.
Example test_mult1: (mult 2 3) = 6.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo. Definir la función
minus :: nat -> nat -> nat
tal que (minus n m) es la diferencia de n y m. Por ejemplo,
mult 3 2 = 1
------------------------------------------------------------------ *)
Fixpoint minus (n m:nat) : nat :=
match (n, m) with
| (O , _) => O
| (S _ , O) => n
| (S n', S m') => minus n' m'
end.
(* ---------------------------------------------------------------------
Ejemplo. Cerrar el módulo NatPlayground2.
------------------------------------------------------------------ *)
End NatPlayground2.