Menu Close

LMF2019: Definiciones inductivas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir en Isabelle/HOL conjuntos y relaciones inductivas y cómo demostrar sus propiedades.

La clase se ha dado mediante videoconferencia y el vídeo correspondiente es

La teoría con los ejemplos presentados en la clase es la siguiente:

chapter ‹Tema 9: Definiciones inductivas›
 
theory T9_Definiciones_inductivas
imports Main
begin
 
section ‹Definición inductiva del conjunto de los números pares›
 
text ‹
  · El conjunto de los números pares se define inductivamente como el
    menor conjunto que contiene al 0 y es cerrado por la operación (+2).
 
  · El conjunto de los números pares también puede definirse como los 
    naturales divisible por 2.
 
  · Veremos cómo se escriben las dos definiciones en Isabelle/HOL y cómo
    se demuestra su equivalencia.›
 
inductive_set par :: "nat set" where
  cero: "0 ∈ par" 
| paso: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
 
text ‹La definición inductiva genera varios teoremas:
   · par.cero:   0 ∈ par
   · par.paso:   n ∈ par ⟹ Suc (Suc n) ∈ par
   · par.simps:  (a ∈ par) = (a = 0(∃n. a = Suc (Suc n) ∧ n ∈ par))
›
 
thm par.cero
thm par.paso
thm par.simps
 
subsection ‹Uso de las reglas de introducción›
 
text ‹Lema: Los números de la forma 2*k son pares.›
 
― ‹La demostración aplicativa es›
lemma dobles_son_pares: 
  "2*k ∈ par"
  apply (induct k) 
     (* 1. 2 * 0 ∈ par
        2. ⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par *)
   apply (simp add: par.cero)
     (* ⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par *)
  apply (simp add: par.paso)
  done
 
― ‹La demostración automática es›
lemma dobles_son_pares_2: 
  "2*k ∈ par"
  by (induct k) (simp_all add: par.cero par.paso)
 
― ‹La demostración estructurada es›
lemma dobles_son_pares_3:
  "2*k ∈ par"
proof (induct k)
  show "2 * 0 ∈ par" 
    by (simp add: par.cero)
next
  show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" 
    by (simp add: par.paso)
qed
 
― ‹La demostración detallada es›
lemma dobles_son_pares_4:
  "2*k ∈ par"
proof (induct k) 
  have "2 * 0 = (0::nat)"
    by (simp only: mult_0_right)
  then show "2 * 0 ∈ par"
    by (simp only: par.cero)
next
  fix k :: "nat" 
  assume "2 * k ∈ par" 
  have "2 * Suc k = Suc (Suc (2 * k))" 
  proof -
    have "2 * Suc k = 2 + 2 * k"
      by (simp only: mult_Suc_right)
    also have "… = Suc (Suc (2 * k))"
      by (simp only: add_2_eq_Suc)
    finally show "2 * Suc k = Suc (Suc (2 * k))"
      by this
  qed
  then show "2 * Suc k ∈ par"
    using2 * k ∈ par›
    by (simp only: par.paso)
qed
 
text ‹Nota: Nuestro objetivo es demostrar la equivalencia de la 
  definición anterior y la definición mediante divisibilidad (even).
 
  Lema: Si n es divisible por 2, entonces es par.›
 
― ‹La demostración declarativa detallada es›
lemma "even n ⟹ n ∈ par" 
proof -
  assume "even n"
  then have "∃k. n = 2*k"
    by (simp only: dvd_def)
  then obtain k where "n = 2*k"
    by (rule exE)
  then show "n ∈ par"
    by (simp only: dobles_son_pares)
qed
 
― ‹La demostación automática es›
lemma even_imp_par: "even n ⟹ n ∈ par"
  by (auto simp only: dobles_son_pares)
 
subsection ‹Regla de inducción› 
 
text ‹Entre las reglas generadas por la definión de par está la de
  inducción:
  · par.induct: ⟦ x ∈ par; 
                 P 0; 
                 ⋀n. ⟦n ∈ par; P n⟧ ⟹ P (Suc (Suc n))⟧ 
                ⟹ P x
›
 
thm par.induct
 
text ‹Lema: Los números pares son divisibles por 2.› 
 
