;;; 1
;;; *********************************************************
;;; ACL2 DEMO: Corrección de un algoritmo de ordenación
;;; *********************************************************


;;; Vamos a definir el conocido algoritmo mergesort para ordenar
;;; listas. Mergesort es un algoritmo recursivo, que consiste en
;;; partir la lista a ordenar en dos trozos, ordenar (recursivamente
;;; cada trozo) y mezclar de manera ordenada ambas sublistas. 






(encapsulate
 ()
;;; 2)
;;; Función que toma los elementos de lugar impar en una lista
;;; Nótese que (alternos l) y (alternos (rest l)) forman una partición
;;; en dos de la lista original:
 (defun alternos (l)
   (if (endp l)
       nil
     (cons (first l) (alternos (rest (rest l))))))
 





;;; 3)
;;; Función que mezcla dos listas que ya están ordenadas, para
;;; devolver un resultado ordenado:
 (defun mezcla (l m)
   (declare (xargs :measure (+ (acl2-count l) (acl2-count m))))
   (cond ((endp l) m)
	 ((endp m) l)
	 (t (if (<= (first l) (first m))
		(cons (first l) (mezcla (rest l) m))
	      (cons (first m) (mezcla l (rest m)))))))
 
 



 (defthm len-alternos
   (implies (consp (rest l))
	    (< (len (alternos l)) (len l)))
   :rule-classes :linear)


;;; 4
;;; Nuestro algoritmo de ordenación:
;;; - Si es la lista vacía o unitaria, devolverla tal cual
;;; - Si no, ordenar los de lugar impar (recursivamente)
;;;          ordenar los de lugar par (recursivamente)
;;;          y mezclar ambas listas.
              
 (defun mergesort (l)
   (declare (xargs :measure (len l)))
   (if (or (endp l) (endp (rest l)))
       l
     (mezcla (mergesort (alternos l)) (mergesort (alternos (rest l)))))))
 

;;; 5
;;; ---------------
;;; La función definida es ejecutable:

(mergesort '(23 12 35 21 1 -4 3 7/12 3/4 200))

(mergesort '(20 19 18 17 16 15 14 13 12 11 10 9 8 7 6 5 4 3 2 1))

 
;;; Testeando, PARECE que es correcta. 
;;; Pero ¿podemos estar seguros de que la función ordenará bien SEA
;;; CUAL SEA su entrada? Demostrémoslo en la lógica.
;;; -----------------

;;; 6
;;; Primero, debemos definir las propiedades que deseamos verificar.
;;; En primer lugar, la siguiente función define el concepto "estar ordenada"
;;; NOTA: El propio lenguaje sirve tanto para definir los algoritmos, 
;;;       como las propiedades que deben verificar 
(defun ordenada (l)
  (if (or (endp l) (endp (rest l)))
      t
    (and (<= (first l) (second l))
	 (ordenada (rest l)))))





;;; 7
;;; La siguiente función define el número de veces que un número
;;; ocurre en una lista
(defun ocurrencias (x l)
  (cond ((endp l) 0)
	((equal x (first l)) (1+ (ocurrencias x (rest l))))
	(t (ocurrencias x (rest l)))))







;;; 8
;;; Lo que sigue son las dos propiedades que especifican la corrección
;;; del algoritmo de ordenación (nótese que son fórmulas universalmente cuantificadas)

;;; El algoritmo devuelve listas ordenadas:
; (defthm ordenada-mergesort
;    (ordenada (mergesort l)))

;;; La lista devuelta tiene los mismos elementos y con el mismo número
;;; de repeticiones que la lista original:
; (defthm ocurrencias-mergesort
;   (equal (ocurrencias x (mergesort l))
;	   (ocurrencias x l)))


;;; 9
;;; Intentemos probar la primera propiedad:
(defthm ordenada-mergesort
  (ordenada (mergesort l)))

;;; Exito!!

;;; Nótese el lema (Subgoal *1.1) que ha descubierto y que ha probado
;;; como parte de la demostración:
;   (IMPLIES (AND (ORDENADA MT0) (ORDENADA MT))
;            (ORDENADA (MEZCLA MT0 MT))).




;;; 10
;;; Intentamos ahora la segunda propiedad:
(defthm ocurrencias-mergesort
  (equal (ocurrencias x (mergesort l))
	 (ocurrencias x l)))


;;; Fallo!! (no quiere decir que no sea cierto, sino simplemente que 
;;;          no ha encontrado una demostración) 

;;; Observando la prueba fallida podemos deducir que el sistema
;;; necesita demostrar un lema sobre la relación entre las funciones
;;; ocurrencia y mezcla. No ha sido capaz de encontrarlo por sí mismo,
;;; así que guiamos al demostrador especificando esa relación y demostrándola.

;;; 11
;;; Esta es la relación entre mezcla y ocurrencias:
(defthm ocurrencias-mezcla
  (equal (ocurrencias x (mezcla l1 l2))
	 (+ (ocurrencias x l1) (ocurrencias x l2))))


;;; Probado!! 





;;; 12 
;;; Intentamos ahora de nuevo la anterior propiedad:
(defthm ocurrencias-mergesort
  (equal (ocurrencias x (mergesort l))
	 (ocurrencias x l)))

;;; Falla de nuevo!!
;;; De nuevo observando la prueba fallida, vemos que el sistema
;;; necesita saber un lema que relacione ocurrencias con alternos. En
;;; concreto, saber que la suma de las ocurrencias de un elemento en
;;; cada una de las particiones que realiza el algoritmo es igual a
;;; las ocurrencias del elemento en la lista original


;;; 13
;;; Es decir, necesitamos probar esto:
(defthm ocurrencias-alternos
  (equal (+ (ocurrencias x (alternos l))
	    (ocurrencias x (alternos (rest l))))
	 (ocurrencias x l)))


;;; Probado!!!
;;; Volvamos a intentar nuestro objetivo de nuevo





;;; 14 
;;; Tercer intento:
(defthm ocurrencias-mergesort
  (equal (ocurrencias x (mergesort l))
	 (ocurrencias x l)))

;;; Probado!!!
;;; El algoritmo mergesort ha sido verificado formalmente.
;;; ---------------------------------------------------------------