Require Export T1_PF_en_Coq.
(* El contenido de la teoría es
1. Demostraciones por inducción.
2. Demostraciones anidadas.
3. Demostraciones formales vs demostraciones informales.
4. Ejercicios complementarios *)
(* =====================================================================
§ 1. Demostraciones por inducción
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 1.1. Demostrar que
forall n:nat, n = n + 0.
------------------------------------------------------------------ *)
(* 1º intento: con métodos elementales *)
Theorem suma_n_0_a: forall n : nat, n = n + 0.
Proof.
intros n. (* n : nat
============================
n = n + 0 *)
simpl. (* n : nat
============================
n = n + 0 *)
Abort.
(* 2º intento: con casos *)
Theorem suma_n_0_b : forall n : nat,
n = n + 0.
Proof.
intros n. (* n : nat
============================
n = n + 0 *)
destruct n as [| n'].
- (*
============================
0 = 0 + 0 *)
reflexivity.
- (* n' : nat
============================
S n' = S n' + 0 *)
simpl. (* n' : nat
============================
S n' = S (n' + 0) *)
Abort.
(* 3ª intento: con inducción *)
Theorem suma_n_0 : forall n : nat,
n = n + 0.
Proof.
intros n. (* n : nat
============================
n = n + 0 *)
induction n as [| n' IHn'].
+ (*
============================
0 = 0 + 0 *)
reflexivity.
+ (* n' : nat
IHn' : n' = n' + 0
============================
S n' = S n' + 0 *)
simpl. (* S n' = S (n' + 0) *)
rewrite <- IHn'. (* S n' = S n' *)
reflexivity.
Qed.
(* ---------------------------------------------------------------------
Ejemplo 1.2. Demostrar que
forall n, n - n = 0.
------------------------------------------------------------------ *)
Theorem resta_n_n: forall n : nat, n - n = 0.
Proof.
intros n. (* n : nat
============================
n - n = 0 *)
induction n as [| n' IHn'].
+ (*
============================
0 - 0 = 0 *)
reflexivity.
+ (* n' : nat
IHn' : n' - n' = 0
============================
S n' - S n' = 0 *)
simpl. (* n' - n' = 0 *)
rewrite IHn'. (* 0 = 0 *)
reflexivity.
Qed.
(* =====================================================================
§ 2. Demostraciones anidadas
================================================================== *)
(* ---------------------------------------------------------------------
Ejemplo 2.1. Demostrar que
forall n m : nat, (0 + n) * m = n * m.
------------------------------------------------------------------ *)
Theorem producto_0_suma': forall n m : nat, (0 + n) * m = n * m.
Proof.
intros n m. (* n, m : nat
============================
(0 + n) * m = n * m *)
assert (H: 0 + n = n).
- (* n, m : nat
============================
0 + n = n *)
reflexivity.
- (* n, m : nat
H : 0 + n = n
============================
(0 + n) * m = n * m *)
rewrite -> H. (* n * m = n * m *)
reflexivity.
Qed.
(* =====================================================================
§ Bibliografía
================================================================== *)
(*
+ "Demostraciones por inducción" de Peirce et als. http://bit.ly/2NRSWTF
*)
