Acciones

Diferencia entre revisiones de «Tema 5: Tácticas básicas de Coq»

De Razonamiento automático (2018-19)

(Página creada con «<source lang="coq"> Set Warnings "-notation-overridden,-parsing". Require Export T4_PolimorfismoyOS. Require Export R2_Induccion_sol. (* El contenido del tema es 1. La…»)
 
m (Protegió «Tema 5: Tácticas básicas de Coq» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido)))
 
(Sin diferencias)

Revisión actual del 08:37 14 feb 2019

Set Warnings "-notation-overridden,-parsing".
Require Export T4_PolimorfismoyOS.
Require Export R2_Induccion_sol.

(* El contenido del tema es
   1. La táctica 'apply'
   2. La táctica 'apply ... with ...'
   3. La táctica 'inversion'
   4. Uso de tácticas sobre las hipótesis
   5. Control de la hipótesis de inducción  
   6. Expansión de definiciones 
   7. Uso de 'destruct' sobre expresiones compuestas
   8. Resumen de tácticas básicas 
*)

(* =====================================================================
   § 1. La táctica 'apply'
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 1.1. Demostrar que 
          n = m  ->
          [n;o] = [n;p] ->
          [n;o] = [m;p].
   ------------------------------------------------------------------ *)

(* Demostración sin apply *)
Theorem artificial_1a : forall (n m o p : nat),
    n = m  ->
    [n;o] = [n;p] ->
    [n;o] = [m;p].
Proof.
  intros n m o p H1 H2. (* n, m, o, p : nat
                           H1 : n = m
                           H2 : [n; o] = [n; p]
                           ============================
                           [n; o] = [m; p] *)
  rewrite <- H1.         (* [n; o] = [n; p] *)
  rewrite H2.           (* [n; p] = [n; p] *)
  reflexivity.
Qed.

(* Demostración con apply *)
Theorem artificial_1b : forall (n m o p : nat),
    n = m  ->
    [n;o] = [n;p] ->
    [n;o] = [m;p].
Proof.
  intros n m o p H1 H2. (* n, m, o, p : nat
                           H1 : n = m
                           H2 : [n; o] = [n; p]
                           ============================
                           [n; o] = [m; p] *)
  rewrite <- H1.         (* [n; o] = [n; p] *)
  apply H2.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'apply'.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 1.2. Demostrar que 
      n = m  ->
      (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
      [n;o] = [m;p].
   ------------------------------------------------------------------ *)

Theorem artificial2 : forall (n m o p : nat),
    n = m  ->
    (forall (q r : nat), q = r -> [q;o] = [r;p]) ->
    [n;o] = [m;p].
Proof.
  intros n m o p H1 H2. (* n, m, o, p : nat
                           H1 : n = m
                           H2 : forall q r : nat, q = r -> [q; o] = [r; p]
                           ============================
                           [n; o] = [m; p] *)
  apply H2.             (* n = m *)
  apply H1.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'apply' en hipótesis condicionales y
   razonamiento hacia atrás
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 1.3. Demostrar que 
      (n,n) = (m,m)  ->
      (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
      [n] = [m].
   ------------------------------------------------------------------ *)

Theorem artificial2a : forall (n m : nat),
    (n,n) = (m,m)  ->
    (forall (q r : nat), (q,q) = (r,r) -> [q] = [r]) ->
    [n] = [m].
Proof.
  intros n m H1 H2. (* n, m : nat
                       H1 : (n, n) = (m, m)
                       H2 : forall q r : nat, (q, q) = (r, r) -> [q] = [r]
                       ============================
                       [n] = [m] *)
  apply H2.         (* (n, n) = (m, m) *)
  apply H1.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 1.4. Demostrar que 
      true = iguales_nat n 5  ->
      iguales_nat (S (S n)) 7 = true.
   ------------------------------------------------------------------ *)

Theorem artificial3a: forall (n : nat),
    true = iguales_nat n 5  ->
    iguales_nat (S (S n)) 7 = true.
Proof.
  intros n H. (* n : nat
                 H : true = iguales_nat n 5
                 ============================
                 iguales_nat (S (S n)) 7 = true *)
  symmetry.   (* true = iguales_nat (S (S n)) 7 *)
  simpl.      (* true = iguales_nat n 5 *)
  apply H.
Qed.

(* ---------------------------------------------------------------------
   Nota. Necesidad de usar symmetry antes de apply.
   ------------------------------------------------------------------ *)

(* =====================================================================
   § 2. La táctica 'apply ... with ...'
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 2.1. Demostrar que
      forall (a b c d e f : nat),
       [a;b] = [c;d] ->
       [c;d] = [e;f] ->
       [a;b] = [e;f].
   ------------------------------------------------------------------ *)

