Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header "Hoare Logic"

theory Hoare_b imports Big_Step_b begin

text{*
La Lógica de Hoare (creada por Tony Hoare) es una lógica para
probar propiedades de programas imperativos. Las fórmulas de 
esta lógica son ternas de la forma
                        {P} c {Q}
El significado es el siguiente: si la fórmula P es cierta antes 
de ejecutar la instrucción c, entonces la fórmula Q es cierta
después de ejecutar c.

Por ejemplo,
                  {x = y} y:= y + 1 {x < y}
*}

subsection "Pruebas mediante semántica operacional"

text{* Veamos un ejemplo de cómo usar la semántica oparacional
para probar propiedades de programas. Consideremos el programa
siguiente:
    y:= 0;
    WHILE 0 < x DO (y:= y + x; x := x-1)

que suma en y los números de 1 a x.
*}

text{* Formalmente, el programa en el lenguaje IMP es la 
sucesión de la asignación y:=0 y el siguiente programa
*}

abbreviation "wsum ==
  WHILE Less (N 0) (V ''x'')
  DO (''y'' ::= Plus (V ''y'') (V ''x'');;
      ''x'' ::= Plus (V ''x'') (N -1))"

text{* Para probar que, efectivamente, el programa realiza
la suma de los números de 1 a x, definimos la función suma
como sigue:
*}

fun sum :: "int ⇒ int" where
"sum i = (if i ≤ 0 then 0 else sum (i - 1) + i)"

text{* Establecemos las siguientes reglas de simplificación, que
sustituyen a las reglas de simplificación generadas por la 
definición.
*}

lemma sum_simps[simp]:
  "0 < i ⟹ sum i = sum (i - 1) + i"
  "i ≤ 0 ⟹ sum i = 0"
by(simp_all)

declare sum.simps[simp del]

text{* El comportamiento del bucle while con respecto a la 
función sum es el siguiente: si t es el estado que resulta de 
aplicar wsum al estado inicial s, entonces el valor de y en t es
el valor inicial de y en s más la suma de los números desde 1
hasta el valor de x en s. *}

lemma while_sum:
  "(wsum, s) ⇒ t ⟹ t ''y'' = s ''y'' + sum(s ''x'')"
apply(induction wsum s t rule: big_step_induct)
apply(auto)
done

text{* Nota: la prueba es por inducción con el esquema inducido 
por la definición de big_step. El resto de la prueba se hace de forma
automática, debido a que las reglas de inversión que se aplican 
automáticamente como reglas de eliminación.
*}

text{* Ahora fijamos el valor inicial de y antes del bucle:
*}

lemma sum_via_bigstep:
  assumes "(''y'' ::= N 0;; wsum, s) ⇒ t"
  shows "t ''y'' = sum (s ''x'')"
proof -
  from assms have "(wsum,s(''y'':=0)) ⇒ t" by auto
  thus ?thesis by (simp add: while_sum)
(*  from while_sum[OF this] show ?thesis by simp *)
qed

subsection "Lógica de Hoare: corrección parcial"

text{* Las fórmulas de la Lógica de Hoare son ternas de la forma
{P}c{Q}, donde P se denomina precodición, y Q postcondición. Se dice
que {P}c{Q} es válida (o correcta parcialmente) si se verifica lo 
siguiente:

Si P es cierta antes de la ejecución de c y c termina, entonces
Q es cierta después.
*}

text{* Nota: la corrección total de la fórmula {P}c{Q} sería como 
sigue:

Si P es cierta antes de la ejecución de c, entonces c termina y
Q es cierta después.
*}

text{*
Las pre y postcondiciones, también denominados asertos, se pueden 
representar bien como objetos sintácticos concretos (como las 
expresiones booleanas), o bien como predicados sobre estados. 
Elegimos esta segunda representación porque es más adecuada 
para el razonamiento automático.

Formalizamos los asertos (assn) como predicados sobre estados.

*}

type_synonym assn = "state ⇒ bool"

text{* Validez de una terna {P}c{Q}:
*}

definition
hoare_valid :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊨ {(1_)}/ (_)/ {(1_)}" 50) where
"⊨ {P}c{Q} = (∀s t. P s ∧ (c,s) ⇒ t  ⟶  Q t)"

text{* Notación: El estado s en el que el valor de la variable
x es el valor de la expresión a en s,  s(x := aval a s), se 
denotará por s[a/x].
*}

abbreviation state_subst :: "state ⇒ aexp ⇒ vname ⇒ state"
  ("_[_'/_]" [1000,0,0] 999)
where "s[a/x] == s(x := aval a s)"

text{* Sistema deductivo:

Hemos definido cuando una terna de Hoare es válida. Ahora presentamos 
un conjunto de reglas de inferencia o sistema deductivo para obtener 
o demostrar ternas de Hoare.

Y definimos cuando la terna {P}c{Q} es demostrable a partir del conjunto 
de reglas (⊢ {P}c{Q}).

Posteriormente, probaremos que ambas nociones son equivalentes:

           ⊨ {P}c{Q} si y sólo si ⊢ {P}c{Q}
*}

