Set Warnings "-notation-overridden,-parsing".
Require Export T5_Tacticas.
(* El contenido del tema es
1. Introducción
2. Conectivas lógicas
1. Conjunción
2. Disyunción
3. Falsedad y negación
4. Verdad
5. Equivalencia lógica
6. Cuantificación existencial
3. Programación con proposiciones
4. Aplicando teoremas a argumentos
5. Coq vs. teoría de conjuntos
1. Extensionalidad funcional
2. Proposiciones y booleanos
3. Lógica clásica vs. constructiva
Bibliografía
*)
(* =====================================================================
§ 1. Introducción
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.1. Calcular el tipo de las siguientes expresiones
3 = 3.
3 = 4.
forall n m : nat, n + m = m + n.
forall n : nat, n = 2.
------------------------------------------------------------------ *)
Check 3 = 3.
(* ===> Prop *)
Check 3 = 4.
(* ===> Prop *)
Check forall n m : nat, n + m = m + n.
(* ===> Prop *)
Check forall n : nat, n = 2.
(* ===> Prop *)
(* ---------------------------------------------------------------------
Nota. El tipo de las fórmulas es Prop.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 1.2.3. Demostrar que 2 más dos es 4.
------------------------------------------------------------------ *)
Theorem suma_2_y_2:
2 + 2 = 4.
Proof. reflexivity. Qed.
(* ---------------------------------------------------------------------
Nota. Usa la proposición '2 + 2 = 4'.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 1.2.2. Definir la proposición
prop_suma: Prop
que afirma que la suma de 2 y 2 es 4.
------------------------------------------------------------------ *)
Definition prop_suma: Prop := 2 + 2 = 4.
(* ---------------------------------------------------------------------
Ejemplo 1.2.3. Calcular el tipo de prop_suma
------------------------------------------------------------------ *)
Check prop_suma.
(* ===> prop_suma : Prop *)
(* ---------------------------------------------------------------------
Ejemplo 1.2.4. Usando prop_suma, demostrar que la suma de 2 y 2 es 4.
------------------------------------------------------------------ *)
Theorem prop_suma_es_verdadera:
prop_suma.
Proof. reflexivity. Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.3.1. Definir la proposición
es_tres (n : nat) : Prop
tal que (es_tres n) se verifica si n es el número 3.
------------------------------------------------------------------ *)
Definition es_tres (n : nat) : Prop :=
n = 3.
(* ---------------------------------------------------------------------
Ejemplo 1.3.2. Calcular el tipo de las siguientes expresiones
es_tres.
es_tres 3.
es_tres 5.
------------------------------------------------------------------ *)
Check es_tres.
(* ===> nat -> Prop *)
Check es_tres 3.
(* ===> Prop *)
Check es_tres 5.
(* ===> Prop *)
(* ---------------------------------------------------------------------
Nota. Ejemplo de proposición parametrizada.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 1.4.1. Definir la función
inyectiva {A B : Type} (f : A -> B) : Prop :=
tal que (inyectiva f) se verifica si f es inyectiva.
------------------------------------------------------------------ *)
Definition inyectiva {A B : Type} (f : A -> B) : Prop :=
forall x y : A, f x = f y -> x = y.
(* ---------------------------------------------------------------------
Ejemplo 1.4.2. Demostrar que la funcion sucesor es inyectiva; es
decir,
inyectiva S.
------------------------------------------------------------------ *)
Lemma suc_iny: inyectiva S.
Proof.
intros n m H. (* n, m : nat
H : S n = S m
============================
n = m *)
inversion H. (* n, m : nat
H : S n = S m
H1 : n = m
============================
m = m *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.5. Calcular los tipos de las siguientes expresiones
3 = 5.
eq 3 5.
eq 3.
@eq.
------------------------------------------------------------------ *)
Check (3 = 5).
(* ===> Prop *)
Check (eq 3 5).
(* ===> Prop *)
Check (eq 3).
(* ===> nat -> Prop *)
Check @eq.
(* ===> forall A : Type, A -> A -> Prop *)
(* ---------------------------------------------------------------------
Notas.
1. La expresión (x = y) es una abreviatura de (eq x y).
2. Se escribe @eq en lugar de eq para ver los argumentos implícitos.
------------------------------------------------------------------ *)
(* =====================================================================
§ 2. Conectivas lógicas
================================================================== *)
(* =====================================================================
§§ 2.1. Conjunción
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.1. Demostrar que
3 + 4 = 7 /\ 2 * 2 = 4.
------------------------------------------------------------------ *)
Example ej_conjuncion: 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
split.
- (*
============================
3 + 4 = 7 *)
reflexivity.
- (*
============================
2 * 2 = 4 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. El símbolo de conjunción se escribe con /\
2. La táctica 'split' sustituye el objetivo (P /\ Q) por los
subobjetivos P y Q.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.2. Demostrar que
forall A B : Prop, A -> B -> A /\ B.
------------------------------------------------------------------ *)
Lemma conj_intro: forall A B : Prop, A -> B -> A /\ B.
Proof.
intros A B HA HB. (* A, B : Prop
HA : A
HB : B
============================
A /\ B *)
split.
- (* A, B : Prop
HA : A
HB : B
============================
A *)
apply HA.
- (* A, B : Prop
HA : A
HB : B
============================
B *)
apply HB.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.3. Demostrar, con conj_intro, que
3 + 4 = 7 /\ 2 * 2 = 4.
------------------------------------------------------------------ *)
Example ej_conjuncion': 3 + 4 = 7 /\ 2 * 2 = 4.
Proof.
apply conj_intro.
- (* 3 + 4 = 7 *)
reflexivity.
- (* 2 * 2 = 4 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.4. Demostrar que
forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
------------------------------------------------------------------ *)
Lemma ej_conjuncion2 :
forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof.
intros n m H. (* n, m : nat
H : n = 0 /\ m = 0
============================
n + m = 0 *)
destruct H as [Hn Hm]. (* n, m : nat
Hn : n = 0
Hm : m = 0
============================
n + m = 0 *)
rewrite Hn. (* 0 + m = 0 *)
rewrite Hm. (* 0 + 0 = 0 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de la táctica 'destruct H as [HA HB]' que sustituye la
hipótesis H de la forma (A /\ B) por las hipótesis HA (que afirma
que A es verdad) y HB (que afirma que B es verdad).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.5. Demostrar que
forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
------------------------------------------------------------------ *)
Lemma ej_conjuncion2' :
forall n m : nat, n = 0 /\ m = 0 -> n + m = 0.
Proof.
intros n m [Hn Hm]. (* n, m : nat
Hn : n = 0
Hm : m = 0
============================
n + m = 0 *)
rewrite Hn. (* 0 + m = 0 *)
rewrite Hm. (* 0 + 0 = 0 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. La táctica 'intros x [HA HB]', cuando el objetivo es de la
forma (forall x, A /\ B -> C), introduce la variable x y las
hipótesis HA y HB afirmando la certeza de A y de B, respectivamente.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.1.6. Demostrar que
forall n m : nat, n = 0 -> m = 0 -> n + m = 0.
------------------------------------------------------------------ *)
Lemma ej_conjuncion2'' :
forall n m : nat, n = 0 -> m = 0 -> n + m = 0.
Proof.
intros n m Hn Hm. (* n, m : nat
Hn : n = 0
Hm : m = 0
============================
n + m = 0 *)
rewrite Hn. (* 0 + m = 0 *)
rewrite Hm. (* 0 + 0 = 0 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.8. Demostrar que
forall P Q : Prop,
P /\ Q -> P.
------------------------------------------------------------------ *)
Lemma conj_e1 : forall P Q : Prop,
P /\ Q -> P.
Proof.
intros P Q [HP HQ]. (* P, Q : Prop
HP : P
HQ : Q
============================
P *)
apply HP.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.9. Demostrar que
forall P Q : Prop,
P /\ Q -> Q /\ P.
------------------------------------------------------------------ *)
Theorem conj_conmutativa: forall P Q : Prop,
P /\ Q -> Q /\ P.
Proof.
intros P Q [HP HQ]. (* P, Q : Prop
HP : P
HQ : Q
============================
Q /\ P *)
split.
- (* P, Q : Prop
HP : P
HQ : Q
============================
Q *)
apply HQ.
- (* P, Q : Prop
HP : P
HQ : Q
============================
P *)
apply HP.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.1.10. Calcular el tipo de la expresión
and
------------------------------------------------------------------ *)
Check and.
(* ===> and : Prop -> Prop -> Prop *)
(* ---------------------------------------------------------------------
Nota. (x /\ y) es una abreviatura de (and x y).
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.2. Disyunción
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.1. Demostrar que
forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Lemma disy_ej1:
forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
intros n m H.
destruct H as [Hn | Hm].
- (* n, m : nat
Hn : n = 0
============================
n * m = 0 *)
rewrite Hn. (* 0 * m = 0 *)
reflexivity.
- (* n, m : nat
Hm : m = 0
============================
n * m = 0 *)
rewrite Hm. (* n * 0 = 0 *)
rewrite <- mult_n_O. (* 0 = 0 *)
reflexivity.
Qed.
(* 2ª demostración *)
Lemma disy_ej:
forall n m : nat, n = 0 \/ m = 0 -> n * m = 0.
Proof.
intros n m [Hn | Hm].
- (* n, m : nat
Hn : n = 0
============================
n * m = 0 *)
rewrite Hn. (* 0 * m = 0 *)
reflexivity.
- (* n, m : nat
Hm : m = 0
============================
n * m = 0 *)
rewrite Hm. (* n * 0 = 0 *)
rewrite <- mult_n_O. (* 0 = 0 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. La táctica 'destruct H as [Hn | Hm]', cuando la hipótesis H es de
la forma (A \/ B), la divide en dos casos: uno con hipótesis HA
(afirmando la certeza de A) y otro con la hipótesis HB (afirmando
la certeza de B).
2. La táctica 'intros x [HA | HB]', cuando el objetivo es de la
forma (forall x, A \/ B -> C), intoduce la variable x y dos casos:
uno con hipótesis HA (afirmando la certeza de A) y otro con la
hipótesis HB (afirmando la certeza de B).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.2. Demostrar que
forall A B : Prop, A -> A \/ B.
------------------------------------------------------------------ *)
Lemma disy_intro: forall A B : Prop, A -> A \/ B.
Proof.
intros A B HA. (* A, B : Prop
HA : A
============================
A \/ B *)
left. (* A *)
apply HA.
Qed.
(* ---------------------------------------------------------------------
Nota. La táctica 'left' sustituye el objetivo de la forma (A \/ B)
por A.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.3. Demostrar que
forall n : nat, n = 0 \/ n = S (pred n).
------------------------------------------------------------------ *)
Lemma cero_o_sucesor:
forall n : nat, n = 0 \/ n = S (pred n).
Proof.
intros [|n].
- (*
============================
0 = 0 \/ 0 = S (Nat.pred 0) *)
left. (* 0 = 0 *)
reflexivity.
- (* n : nat
============================
S n = 0 \/ S n = S (Nat.pred (S n)) *)
right. (* S n = S (Nat.pred (S n)) *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. La táctica 'right' sustituye el objetivo de la forma (A \/ B)
por B.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.2.4. Calcular el tipo de la expresión
or
------------------------------------------------------------------ *)
Check or.
(* ===> or : Prop -> Prop -> Prop *)
(* ---------------------------------------------------------------------
Nota. (x \/ y) es una abreviatura de (or x y).
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.3. Falsedad y negación
================================================================== *)
Module DefNot.
(* ---------------------------------------------------------------------
Ejemplo 2.3.1. Definir la función
not (P : Prop) : Prop
tal que (not P) es la negación de P
------------------------------------------------------------------ *)
Definition not (P:Prop) : Prop :=
P -> False.
(* ---------------------------------------------------------------------
Ejemplo 2.3.2. Definir (~ x) como abreviatura de (not x).
------------------------------------------------------------------ *)
Notation "~ x" := (not x) : type_scope.
(* ---------------------------------------------------------------------
Nota. Esta es la forma como está definida la negación en Coq.
------------------------------------------------------------------ *)
End DefNot.
(* ---------------------------------------------------------------------
Ejemplo 2.3.3. Demostrar que
forall (P:Prop),
False -> P.
------------------------------------------------------------------ *)
Theorem ex_falso_quodlibet: forall (P:Prop),
False -> P.
Proof.
intros P H. (* P : Prop
H : False
============================
P *)
destruct H.
Qed.
(* ---------------------------------------------------------------------
Nota. En latín, "ex falso quodlibet" significa "de lo falso (se
sigue) cualquier cosa".
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.3.4. Demostrar que
~(0 = 1).
------------------------------------------------------------------ *)
Theorem cero_no_es_uno: ~(0 = 1).
Proof.
intros H. (* H : 0 = 1
============================
False *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Nota. La expresión (x <> y) es una abreviatura de ~(x = y).
------------------------------------------------------------------ *)
Theorem cero_no_es_uno': 0 <> 1.
Proof.
intros H. (* H : 0 = 1
============================
False *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.5. Demostrar que
~ False
------------------------------------------------------------------ *)
Theorem not_False :
~ False.
Proof.
unfold not. (*
============================
False -> False *)
intros H. (* H : False
============================
False *)
destruct H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.6. Demostrar que
forall P Q : Prop,
(P /\ ~P) -> Q.
------------------------------------------------------------------ *)
Theorem contradiccion_implica_cualquiera: forall P Q : Prop,
(P /\ ~P) -> Q.
Proof.
intros P Q [HP HNP]. (* P, Q : Prop
HP : P
HNP : ~ P
============================
Q *)
unfold not in HNP. (* P, Q : Prop
HP : P
HNP : P -> False
============================
Q *)
apply HNP in HP. (* P, Q : Prop
HP : False
HNP : P -> False
============================
Q *)
destruct HP.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.7. Demostrar que
forall P : Prop,
P -> ~~P.
------------------------------------------------------------------ *)
Theorem doble_neg: forall P : Prop,
P -> ~~P.
Proof.
intros P H. (* P : Prop
H : P
============================
~ ~ P *)
unfold not. (* (P -> False) -> False *)
intros G. (* P : Prop
H : P
G : P -> False
============================
False *)
apply G. (* P *)
apply H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.3.8. Demostrar que
forall b : bool,
b <> true -> b = false.
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem no_verdadero_es_falso: forall b : bool,
b <> true -> b = false.
Proof.
intros [] H.
- (* H : true <> true
============================
true = false *)
unfold not in H. (* H : true = true -> False
============================
true = false *)
apply ex_falso_quodlibet. (* H : true = true -> False
============================
False *)
apply H. (* true = true *)
reflexivity.
- (* H : false <> true
============================
false = false *)
reflexivity.
Qed.
(* 2ª demostración *)
Theorem no_verdadero_es_falso': forall b : bool,
b <> true -> b = false.
Proof.
intros [] H.
- (* H : true <> true
============================
true = false *)
unfold not in H. (* H : true = true -> False
============================
true = false *)
exfalso. (* H : true = true -> False
============================
False *)
apply H. (* true = true *)
reflexivity.
- (* H : false <> true
============================
false = false *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. Uso de 'apply ex_falso_quodlibet' en la primera demostración.
2. Uso de 'exfalso' en la segunda demostración.
3. La táctica 'exfalso' sustituye el objetivo por falso.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.4. Verdad
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.4.1. Demostrar que la proposición True es verdadera.
------------------------------------------------------------------ *)
Lemma True_es_verdadera : True.
Proof.
apply I.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso del constructor I.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.5. Equivalencia lógica
================================================================== *)
Module DefIff.
(* ---------------------------------------------------------------------
Ejemplo 2.5.1. Definir la función
iff (P Q : Prop) : Prop
tal que (iff P Q) es la equivalencia de P y Q.
------------------------------------------------------------------ *)
Definition iff (P Q : Prop) : Prop := (P -> Q) /\ (Q -> P).
(* ---------------------------------------------------------------------
Ejemplo 2.5.2. Definir (P <-> Q) como una abreviatura de (iff P Q).
------------------------------------------------------------------ *)
Notation "P <-> Q" := (iff P Q)
(at level 95, no associativity)
: type_scope.
End DefIff.
(* ---------------------------------------------------------------------
Ejemplo 2.5.3. Demostrar que
forall P Q : Prop,
(P <-> Q) -> (Q <-> P).
------------------------------------------------------------------ *)
Theorem iff_sim : forall P Q : Prop,
(P <-> Q) -> (Q <-> P).
Proof.
intros P Q [HPQ HQP]. (* P, Q : Prop
HPQ : P -> Q
HQP : Q -> P
============================
Q <-> P *)
split.
- (* P, Q : Prop
HPQ : P -> Q
HQP : Q -> P
============================
Q -> P *)
apply HQP.
- (* P, Q : Prop
HPQ : P -> Q
HQP : Q -> P
============================
P -> Q *)
apply HPQ.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.5.4. Demostrar que
forall b : bool,
b <> true <-> b = false.
------------------------------------------------------------------ *)
Lemma not_true_iff_false : forall b : bool,
b <> true <-> b = false.
Proof.
intros b. (* b : bool
============================
b <> true <-> b = false *)
split.
- (* b : bool
============================
b <> true -> b = false *)
apply no_verdadero_es_falso.
- (* b : bool
============================
b = false -> b <> true *)
intros H. (* b : bool
H : b = false
============================
b <> true *)
rewrite H. (* false <> true *)
intros H'. (* b : bool
H : b = false
H' : false = true
============================
False *)
inversion H'.
Qed.
(* ---------------------------------------------------------------------
Nota. Se importa la librería Coq.Setoids.Setoid para usar las
tácticas reflexivity y rewrite con iff.
------------------------------------------------------------------ *)
Require Import Coq.Setoids.Setoid.
(* ---------------------------------------------------------------------
Ejercicio 2.2.1. Demostrar que
forall n m, n * m = 0 -> n = 0 \/ m = 0.
------------------------------------------------------------------ *)
Lemma mult_eq_0 :
forall n m, n * m = 0 -> n = 0 \/ m = 0.
Proof.
intros n m H. (* n, m : nat
H : n * m = 0
============================
n = 0 \/ m = 0 *)
destruct n as [|n'].
- (* m : nat
H : 0 * m = 0
============================
0 = 0 \/ m = 0 *)
left. (* 0 = 0 *)
reflexivity.
- (* n', m : nat
H : S n' * m = 0
============================
S n' = 0 \/ m = 0 *)
destruct m as [|m'].
+ (* n' : nat
H : S n' * 0 = 0
============================
S n' = 0 \/ 0 = 0 *)
right. (* 0 = 0 *)
reflexivity.
+ (* n', m' : nat
H : S n' * S m' = 0
============================
S n' = 0 \/ S m' = 0 *)
simpl in H. (* n', m' : nat
H : S (m' + n' * S m') = 0
============================
S n' = 0 \/ S m' = 0 *)
inversion H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.5.5. Demostrar que
forall n m : nat, n * m = 0 <-> n = 0 \/ m = 0.
------------------------------------------------------------------ *)
Lemma mult_0 : forall n m : nat, n * m = 0 <-> n = 0 \/ m = 0.
Proof.
split.
- (* n, m : nat
============================
n * m = 0 -> n = 0 \/ m = 0 *)
apply mult_eq_0.
- (* n, m : nat
============================
n = 0 \/ m = 0 -> n * m = 0 *)
apply disy_ej.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.5.6. Demostrar que
forall P Q R : Prop,
P \/ (Q \/ R) <-> (P \/ Q) \/ R.
------------------------------------------------------------------ *)
Lemma disy_asociativa :
forall P Q R : Prop, P \/ (Q \/ R) <-> (P \/ Q) \/ R.
Proof.
intros P Q R. (* P, Q, R : Prop
============================
P \/ (Q \/ R) <-> (P \/ Q) \/ R *)
split.
- (* P, Q, R : Prop
============================
P \/ (Q \/ R) -> (P \/ Q) \/ R *)
intros [H | [H | H]].
+ (* P, Q, R : Prop
H : P
============================
(P \/ Q) \/ R *)
left. (* P \/ Q *)
left. (* P *)
apply H.
+ (* P, Q, R : Prop
H : Q
============================
(P \/ Q) \/ R *)
left. (* P \/ Q *)
right. (* Q *)
apply H.
+ (* P, Q, R : Prop
H : R
============================
(P \/ Q) \/ R *)
right. (* R *)
apply H.
- (* P, Q, R : Prop
============================
(P \/ Q) \/ R -> P \/ (Q \/ R) *)
intros [[H | H] | H].
+ (* P, Q, R : Prop
H : P
============================
(P \/ Q) \/ R *)
left. (* P *)
apply H.
+ (* P, Q, R : Prop
H : Q
============================
P \/ (Q \/ R) *)
right. (* Q \/ R *)
left. (* Q *)
apply H.
+ (* P, Q, R : Prop
H : R
============================
P \/ (Q \/ R) *)
right. (* Q \/ R *)
right. (* R *)
apply H.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 2.5.7. Demostrar que
forall n m p : nat,
n * m * p = 0 <-> n = 0 \/ m = 0 \/ p = 0.
------------------------------------------------------------------ *)
Lemma mult_0_3: forall n m p : nat,
n * m * p = 0 <-> n = 0 \/ m = 0 \/ p = 0.
Proof.
intros n m p. (* n, m, p : nat
============================
n * (m * p) = 0 <-> n = 0 \/ (m = 0 \/ p = 0) *)
rewrite mult_0. (* n * m = 0 \/ p = 0 <->
n = 0 \/ (m = 0 \/ p = 0) *)
rewrite mult_0. (* (n = 0 \/ m = 0) \/ p = 0 <->
n = 0 \/ (m = 0 \/ p = 0) *)
rewrite disy_asociativa. (* (n = 0 \/ m = 0) \/ p = 0 <->
(n = 0 \/ m = 0) \/ p = 0 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de reflexivity y rewrite con iff.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.5.8. Demostrar que
forall n m : nat,
n * m = 0 -> n = 0 \/ m = 0.
------------------------------------------------------------------ *)
Lemma ej_apply_iff: forall n m : nat,
n * m = 0 -> n = 0 \/ m = 0.
Proof.
intros n m H. (* n, m : nat
H : n * m = 0
============================
n = 0 \/ m = 0 *)
apply mult_0. (* n * m = 0 *)
apply H.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso de apply sobre iff.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 2.6. Cuantificación existencial
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.6.1. Demostrar que
exists n : nat, 4 = n + n.
------------------------------------------------------------------ *)
Lemma cuatro_es_par: exists n : nat, 4 = n + n.
Proof.
exists 2. (*
============================
4 = 2 + 2 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. La táctica 'exists a' sustituye el objetivo de la forma
(exists x, P(x)) por P(a).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 2.6.2. Demostrar que
forall n : nat,
(exists m, n = 4 + m) -> (exists o, n = 2 + o).
------------------------------------------------------------------ *)
(* 1ª demostración *)
Theorem ej_existe_2a: forall n : nat,
(exists m, n = 4 + m) ->
(exists o, n = 2 + o).
Proof.
intros n H. (* n : nat
H : exists m : nat, n = 4 + m
============================
exists o : nat, n = 2 + o *)
destruct H as [a Ha]. (* n, a : nat
Ha : n = 4 + a
============================
exists o : nat, n = 2 + o *)
exists (2 + a). (* n = 2 + (2 + a) *)
apply Ha.
Qed.
(* 2ª demostración *)
Theorem ej_existe_2b: forall n : nat,
(exists m, n = 4 + m) ->
(exists o, n = 2 + o).
Proof.
intros n [a Ha]. (* n, a : nat
Ha : n = 4 + a
============================
exists o : nat, n = 2 + o *)
exists (2 + a). (* n = 2 + (2 + a) *)
apply Ha.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. 'destruct H [a Ha]' sustituye la hipótesis (H : exists x, P(x))
por (Ha : P(a)).
2. 'intros x [a Ha]' sustituye el objetivo
(forall x, (exists y P(y)) -> Q(x)) por Q(x) y le añade la
hipótesis (Ha : P(a)).
------------------------------------------------------------------ *)
(* =====================================================================
§ 3. Programación con proposiciones
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 3.1.1. Definir la función
En {A : Type} (x : A) (xs : list A) : Prop :=
tal que (En x xs) se verifica si x pertenece a xs.
------------------------------------------------------------------ *)
Fixpoint En {A : Type} (x : A) (xs : list A) : Prop :=
match xs with
| [] => False
| x' :: xs' => x' = x \/ En x xs'
end.
(* ---------------------------------------------------------------------
Ejemplo 3.1.2. Demostrar que
En 4 [1; 2; 3; 4; 5].
------------------------------------------------------------------ *)
Example En_ejemplo_1 : En 4 [1; 2; 3; 4; 5].
Proof.
simpl. (* 1 = 4 \/ 2 = 4 \/ 3 = 4 \/ 4 = 4 \/ 5 = 4 \/ False *)
right. (* 2 = 4 \/ 3 = 4 \/ 4 = 4 \/ 5 = 4 \/ False *)
right. (* 3 = 4 \/ 4 = 4 \/ 5 = 4 \/ False *)
right. (* 4 = 4 \/ 5 = 4 \/ False *)
left. (* 4 = 4 *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 3.1.3. Demostrar que
forall n : nat,
En n [2; 4] -> exists n', n = 2 * n'.
------------------------------------------------------------------ *)
Example En_ejemplo_2: forall n : nat,
En n [2; 4] -> exists n', n = 2 * n'.
Proof.
simpl. (*
============================
forall n : nat,
2 = n \/ 4 = n \/ False ->
exists n' : nat, n = n' + (n' + 0) *)
intros n [H | [H | []]].
- (* n : nat
H : 2 = n
============================
exists n' : nat, n = n' + (n' + 0) *)
exists 1. (* n = 1 + (1 + 0) *)
rewrite <- H. (* 2 = 1 + (1 + 0) *)
reflexivity.
- (* n : nat
H : 4 = n
============================
exists n' : nat, n = n' + (n' + 0) *)
exists 2. (* n = 2 + (2 + 0) *)
rewrite <- H. (* 4 = 2 + (2 + 0) *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Uso del patrón vacío para descartar el último caso.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 3.2. Demostrar que
forall (A B : Type) (f : A -> B) (xs : list A) (x : A),
En x xs ->
En (f x) (map f xs).
------------------------------------------------------------------ *)
Lemma En_map: forall (A B : Type) (f : A -> B) (xs : list A) (x : A),
En x xs ->
En (f x) (map f xs).
Proof.
intros A B f xs x. (* A : Type
B : Type
f : A -> B
xs : list A
x : A
============================
En x xs -> En (f x) (map f xs) *)
induction xs as [|x' xs' HI].
- (* A : Type
B : Type
f : A -> B
x : A
============================
En x [ ] -> En (f x) (map f [ ]) *)
simpl. (* False -> False *)
intros [].
- (* A : Type
B : Type
f : A -> B
x' : A
xs' : list A
x : A
HI : En x xs' -> En (f x) (map f xs')
============================
En x (x'::xs') ->
En (f x) (map f (x'::xs')) *)
simpl. (* x' = x \/ En x xs' ->
f x' = f x \/ En (f x) (map f xs') *)
intros [H | H].
+ (* A : Type
B : Type
f : A -> B
x' : A
xs' : list A
x : A
HI : En x xs' -> En (f x) (map f xs')
H : x' = x
============================
f x' = f x \/ En (f x) (map f xs') *)
rewrite H. (* f x = f x \/ En (f x) (map f xs') *)
left. (* f x = f x *)
reflexivity.
+ (* A : Type
B : Type
f : A -> B
x' : A
xs' : list A
x : A
HI : En x xs' -> En (f x) (map f xs')
H : En x xs'
============================
f x' = f x \/ En (f x) (map f xs') *)
right. (* En (f x) (map f xs') *)
apply HI. (* En x xs' *)
apply H.
Qed.
(* =====================================================================
§ 4. Aplicando teoremas a argumentos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 4.1. Evaluar la expresión
Check suma_conmutativa.
------------------------------------------------------------------ *)
Check suma_conmutativa.
(* ===> forall n m : nat, n + m = m + n *)
(* ---------------------------------------------------------------------
Notas.
1. En Coq, las demostraciones son objetos de primera clase.
2. Coq devuelve el tipo de suma_conmutativa como el de cualquier
expresión.
3. El identificador suma_conmutativa representa un objeto prueba de
(forall n m : nat, n + m = m + n).
4. Un término de tipo (nat -> nat -> nat) transforma dos naturales en
un natural.
5. Análogamente, un término de tipo (n = m -> n + n = m + m)
transforma un argumento de tipo (n = m) en otro de tipo
(n + n = m + m).
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 4.2. Demostrar que
forall x y z : nat,
x + (y + z) = (z + y) + x.
------------------------------------------------------------------ *)
(* 1º intento *)
Lemma suma_conmutativa3a :
forall x y z : nat,
x + (y + z) = (z + y) + x.
Proof.
intros x y z. (* x, y, z : nat
============================
x + (y + z) = (z + y) + x *)
rewrite suma_conmutativa. (* (y + z) + x = (z + y) + x *)
rewrite suma_conmutativa. (* x + (y + z) = (z + y) + x *)
Abort.
(* 2º intento *)
Lemma suma_conmutativa3b :
forall x y z,
x + (y + z) = (z + y) + x.
Proof.
intros x y z. (* x, y, z : nat
============================
x + (y + z) = z + y + x *)
rewrite suma_conmutativa. (* (y + z) + x = (z + y) + x *)
assert (H : y + z = z + y).
- (* x, y, z : nat
============================
y + z = z + y *)
rewrite suma_conmutativa. (* z + y = z + y *)
reflexivity.
- (* x, y, z : nat
H : y + z = z + y
============================
(y + z) + x = (z + y) + x *)
rewrite H. (* (z + y) + x = (z + y) + x *)
reflexivity.
Qed.
(* 3º intento *)
Lemma suma_conmutativa3c:
forall x y z,
x + (y + z) = (z + y) + x.
Proof.
intros x y z. (* x, y, z : nat
============================
x + (y + z) = (z + y) + x *)
rewrite suma_conmutativa. (* (y + z) + x = (z + y) + x *)
rewrite (suma_conmutativa y z). (* (z + y) + x = (z + y) + x *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Nota. Indicación en (rewrite (suma_conmutativa y z)) de los
argumentos con los que se aplica, análogamente a las funciones
polimórficas.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 4.3. Demostrar que
forall {n : nat} {ns : list nat},
En n (map (fun m => m * 0) ns) ->
n = 0.
------------------------------------------------------------------ *)
(* Lema auxiliar *)
Lemma producto_n_0:
forall n : nat, n * 0 = 0.
Proof.
induction n as [|n' HI].
- (*
============================
0 * 0 = 0 *)
reflexivity.
- (* n' : nat
HI : n' * 0 = 0
============================
S n' * 0 = 0 *)
simpl. (* n' * 0 = 0 *)
apply HI.
Qed.
(* Lema auxiliar. *)
Lemma En_map_iff: forall (A B : Type) (f : A -> B) (xs : list A) (y : B),
En y (map f xs) <->
exists x, f x = y /\ En x xs.
Proof.
intros A B f xs y. (* A : Type
B : Type
f : A -> B
xs : list A
y : B
============================
En y (map f xs) <->
(exists x : A, f x = y /\ En x xs) *)
induction xs as [|x xs' HI].
- (* A : Type
B : Type
f : A -> B
y : B
============================
En y (map f [ ]) <->
(exists x : A, f x = y /\ En x [ ]) *)
simpl. (* En y (map f [ ]) <->
(exists x : A, f x = y /\ En x [ ]) *)
split.
+ (* A : Type
B : Type
f : A -> B
y : B
============================
False ->
exists x : A, f x = y /\ False *)
intros [].
+ (* A : Type
B : Type
f : A -> B
y : B
============================
(exists x : A, f x = y /\ False) ->
False *)
intros [a [H []]].
- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
============================
En y (map f (x :: xs')) <->
(exists x0 : A,
f x0 = y /\ En x0 (x :: xs')) *)
simpl. (* f x = y \/ En y (map f xs') <->
(exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs')) *)
split.
+ (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
============================
f x = y \/ En y (map f xs') ->
exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs') *)
intros [H1 | H2].
* (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
H1 : f x = y
============================
exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs') *)
exists x. (* f x = y /\ (x = x \/ En x xs') *)
split.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
H1 : f x = y
============================
f x = y *)
apply H1.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
H1 : f x = y
============================
x = x \/ En x xs' *)
left. (* x = x *)
reflexivity.
* (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
H2 : En y (map f xs')
============================
exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs') *)
apply HI in H2. (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
H2 : exists x : A, f x = y /\ En x xs'
============================
exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs') *)
destruct H2 as [a [Ha1 Ha2]]. (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha2 : En a xs'
============================
exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs') *)
exists a. (* En y (map f xs) <->
(exists x : A, f x = y /\ En x xs) *)
split.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha2 : En a xs'
============================
f a = y *)
apply Ha1.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha2 : En a xs'
============================
x = a \/ En a xs' *)
right. (* En a xs' *)
apply Ha2.
+ (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x : A,
f x = y /\ En x xs')
============================
(exists x0 : A,
f x0 = y /\ (x = x0 \/ En x0 xs')) ->
f x = y \/ En y (map f xs') *)
intros [a [Ha1 [Ha2 | Ha3]]].
* (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha2 : x = a
============================
f x = y \/ En y (map f xs') *)
left. (* f x = y *)
rewrite Ha2. (* f a = y *)
rewrite Ha1. (* y = y *)
reflexivity.
* (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha3 : En a xs'
============================
f x = y \/ En y (map f xs') *)
right. (* En y (map f xs') *)
apply HI. (* exists x0 : A, f x0 = y /\ En x0 xs' *)
exists a. (* f a = y /\ En a xs' *)
split.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha3 : En a xs'
============================
f a = y *)
apply Ha1.
-- (* A : Type
B : Type
f : A -> B
x : A
xs' : list A
y : B
HI : En y (map f xs') <->
(exists x:A, f x = y /\ En x xs')
a : A
Ha1 : f a = y
Ha3 : En a xs'
============================
En a xs' *)
apply Ha3.
Qed.
(* 1ª demostración *)
Example ej_aplicacion_de_lema_1:
forall {n : nat} {ns : list nat},
En n (map (fun m => m * 0) ns) ->
n = 0.
Proof.
intros n ns H. (* n : nat
ns : list nat
H : En n (map (fun m : nat => m * 0) ns)
============================
n = 0 *)
rewrite En_map_iff in H. (* n : nat
ns : list nat
H : exists x : nat, x * 0 = n /\ En x ns
============================
n = 0 *)
destruct H as [m [Hm _]]. (* n : nat
ns : list nat
m : nat
Hm : m * 0 = n
============================
n = 0 *)
rewrite producto_n_0 in Hm. (* n : nat
ns : list nat
m : nat
Hm : 0 = n
============================
n = 0 *)
symmetry. (* 0 = n *)
apply Hm.
Qed.
(* 2ª demostración *)
Example ej_aplicacion_de_lema:
forall {n : nat} {ns : list nat},
En n (map (fun m => m * 0) ns) ->
n = 0.
Proof.
intros n ns H. (* n : nat
ns : list nat
H : En n (map (fun m : nat => m * 0) ns)
============================
n = 0 *)
destruct (conj_e1 _ _
(En_map_iff _ _ _ _ _)
H)
as [m [Hm _]]. (* n : nat
ns : list nat
H : En n (map (fun m : nat => m * 0) ns)
m : nat
Hm : m * 0 = n
============================
n = 0 *)
rewrite producto_n_0 in Hm. (* n : nat
ns : list nat
H : En n (map (fun m : nat => m * 0) ns)
m : nat
Hm : 0 = n
============================
n = 0 *)
symmetry. (* 0 = n *)
apply Hm.
Qed.
(* ---------------------------------------------------------------------
Nota. Aplicación de teoremas a argumentos con
(conj_e1 _ _ (En_map_iff _ _ _ _ _) H)
------------------------------------------------------------------ *)
(* =====================================================================
§ 5. Coq vs. teoría de conjuntos
================================================================== *)
(* ---------------------------------------------------------------------
Notas.
1. En lugar de decir que un elemento pertenece a un conjunto se puede
decir que verifica la propiedad que define al conjunto.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 5.1. Extensionalidad funcional
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 5.1.1. Demostrar que
plus 3 = plus (pred 4).
------------------------------------------------------------------ *)
Example igualdad_de_funciones_ej1:
suma 3 = suma (pred 4).
Proof.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.1.2. Definir el axioma de extensionalidad funcional que
afirma que dos funciones son giuales cuando tienen los mismos
valores.
------------------------------------------------------------------ *)
Axiom extensionalidad_funcional : forall {X Y: Type}
{f g : X -> Y},
(forall (x:X), f x = g x) -> f = g.
(* ---------------------------------------------------------------------
Ejemplo 5.1.3. Demostrar que
(fun x => suma x 1) = (fun x => suma 1 x).
------------------------------------------------------------------ *)
Example igualdad_de_funciones_ej2 :
(fun x => suma x 1) = (fun x => suma 1 x).
Proof.
apply extensionalidad_funcional. (*
============================
forall x : nat, suma x 1 = suma 1 x *)
intros x. (* x : nat
============================
suma x 1 = suma 1 x *)
apply suma_conmutativa.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. No se puede demostrar sin el axioma.
2. Hay que ser cuidadoso en la definición de axiomas, porque se
pueden introducir inconsistencias.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 5.1.4. Calcular los axiomas usados en la prueba de
igualdad_de_funciones_ej2
------------------------------------------------------------------ *)
Print Assumptions igualdad_de_funciones_ej2.
(* ===>
Axioms:
extensionalidad_funcional :
forall (X Y : Type) (f g : X -> Y),
(forall x : X, f x = g x) -> f = g *)
(* =====================================================================
§§ 5.2. Proposiciones y booleanos
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 5.2.1. Demostrar que
forall k : nat,
esPar (doble k) = true.
------------------------------------------------------------------ *)
Theorem esPar_doble:
forall k : nat, esPar (doble k) = true.
Proof.
intros k. (* k : nat
============================
esPar (doble k) = true *)
induction k as [|k' HI].
- (*
============================
esPar (doble 0) = true *)
reflexivity.
- (* k' : nat
HI : esPar (doble k') = true
============================
esPar (doble (S k')) = true *)
simpl. (* esPar (doble k') = true *)
apply HI.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.2.2. Demostrar que
forall n : nat,
esPar n = true <-> exists k, n = doble k.
Es decir, que la computación booleana (esPar n) refleja la
proposición (exists k, n = doble k).
------------------------------------------------------------------ *)
(* Lema auxiliar. *)
Lemma esPar_doble_aux :
forall n : nat,
exists k : nat, n = if esPar n
then doble k
else S (doble k).
Proof.
induction n as [|n' HI].
- (*
============================
exists k : nat,
0 = (if esPar 0
then doble k
else S (doble k)) *)
exists 0. (* 0 = (if esPar 0
then doble 0
else S (doble 0)) *)
reflexivity.
- (* n' : nat
HI : exists k : nat,
n' = (if esPar n'
then doble k
else S (doble k))
============================
exists k : nat,
S n' = (if esPar (S n')
then doble k
else S (doble k)) *)
destruct (esPar n') eqn:H.
+ (* n' : nat
H : esPar n' = true
HI : exists k : nat, n' = doble k
============================
exists k : nat,
S n' = (if esPar (S n')
then doble k
else S (doble k)) *)
rewrite esPar_S. (* exists k : nat,
S n' = (if negacion (esPar n')
then doble k
else S (doble k)) *)
rewrite H. (* exists k : nat,
S n' = (if negacion true
then doble k
else S (doble k)) *)
simpl. (* exists k : nat, S n' = S (doble k) *)
destruct HI as [k' Hk']. (* n' : nat
H : esPar n' = true
k' : nat
Hk' : n' = doble k'
============================
exists k : nat, S n' = S (doble k) *)
exists k'. (* S n' = S (doble k') *)
rewrite Hk'. (* S (doble k') = S (doble k') *)
reflexivity.
+ (* n' : nat
H : esPar n' = false
HI : exists k : nat, n' = S (doble k)
============================
exists k : nat,
S n' = (if esPar (S n')
then doble k
else S (doble k)) *)
rewrite esPar_S. (* exists k : nat,
S n' = (if negacion (esPar n')
then doble k
else S (doble k)) *)
rewrite H. (* exists k : nat,
S n' = (if negacion false
then doble k
else S (doble k)) *)
simpl. (* exists k : nat, S n' = doble k *)
destruct HI as [k' Hk']. (* n' : nat
H : esPar n' = false
k' : nat
Hk' : n' = S (doble k')
============================
exists k : nat, S n' = doble k *)
exists (1 + k'). (* S n' = doble (1 + k') *)
rewrite Hk'. (* S (S (doble k')) = doble (1 + k') *)
reflexivity.
Qed.
Theorem esPar_bool_prop:
forall n : nat,
esPar n = true <-> exists k, n = doble k.
Proof.
intros n. (* n : nat
============================
esPar n = true <-> (exists k : nat, n = doble k) *)
split.
- (* n : nat
============================
esPar n = true -> exists k : nat, n = doble k *)
intros H. (* n : nat
H : esPar n = true
============================
exists k : nat, n = doble k *)
destruct
(esPar_doble_aux n)
as [k Hk]. (* n : nat
H : esPar n = true
k : nat
Hk : n = (if esPar n then doble k else S (doble k))
============================
exists k0 : nat, n = doble k0 *)
rewrite Hk. (* exists k0 : nat,
(if esPar n
then doble k
else S (doble k))
= doble k0 *)
rewrite H. (* exists k0 : nat, doble k = doble k0 *)
exists k. (* doble k = doble k *)
reflexivity.
- (* n : nat
============================
(exists k : nat, n = doble k) -> esPar n = true *)
intros [k Hk]. (* n, k : nat
Hk : n = doble k
============================
esPar n = true *)
rewrite Hk. (* esPar (doble k) = true *)
apply esPar_doble.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.2.3. Demostrar que
forall n m : nat,
iguales_nat n m = true <-> n = m.
------------------------------------------------------------------ *)
Theorem iguales_nat_bool_prop:
forall n m : nat,
iguales_nat n m = true <-> n = m.
Proof.
intros n m. (* n, m : nat
============================
iguales_nat n m = true <-> n = m *)
split.
- (* n, m : nat
============================
iguales_nat n m = true -> n = m *)
apply iguales_nat_true.
- (* n, m : nat
============================
n = m -> iguales_nat n m = true *)
intros H. (* n, m : nat
H : n = m
============================
iguales_nat n m = true *)
rewrite H. (* iguales_nat m m = true *)
rewrite iguales_nat_refl. (* true = true *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.2.4. Definir la función es_primo_par tal que
(es_primo_par n) es verifica si n es un primo par.
------------------------------------------------------------------ *)
(* 1º intento *)
Fail Definition es_primo_par n :=
if n = 2
then true
else false.
(* 2º intento *)
Definition es_primo_par n :=
if iguales_nat n 2
then true
else false.
(* ---------------------------------------------------------------------
Ejemplo 5.2.5.1. Demostrar que
exists k : nat, 1000 = doble k.
------------------------------------------------------------------ *)
Example esPar_1000: exists k : nat, 1000 = doble k.
Proof.
exists 500.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.2.5.2. Demostrar que
esPar 1000 = true.
------------------------------------------------------------------ *)
Example esPar_1000' : esPar 1000 = true.
Proof.
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.2.5.3. Demostrar que
exists k : nat, 1000 = doble k.
------------------------------------------------------------------ *)
Example esPar_1000'': exists k : nat, 1000 = doble k.
Proof.
apply esPar_bool_prop. (* esPar 1000 = true *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. En la proposicional se necesita proporcionar un testipo.
2. En la booleano se calcula sin testigo.
3. Se puede demostrar la proposicional usando la equivalencia con la
booleana sin necesidad de testigo.
------------------------------------------------------------------ *)
(* =====================================================================
§§ 5.3. Lógica clásica vs. constructiva
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 5.3.1. Definir la proposicion
tercio_excluso
que afirma que (forall P : Prop, P \/ ~ P).
------------------------------------------------------------------ *)
Definition tercio_excluso : Prop := forall P : Prop,
P \/ ~ P.
(* ---------------------------------------------------------------------
Nota. La proposición tercio_excluso no es demostrable en Coq.
------------------------------------------------------------------ *)
(* ---------------------------------------------------------------------
Ejemplo 5.3.2. Demostrar que
forall (P : Prop) (b : bool),
(P <-> b = true) -> P \/ ~ P.
------------------------------------------------------------------ *)
Theorem tercio_exluso_restringido :
forall (P : Prop) (b : bool),
(P <-> b = true) -> P \/ ~ P.
Proof.
intros P [] H.
- (* P : Prop
H : P <-> true = true
============================
P \/ ~ P *)
left. (* P *)
rewrite H. (* true = true *)
reflexivity.
- (* P : Prop
H : P <-> false = true
============================
P \/ ~ P *)
right. (* ~ P *)
rewrite H. (* false <> true *)
intros H1. (* H1 : false = true
============================
False *)
inversion H1.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 5.3.3. Demostrar que
forall (n m : nat),
n = m \/ n <> m.
------------------------------------------------------------------ *)
Theorem tercio_exluso_restringido_eq:
forall (n m : nat),
n = m \/ n <> m.
Proof.
intros n m. (* n, m : nat
============================
n = m \/ n <> m *)
apply (tercio_exluso_restringido
(n = m)
(iguales_nat n m)). (* n = m <-> iguales_nat n m = true *)
symmetry. (* iguales_nat n m = true <-> n = m *)
apply iguales_nat_bool_prop.
Qed.
(* ---------------------------------------------------------------------
Notas.
1. En Coq no se puede demostrar el principio del tercio exluso.
2. Las demostraciones de las fórmulas existenciales tienen que
proporcionar un testigo.
2. La lógica de Coq es constructiva.
------------------------------------------------------------------ *)
(* =====================================================================
§ Bibliografía
================================================================== *)
(*
+ "Logic in Coq" de Peirce et als. http://bit.ly/2nv1T9Z *)