Example ejemplo_con_transitiva: forall (a b c d e f : nat),
    [a;b] = [c;d] ->
    [c;d] = [e;f] ->
    [a;b] = [e;f].
Proof.
  intros a b c d e f H1 H2. (* a, b, c, d, e, f : nat
                               H1 : [a; b] = [c; d]
                               H2 : [c; d] = [e; f]
                               ============================
                               [a; b] = [e; f] *)
  rewrite -> H1.             (* [c; d] = [e; f] *)
  rewrite -> H2.             (* [e; f] = [e; f] *)
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 2.2. Demostrar que
      forall (X : Type) (n m o : X),
       n = m -> m = o -> n = o.
   ------------------------------------------------------------------ *)

Theorem igualdad_transitiva: forall (X:Type) (n m o : X),
    n = m -> m = o -> n = o.
Proof.
  intros X n m o H1 H2. (* X : Type
                           n, m, o : X
                           H1 : n = m
                           H2 : m = o
                           ============================
                           n = o *)
  rewrite -> H1.         (* m = o *)
  rewrite -> H2.         (* o = o *)
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. El ejercicio 2.2 es una generalización del 2.1, sus
   demostraciones son isomorfas y se puede usar el 2.2 en la
   demostración del 2.1.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 2.3. Demostrar que
      forall (X : Type) (n m o : X),
       n = m -> m = o -> n = o.
   ------------------------------------------------------------------ *)

(* 1ª demostración *)
Example ejemplo_con_transitiva' : forall (a b c d e f : nat),
    [a;b] = [c;d] ->
    [c;d] = [e;f] ->
    [a;b] = [e;f].
Proof.
  intros a b c d e f H1 H2.                  (* a, b, c, d, e, f : nat
                                                H1 : [a; b] = [c; d]
                                                H2 : [c; d] = [e; f]
                                                ============================
                                                [a; b] = [e; f] *)
  apply igualdad_transitiva with (m:=[c;d]).
  -                                          (* [a; b] = [c; d] *)
    apply H1.
  -                                          (* [c; d] = [e; f] *)
    apply H2.
Qed.

(* 2ª demostración *)
Example ejemplo_con_transitiva'' : forall (a b c d e f : nat),
    [a;b] = [c;d] ->
    [c;d] = [e;f] ->
    [a;b] = [e;f].
Proof.
  intros a b c d e f H1 H2.             (* a, b, c, d, e, f : nat
                                           H1 : [a; b] = [c; d]
                                           H2 : [c; d] = [e; f]
                                           ============================
                                           [a; b] = [e; f] *)
  apply igualdad_transitiva with [c;d].
  -                                     (* [a; b] = [c; d] *)
    apply H1.
  -                                     (* [c; d] = [e; f] *)
    apply H2.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'apply ... whith ...'
   ------------------------------------------------------------------ *)

(* =====================================================================
   § 3. La táctica 'inversion'
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 3.1. Demostrar que
      forall (n m : nat),
       S n = S m -> n = m.
   ------------------------------------------------------------------ *)

Theorem S_inyectiva: forall (n m : nat),
  S n = S m ->
  n = m.
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.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'inversion'
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 3.2. Demostrar que
      forall (n m o : nat),
       [n; m] = [o; o] -> [n] = [m].
   ------------------------------------------------------------------ *)

Theorem inversion_ej1: forall (n m o : nat),
    [n; m] = [o; o] ->
    [n] = [m].
Proof.
  intros n m o H. (* n, m, o : nat
                     H : [n; m] = [o; o]
                     ============================
                     [n] = [m] *)
  inversion H.    (* n, m, o : nat
                     H : [n; m] = [o; o]
                     H1 : n = o
                     H2 : m = o
                     ============================
                     [o] = [o] *)
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.3. Demostrar que
      forall (n m : nat),
       [n] = [m] ->
       n = m.
   ------------------------------------------------------------------ *)

Theorem inversion_ej2: forall (n m : nat),
    [n] = [m] ->
    n = m.
Proof.
  intros n m H.         (* n, m : nat
                           H : [n] = [m]
                           ============================
                           n = m *)
  inversion H as [Hnm]. (* n, m : nat
                           H : [n] = [m]
                           Hnm : n = m
                           ============================
                           m = m *)
  reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Nombramiento de las hipótesis generadas por inversión.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 3.4. Demostrar que
      forall n:nat,
       iguales_nat 0 n = true -> n = 0.
   ------------------------------------------------------------------ *)

Theorem iguales_nat_0_n: forall n:nat,
    iguales_nat 0 n = true -> n = 0.
