(* A sorting example :
   (C) Yves Bertot, Pierre Casteran. Ver libro.
         Slightly modified by J. L. Freire (2005)
*)

(** En este m%\'o%dulo vamos a especificar y programar (a partir de una prueba) 
el m%\'e%todo de %{\sc ordenaci\'on de listas de enteros}%
conocido como %{\em isertion sort}%, basado en el que viene en el libro de texto *)
 
(** %\section{Definiciones}% *)

Require Import List.

Require Export ZArith.

Open Scope Z_scope.


(** Primero especificamos, mediante el predicado [sorted] lo que significa que una
lista est%{\'e}% ordenada. Se hace mediante tres axiomas (constructores) que nos
garantizan tres hechos que caracterizan este significado. El primero nos dice que
una lista vac%\'{\i}%a est%{\'a}% ordenada,  el segundo que una lista con un solo elemento
est%{\'a}% ordenada y, finalmente, que si una lista %$ z_2::l $% 
est%{\'a}% ordenada y si %$z_1 \le z_2$%, entonces la lista  %$ z_1::z_2::l $% est%{\'a}% 
tambi%\'e%n ordenada: *)

Inductive sorted : list Z -> Prop :=
  | sorted0 : sorted nil
  | sorted1 : forall z:Z, sorted (z :: nil)
  | sorted2 :
      forall (z1 z2:Z) (l:list Z),
        z1 <= z2 ->
        sorted (z2 :: l) -> sorted (z1 :: z2 :: l).

Hint Resolve sorted0 sorted1 sorted2 : sort.


(** Despu%{\'e}%s de a%\~n%adir a la base de [Hints] llamada [sort] las constantes [sorted0 
sorted1 sorted2] (con lo cual, cuando hagamos [auto with sort] se aplicar%\'a%n tambi%{\'e}%n 
estas constantes), podemos ver algunos ejemplos. N%\'o%tese el uso de [inversion] en la
prueba negativa: *)
 

Lemma sort_2357 :
 sorted (2 :: 3 :: 5 :: 7 :: nil).
Proof.
 auto with sort zarith.
Qed.

Lemma no_sort3425:
~sorted (3::4::2::5::nil).
red;intro.
inversion H.
inversion H4.
auto with arith.
Qed.

(** Probemnos ahora que si una lista %$ z::l $% est%{\'a}% ordenada, entonces la 
lista %$l$%  tambi%{\'e}%n lo estar%{\'a}%: *)

Theorem sorted_inv :
 forall (z:Z) (l:list Z), sorted (z :: l) -> sorted l.
Proof.
 intros z l H.
inversion H.
auto with sort.
assumption.
Qed.

 
(** %\section{N\'umero de apariciones de un elemento en una lista}% *)

(** En esta secci%\'o%n programaremos primero una funci%\'o%n que admite un elemento
y una lista y nos devuelve un natural (n%\'o%tese  que necesitamos el [%nat] para aclarar
que se trata de un [nat] porque el [Scope] abierto por defecto es [Z_scope]). En este programa
utilizamos el programa de decisi%\'o%n [Z_eq_dec] cuyo tipo
es [forall x y : Z, {x = y} + {x <> y}] : *)

 

Fixpoint nb_occ (z:Z) (l:list Z) {struct l} : nat :=
  match l with
  | nil => 0%nat
  | (z' :: l') =>
      match Z_eq_dec z z' with
      | left _ => S (nb_occ z l')
      | right _ => nb_occ z l'
      end
  end.

Eval compute in (nb_occ 3 (3 :: 7 :: 3 :: nil)).

Eval compute in (nb_occ 33 (3 :: 7 :: 3 :: nil)).

(** %\section{Permutaciones de una lista}% *)

(** Especifiquemos cuando un lista %$l'$% es una permutaci%\'o%n de otra %$l$% mediante
el predicado [equiv :list Z -> list Z -> Prop]: *)

Definition equiv (l l':list Z) :=
    forall z:Z, nb_occ z l = nb_occ z l'.
 
(** Esta resulta ser una relaci%\'o%n reflexiva sim%\'e%trica y transitiva. Para
probar esto %\'u%ltimo utilizaremos la constante [trans_eq] de tipo
     [: forall (A : Type) (x y z : A), x = y -> y = z -> x = z] que nos 
garantiza la transitividad de la igualdad. *)

Lemma equiv_refl : forall l:list Z, equiv l l.
Proof.
 unfold equiv; trivial.
Qed.

Lemma equiv_sym : forall l l':list Z, equiv l l' -> equiv l' l.
Proof.
  unfold equiv; auto.
Qed.

Lemma equiv_trans :
 forall l l' l'':list Z, equiv l l' ->
                         equiv l' l'' ->
                         equiv l l''.
Proof.
 intros l l' l'' H H0 z.
 eapply trans_eq; eauto.
Qed.


(** Se cumple tambi%{\'e}%n la congruencia de la equivalencia con el
constructor [cons]: *)

Lemma equiv_cons :
 forall (z:Z) (l l':list Z), equiv l l' ->
                             equiv (z :: l) (z :: l').
Proof.
 intros z l l' H z'.
 simpl; case (Z_eq_dec z' z); auto.
Qed.

(** y la siguiente propiedad: *)

Lemma equiv_perm :
 forall (a b:Z) (l l':list Z),
   equiv l l' ->
   equiv (a :: b :: l) (b :: a :: l').
Proof.
 intros a b l l' H z; simpl.
 case (Z_eq_dec z a); case (Z_eq_dec z b);
  simpl; case (H z); auto.
Qed.

Hint Resolve equiv_cons equiv_refl equiv_perm : sort.

(* Debemos ahora implementar la inserci%\'o%n de un elemento en
una lista de modo que si %\'e%sta es ordenada, entonces la resultante
de la insercci%\'o%n tambi%{\'e}%n lo ser%{\'a}%: *)

Fixpoint insertion (z:Z) (l:list Z) {struct l} : list Z :=
  match l with
  | nil => z :: nil
  | cons a l' =>
      match Z_le_gt_dec z a with
      | left _ =>  z :: a :: l'
      | right _ => a :: (insertion z l')
      end
  end.

Eval compute in (insertion 4 (2 :: 5 :: nil)).

Eval compute in (insertion 4 (24 :: 50 ::nil)).

(** Esta funci%\'o%n tiene las siguientes propiedades que confirman
que es adecuada para ordenar listas de acuerdo con nuestra 
especificaci%\'o%n *)

Lemma insertion_equiv : forall (l:list Z) (x:Z),
                  equiv (x :: l) (insertion x l).
Proof.
 induction l as [|a l0 H]; simpl ; auto with sort.
 intros x; case (Z_le_gt_dec x a);
   simpl; auto with sort.
 intro; apply equiv_trans with (a :: x :: l0);
   auto with sort.
Qed.


Lemma insertion_sorted :
 forall (l:list Z) (x:Z), sorted l -> sorted (insertion x l).
Proof.
 intros l x H; elim H; simpl; auto with sort.
 intro z; case (Z_le_gt_dec x z); simpl;
   auto with sort zarith.
 intros z1 z2; case (Z_le_gt_dec x z2); simpl; intros;
  case (Z_le_gt_dec x z1); simpl; auto with sort zarith.
Qed.

(** Finalmente, definimos la funci%\'o%n que ordena listas *)

Definition sort :
  forall l:list Z, {l' : list Z | equiv l l' /\ sorted l'}.
 induction l as [| a l IHl].
 exists (nil (A:=Z)); split; auto with sort.
 case IHl; intros l' [H0 H1].
 exists (insertion a l'); split.
 apply equiv_trans with (a :: l'); auto with sort.
 apply insertion_equiv.
 apply insertion_sorted; auto.
Defined.

Definition pr1 (A : Set) (P : A -> Prop) (H : {x : A | P x}) :=
  let (a, p) := H in a.
Implicit Arguments pr1 [A].

Definition pr2 (A : Set) (P : A -> Prop) (H : {x : A | P x}) :=
  let (a, p) as H return (P (pr1 P H)) := H in p.

Implicit Arguments pr2 [A].

Definition Sort:=fun (l:list Z) => pr1 (fun (l':list Z)=>
equiv l l' /\ sorted l') (sort l).

Eval compute in sort (3::1::4::nil).

Eval compute in Sort (3::6::21::-4::0::4::nil).

(** %\section{Ejercicios}% *)

Inductive lelist (a:Z) : list Z -> Prop :=
   | nil_le : lelist a nil
   | cons_le : forall (b:Z) (l:list Z), a <= b -> lelist a (b :: l).

Hint Constructors lelist.

Definition lista1:=3::1::7::8::nil.
Lemma k: (lelist 1 lista1).
Check cons_le. 
unfold lista1.
apply (cons_le 1 3).
auto with zarith.
Qed.

Lemma minv:forall (a:Z) (l: list Z), (lelist a l)->(l=nil) \/ (exists b:Z,exists l':list Z,
 l=b::l'/\(a <= b)). 
Admitted.

 

(** Hacer la siguiente prueba utilizando el lema de inversion
anterior [minv] y sin usar [inversion]:*)
Lemma lelist_inv' : forall (a b:Z) (l:list Z), lelist a (b :: l) -> a <= b.
Proof.

Admitted.
 

(** Hacerlo usando inversi%\'o%n de H. Le cambio el nombre para
que no coincida con el anterior:*)
 Lemma lelist_inv : forall (a b:Z) (l:list Z), lelist a (b :: l) -> a <= b.
 Proof.
Admitted.

 

Lemma sorted_lelist: forall (a:Z) (l:list Z), sorted l -> lelist a l ->
sorted (a::l).
Proof.
Admitted.
 

(** Una nueva definici%\'o%n de sorted *)

 Inductive ord : list Z -> Prop :=
   | nil_sort : ord nil
   | cons_sort :
       forall (a:Z) (l:list Z), ord l -> lelist a l -> ord (a :: l).
 Hint Constructors ord.

 Lemma ord_inv :
  forall (a:Z) (l:list Z), ord (a :: l) -> ord l /\ lelist a l.
 Proof.
 intros; inversion H; auto with datatypes.
 Qed.

Lemma ord_singl:forall (z:Z), ord (z::nil).
auto with sort datatypes.
Qed. 


 Lemma ord_rec :
  forall P:list Z -> Set,
    P nil ->
    (forall (a:Z) (l:list Z), ord l -> P l -> lelist a l -> P (a :: l)) ->
    forall y:list Z, ord y -> P y.
 Proof.
Admitted.
 
(** Probar que [ord] y [sorted] son equivalentes *)

Lemma ord_sort: forall l:list Z, ord l -> sorted l. 
Proof.
Admitted.
 

Lemma sort_ord:forall l:list Z, sorted l-> ord l.
Proof.
Admitted.
 

(*
Extraction "cursos/md2/c05-06/materiales/insertion_sort" Sort.
*)