Acciones

Diferencia entre revisiones de «Tema 7: Definiciones inductivas en Coq»

De Razonamiento automático (2018-19)

(Página creada con «<source lang="coq"> (* T7: Proposiciones definidas inductivamente *) Set Warnings "-notation-overridden,-parsing". Require Export T6_Logica. Require Coq.omega.Omega. (* E…»)
 
m (Protegió «Tema 7: Definiciones inductivas en Coq» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido)))
 
(Sin diferencias)

Revisión actual del 14:08 14 feb 2019

(* T7: Proposiciones definidas inductivamente *)

Set Warnings "-notation-overridden,-parsing".
Require Export T6_Logica.
Require Coq.omega.Omega.

(* El contenido del tema es
   1. Proposiciones definidas inductivamente.
   2. Usando evidencias en demostraciones.
      1. Inversión sobre evidencias.
      2. Inducción sobre evidencias.
   3. Relaciones inductivas.
*)

(* =====================================================================
   § 1. Proposiciones definidas inductivamente. 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 1.1. Definir inductivamente la proposición
      es_par: nat -> Prop
   tal que (es_par n) expresa que n es un número par.
   ------------------------------------------------------------------ *)

Inductive es_par: nat -> Prop :=
| es_par_0  : es_par 0
| es_par_SS : forall n : nat, es_par n -> es_par (S (S n)).

(* ---------------------------------------------------------------------
   Ejemplo 1.2. Demostrar que
      es_par 4.
   ------------------------------------------------------------------ *)

(* 1ª demostración *)
Theorem es_par_4: es_par 4.
Proof.
  apply es_par_SS. (* es_par 2 *)
  apply es_par_SS. (* es_par 0 *)
  apply es_par_0.
Qed.

(* 2ª demostración *)
Theorem es_par_4': es_par 4.
Proof.
  apply (es_par_SS 2 (es_par_SS 0 es_par_0)).
Qed.

(* Nota *)
Check es_par_0.                             (* es_par 0 *)
Check es_par_SS.                            (* forall n : nat, 
                                                es_par n -> es_par (S (S n)) *)
Check (es_par_SS 0).                        (* es_par 0 -> es_par 2 *)
Check (es_par_SS 0 es_par_0).               (* es_par 2 *)
Check (es_par_SS 2).                        (* es_par 2 -> es_par 4 *)
Check (es_par_SS 2 (es_par_SS 0 es_par_0)). (* es_par 4 *)

(* ---------------------------------------------------------------------
   Ejemplo 1.3. Demostrar que
      forall n : nat, es_par n -> es_par (4 + n).
   ------------------------------------------------------------------ *)

Theorem es_par_suma4:
  forall n : nat, es_par n -> es_par (4 + n).
Proof.
  intros n.        (* n : nat
                      ============================
                      es_par n -> es_par (4 + n) *)
  simpl.           (* es_par n -> es_par (S (S (S (S n)))) *)
  intros Hn.       (* Hn : es_par n
                      ============================
                      es_par (S (S (S (S n)))) *)
  apply es_par_SS. (* es_par (S (S n)) *)
  apply es_par_SS. (* es_par n *)
  apply Hn.
Qed.

(* =====================================================================
   § 2. Usando evidencias en demostraciones 
   ================================================================== *)

(* ---------------------------------------------------------------------
   Nota. Programación y demostración en Coq son dos lados de la misma
   moneda. En programación se procesan datos y en demostración se
   procesan evidencias.  
   ------------------------------------------------------------------ *)

(* =====================================================================
   §§ 2.1. Inversión sobre evidencias
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 2.1.1. Demostrar que
      forall n : nat,
        es_par n -> es_par (pred (pred n)).
      ------------------------------------------------------------------ *)

(* 1ª demostración *)
Theorem es_par_menos_2:
  forall n : nat,
    es_par n -> es_par (pred (pred n)).
