(* El contenido de la teoría es
1. Datos y funciones
1. Tipos enumerados
2. Booleanos
3. Tipos de las funciones
4. Tipos compuestos
5. Módulos
6. Números naturales
2. Métodos elementales de demostración
1. Demostraciones por simplificación
2. Demostraciones por reescritura
3. Demostraciones por análisis de casos *)
(* =====================================================================
§ 1. Datos y funciones
================================================================== *)
(* =====================================================================
§§ 1.1. Tipos enumerados
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.1.1. Definir el tipo dia cuyos constructores sean los días
de la semana.
------------------------------------------------------------------ *)
Inductive dia: Type :=
| lunes : dia
| martes : dia
| miercoles : dia
| jueves : dia
| viernes : dia
| sabado : dia
| domingo : dia.
(* ---------------------------------------------------------------------
Ejemplo 1.1.2. Definir la función
siguiente_laborable : dia -> dia
tal que (siguiente_laborable d) es el día laboral siguiente a d.
------------------------------------------------------------------ *)
Definition siguiente_laborable (d : dia) : dia:=
match d with
| lunes => martes
| martes => miercoles
| miercoles => jueves
| jueves => viernes
| viernes => lunes
| sabado => lunes
| domingo => lunes
end.
(* ---------------------------------------------------------------------
Ejemplo 1.1.3. Calcular el valor de las siguientes expresiones
+ siguiente_laborable jueves
+ siguiente_laborable viernes
+ siguiente_laborable (siguiente_laborable sabado)
------------------------------------------------------------------ *)
Compute (siguiente_laborable jueves).
(* ==> viernes : dia *)
Compute (siguiente_laborable viernes).
(* ==> lunes : dia *)
Compute (siguiente_laborable (siguiente_laborable sabado)).
(* ==> martes : dia *)
(* ---------------------------------------------------------------------
Ejemplo 1.1.4. Demostrar que
siguiente_laborable (siguiente_laborable sabado) = martes
------------------------------------------------------------------ *)
Example siguiente_laborable1:
siguiente_laborable (siguiente_laborable sabado) = martes.
Proof.
simpl. (* ⊢ martes = martes *)
reflexivity. (* ⊢ *)
Qed.
(* =====================================================================
§§ 1.2. Booleanos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.2.1. Definir el tipo bool (𝔹) cuyos constructores son true
y false.
------------------------------------------------------------------ *)
Inductive bool : Type :=
| true : bool
| false : bool.
(* ---------------------------------------------------------------------
Ejemplo 1.2.2. Definir la función
negacion : bool -> bool
tal que (negacion b) es la negacion de b.
------------------------------------------------------------------ *)
Definition negacion (b : bool) : bool :=
match b with
| true => false
| false => true
end.
(* ---------------------------------------------------------------------
Ejemplo 1.2.3. Definir la función
conjuncion : bool -> bool -> bool
tal que (conjuncion b1 b2) es la conjuncion de b1 y b2.
------------------------------------------------------------------ *)
Definition conjuncion (b1 b2 : bool) : bool :=
match b1 with
| true => b2
| false => false
end.
(* ---------------------------------------------------------------------
Ejemplo 1.2.4. Definir la función
disyuncion : bool -> bool -> bool
tal que (disyuncion b1 b2) es la disyunción de b1 y b2.
------------------------------------------------------------------ *)
Definition disyuncion (b1 b2 : bool) : bool :=
match b1 with
| true => true
| false => b2
end.
(* ---------------------------------------------------------------------
Ejemplo 1.2.5. Demostrar las siguientes propiedades
disyuncion true false = true.
disyuncion false false = false.
disyuncion false true = true.
disyuncion true true = true.
------------------------------------------------------------------ *)
Example disyuncion1: disyuncion true false = true.
Proof. simpl. reflexivity. Qed.
Example disyuncion2: disyuncion false false = false.
Proof. simpl. reflexivity. Qed.
Example disyuncion3: disyuncion false true = true.
Proof. simpl. reflexivity. Qed.
Example disyuncion4: disyuncion true true = true.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.2.6. Definir los operadores (&&) y (||) como abreviaturas
de las funciones conjuncion y disyuncion.
------------------------------------------------------------------ *)
Notation "x && y" := (conjuncion x y).
Notation "x || y" := (disyuncion x y).
(* ---------------------------------------------------------------------
Ejemplo 1.2.7. Demostrar que
false || false || true = true.
------------------------------------------------------------------ *)
Example disyuncion5: false || false || true = true.
Proof. simpl. reflexivity. Qed.
(* =====================================================================
§§ 1.3. Tipos de las funciones
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.3.1. Calcular el tipo de las siguientes expresiones
+ true
+ (negacion true)
+ negacion
------------------------------------------------------------------ *)
Check true.
(* ===> true : bool *)
Check (negacion true).
(* ===> negacion true : bool *)
Check negacion.
(* ===> negacion : bool -> bool *)
(* =====================================================================
§§ 1.4. Tipos compuestos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.4.1. Definir el tipo rva cuyos constructores son rojo, verde
y azul.
------------------------------------------------------------------ *)
Inductive rva : Type :=
| rojo : rva
| verde : rva
| azul : rva.
(* ---------------------------------------------------------------------
Ejemplo 1.4.2. Definir el tipo color cuyos constructores son negro,
blanco y primario, donde primario es una función de rva en color.
------------------------------------------------------------------ *)
Inductive color : Type :=
| negro : color
| blanco : color
| primario : rva -> color.
(* ---------------------------------------------------------------------
Ejemplo 1.4.3. Definir la función
monocromático : color -> bool
tal que (monocromático c) se verifica si c es monocromático.
------------------------------------------------------------------ *)
Definition monocromático (c : color) : bool :=
match c with
| negro => true
| blanco => true
| primario p => false
end.
(* ---------------------------------------------------------------------
Ejemplo 1.4.4. Definir la función
esRojo : color -> bool
tal que (esRojo c) se verifica si c es rojo.
------------------------------------------------------------------ *)
Definition esRojo (c : color) : bool :=
match c with
| negro => false
| blanco => false
| primario rojo => true
| primario _ => false
end.
(* =====================================================================
§§ 1.5. Módulos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.5.1. Iniciar el módulo Naturales.
------------------------------------------------------------------ *)
Module Naturales.
(* =====================================================================
§§ 1.6. Números naturales
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.1. 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 1.6.2. 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 1.6.3. Finalizar el módulo Naturales.
------------------------------------------------------------------ *)
End Naturales.
(* ---------------------------------------------------------------------
Ejemplo 1.6.4. Calcular el tipo y valor de la expresión
(S (S (S (S O)))).
------------------------------------------------------------------ *)
Check (S (S (S (S O)))).
(* ===> 4 : nat *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.5. Definir la función
menosDos : nat -> nat
tal que (menosDos n) es n-2.
------------------------------------------------------------------ *)
Definition menosDos (n : nat) : nat :=
match n with
| O => O
| S O => O
| S (S n') => n'
end.
(* ---------------------------------------------------------------------
Ejemplo 1.6.6. Evaluar la expresión (menosDos 4).
------------------------------------------------------------------ *)
Compute (menosDos 4).
(* ===> 2 : nat *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.7. Calcular et tipo de las funcionse S, pred y menosDos.
------------------------------------------------------------------ *)
Check S.
(* ===> S : nat -> nat *)
Check pred.
(* ===> pred : nat -> nat *)
Check menosDos.
(* ===> menosDos : nat -> nat *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.8. Definir la función
esPar : nat -> bool
tal que (esPar n) se verifica si n es par.
------------------------------------------------------------------ *)
Fixpoint esPar (n : nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => esPar n'
end.
(* ---------------------------------------------------------------------
Ejemplo 1.6.9. Definir la función
esImpar : nat -> bool
tal que (esImpar n) se verifica si n es impar.
------------------------------------------------------------------ *)
Definition esImpar (n : nat) : bool :=
negacion (esPar n).
(* ---------------------------------------------------------------------
Ejemplo 1.6.10. Demostrar que
+ esImpar 1 = true.
+ esImpar 4 = false.
------------------------------------------------------------------ *)
Example esImpar1: esImpar 1 = true.
Proof. simpl. reflexivity. Qed.
Example esImpar2: esImpar 4 = false.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.6.12. Iniciar el módulo Naturales2.
------------------------------------------------------------------ *)
(* Module Naturales2. *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.13. Definir la función
suma : nat -> nat -> nat
tal que (suma n m) es la suma de n y m. Por ejemplo,
suma 3 2 = 5
Nota: Es equivalente a la predefinida plus
------------------------------------------------------------------ *)
Fixpoint suma (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (suma n' m)
end.
Compute (suma 3 2).
(* ===> 5 : nat *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.14. Definir la función
producto : nat -> nat -> nat
tal que (producto n m) es el producto de n y m. Por ejemplo,
producto 3 2 = 6
Nota: Es equivalente a la predefinida mult.
------------------------------------------------------------------ *)
Fixpoint producto (n m : nat) : nat :=
match n with
| O => O
| S n' => suma m (producto n' m)
end.
Example producto1: (producto 2 3) = 6.
Proof. simpl. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.6.15. Definir la función
resta : nat -> nat -> nat
tal que (resta n m) es la diferencia de n y m. Por ejemplo,
resta 3 2 = 1
Nota: Es equivalente a la predefinida minus.
------------------------------------------------------------------ *)
Fixpoint resta (n m : nat) : nat :=
match (n, m) with
| (O , _) => O
| (S _ , O) => n
| (S n', S m') => resta n' m'
end.
(* ---------------------------------------------------------------------
Ejemplo 1.6.16. Cerrar el módulo Naturales2.
------------------------------------------------------------------ *)
(* End Naturales2. *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.17. Definir la función
potencia : nat -> nat -> nat
tal que (potencia x n) es la potencia n-ésima de x. Por ejemplo,
potencia 2 3 = 8
Nota: En lugar de producto, usar la predefinida mult.
------------------------------------------------------------------ *)
Fixpoint potencia (x n : nat) : nat :=
match n with
| O => S O
| S m => mult x (potencia x m)
end.
Compute (potencia 2 3).
(* ===> 8 : nat *)
(* ---------------------------------------------------------------------
Ejemplo 1.6.18. Definir los operadores +, - y * como abreviaturas de
las funciones plus, rminus y mult.
------------------------------------------------------------------ *)
Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x - y" := (minus x y)
(at level 50, left associativity)
: nat_scope.
Notation "x * y" := (mult x y)
(at level 40, left associativity)
: nat_scope.
(* ---------------------------------------------------------------------
Ejemplo 1.6.19. Definir la función
iguales_nat : nat -> nat -> bool
tal que (iguales_nat n m) se verifica si n y me son iguales.
------------------------------------------------------------------ *)
Fixpoint iguales_nat (n m : nat) : bool :=
match n with
| O => match m with
| O => true
| S m' => false
end
| S n' => match m with
| O => false
| S m' => iguales_nat n' m'
end
end.
(* ---------------------------------------------------------------------
Ejemplo 1.6.20. Definir la función
menor_o_igual : nat -> nat -> bool
tal que (menor_o_igual n m) se verifica si n es menor o igual que m.
------------------------------------------------------------------ *)
Fixpoint menor_o_igual (n m : nat) : bool :=
match n with
| O => true
| S n' => match m with
| O => false
| S m' => menor_o_igual n' m'
end
end.
(* ---------------------------------------------------------------------
Ejemplo 1.6.21. Demostrar las siguientes propiedades
+ menor_o_igual 2 2 = true.
+ menor_o_igual 2 4 = true.
+ menor_o_igual 4 2 = false.
------------------------------------------------------------------ *)
Example menor_o_igual1: menor_o_igual 2 2 = true.
Proof. simpl. reflexivity. Qed.
Example menor_o_igual2: menor_o_igual 2 4 = true.
Proof. simpl. reflexivity. Qed.
Example menor_o_igual3: menor_o_igual 4 2 = false.
Proof. simpl. reflexivity. Qed.
(* =====================================================================
§ 2. Métodos elementales de demostración
================================================================== *)
(* =====================================================================
§ 2.1. Demostraciones por simplificación
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.1. Demostrar que el 0 es el elemento neutro por la
izquierda de la suma de los números naturales.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem suma_O_n : forall n : nat, 0 + n = n.
Proof.
intros n. (* n : nat
============================
0 + n = n *)
simpl. (* n = n *)
reflexivity.
Qed.
(* 2ª demostración *)
Theorem suma_O_n' : forall n : nat, 0 + n = n.
Proof.
intros n. (* n : nat
============================
0 + n = n *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.2. Demostrar que la suma de 1 y n es el siguiente de n.
------------------------------------------------------------------ *)
Theorem suma_1_l : forall n : nat, 1 + n = S n.
Proof.
intros n. (* n : nat
============================
1 + n = S n *)
simpl. (* S n = S n *)
reflexivity.
Qed.
Theorem suma_1_l' : forall n : nat, 1 + n = S n.
Proof.
intros n.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.3. Demostrar que el producto de 0 por n es 0.
------------------------------------------------------------------ *)
Theorem producto_0_l : forall n : nat, 0 * n = 0.
Proof.
intros n. (* n : nat
============================
0 * n = 0 *)
simpl. (* 0 = 0 *)
reflexivity.
Qed.
(* =====================================================================
§ 2.2. Demostraciones por reescritura
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.1. Demostrar que si n = m, entonces n + n = m + m.
------------------------------------------------------------------ *)
Theorem suma_iguales : forall n m : nat,
n = m ->
n + n = m + m.
Proof.
intros n m. (* n : nat
m : nat
============================
n = m -> n + n = m + m *)
intros H. (* n : nat
m : nat
H : n = m
============================
n + n = m + m *)
rewrite H. (* m + m = m + m *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.2.2. Demostrar que (0 + n) * m = n * m.
------------------------------------------------------------------ *)
Theorem producto_0_mas : forall n m : nat,
(0 + n) * m = n * m.
Proof.
intros n m. (* n : nat
m : nat
============================
(0 + n) * m = n * m *)
rewrite suma_O_n. (* n * m = n * m *)
reflexivity.
Qed.
(* =====================================================================
§ 2.3. Demostraciones por análisis de casos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.3.1. Demostrar que n + 1 es distinto de 0.
------------------------------------------------------------------ *)
(* 1º intento *)
Theorem siguiente_distinto_cero_primer_intento : forall n : nat,
iguales_nat (n + 1) 0 = false.
Proof.
intros n. (* n : nat
============================
iguales_nat (n + 1) 0 = false *)
simpl. (* n : nat
============================
iguales_nat (n + 1) 0 = false *)
Abort.
(* 2º intento *)
Theorem siguiente_distinto_cero : forall n : nat,
iguales_nat (n + 1) 0 = false.
Proof.
intros n. (* n : nat
============================
iguales_nat (n + 1) 0 = false *)
destruct n as [| n'].
- (*
============================
iguales_nat (0 + 1) 0 = false *)
reflexivity.
- (* n' : nat
============================
iguales_nat (S n' + 1) 0 = false *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.2. Demostrar que la negacion es involutiva; es decir, la
negacion de la negacion de b es b.
------------------------------------------------------------------ *)
Theorem negacion_involutiva : forall b : bool,
negacion (negacion b) = b.
Proof.
intros b. (*
============================
negacion (negacion b) = b *)
destruct b.
- (*
============================
negacion (negacion true) = true *)
reflexivity.
- (*
============================
negacion (negacion false) = false *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.3. Demostrar que la conjuncion es conmutativa.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem conjuncion_commutativa : forall b c : bool,
conjuncion b c = conjuncion c b.
Proof.
intros b c. (* b : bool
c : bool
============================
b && c = c && b *)
destruct b.
- (* c : bool
============================
true && c = c && true *)
destruct c.
+ (* ============================
true && true = true && true *)
reflexivity.
+ (*
============================
true && false = false && true *)
reflexivity.
- (* c : bool
============================
false && c = c && false *)
destruct c.
+ (*
============================
false && true = true && false *)
reflexivity.
+ (*
============================
false && false = false && false *)
reflexivity.
Qed.
(* 2ª demostración *)
Theorem conjuncion_commutativa2 : forall b c : bool,
conjuncion b c = conjuncion c b.
Proof.
intros b c.
destruct b.
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
{ destruct c.
{ reflexivity. }
{ reflexivity. } }
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.4. Demostrar que
conjuncion (conjuncion b c) d = conjuncion (conjuncion b d) c.
------------------------------------------------------------------ *)
Theorem conjuncion_intercambio : forall b c d : bool,
conjuncion (conjuncion b c) d = conjuncion (conjuncion b d) c.
Proof.
intros b c d.
destruct b.
- destruct c.
{ destruct d.
- reflexivity. (* (true && true) && true = (true && true) && true *)
- reflexivity. } (* (true && true) && false = (true && false) && true *)
{ destruct d.
- reflexivity. (* (true && false) && true = (true && true) && false *)
- reflexivity. } (* (true && false) && false = (true && false) && false *)
- destruct c.
{ destruct d.
- reflexivity. (* (false && true) && true = (false && true) && true *)
- reflexivity. } (* (false && true) && false = (false && false) && true *)
{ destruct d.
- reflexivity. (* (false && false) && true = (false && true) && false *)
- reflexivity. } (* (false && false) && false = (false && false) && false *)
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.5. Demostrar que n + 1 es distinto de 0.
------------------------------------------------------------------ *)
Theorem siguiente_distinto_cero' : forall n : nat,
iguales_nat (n + 1) 0 = false.
Proof.
intros [|n].
- reflexivity. (* iguales_nat (0 + 1) 0 = false *)
- reflexivity. (* iguales_nat (S n + 1) 0 = false *)
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.6. Demostrar que la conjunción es conmutativa.
------------------------------------------------------------------ *)
Theorem conjuncion_commutativa'' : forall b c : bool,
conjuncion b c = conjuncion c b.
Proof.
intros [] [].
- reflexivity. (* true && true = true && true *)
- reflexivity. (* true && false = false && true *)
- reflexivity. (* false && true = true && false *)
- reflexivity. (* false && false = false && false *)
Qed.
(* =====================================================================
§ Bibliografía
================================================================== *)
(*
+ "Functional programming in Coq" de Peirce et als. http://bit.ly/2zRCL6t
*)
