(** * Certification de programmes *)

(** Dans ce TD, on certifie plusieurs programmes vérifiant qu'un tableau 
    d'entiers est trié de manière croissante et retournant, dans le cas 
    négatif, un indice du tableau où l'inégalité n'est pas satisfaite. *)

(** ** Programmes fonctionnels *)

(** Dans cette première partie, on s'intéresse à des programmes fonctionnels,
    et des tableaux représentés par des fonctions de type [nat->nat]. *)

Definition array := nat -> nat.

(** *** Fonction récursive + preuve. 
    Écrire une fonction [is_sorted] prenant 
    en arguments [t:array], [m:nat] et retournant une valeur de type
    [(option nat)] valant [None] si le tableau [t[0]...t[m]] est trié de
    manière croissante et [(Some i)] avec [0 <= i < m] si [t[i] > t[i+1]]. *)

(* Indication: on pourra effectuer la recherche de haut en bas (récurrence
   structurelle sur [m]). *)

Require Arith.
Require Compare_dec.

Fixpoint is_sorted [t:array; m:nat] : (option nat) := 
  Cases m of 
  | O => 
      (None nat)
  | (S m') => 
      if (le_gt_dec (t m') (t m)) then [_](is_sorted t m') else [_](Some nat m')
  end.

(* Écrire la spécification de [is_sorted] et montrer sa correction. *)

Definition sorted := 
  [t:array][m:nat](i:nat)(le O i) -> (lt i m) -> (le (t i) (t (S i))).

Lemma is_sorted_correct : 
  (t:array)(m:nat)Cases (is_sorted t m) of
                    | None => (sorted t m)
                    | (Some i) => (gt (t i) (t (S i))) end.
Proof.
Induction m; Simpl.
Unfold sorted; Intros; Absurd (le O i); Auto with arith.
Intros m'; Case (le_gt_dec (t m') (t (S m'))); Auto.
Case (is_sorted t m'); Auto.
Unfold sorted; Intros.
Case (le_lt_eq_dec i m'); Auto with arith.
Intro Hi; Rewrite Hi; Auto.
Save.

(** *** Extraction *)

(** Écrire un type inductif correspondant à la spécification de [is_sorted]. *)

Inductive is_sorted_spec [t:array; m:nat] : Set := 
  | Sorted : (sorted t m) -> (is_sorted_spec t m)
  | Unsorted : (i:nat)(gt (t i) (t (S i))) -> (is_sorted_spec t m).

(** L'extraction de ce type inductif doit être isomorphe à [option nat] *)

Extraction is_sorted_spec.

(** Montrer directement cette spécification et extraire le programme. *)

Lemma is_sorted_2 : (t:array)(m:nat)(is_sorted_spec t m).
Proof.
Induction m. 
Apply Sorted; Unfold sorted; Intros; Absurd (le O i); Auto with arith.
Intros n Hn; Case (le_gt_dec (t n) (t (S n))); Intro.
Elim Hn; Unfold sorted; Intros.
Apply Sorted; Unfold sorted; Intros.
Case (le_lt_eq_dec i n); Auto with arith.
Intro Hi; Rewrite Hi; Auto.
Apply Unsorted with i; Auto.
Apply Unsorted with n; Auto.
Save.

Extraction is_sorted_2.


(** ** Programmes impératifs *)

(** Le tableau est maintenant un tableau global au sens de Correctness, donc
    indexés par le type [Z]. Sa taille est un paramètre [N]. *)

Require Correctness.
Require Omega.

Parameter N : Z.
Axiom N_strictement_positif : `N >= 1`.

Global Variable t : array N of Z.

(** La spécification du programme impératif est maintenant la suivante :
    il retourne un booléen indiquant si le tableau est trié ; lorsque ce
    booléen vaut [false], une variable globale [index] désigne un indice
    du tableau où l'inégalité n'est pas satisfaite. *)

Global Variable index : Z ref.

Definition Zsorted := 
  [t:(array N Z)](i:Z)`0 <= i < N-1` -> `(access t i) <= (access t (i+1))`.

Definition is_sorted_imp_spec :=
  [t:(array N Z)][r:bool][i:Z]
  if r then (Zsorted t) else `(access t i) > (access t (i+1))`.

(** *** Premier programme impératif avec une boucle while.
    La recherche est effectuée de haut en bas avec un indice [i] ;
    on sort de la boucle lorsque [i] vaut -1.
    Déterminer l'invariant de boucle, le variant, et établir les
    obligations de preuve. *)

(* REMARQUE: un petit bug de la 7.2 oblige à écrire [Zopp 1] au lieu de [-1] *)

Correctness is_sorted_3 
  (let i = ref (N-2) in
   begin
     index := (Zopp 1);
     while !i >= 0 do
       { invariant 
           `-1 <= i < N-1` /\
	   ((`index = -1` /\
              (j:Z)`i < j < N-1` -> `(access t j) <= (access t (j+1))`) \/
	   (`index >= 0` /\ `(access t index) > (access t (index+1))`))
         variant `i+1` 
       }
       if t[!i] <= t[!i+1] then
	 i := !i - 1
       else begin
         index := !i;
	 i := (Zopp 1)
       end
     done;
     !index = (Zopp 1)
   end)
  { (is_sorted_imp_spec t result index) }.
Proof.
Omega.
Omega.
(* then *)
Repeat Split; Try Omega.
Intuition.
Left. Split. Assumption.
Intros; Case (Z_le_lt_eq_dec i0 j).
Omega.
Intro; Apply H3; Omega.
Intro Hj; Rewrite <- Hj; Assumption.
(* else *)
Repeat Split; Try Omega.
Intuition.
(* initial invariant *)
Split. Generalize N_strictement_positif; Omega.
Left. Split. Trivial.
Intros; Absurd `N-2 < j < N-1`; Omega.
(* post-condition *)
Decompose [and or] Post8; Clear Post8; 
  Unfold is_sorted_imp_spec; Induction result0.
Unfold Zsorted; Intros; Apply H4; Omega.
Absurd `index1 = -1`; Omega.
Absurd `index1 = -1`; Omega.
Assumption.
Save.

(** ** Deuxième programme impératif, avec cette fois une fonction récursive.
    Déterminer les pré- et post-conditions de la fonction [check] et
    établir les obligations de preuve. *)

Correctness is_sorted_4
 (let rec check (i:Z) : bool { variant `i+1` } =
   { `-1 <= i < N-1` /\
     (j:Z)`i < j < N-1` -> `(access t j) <= (access t (j+1))` }
   (if i = (Zopp 1) then
      true
    else if t[i] > t[i+1] then begin
      index := i;
      false
    end else
      (check (i-1)))
    { if result then (Zsorted t) 
                else `(access t index) > (access t (index+1))` }
  in
  check (N-2))
  { (is_sorted_imp_spec t result index) };
Try Clear vf; Try Clear check.
Proof.
Split. Generalize N_strictement_positif; Omega.
Intros; Absurd `N-2 < j < N-1`; Omega.
Decompose [and] Pre3.
Unfold Zsorted; Intros; Apply H0; Omega.
Omega.
Omega.
Unfold Zwf; Omega.
Split.
Omega.
Decompose [and] Pre3; Clear Pre3.
Intros; Case (Z_le_lt_eq_dec i0 j). Omega.
Intro; Apply H0; Omega.
Intro Hj; Rewrite <- Hj; Assumption.
Save.