Proof.
  intros n.             (* n : nat
                           ============================
                           iguales_nat 0 n = true -> n = 0 *)
  destruct n as [| n']. 
  -                     (* 
                           ============================
                           iguales_nat 0 0 = true -> 0 = 0 *)
    intros H.           (* H : iguales_nat 0 0 = true
                           ============================
                           0 = 0 *)
    reflexivity.
  -                     (* n' : nat
                           ============================
                           iguales_nat 0 (S n') = true -> S n' = 0 *)
    simpl.              (* n' : nat
                           ============================
                           false = true -> S n' = 0 *)
    intros H.           (* n' : nat
                           H : false = true
                           ============================
                           S n' = 0 *)
    inversion H.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.5. Demostrar que
      forall (n : nat),
       S n = O -> 2 + 2 = 5.
   ------------------------------------------------------------------ *)

Theorem inversion_ej4: forall (n : nat),
    S n = O ->
    2 + 2 = 5.
Proof.
  intros n H.  (* n : nat
                  H : S n = 0
                  ============================
                  2 + 2 = 5 *)
  inversion H.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.6. Demostrar que
      forall (n m : nat),
       false = true -> [n] = [m].
   ------------------------------------------------------------------ *)

Theorem inversion_ej5: forall (n m : nat),
    false = true -> [n] = [m].
Proof.
  intros n m H. (* n, m : nat
                   H : false = true
                   ============================
                   [n] = [m] *)
  inversion H.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.7. Demostrar que
      forall (A B : Type) (f: A -> B) (x y: A),
       x = y -> f x = f y.
   ------------------------------------------------------------------ *)

Theorem funcional: forall (A B : Type) (f: A -> B) (x y: A),
    x = y -> f x = f y.
Proof.
  intros A B f x y H. (* A : Type
                         B : Type
                         f : A -> B
                         x, y : A
                         H : x = y
                         ============================
                         f x = f y *)
  rewrite H.          (* f y = f y *)
  reflexivity.
Qed.

(* =====================================================================
   § 4. Uso de tácticas sobre las hipótesis
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 4.1. Demostrar que
      forall (n m : nat) (b : bool),
       iguales_nat (S n) (S m) = b  ->
       iguales_nat n m = b.
   ------------------------------------------------------------------ *)

Theorem S_inj: forall (n m : nat) (b : bool),
    iguales_nat (S n) (S m) = b  ->
    iguales_nat n m = b.
Proof.
  intros n m b H. (* n, m : nat
                     b : bool
                     H : iguales_nat (S n) (S m) = b
                     ============================
                     iguales_nat n m = b *)
  simpl in H.     (* n, m : nat
                     b : bool
                     H : iguales_nat n m = b
                     ============================
                     iguales_nat n m = b *)
  apply H.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de táctica 'simpl in ...'
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 4.1. Demostrar que
      forall (n : nat),
       (iguales_nat n 5 = true -> iguales_nat (S (S n)) 7 = true) ->
       true = iguales_nat n 5  ->
       true = iguales_nat (S (S n)) 7.
   ------------------------------------------------------------------ *)

Theorem artificial3': forall (n : nat),
  (iguales_nat n 5 = true -> iguales_nat (S (S n)) 7 = true) ->
  true = iguales_nat n 5  ->
  true = iguales_nat (S (S n)) 7.
Proof.
  intros n H1 H2. (* n : nat
                     H1 : iguales_nat n 5 = true -> 
                          iguales_nat (S (S n)) 7 = true
                     H2 : true = iguales_nat n 5
                     ============================
                     true = iguales_nat (S (S n)) 7 *)
  symmetry in H2. (* n : nat
                     H1 : iguales_nat n 5 = true -> 
                          iguales_nat (S (S n)) 7 = true
                     H2 : iguales_nat n 5 = true
                     ============================
                     true = iguales_nat (S (S n)) 7 *)
  apply H1 in H2. (* n : nat
                     H1 : iguales_nat n 5 = true -> 
                          iguales_nat (S (S n)) 7 = true
                     H2 : iguales_nat (S (S n)) 7 = true
                     ============================
                     true = iguales_nat (S (S n)) 7 *)
  symmetry in H2. (* n : nat
                     H1 : iguales_nat n 5 = true -> 
                          iguales_nat (S (S n)) 7 = true
                     H2 : true = iguales_nat (S (S n)) 7
                     ============================
                     true = iguales_nat (S (S n)) 7 *)
  apply H2.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de las tácticas 'apply H1 in H2' y 'symmetry in H'.
   ------------------------------------------------------------------ *)

(* =====================================================================
   § 5. Control de la hipótesis de inducción  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 5.1. Demostrar que
      forall n m : nat,
       doble n = doble m -> n = m.
   ------------------------------------------------------------------ *)

(* 1ª intento *)
Theorem doble_inyectiva_fallado : forall n m : nat,
    doble n = doble m ->
    n = m.