― ‹Demostración aplicativa›
lemma par_imp_even: 
  "n ∈ par ⟹ even n"
  apply (induction rule: par.induct)
     (* 1. even 0
        2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
   apply (simp only: dvd_def)
     (* 1. ∃k. 0 = 2 * k
        2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
   apply (rule_tac x=0 in exI)
     (* 1. 0 = 2 * 0
        2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
   apply simp
     (* ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
  apply (simp only: dvd_def)
     (* ⋀n. ⟦n ∈ par; ∃k. n = 2 * k⟧ ⟹ ∃k. Suc (Suc n) = 2 * k *)
  apply (erule exE)
     (* ⋀n k. ⟦n ∈ par; n = 2 * k⟧ ⟹ ∃k. Suc (Suc n) = 2 * k*)
  apply (rule_tac x="k+1" in exI)
     (* ⋀n k. ⟦n ∈ par; n = 2 * k⟧ ⟹ Suc (Suc n) = 2 * (k + 1) *)
  apply simp
     (* *)
  done
 
― ‹2ª demostración aplicativa›
lemma par_imp_even_2: 
  "n ∈ par ⟹ even n"
  apply (induction rule: par.induct)
     (* 1. even 0
        2. ⋀n. ⟦n ∈ par; even n⟧ ⟹ even (Suc (Suc n)) *)
   apply simp_all
     (* *)
  done
 
― ‹Demostración automática›
lemma par_imp_even_3: 
  "n ∈ par ⟹ even n"
  by (induction rule: par.induct) simp_all
 
― ‹2ª demostración declarativa›
lemma par_imp_even_4: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even 0" 
    by simp
next
  fix n :: nat
  assume H1: "n ∈ par" and
         H2: "even n"
  then show "even (Suc (Suc n))" 
    by simp
qed
 
― ‹Demostración declarativa detallada›
lemma par_imp_even_5: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even 0" 
    by (simp only: even_zero)
next
  fix n :: nat
  assume H1: "n ∈ par" and
         H2: "even n"
  have "∃k. n = 2*k" 
    using H2 by (simp only: dvd_def)
  then obtain k where "n = 2*k" 
    by (rule exE)
  then have "Suc (Suc n) = 2*(k+1)" 
  proof -
    have "Suc (Suc n) = 2 + n"
      by (simp only: add_2_eq_Suc)
    also have "… = 2 + 2 * k"
      by (simp only: ‹n = 2 * k›)
    also have "… = 2 * Suc k"
      by (simp only: mult_Suc_right)
    also have "… = 2 * (k + 1)"
      by (simp only: Suc_eq_plus1)
    finally show "Suc (Suc n) = 2*(k+1)"
      by this
  qed
  then have "∃k. Suc (Suc n) = 2*k" 
    by (rule exI)
  then show "even (Suc (Suc n))" 
    by (simp only: dvd_def)
qed
 
text ‹Lema: Un número n es par syss es divisible por 2.›
 
― ‹La demostración detallada es›
theorem par_iff_even: "(n ∈ par) = (even n)" 
proof (rule iffI)
  show "n ∈ par ⟹ even n"
    by (rule par_imp_even)
next
  show "even n ⟹ n ∈ par"
    by (rule even_imp_par)
qed
 
― ‹La demostración automática es›
theorem par_iff_even_2: "(n ∈ par) = (even n)"
  by (auto simp only: par_imp_even even_imp_par)
 
subsection ‹Generalización y regla de inducción›
 
text ‹
  · Antes de aplicar inducción se debe de generalizar la fórmula a
    probar.
 
  · Vamos a ilustrar el principio anterior en el caso de los conjuntos
    inductivamente definidos, con el siguiente ejemplo: si n+2 es par,
    entonces n también lo es.
 
  · El siguiente intento falla:›
 
lemma "Suc (Suc n) ∈ par ⟹ n ∈ par"
  apply (erule par.induct) 
    (* 1. n ∈ par
       2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par *)
oops
 
text ‹En el intento anterior, los subobjetivos generados son
     1. n ∈ par
     2. ⋀na. ⟦na ∈ par; n ∈ par⟧ ⟹ n ∈ par
  que no se pueden demostrar.
 
  Se ha perdido la información sobre Suc (Suc n).›
 
text ‹Reformulación del lema: Si n es par, entonces n-2 también lo es.›
 
― ‹La demostración aplicativa es›
lemma par_imp_par_menos: 
  "n ∈ par ⟹ n - 2 ∈ par"
  apply (induction rule: par.induct) 
     (* 1. 0 - 2 ∈ par
        2. ⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par *)
   apply (simp add: par.cero)
  apply (simp add: par.paso)
     (* *)
  done
 
― ‹La demostración automática es›
lemma par_imp_par_menos_2: 
  "n ∈ par ⟹ n - 2 ∈ par"
  by (induction rule: par.induct) (auto simp add: par.cero par.paso)
 
― ‹La demostración estructurada es›
lemma "n ∈  par ⟹ n - 2 ∈ par"
proof (induction rule: par.induct)
  show "0 - 2 ∈ par" 
    by (auto simp add: par.cero)
next
  show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" 
    by (auto simp add: par.paso)
qed
 
text ‹Con el lema anterior se puede demostrar el original.›
 
― ‹La demostración aplicativa es›
lemma 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
  apply (drule par_imp_par_menos_2)
    (* Suc (Suc n) - 2 ∈ par ⟹ n ∈ par *)
  apply simp
    (* *)
  done
 
― ‹La demostración automática es›
lemma Suc_Suc_par_imp_par: 
  "Suc (Suc n) ∈ par ⟹ n ∈ par" 
  by (drule par_imp_par_menos_2, simp)
 
― ‹La demostración declarativa es›
lemma
  assumes "Suc (Suc n) ∈ par" 
  shows   "n ∈ par"
proof -
  have "Suc (Suc n) - 2 ∈ par" 
    using assms by (rule par_imp_par_menos_2)
  then show "n ∈ par" 
    by simp 
qed
 
text ‹Lemma. Un número natural n es par syss n+2 es par.›
 
lemma "((Suc (Suc n)) ∈ par) = (n ∈ par)"
  using Suc_Suc_par_imp_par par.paso by blast
 
section ‹Definiciones mutuamente inductivas›
 
text ‹Definición cruzada de los conjuntos inductivos de los pares y de los 
  impares:›
 
inductive_set
  Pares    :: "nat set" and
  Impares  :: "nat set"
where
  ceroP:    "0 ∈ Pares"
| ParesI:   "n ∈ Impares ⟹ Suc n ∈ Pares"
| ImparesI: "n ∈ Pares   ⟹ Suc n ∈ Impares"
 
text ‹El esquema de inducción generado por la definición anterior es
  · Pares_Impares.induct:
    ⟦P1 0; 
     ⋀n. ⟦n ∈ Impares; P2 n⟧ ⟹ P1 (Suc n);
     ⋀n. ⟦n ∈ Pares;   P1 n⟧ ⟹ P2 (Suc n)⟧
    ⟹ (x1 ∈ Pares ⟶ P1 x1)(x2 ∈ Impares ⟶ P2 x2)
›
 
thm Pares_Impares.induct
 
text ‹Ejemplo de demostración usando el esquema anterior.›
 
― ‹Demostración aplicativa›
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
  apply (induction rule: Pares_Impares.induct)
      (* 1. even 0
         2. ⋀n. ⟦n ∈ Impares; even (Suc n)⟧ ⟹ even (Suc n)
         3. ⋀n. ⟦n ∈ Pares; even n⟧ ⟹ even (Suc (Suc n))*)
    apply simp_all
      (* *)
  done
 
― ‹Demostración automática›
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
  by (induction rule: Pares_Impares.induct) simp_all
 
― ‹La demostración declarativa es›
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule: Pares_Impares.induct)
  show "even 0" 
    by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Impares" and
         H2: "even (Suc n)"
  show "even (Suc n)" 
    using H2 by simp
next
  fix n :: "nat"
  assume H1: "n ∈ Pares" and
         H2: "even n"
  have "∃k. n = 2*k" 
    using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" 
    by (rule exE)
  then have "Suc (Suc n) = 2*(k+1)" 
    by simp
  then have "∃k. Suc (Suc n) = 2*k" 
    by (rule exI)
  then show "even (Suc (Suc n))" 
    by (simp add: dvd_def)
qed
 
section ‹Definición inductiva de predicados›
 
text ‹Definición inductiva del predicado es_par tal que (es_par n) se
  verifica si n es par.›
 
inductive es_par :: "nat ⇒ bool" where
  "es_par 0" 
| "es_par n ⟹ es_par (Suc (Suc n))"
 
text ‹Heurística para elegir entre definir conjuntos o predicados:
  · si se va a combinar con operaciones conjuntistas, definir conjunto;
  · en caso contrario, definir predicado.›
 
end
LMF2019