Proof.
  intros n E.               (* n : nat
                               E : es_par n
                               ============================
                               es_par (Nat.pred (Nat.pred n)) *)
  inversion E as [| n' E']. 
  -                         (* H : 0 = n
                               ============================
                               es_par (Nat.pred (Nat.pred 0)) *)
    simpl.                  (* es_par 0 *)
    apply es_par_0.
  -                         (* n' : nat
                               E' : es_par n'
                               H : S (S n') = n
                               ============================
                               es_par (Nat.pred (Nat.pred (S (S n')))) *)
    simpl.                  (* es_par n' *)
    apply E'.
Qed.

(* ---------------------------------------------------------------------
   Nota. La táctica (inversion E), donde E es la etiqueta de una
   proposición P definida inductivamente, genera para cada uno de los
   constructores de P las condiciones bajo las que se puede usar el
   constructor para demostrar P.
   ------------------------------------------------------------------ *)

(* 2ª demostración *)
Theorem es_par_menos_2':
  forall n : nat,
    es_par n -> es_par (pred (pred n)).
Proof.
  intros n E.              (* n : nat
                              E : es_par n
                              ============================
                              es_par (Nat.pred (Nat.pred n)) *)
  destruct E as [| n' E']. 
  -                        (* es_par (Nat.pred (Nat.pred 0)) *)
    simpl.                 (* es_par 0 *)
    apply es_par_0.
  -                        (* E' : es_par n'
                              ============================
                              es_par (Nat.pred (Nat.pred (S (S n')))) *)
    simpl.                 (* es_par n' *)
    apply E'.
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de destruct sobre evidencia con (destruct E as [| n' E']).
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 2.1.2. Demostrar que
      forall n : nat,
       es_par (S (S n)) -> es_par n.
   ------------------------------------------------------------------ *)

(* 1º intento *)
Theorem es_parSS_es_par:
  forall n : nat,
    es_par (S (S n)) -> es_par n.
Proof.
  intros n E.              (* n : nat
                              E : es_par (S (S n))
                              ============================
                              es_par n *)
  destruct E as [| n' E']. 
  -                        (* n : nat
                              ============================
                              es_par n *)
Abort.

(* ---------------------------------------------------------------------
   Nota. Mal funcionamiento de destruct sobre evidencias de términos
   compuestos. 
   ------------------------------------------------------------------ *)

(* 2º intento *)
Theorem es_parSS_es_par:
  forall n : nat,
    es_par (S (S n)) -> es_par n.
Proof.
  intros n E.               (* n : nat
                               E : es_par (S (S n))
                               ============================
                               es_par n *)
  inversion E as [| n' E']. (* n' : nat
                               E' : es_par n
                               H : n' = n
                               ============================
                               es_par n *)
  apply E'.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 2.1.3. Demostrar que
      ~ es_par 1.
   ------------------------------------------------------------------ *)

Theorem uno_no_es_par:
  ~ es_par 1.
Proof.
  intros H.    (* H : es_par 1
                  ============================
                  False *)
  inversion H. 
Qed.

(* ---------------------------------------------------------------------
   Nota. Uso de inversión sobre evidencia para contradicción.
   ------------------------------------------------------------------ *)

(* =====================================================================
   §§ 2.2. Inducción sobre evidencias  
   ================================================================== *)

(* ---------------------------------------------------------------------
   Ejemplo 2.2.1. Demostrar que
      forall n : nat,
        es_par n -> exists k, n = doble k.
   ------------------------------------------------------------------ *)

(* 1º intento*)
Lemma es_par_par_1:
  forall n : nat,
    es_par n -> exists k, n = doble k.
Proof.
  intros n E.               (* n : nat
                               E : es_par n
                               ============================
                               exists k : nat, n = doble k *)
  inversion E as [| n' E']. 
  -                         (* H : 0 = n
                               ============================
                               exists k : nat, 0 = doble k *)
    exists 0.                    (* 0 = doble 0 *)
    reflexivity.
  -                         (* n' : nat
                               E' : es_par n'
                               H : S (S n') = n
                               ============================
                               exists k : nat, S (S n') = doble k *)
    simpl.                  (* exists k : nat, S (S n') = doble k *)
    assert (I : (exists k', n' = doble k') ->
                (exists k, S (S n') = doble k)).
    +                       (* (exists k' : nat, n' = doble k') -> 
                               exists k : nat, S (S n') = doble k *)
      intros [k' Hk'].      (* k' : nat
                               Hk' : n' = doble k'
                               ============================
                               exists k : nat, S (S n') = doble k *)
      rewrite Hk'.          (* exists k : nat, S (S (doble k')) = doble k *)
      exists (S k').             (* S (S (doble k')) = doble (S k') *)
      reflexivity.
    +                       (* I : (exists k' : nat, n' = doble k') -> 
                                   exists k : nat, S (S n') = doble k
                               ============================
                               exists k : nat, S (S n') = doble k *)
      apply I.              (* exists k' : nat, n' = doble k' *)
Abort.

(* 2º intento *)
Lemma es_par_par:
  forall n : nat,
    es_par n -> exists k, n = doble k.
Proof.
  intros n E.                 (* n : nat
                                 E : es_par n
                                 ============================
                                 exists k : nat, n = doble k *)
  induction E as [|n' E' HI]. 
  -                           (* exists k : nat, 0 = doble k *)
    exists 0.                      (* 0 = doble 0 *)
    reflexivity.
  -                           (* n' : nat
                                 E' : es_par n'
                                 HI : exists k : nat, n' = doble k
                                 ============================
                                 exists k : nat, S (S n') = doble k *)
    destruct HI as [k' Hk'].  (* k' : nat
                                 Hk' : n' = doble k'
                                 ============================
                                 exists k : nat, S (S n') = doble k *)
    rewrite Hk'.              (* exists k : nat, S (S (doble k')) = doble k *)
    exists (S k').                 (* S (S (doble k')) = doble (S k') *)
    reflexivity.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 2.2.2. Demostrar que
      forall n : nat,
        es_par n <-> exists k, n = doble k.
   ------------------------------------------------------------------ *)


Lemma es_par_doble:
  forall n : nat, es_par (doble n).
Proof.
  induction n as [|n' HI]. 
  -                        (* es_par (doble 0) *)
    simpl.                 (* es_par 0 *)
    apply es_par_0.
  -                        (* n' : nat
                              HI : es_par (doble n')
                              ============================
                              es_par (doble (S n')) *)
    simpl.                 (* es_par (S (S (doble n'))) *)
    apply es_par_SS.       (* es_par (doble n') *)
    apply HI.
Qed.

Theorem es_par_par_syss:
  forall n : nat,
    es_par n <-> exists k, n = doble k.
Proof.
  intros n.             (* n : nat
                           ============================
                           es_par n <-> (exists k : nat, n = doble k) *)
  split.
  -                     (* es_par n -> exists k : nat, n = doble k *)
    apply es_par_par.
  -                     (* (exists k : nat, n = doble k) -> es_par n *)
    intros [k Hk].      (* n, k : nat
                           Hk : n = doble k
                           ============================
                           es_par n *)
    rewrite Hk.         (* es_par (doble k) *)
    apply es_par_doble. 
Qed.

(* =====================================================================
   § 3. Relaciones inductivas
   ================================================================== *)

(* ---------------------------------------------------------------------
   Notas.
   1. Las proposiciones con un argumento definen conjuntos; por ejemplo,
      es_par define el conjunto de los números pares.
   2. Las proposiciones con dos argumento definen relaciones.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Nota. Creamos el módulo para redefinir la relación menor o igual
   (definida por le) como menOig. 
   ------------------------------------------------------------------ *)

Module RelInd. 

(* ---------------------------------------------------------------------
   Ejemplo 3.1. Definir inductivamente la relación
      menOig: nat -> nat -> Prop
   tal que (menOig n m) expresa que n es menor o igual que m.
   ------------------------------------------------------------------ *)
  
Inductive menOig: nat -> nat -> Prop :=
  | menOig_n : forall n, menOig n n
  | menOig_S : forall n m, (menOig n m) -> (menOig n (S m)).

(* ---------------------------------------------------------------------
   Ejemplo 3.2. Definir (m <= n) como abreviatura de (menOig m n).
   ------------------------------------------------------------------ *)

Notation "m <= n" := (menOig m n).

(* ---------------------------------------------------------------------
   Nota. Sobre la relaciones (p.e. <=) se pueden usar las mismas
   tácticas que sobre las propiedades (p.e. es_par).
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 3.3. Demostrar que
      3 <= 3.
   ------------------------------------------------------------------ *)

Theorem prop_menOig1:
  3 <= 3.
Proof.
  apply menOig_n.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.4. Demostrar que
      3 <= 6.
   ------------------------------------------------------------------ *)

Theorem prop_menOig2 :
  3 <= 6.
Proof.
  apply menOig_S. (* 3 <= 5 *)
  apply menOig_S. (* 3 <= 4 *)
  apply menOig_S. (* 3 <= 3 *)
  apply menOig_n.
Qed.

(* ---------------------------------------------------------------------
   Ejemplo 3.5. Demostrar que
      (2 <= 1) -> 2 + 2 = 5.
   ------------------------------------------------------------------ *)

Theorem prop_menOig3 :
  (2 <= 1) -> 2 + 2 = 5.
Proof.
  intros H.       (* H : 2 <= 1
                     ============================
                     2 + 2 = 5 *)
  inversion H.    (* n, m : nat
                     H2 : 2 <= 0
                     H1 : n = 2
                     H0 : m = 0
                     ============================
                     2 + 2 = 5 *)
  inversion H2. 
Qed.

End RelInd.

(* ---------------------------------------------------------------------
   Nota. En lo que sigue, usaremos la predefiida le en lugar de menOig.
   ------------------------------------------------------------------ *)

(* ---------------------------------------------------------------------
   Ejemplo 3.6. Definir la relación
      mayor : nat -> nat -> Prop
   tal que (menor m n) expresa que m es menor que n.
   ------------------------------------------------------------------ *)

Definition menor (n m : nat) := le (S n) m.

(* ---------------------------------------------------------------------
   Ejemplo 3.7. Definir la abreviatura (m < n) para (menor m n).
   ------------------------------------------------------------------ *)

Notation "m < n" := (menor m n).

(* ---------------------------------------------------------------------
   Ejemplo 3.8. Definir inductivamente la relación
      cuadrado_de: nat -> nat -> Prop :=
   tal que (cuadrado x y) expresa que y es el cuadrado de x.
   ------------------------------------------------------------------ *)

Inductive cuadrado_de: nat -> nat -> Prop :=
  | cuad : forall n : nat, cuadrado_de n (n * n).

(* ---------------------------------------------------------------------
   Ejemplo 3.9. Definir inductivamente la relación
      siguiente_nat : nat -> nat -> Prop
   tal que (siguiente_nat x y) expresa que y es el siguiente de x.
   ------------------------------------------------------------------ *)

Inductive siguiente_nat : nat -> nat -> Prop :=
  | sn : forall n : nat, siguiente_nat n (S n).

(* ---------------------------------------------------------------------
   Ejemplo 3.9. Definir inductivamente la relación
      siguiente_par : nat -> nat -> Prop :=
   tal que (siguiente_par x y) expresa que y es el siguiente  número par
   de x. 
   ------------------------------------------------------------------ *)

Inductive siguiente_par : nat -> nat -> Prop :=
  | sp_1 : forall n, es_par (S n) -> siguiente_par n (S n)
  | sp_2 : forall n, es_par (S (S n)) -> siguiente_par n (S (S n)).

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

+ "Inductively defined propositions" de Peirce et als. 
  http://bit.ly/2Lejw7s *)