Proof.
  intros n m.             (* n, m : nat
                             ============================
                             doble n = doble m -> n = m *)
  induction n as [| n' HI].
  -                       (* m : nat
                             ============================
                             doble 0 = doble m -> 0 = m *)
    simpl.                (* m : nat
                             ============================
                             0 = doble m -> 0 = m *)
    intros H.             (* m : nat
                             H : 0 = doble m
                             ============================
                             0 = m *)
    destruct m as [| m']. 
    +                     (* H : 0 = doble 0
                             ============================
                             0 = 0 *)
      reflexivity.
    +                     (* m' : nat
                             H : 0 = doble (S m')
                             ============================
                             0 = S m' *)
      inversion H.
  -                       (* n', m : nat
                             HI : doble n' = doble m -> n' = m
                             ============================
                             doble (S n') = doble m -> S n' = m *)
    intros H.             (* n', m : nat
                             HI : doble n' = doble m -> n' = m
                             H : doble (S n') = doble m
                             ============================
                             S n' = m *)
    destruct m as [| m'].
    +                     (* n' : nat
                             HI : doble n' = doble 0 -> n' = 0
                             H : doble (S n') = doble 0
                             ============================
                             S n' = 0 *)
      simpl in H.         (* n' : nat
                             HI : doble n' = doble 0 -> n' = 0
                             H : S (S (doble n')) = 0
                             ============================
                             S n' = 0 *)
      inversion H.
    +                     (* n', m' : nat
                             HI : doble n' = doble (S m') -> n' = S m'
                             H : doble (S n') = doble (S m')
                             ============================
                             S n' = S m' *)
      apply funcional.    (* n', m' : nat
                             HI : doble n' = doble (S m') -> n' = S m'
                             H : doble (S n') = doble (S m')
                             ============================
                             n' = m' *)
      Abort.

(* 2º intento *)
Theorem doble_inyectiva: forall n m,
    doble n = doble m ->
    n = m.
Proof.
  intros n.               (* n : nat
                             ============================
                             forall m : nat, doble n = doble m -> n = m *)
  induction n as [| n' HI].
  -                       (* 
                             ============================
                             forall m : nat, doble 0 = doble m -> 0 = m *)
    simpl.                (* forall m : nat, 0 = doble m -> 0 = m *)
    intros m H.           (* m : nat
                             H : 0 = doble m
                             ============================
                             0 = m *)
    destruct m as [| m'].
    +                     (* H : 0 = doble 0
                             ============================
                             0 = 0 *)
      reflexivity.
    +                     (* m' : nat
                             H : 0 = doble (S m')
                             ============================
                             0 = S m' *)
      inversion H.
  -                       (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             ============================
                             forall m : nat, doble (S n') = doble m 
                                             -> S n' = m *)
    simpl.                (* forall m : nat, S (S (doble n')) = doble m 
                                             -> S n' = m *)
    intros m H.           (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             m : nat
                             H : S (S (doble n')) = doble m
                             ============================
                             S n' = m *)
    destruct m as [| m']. 
    +                     (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             H : S (S (doble n')) = doble 0
                             ============================
                             S n' = 0 *)
      simpl in H.         (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             H : S (S (doble n')) = 0
                             ============================
                             S n' = 0 *)
      inversion H.
    +                     (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             m' : nat
                             H : S (S (doble n')) = doble (S m')
                             ============================
                             S n' = S m' *)
      apply funcional.    (* n' = m' *)
      apply HI.           (* doble n' = doble m' *)
      inversion H.        (* n' : nat
                             HI : forall m : nat, doble n' = doble m -> n' = m
                             m' : nat
                             H : S (S (doble n')) = doble (S m')
                             H1 : doble n' = doble m'
                             ============================
                             doble n' = doble n' *)
      reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la estrategia de generalización.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 5.2. Demostrar que
      forall n m : nat,
       doble n = doble m ->
       n = m.
   ------------------------------------------------------------------ *)

(* 1º intento *)
Theorem doble_inyectiva_2a: forall n m : nat,
    doble n = doble m ->
    n = m.
Proof.
  intros n m.                   (* n, m : nat
                                   ============================
                                   doble n = doble m -> n = m *)
  induction m as [| m' HI].
  -                             (* n : nat
                                   ============================
                                   doble n = doble 0 -> n = 0 *)
    simpl.                      (* doble n = 0 -> n = 0 *)
    intros H.                   (* n : nat
                                   H : doble n = 0
                                   ============================
                                   n = 0 *)
    destruct n as [| n'].
    +                           (* H : doble 0 = 0
                                   ============================
                                   0 = 0 *)
      reflexivity.
    +                           (* n' : nat
                                   H : doble (S n') = 0
                                   ============================
                                   S n' = 0 *)
      simpl in H.               (* n' : nat
                                   H : S (S (doble n')) = 0
                                   ============================
                                   S n' = 0 *)
      inversion H.
  -                             (* n, m' : nat
                                   HI : doble n = doble m' -> n = m'
                                   ============================
                                   doble n = doble (S m') -> n = S m' *)

    intros H.                   (* n, m' : nat
                                   HI : doble n = doble m' -> n = m'
                                   H : doble n = doble (S m')
                                   ============================
                                   n = S m' *)
    destruct n as [| n']. 
    +                           (* m' : nat
                                   HI : doble 0 = doble m' -> 0 = m'
                                   H : doble 0 = doble (S m')
                                   ============================
                                   0 = S m' *)
      simpl in H.               (* m' : nat
                                   HI : doble 0 = doble m' -> 0 = m'
                                   H : 0 = S (S (doble m'))
                                   ============================
                                   0 = S m' *)
      inversion H.
    +                           (* n', m' : nat
                                   HI : doble (S n') = doble m' -> S n' = m'
                                   H : doble (S n') = doble (S m')
                                   ============================
                                   S n' = S m' *)
      apply funcional.          (* n' = m' *)
Abort.

(* 2º intento *)
Theorem doble_inyectiva_2 : forall n m,
    doble n = doble m ->
    n = m.
Proof.
  intros n m.               (* n, m : nat
                               ============================
                               doble n = doble m -> n = m *)
  generalize dependent n.   (* m : nat
                               ============================
                               forall n : nat, doble n = doble m -> n = m *)
  induction m as [| m' HI]. 
  -                         (*  
                               ============================
                               forall n : nat, doble n = doble 0 -> n = 0 *)
    simpl.                  (* forall n : nat, doble n = 0 -> n = 0 *)
    intros n H.             (* n : nat
                               H : doble n = 0
                               ============================
                               n = 0 *)
    destruct n as [| n'].
    +                       (* H : doble 0 = 0
                               ============================
                               0 = 0 *)
      reflexivity.
    +                       (* n' : nat
                               H : doble (S n') = 0
                               ============================
                               S n' = 0 *)
      simpl in H.           (* n' : nat
                               H : S (S (doble n')) = 0
                               ============================
                               S n' = 0 *)
      inversion H.
  -                         (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               ============================
                               forall n : nat, doble n = doble (S m') 
                                               -> n = S m' *)
    intros n H.             (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               n : nat
                               H : doble n = doble (S m')
                               ============================
                               n = S m' *)
    destruct n as [| n']. 
    +                       (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               H : doble 0 = doble (S m')
                               ============================
                               0 = S m' *)
      simpl in H.           (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               H : 0 = S (S (doble m'))
                               ============================
                               0 = S m' *)
      inversion H.
    +                       (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               n' : nat
                               H : doble (S n') = doble (S m')
                               ============================
                               S n' = S m' *)
      apply funcional.      (* n' = m' *)
      apply HI.             (* doble n' = doble m' *)
      simpl in H.           (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               n' : nat
                               H : S (S (doble n')) = S (S (doble m'))
                               ============================
                               doble n' = doble m' *)
      inversion H.          (* m' : nat
                               HI : forall n : nat, doble n = doble m' -> n = m'
                               n' : nat
                               H : S (S (doble n')) = S (S (doble m'))
                               H1 : doble n' = doble m'
                               ============================
                               doble n' = doble n' *)
      reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'generalize dependent n'.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 5.3. Demostrar que
      forall n m : nat,
        iguales_nat n m = true -> n = m.
   ------------------------------------------------------------------ *)

Theorem iguales_nat_true : forall n m : nat,
    iguales_nat n m = true -> n = m.
Proof.
  induction n as [|n' HIn'].
  -                             (* 
                                   ============================
                                   forall m : nat, iguales_nat 0 m = true 
                                              -> 0 = m *)
    induction m as [|m' HIm'].
    +                           (* 
                                   ============================
                                   iguales_nat 0 0 = true -> 0 = 0 *)
      reflexivity.
    +                           (* m' : nat
                                   HIm' : iguales_nat 0 m' = true -> 0 = m'
                                   ============================
                                   iguales_nat 0 (S m') = true -> 0 = S m' *)
      simpl.                    (* false = true -> 0 = S m' *)
      intros H.                 (* m' : nat
                                   HIm' : iguales_nat 0 m' = true -> 0 = m'
                                   H : false = true
                                   ============================
                                   0 = S m' *)
      inversion H.
  -                             (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                         -> n' = m
                                   ============================
                                   forall m : nat, iguales_nat (S n') m = true
                                                   -> S n' = m *)
    induction m as [|m' HIm'].
    +                           (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                         -> n' = m
                                   ============================
                                   iguales_nat (S n') 0 = true -> S n' = 0 *)
      simpl.                    (* false = true -> S n' = 0 *)
      intros H.                 (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                        -> n' = m
                                   H : false = true
                                   ============================
                                   S n' = 0 *)
      inversion H.
    +                           (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                         -> n' = m
                                   m' : nat
                                   HIm' : iguales_nat (S n') m' = true 
                                          -> S n' = m'
                                   ============================
                                   iguales_nat (S n') (S m') = true 
                                   -> S n' = S m' *)
      simpl.                    (* iguales_nat n' m' = true -> S n' = S m' *)
      intros H.                 (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                         -> n' = m
                                   m' : nat
                                   HIm' : iguales_nat (S n') m' = true 
                                          -> S n' = m'
                                   H : iguales_nat n' m' = true
                                   ============================
                                   S n' = S m' *)
      apply HIn' in H.          (* n' : nat
                                   HIn' : forall m:nat, iguales_nat n' m = true
                                                         -> n' = m
                                   m' : nat
                                   HIm' : iguales_nat (S n') m' = true 
                                          -> S n' = m'
                                   H : n' = m'
                                   ============================
                                   S n' = S m' *)
      rewrite H.                (* S m' = S m' *)
      reflexivity.
Qed.
    
(* ---------------------------------------------------------------------
   Ejemplo 5.3. Demostrar que
      forall x y : id,
       iguales_id x y = true -> x = y.
   ------------------------------------------------------------------ *)

Theorem iguales_id_true: forall x y : id,
  iguales_id x y = true -> x = y.
Proof.
  intros [m] [n].           (* m, n : nat
                               ============================
                               iguales_id (Id m) (Id n) = true -> Id m = Id n *)
  simpl.                    (* iguales_nat m n = true -> Id m = Id n *)
  intros H.                 (* m, n : nat
                               H : iguales_nat m n = true
                               ============================
                               Id m = Id n *)
  assert (H' : m = n).
  -                         (* m, n : nat
                               H : iguales_nat m n = true
                               ============================
                               m = n *)
    apply iguales_nat_true. (* iguales_nat m n = true *)
    apply H. 
  -                         (* m, n : nat
                               H : iguales_nat m n = true
                               H' : m = n
                               ============================
                               Id m = Id n *)
    rewrite H'.             (* Id n = Id n *)
    reflexivity.
Qed.

(* =====================================================================
   § 6. Expansión de definiciones 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 6.1. Definir la función
      cuadrado : nata -> nat
   tal que (cuadrado n) es el cuadrado de n.
   ------------------------------------------------------------------ *)

Definition cuadrado (n:nat) : nat := n * n.

(* ---------------------------------------------------------------------
   Ejemplo 6.2. Demostrar que
      forall n m : nat,
       cuadrado (n * m) = cuadrado n * cuadrado m.
   ------------------------------------------------------------------ *)

Lemma cuadrado_mult : forall n m : nat,
    cuadrado (n * m) = cuadrado n * cuadrado m.
Proof.
  intros n m.                            (* n, m : nat
                                            ============================
                                            cuadrado (n * m) = 
                                            cuadrado n * cuadrado m *)
  unfold cuadrado.                       (* (n * m) * (n * m) = 
                                            (n * n) * (m * m) *)
  rewrite producto_asociativa.           (* ((n * m) * n) * m = 
                                            (n * n) * (m * m) *)
  assert (H : (n * m) * n = (n * n) * m). 
  -                                      (* (n * m) * n = (n * n) * m) *)
    rewrite producto_conmutativa.        (* n * (n * m) = (n * n) * m *)
    apply producto_asociativa.           
  -                                      (* n, m : nat
                                            H : (n * m) * n = (n * n) * m
                                            ============================
                                            ((n * m) * n) * m = 
                                            (n * n) * (m * m) *)
    rewrite H.                           (* ((n * n) * m) * m = 
                                            (n * n) * (m * m) *)
    rewrite producto_asociativa.         (* ((n * n) * m) * m = 
                                            ((n * n) * m) * m *)
    reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'unfold'
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 6.4. Definir la función
      const5 : nat -> nat
   tal que (const5 x) es el número 5.
   ------------------------------------------------------------------ *)

Definition const5 (x: nat) : nat := 5.

(* ---------------------------------------------------------------------
   Ejemplo 6.5. Demostrar que
      forall m : nat,
       const5 m + 1 = const5 (m + 1) + 1.
   ------------------------------------------------------------------ *)

Fact prop_const5 : forall m : nat,
    const5 m + 1 = const5 (m + 1) + 1.
Proof.
  intros m.    (* m : nat
                  ============================
                  const5 m + 1 = const5 (m + 1) + 1 *)
  simpl.       (* 6 = 6 *)
  reflexivity. 
Qed.

(* ---------------------------------------------------------------------
   Nota. Expansión automática de la definición de const5.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 6.6. Se coonsidera la siguiente definición
      Definition const5b (x:nat) : nat :=
        match x with
        | O   => 5
        | S _ => 5
        end.

   Demostrar que
      forall m : nat,
       const5b m + 1 = const5b (m + 1) + 1.
   ------------------------------------------------------------------ *)

Definition const5b (x:nat) : nat :=
  match x with
  | O   => 5
  | S _ => 5
  end.

(* 1º intento *)
Fact prop_const5b_1: forall m : nat,
    const5b m + 1 = const5b (m + 1) + 1.
Proof.
  intros m. (* m : nat
               ============================
               const5b m + 1 = const5b (m + 1) + 1 *)
  simpl.    (* const5b m + 1 = const5b (m + 1) + 1 *)
Abort.

(* 1ª demostración *)
Fact prop_const5b_2: forall m : nat,
    const5b m + 1 = const5b (m + 1) + 1.
Proof.
  intros m.      (* m : nat
                    ============================
                    const5b m + 1 = const5b (m + 1) + 1 *)
  destruct m.
  -              (* 
                    ============================
                    const5b 0 + 1 = const5b (0 + 1) + 1 *)
    simpl.       (* 6 = 6 *)
    reflexivity. 
  -              (* m : nat
                    ============================
                    const5b (S m) + 1 = const5b (S m + 1) + 1 *)
    simpl.       (* 6 = 6 *)
    reflexivity.
Qed.

(* 2ª demostración *)
Fact prop_const5b_3: forall m : nat,
    const5b m + 1 = const5b (m + 1) + 1.
Proof.
  intros m.       (* m : nat
                     ============================
                     const5b m + 1 = const5b (m + 1) + 1 *)
  unfold const5b. (* m : nat
                     ============================
                     match m with
                     | 0 | _ => 5
                     end + 1 = match m + 1 with
                               | 0 | _ => 5
                               end + 1 *)
  destruct m.
  -               (* 
                     ============================
                     5 + 1 = match 0 + 1 with
                             | 0 | _ => 5
                             end + 1 *)
    reflexivity.
  -               (* m : nat
                     ============================
                     5 + 1 = match S m + 1 with
                             | 0 | _ => 5
                             end + 1 *)
    reflexivity.
Qed.

(* =====================================================================
   § 7. Uso de 'destruct' sobre expresiones compuestas
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 7.1. Se considera la siguiente definición 
      Definition const_false (n : nat) : bool :=
        if      iguales_nat n 3 then false
        else if iguales_nat n 5 then false
        else                         false.

   Demostrar que
      forall n : nat,
       const_false n = false.
   ------------------------------------------------------------------ *)

Definition const_false (n : nat) : bool :=
  if      iguales_nat n 3 then false
  else if iguales_nat n 5 then false
  else                         false.

Theorem const_false_false : forall n : nat,
    const_false n = false.
Proof.
  intros n.                     (* n : nat
                                   ============================
                                   const_false n = false *)
  unfold const_false.           (* (if iguales_nat n 3 then false 
                                   else if iguales_nat n 5 then false 
                                   else false) =
                                   false *)
  destruct (iguales_nat n 3).
  -                             (* n : nat
                                   ============================
                                   false = false *)
    reflexivity.
  -                             (* n : nat
                                   ============================
                                   (if iguales_nat n 5 then false 
                                   else false) = false *)
    destruct (iguales_nat n 5). 
    +                           (* n : nat
                                   ============================
                                   false = false *)
      reflexivity.
    +                           (* n : nat
                                   ============================
                                   false = false *)
      reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 7.2. Se considera la siguiente definición 
      Definition ej (n : nat) : bool :=
        if      iguales_nat n 3 then true
        else if iguales_nat n 5 then true
        else                     false.

   Demostrar que
      forall n : nat,
       ej n = true -> esImpar n = true.
   ------------------------------------------------------------------ *)

Definition ej (n : nat) : bool :=
  if      iguales_nat n 3 then true
  else if iguales_nat n 5 then true
  else                     false.

(* 1º intento *)
Theorem ej_impar_a: forall n : nat,
    ej n = true ->
    esImpar n = true.
Proof.
  intros n H.                       (* n : nat
                                       H : ej n = true
                                       ============================
                                       esImpar n = true *)
  unfold ej in H. (* n : nat
                                      H : (if iguales_nat n 3
                                           then true
                                           else if iguales_nat n 5 
                                                then true 
                                                else false) 
                                          = true
                                      ============================
                                      esImpar n = true *)
  destruct (iguales_nat n 3).
  -                                (* n : nat
                                      H : true = true
                                      ============================
                                      esImpar n = true *)
Abort.

(* 2º intento *)
Theorem ej_impar : forall n : nat,
    ej n = true ->
    esImpar n = true.
Proof.
  intros n H.                             (* n : nat
                                             H : ej n = true
                                             ============================
                                             esImpar n = true *)
  unfold ej in H.                         (* n : nat
                                             H : (if iguales_nat n 3
                                                  then true
                                                  else if iguales_nat n 5 
                                                       then true else false) 
                                                 = true
                                             ============================
                                             esImpar n = true *)
  destruct (iguales_nat n 3) eqn: H3.
  -                                       (* n : nat
                                             H3 : iguales_nat n 3 = true
                                             H : true = true
                                             ============================
                                             esImpar n = true *)
    apply iguales_nat_true in H3.         (* n : nat
                                             H3 : n = 3
                                             H : true = true
                                             ============================
                                             esImpar n = true *)
    rewrite H3.                           (* esImpar 3 = true *)
    reflexivity.
  -                                       (* n : nat
                                             H3 : iguales_nat n 3 = false
                                             H : (if iguales_nat n 5 
                                                  then true else false) 
                                                 = true
                                             ============================
                                             esImpar n = true *)
    destruct (iguales_nat n 5) eqn:H5. 
    +                                     (* n : nat
                                             H3 : iguales_nat n 3 = false
                                             H5 : iguales_nat n 5 = true
                                             H : true = true
                                             ============================
                                             esImpar n = true *)
      apply iguales_nat_true in H5.       (* n : nat
                                             H3 : iguales_nat n 3 = false
                                             H5 : n = 5
                                             H : true = true
                                             ============================
                                             esImpar n = true *)
      rewrite H5.                         (* esImpar 5 = true *)
      reflexivity.
    +                                     (* n : nat
                                             H3 : iguales_nat n 3 = false
                                             H5 : iguales_nat n 5 = false
                                             H : false = true
                                             ============================
                                             esImpar n = true *)
      inversion H.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de la táctica 'destruct e eqn: H'.
   ------------------------------------------------------------------ *)

(* =====================================================================
   § 8. Resumen de tácticas básicas 
   ================================================================== *)

(* Las tácticas básicas utilizadas hasta ahora son
  + apply H: 
    + si el objetivo coincide con la hipótesis H, lo demuestra;
    + si H es una implicación,
      + si el objetivo coincide con la conclusión de H, lo sustituye por
        su premisa y
      + si el objetivo coincide con la premisa de H, lo sustituye por
        su conclusión.

  + apply ... with ...: Especifica los valores de las variables que no
    se pueden deducir por emparejamiento.

  + apply H1 in H2: Aplica la igualdad de la hipótesis H1 a la
    hipótesis H2.

  + assert (H: P): Incluye la demostración de la propiedad P y continúa
    la demostración añadiendo como premisa la propiedad P con nombre H. 

  + destruct b: Distingue dos casos según que b sea True o False.

  + destruct n as [| n1]: Distingue dos casos según que n sea 0 o sea S n1. 

  + destruct p as [n m]: Sustituye el par p por (n,m).

  + destruct e eqn: H: Distingue casos según el valor de la expresión
    e y lo añade al contexto la hipótesis H.

  + generalize dependent x: Mueve la variable x (y las que dependan de
    ella) del contexto a una hipótesis explícita en el objetivo.

  + induction n as [|n1 IHn1]: Inicia una demostración por inducción
    sobre n. El caso base en ~n  0~. El paso de la inducción consiste en
    suponer la propiedad para ~n1~ y demostrarla para ~S n1~. El nombre de la
    hipótesis de inducción es ~IHn1~.

  + intros vars: Introduce las variables del cuantificador universal y,
    como premisas, los antecedentes de las implicaciones.

  + inversion: Aplica que los constructores son disjuntos e inyectivos. 

  + reflexivity: Demuestra el objetivo si es una igualdad trivial.

  + rewrite H: Sustituye el término izquierdo de H por el derecho.

  + rewrite <-H: Sustituye el término derecho de H por el izquierdo.

  + simpl: Simplifica el objetivo.

  + simpl in H: Simplifica la hipótesis H.

  + symmetry: Cambia un objetivo de la forma s = t en t = s.

  + symmetry in H: Cambia la hipótesis H de la forma ~st~ en ~ts~.

  + unfold f: Expande la definición de la función f.
 *)

(* =====================================================================
   § Bibliografía
   ================================================================== *)

(*
 + "More Basic Tactics" de Peirce et als. http://bit.ly/2LYFTlZ *)