inductive
  hoare :: "assn ⇒ com ⇒ assn ⇒ bool" ("⊢ ({(1_)}/ (_)/ {(1_)})" 50)
where
Skip: "⊢ {P} SKIP {P}"  |

Assign:  "⊢ {λs. P(s[a/x])} x::=a {P}"  |

Seq: "⟦ ⊢ {P} c⇩1 {Q};  ⊢ {Q} c⇩2 {R} ⟧
      ⟹ ⊢ {P} c⇩1;;c⇩2 {R}"  |

If: "⟦ ⊢ {λs. P s ∧ bval b s} c⇩1 {Q};  ⊢ {λs. P s ∧ ¬ bval b s} c⇩2 {Q} ⟧
     ⟹ ⊢ {P} IF b THEN c⇩1 ELSE c⇩2 {Q}"  |

While: "⊢ {λs. P s ∧ bval b s} c {P} ⟹
        ⊢ {P} WHILE b DO c {λs. P s ∧ ¬ bval b s}"  |

conseq: "⟦ ∀s. P' s ⟶ P s;  ⊢ {P} c {Q};  ∀s. Q s ⟶ Q' s ⟧
        ⟹ ⊢ {P'} c {Q'}"

text{* Nota: es importante no confundir ambas nociones:
(-) Validez (⊨ {P}c{Q}), basada en la semántica operacional.
(-) Demostrabilidad (⊢ {P}c{Q}), basada en el conjunto de reglas.
*}

text{* Reglas de inferencia:

(-) Skip: la terna {P} SKIP {P} es demostrable.

(-) Assign: si P es cierta en el estado s[a/x], después 
    de la asignación  x::=a, P será cierta. Por ejemplo,

            {5 = 5} x:= 5       {x = 5}
          {x+5 = 5} x:= x+5     {x = 5}
     {2*(x+5) > 20} x:= 2*(x+5) {x > 20}
   
    O bien, simplificando las precondiciones,

           {True} x:= 5       {x = 5}
          {x = 0} x:= x+5     {x = 5}
          {x > 5} x:= 2*(x+5) {x > 20}
   
(-) Seq: si se usa hacia atrás, descompone la prueba de c1;;c2
         en dos pruebas relativas a c1 y c2, con un aserto 
         intermedio P2.

(-) If: es necesario probar ambas ramas; la primera, teniendo como
        precondición P y b, y la segunda, P y ¬ b.

(-) While: la premisa dice que si P y b son ciertas antes de la 
           ejecucución del cuerpo del bucle, c, entonces P es cierta
           después (siempre que c termine). En este caso, P se denomina
           un invariante del bucle. Es decir, si se empieza en un estado
           en el que P es cierta, se mantendrá cierta a lo largo de todas
           las iteraciones hasta que b sea falsa, en cuyo caso P seguirá
           siendo cierta.

(-) conseq: la regla de consecuencia es independiente de los constructores
            del lenguaje IMP. Su objetivo es ajustar las pre y post condi-
            ciones. Suele usarse para:
            (+) reforzar la precondición: P' ⟶ P
            (+) debilitar la postcondición: Q ⟶ Q'
*}


text{* Declaramos los siguientes lemas como reglas de 
simplificación y de introducción.
*}

lemmas [simp] = hoare.Skip hoare.Assign hoare.Seq If

lemmas [intro!] = hoare.Skip hoare.Assign hoare.Seq hoare.If

text{* Algunas de las reglas anteriores (por ejemplo, Skip, 
Assing o While) no son fáciles de manejar, pues sólo se pueden
aplicar hacia atrás si la pre o la postcondición tienen una
forma exacta. Por ello, establecemos las reglas siguientes, 
que se prueban usando la regla de consecuencia.
*}

lemma strengthen_pre:
  "⟦ ∀s. P' s ⟶ P s;  ⊢ {P} c {Q} ⟧ ⟹ ⊢ {P'} c {Q}"
by (blast intro: conseq)

lemma weaken_post:
  "⟦ ⊢ {P} c {Q};  ∀s. Q s ⟶ Q' s ⟧ ⟹  ⊢ {P} c {Q'}"
by (blast intro: conseq)

lemma Assign': "∀s. P s ⟶ Q(s[a/x]) ⟹ ⊢ {P} x ::= a {Q}"
by (simp add: strengthen_pre[OF _ Assign])

lemma While':
assumes "⊢ {λs. P s ∧ bval b s} c {P}" and "∀s. P s ∧ ¬ bval b s ⟶ Q s"
shows "⊢ {P} WHILE b DO c {Q}"
by(rule weaken_post[OF While[OF assms(1)] assms(2)])

thm While'

text{* Ejemplo: prueba usando las reglas de inferencia *}

lemma "⊢ {λs. s ''x'' = n} ''y'' ::= N 0;; wsum {λs. s ''y'' = sum n}"
apply(rule Seq)
 prefer 2
 apply(rule While' [where P = "λs. (s ''y'' = sum n - sum(s ''x''))"])
  apply(rule Seq)
   prefer 2
   apply(rule Assign)
  apply(rule Assign')
  apply simp
 apply simp
apply(rule Assign')
apply simp
done


end