Menu Close

Día: 7 febrero, 2019

RA2018: Definiciones inductivas en IsabelleHOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.

La clase se ha basado en la siguiente teoría Isabelle

chapter {* Tema 11: Definiciones inductivas *}
 
theory T11_Definiciones_inductivas
imports Main
begin
 
section {* El 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.
*}
 
subsection {* Definición inductiva del conjunto de los pares *}
 
inductive_set par :: "nat set" where
  cero [intro!]: "0 ∈ par" 
| paso [intro!]: "n ∈ par ⟹ (Suc (Suc n)) ∈ par"
 
text {*
  · Una definición inductiva está formada con reglas de introducción.
 
  · 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))
*}
 
subsection {* Uso de las reglas de introducción *}
 
text {*
  Lema: Los números de la forma 2*k son pares.
*}
 
― ‹La demostración automática es›
lemma dobles_son_pares [intro!]: 
  "2*k ∈ par"
by (induct k) auto
 
― ‹La demostración estructurada es›
lemma dobles_son_pares_2:
  "2*k ∈ par"
proof (induct k)
  show "2 * 0 ∈ par" by auto
next
  show "⋀k. 2 * k ∈ par ⟹ 2 * Suc k ∈ par" by auto
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.
*}
 
lemma even_imp_par: "even n ⟹ n ∈ par"
by auto
 
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
*}
 
text {*
  Lema: Los números pares son divisibles por 2.
*} 
 
― ‹1ª demostración (detallada)lemma par_imp_even: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "2 dvd (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  have "∃k. n = 2*k" using H2 by (simp add: dvd_def)
  then obtain k where "n = 2*k" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
― ‹2ª demostración (con arith)lemma par_imp_even_2: 
  "n ∈ par ⟹ even n"
proof (induction rule: par.induct)
  show "even (0::nat)" by (simp_all add: dvd_def)
next
  fix n::nat
  assume H1: "n ∈ par" and
         H2: "even n"
  then show "even (Suc (Suc n))" by (auto simp add: dvd_def, arith)
qed
 
― ‹3ª demostración (automática)lemma par_imp_even_3: 
  "n ∈ par ⟹ even n"
by (induction rule:par.induct) (auto simp add: dvd_def, arith)
 
text {*
  Lema: Un número n es par syss es divisible por 2. 
*}
 
theorem par_iff_even: "(n ∈ par) = (even n)"
by (blast intro: even_imp_par par_imp_even)
 
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) 
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 automática es›
lemma par_imp_par_menos_2: 
  "n ∈ par ⟹ n - 2 ∈ par"
by (induction rule:par.induct) auto
 
― ‹La demostración estructurada es›
lemma "n ∈  par ⟹ n - 2 ∈ par"
proof (induction rule:par.induct)
  show "0 - 2 ∈ par" by auto
next
  show "⋀n. ⟦n ∈ par; n - 2 ∈ par⟧ ⟹ Suc (Suc n) - 2 ∈ par" by auto
qed
 
text {* 
  Con el lema anterior se puede demostrar el original.
*}
 
― ‹La demostración estructurada 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
 
― ‹La demostración aplicativa es›
lemma 
  "Suc (Suc n) ∈ par ⟹ n ∈ par"
apply (drule par_imp_par_menos_2) 
apply simp
done
 
(* Comentar el uso de drule *)
 
― ‹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)
 
text {*
  Lemma. Un número natural n es par syss n+2 es par.
*}
 
lemma [iff]: "((Suc (Suc n)) ∈ par) = (n ∈ par)"
by (blast dest: Suc_Suc_par_imp_par)
 
text {*
  Se usa el atributo "iff" porque sirve como regla de simplificación.
*}
 
subsection {* 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)
*}
 
text {*
  Ejemplo de demostración usando el esquema anterior.
*}
 
lemma "(m ∈ Pares ⟶ even m) ∧ (n ∈ Impares ⟶ even (Suc n))"
proof (induction rule:Pares_Impares.induct)
  show "even (0::nat)" 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" ..
  then have "Suc (Suc n) = 2*(k+1)" by auto
  then have "∃k. Suc (Suc n) = 2*k" ..
  then show "even (Suc (Suc n))" by (simp add: dvd_def)
qed
 
subsection {* 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

Como ejercicio se propuso la relación 8 sobre gramáticas libres de contexto.