(* T7: Proposiciones definidas inductivamente *)
Set Warnings "-notation-overridden,-parsing".
Require Export T6_Logica.
Require Coq.omega.Omega.
(* El contenido del tema es
1. Proposiciones definidas inductivamente.
2. Usando evidencias en demostraciones.
1. Inversión sobre evidencias.
2. Inducción sobre evidencias.
3. Relaciones inductivas.
*)
(* =====================================================================
§ 1. Proposiciones definidas inductivamente.
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.1. Definir inductivamente la proposición
es_par: nat -> Prop
tal que (es_par n) expresa que n es un número par.
------------------------------------------------------------------ *)
Inductive es_par: nat -> Prop :=
| es_par_0 : es_par 0
| es_par_SS : forall n : nat, es_par n -> es_par (S (S n)).
(* ---------------------------------------------------------------------
Ejemplo 1.2. Demostrar que
es_par 4.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem es_par_4: es_par 4.
Proof.
apply es_par_SS. (* es_par 2 *)
apply es_par_SS. (* es_par 0 *)
apply es_par_0.
Qed.
(* 2ª demostración *)
Theorem es_par_4': es_par 4.
Proof.
apply (es_par_SS 2 (es_par_SS 0 es_par_0)).
Qed.
(* Nota *)
Check es_par_0. (* es_par 0 *)
Check es_par_SS. (* forall n : nat,
es_par n -> es_par (S (S n)) *)
Check (es_par_SS 0). (* es_par 0 -> es_par 2 *)
Check (es_par_SS 0 es_par_0). (* es_par 2 *)
Check (es_par_SS 2). (* es_par 2 -> es_par 4 *)
Check (es_par_SS 2 (es_par_SS 0 es_par_0)). (* es_par 4 *)
(* ---------------------------------------------------------------------
Ejemplo 1.3. Demostrar que
forall n : nat, es_par n -> es_par (4 + n).
------------------------------------------------------------------ *)
Theorem es_par_suma4:
forall n : nat, es_par n -> es_par (4 + n).
Proof.
intros n. (* n : nat
============================
es_par n -> es_par (4 + n) *)
simpl. (* es_par n -> es_par (S (S (S (S n)))) *)
intros Hn. (* Hn : es_par n
============================
es_par (S (S (S (S n)))) *)
apply es_par_SS. (* es_par (S (S n)) *)
apply es_par_SS. (* es_par n *)
apply Hn.
Qed.
(* =====================================================================
§ 2. Usando evidencias en demostraciones
================================================================== *)
(* ---------------------------------------------------------------------
Nota. Programación y demostración en Coq son dos lados de la misma
moneda. En programación se procesan datos y en demostración se
procesan evidencias.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.1. Inversión sobre evidencias
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.1. Demostrar que
forall n : nat,
es_par n -> es_par (pred (pred n)).
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem es_par_menos_2:
forall n : nat,
es_par n -> es_par (pred (pred n)).
Proof.
intros n E. (* n : nat
E : es_par n
============================
es_par (Nat.pred (Nat.pred n)) *)
inversion E as [| n' E'].
- (* H : 0 = n
============================
es_par (Nat.pred (Nat.pred 0)) *)
simpl. (* es_par 0 *)
apply es_par_0.
- (* n' : nat
E' : es_par n'
H : S (S n') = n
============================
es_par (Nat.pred (Nat.pred (S (S n')))) *)
simpl. (* es_par n' *)
apply E'.
Qed.
(* ---------------------------------------------------------------------
Nota. La táctica (inversion E), donde E es la etiqueta de una
proposición P definida inductivamente, genera para cada uno de los
constructores de P las condiciones bajo las que se puede usar el
constructor para demostrar P.
------------------------------------------------------------------ *)
(* 2ª demostración *)
Theorem es_par_menos_2':
forall n : nat,
es_par n -> es_par (pred (pred n)).
Proof.
intros n E. (* n : nat
E : es_par n
============================
es_par (Nat.pred (Nat.pred n)) *)
destruct E as [| n' E'].
- (* es_par (Nat.pred (Nat.pred 0)) *)
simpl. (* es_par 0 *)
apply es_par_0.
- (* E' : es_par n'
============================
es_par (Nat.pred (Nat.pred (S (S n')))) *)
simpl. (* es_par n' *)
apply E'.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de destruct sobre evidencia con (destruct E as [| n' E']).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.2. Demostrar que
forall n : nat,
es_par (S (S n)) -> es_par n.
------------------------------------------------------------------ *)
(* 1º intento *)
Theorem es_parSS_es_par:
forall n : nat,
es_par (S (S n)) -> es_par n.
Proof.
intros n E. (* n : nat
E : es_par (S (S n))
============================
es_par n *)
destruct E as [| n' E'].
- (* n : nat
============================
es_par n *)
Abort.
(* ---------------------------------------------------------------------
Nota. Mal funcionamiento de destruct sobre evidencias de términos
compuestos.
------------------------------------------------------------------ *)
(* 2º intento *)
Theorem es_parSS_es_par:
forall n : nat,
es_par (S (S n)) -> es_par n.
Proof.
intros n E. (* n : nat
E : es_par (S (S n))
============================
es_par n *)
inversion E as [| n' E']. (* n' : nat
E' : es_par n
H : n' = n
============================
es_par n *)
apply E'.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.3. Demostrar que
~ es_par 1.
------------------------------------------------------------------ *)
Theorem uno_no_es_par:
~ es_par 1.
Proof.
intros H. (* H : es_par 1
============================
False *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de inversión sobre evidencia para contradicción.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.2. Inducción sobre evidencias
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.1. Demostrar que
forall n : nat,
es_par n -> exists k, n = doble k.
------------------------------------------------------------------ *)
(* 1º intento*)
Lemma es_par_par_1:
forall n : nat,
es_par n -> exists k, n = doble k.
Proof.
intros n E. (* n : nat
E : es_par n
============================
exists k : nat, n = doble k *)
inversion E as [| n' E'].
- (* H : 0 = n
============================
exists k : nat, 0 = doble k *)
exists 0. (* 0 = doble 0 *)
reflexivity.
- (* n' : nat
E' : es_par n'
H : S (S n') = n
============================
exists k : nat, S (S n') = doble k *)
simpl. (* exists k : nat, S (S n') = doble k *)
assert (I : (exists k', n' = doble k') ->
(exists k, S (S n') = doble k)).
+ (* (exists k' : nat, n' = doble k') ->
exists k : nat, S (S n') = doble k *)
intros [k' Hk']. (* k' : nat
Hk' : n' = doble k'
============================
exists k : nat, S (S n') = doble k *)
rewrite Hk'. (* exists k : nat, S (S (doble k')) = doble k *)
exists (S k'). (* S (S (doble k')) = doble (S k') *)
reflexivity.
+ (* I : (exists k' : nat, n' = doble k') ->
exists k : nat, S (S n') = doble k
============================
exists k : nat, S (S n') = doble k *)
apply I. (* exists k' : nat, n' = doble k' *)
Abort.
(* 2º intento *)
Lemma es_par_par:
forall n : nat,
es_par n -> exists k, n = doble k.
Proof.
intros n E. (* n : nat
E : es_par n
============================
exists k : nat, n = doble k *)
induction E as [|n' E' HI].
- (* exists k : nat, 0 = doble k *)
exists 0. (* 0 = doble 0 *)
reflexivity.
- (* n' : nat
E' : es_par n'
HI : exists k : nat, n' = doble k
============================
exists k : nat, S (S n') = doble k *)
destruct HI as [k' Hk']. (* k' : nat
Hk' : n' = doble k'
============================
exists k : nat, S (S n') = doble k *)
rewrite Hk'. (* exists k : nat, S (S (doble k')) = doble k *)
exists (S k'). (* S (S (doble k')) = doble (S k') *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.2.2. Demostrar que
forall n : nat,
es_par n <-> exists k, n = doble k.
------------------------------------------------------------------ *)
Lemma es_par_doble:
forall n : nat, es_par (doble n).
Proof.
induction n as [|n' HI].
- (* es_par (doble 0) *)
simpl. (* es_par 0 *)
apply es_par_0.
- (* n' : nat
HI : es_par (doble n')
============================
es_par (doble (S n')) *)
simpl. (* es_par (S (S (doble n'))) *)
apply es_par_SS. (* es_par (doble n') *)
apply HI.
Qed.
Theorem es_par_par_syss:
forall n : nat,
es_par n <-> exists k, n = doble k.
Proof.
intros n. (* n : nat
============================
es_par n <-> (exists k : nat, n = doble k) *)
split.
- (* es_par n -> exists k : nat, n = doble k *)
apply es_par_par.
- (* (exists k : nat, n = doble k) -> es_par n *)
intros [k Hk]. (* n, k : nat
Hk : n = doble k
============================
es_par n *)
rewrite Hk. (* es_par (doble k) *)
apply es_par_doble.
Qed.
(* =====================================================================
§ 3. Relaciones inductivas
================================================================== *)
(* ---------------------------------------------------------------------
Notas.
1. Las proposiciones con un argumento definen conjuntos; por ejemplo,
es_par define el conjunto de los números pares.
2. Las proposiciones con dos argumento definen relaciones.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Nota. Creamos el módulo para redefinir la relación menor o igual
(definida por le) como menOig.
------------------------------------------------------------------ *)
Module RelInd.
(* ---------------------------------------------------------------------
Ejemplo 3.1. Definir inductivamente la relación
menOig: nat -> nat -> Prop
tal que (menOig n m) expresa que n es menor o igual que m.
------------------------------------------------------------------ *)
Inductive menOig: nat -> nat -> Prop :=
| menOig_n : forall n, menOig n n
| menOig_S : forall n m, (menOig n m) -> (menOig n (S m)).
(* ---------------------------------------------------------------------
Ejemplo 3.2. Definir (m <= n) como abreviatura de (menOig m n).
------------------------------------------------------------------ *)
Notation "m <= n" := (menOig m n).
(* ---------------------------------------------------------------------
Nota. Sobre la relaciones (p.e. <=) se pueden usar las mismas
tácticas que sobre las propiedades (p.e. es_par).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 3.3. Demostrar que
3 <= 3.
------------------------------------------------------------------ *)
Theorem prop_menOig1:
3 <= 3.
Proof.
apply menOig_n.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.4. Demostrar que
3 <= 6.
------------------------------------------------------------------ *)
Theorem prop_menOig2 :
3 <= 6.
Proof.
apply menOig_S. (* 3 <= 5 *)
apply menOig_S. (* 3 <= 4 *)
apply menOig_S. (* 3 <= 3 *)
apply menOig_n.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.5. Demostrar que
(2 <= 1) -> 2 + 2 = 5.
------------------------------------------------------------------ *)
Theorem prop_menOig3 :
(2 <= 1) -> 2 + 2 = 5.
Proof.
intros H. (* H : 2 <= 1
============================
2 + 2 = 5 *)
inversion H. (* n, m : nat
H2 : 2 <= 0
H1 : n = 2
H0 : m = 0
============================
2 + 2 = 5 *)
inversion H2.
Qed.
End RelInd.
(* ---------------------------------------------------------------------
Nota. En lo que sigue, usaremos la predefiida le en lugar de menOig.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 3.6. Definir la relación
mayor : nat -> nat -> Prop
tal que (menor m n) expresa que m es menor que n.
------------------------------------------------------------------ *)
Definition menor (n m : nat) := le (S n) m.
(* ---------------------------------------------------------------------
Ejemplo 3.7. Definir la abreviatura (m < n) para (menor m n).
------------------------------------------------------------------ *)
Notation "m < n" := (menor m n).
(* ---------------------------------------------------------------------
Ejemplo 3.8. Definir inductivamente la relación
cuadrado_de: nat -> nat -> Prop :=
tal que (cuadrado x y) expresa que y es el cuadrado de x.
------------------------------------------------------------------ *)
Inductive cuadrado_de: nat -> nat -> Prop :=
| cuad : forall n : nat, cuadrado_de n (n * n).
(* ---------------------------------------------------------------------
Ejemplo 3.9. Definir inductivamente la relación
siguiente_nat : nat -> nat -> Prop
tal que (siguiente_nat x y) expresa que y es el siguiente de x.
------------------------------------------------------------------ *)
Inductive siguiente_nat : nat -> nat -> Prop :=
| sn : forall n : nat, siguiente_nat n (S n).
(* ---------------------------------------------------------------------
Ejemplo 3.9. Definir inductivamente la relación
siguiente_par : nat -> nat -> Prop :=
tal que (siguiente_par x y) expresa que y es el siguiente número par
de x.
------------------------------------------------------------------ *)
Inductive siguiente_par : nat -> nat -> Prop :=
| sp_1 : forall n, es_par (S n) -> siguiente_par n (S n)
| sp_2 : forall n, es_par (S (S n)) -> siguiente_par n (S (S n)).
(* =====================================================================
§ Bibliografía
=====================================================================
+ "Inductively defined propositions" de Peirce et als.
http://bit.ly/2Lejw7s *)
