Set Implicit Arguments.

(* SPECIFICATIONS FOR SOME WELL-KNOWN FUNCTIONS *)

Require Import List.
Require Import Arith.
Require Import ZArith.

Definition headPre (A:Type) (l:list A) : Prop := l<>nil.

Inductive headRel (A:Type) (x:A) : list A -> Prop :=
  headIntro : forall l, headRel x (cons x l).

Definition lastPre (A:Type) (l:list A) : Prop := l<>nil.

Inductive lastRel (A:Type) (x:A) : list A -> Prop :=
  lastIntro : forall l y, lastRel x l -> lastRel x (cons y l).

Definition divPre (args:nat*nat) : Prop := (snd args)<>0.

Definition divRel (args:nat*nat) (res:nat*nat) : Prop :=
 let (n,d):=args in let (q,r):=res in q*d+r=n /\ r<d.

(* defined later...
Definition PermRel (l1 l2:list Z) : Prop :=
  forall (z:Z), count z l1 = count z l2.
*)


(*********************************
  PARTIAL FUNCTIONS
**********************************)

(* Attempt to define a partial function... *)
(*
Definition head (A:Type) (l:list A) : A :=
  match l with
  | cons x xs => x
  end.
*)

Definition head (A:Type) (l:list A) (p:l<>nil) : A.
refine (fun A l p=>
  match l return (l<>nil->A) with
  | nil => fun H => _
  | cons x xs => fun H => x
  end p).
elim H; reflexivity.
Defined.

Print head.

Extraction Language Haskell.
Extraction Inline False_rect.

Extraction head.

(*********************************
  MORE ON EXTRACTION
**********************************)


(* Attempt to build a computational object whose control structure depends
   on the structure of logical proofs *)
(*
Definition or_to_bool (A B:Prop) (p:A\/B) : bool :=
  match p with
  | or_introl _ => true
  | or_intror _ => false
  end.
*)


Print sumbool.


Definition sumbool_to_bool (A B:Prop) (p:{A}+{B}) : bool :=
  match p with
  | left _ => true
  | right _ => false
  end.

Extraction Language Haskell.

Extraction sumbool_to_bool.


(*********************************
  IF THEN ELSE
**********************************)

Check le_lt_dec.
Check Z_eq_dec.
Check Z_lt_ge_dec.

SearchPattern ({_}+{~_}).
SearchPattern ({_}+{_}).

(* usage example *)
Fixpoint elem (x:Z) (l:list Z) {struct l}: bool :=
  match l with
    nil => false
  | cons a b => if Z_eq_dec x a then true else elem x b
  end.


(* recall the definition of InL from last lecture *)

Inductive InL (A:Type) (a:A) : list A -> Prop :=
    InHead : forall (xs:list A), InL a (cons a xs)
  | InTail : forall (x:A) (xs:list A), InL a xs -> InL a (cons x xs).

Hint Constructors InL.

(* Exercise *)
Theorem elem_correct_complete : forall (x:Z) (l:list Z),
  InL x l <-> elem x l=true.
Proof.
induction l; simpl.
split.
intro H; inversion H.
intro H; discriminate H.
elim (Z_eq_dec x a); intros.
split.
intros; reflexivity.
intros; rewrite a0; auto.
split.
intros.
inversion H.
contradiction.
inversion_clear IHl; auto.
intros.
apply InTail.
inversion_clear IHl; auto.
Qed.

(* Exercise *)
Theorem InL_dec : forall (x:Z) (l:list Z), {InL x l}+{~InL x l}.
intros x l; elim (elem_correct_complete x l); elim (elem x l); intros.
left; auto.
right; red; intro.
assert (false<>true).
discriminate.
auto.
Qed.


Extraction Inline list_rec list_rect sumbool_rec sumbool_rect
  eq_rec_r eq_rec eq_rect and_rec and_rect bool_rec bool_rect.
Extraction InL_dec.



(* repeated Exercise *)
Theorem InL_dec' : forall (x:Z) (l:list Z), {InL x l}+{~InL x l}.
Proof.
induction l.
right; red; intro H; inversion H.
elim (Z_eq_dec x a); intro H.
subst; left; auto.
elim IHl.
intros.
left; auto.
right; red; intro.
inversion H0; contradiction.
Defined.


(*********************************
  NON-OBVIOUS USES OF X_rec
**********************************)

(* merge function in haskell:
merge :: [a] -> [a] -> a
merge [] l = l
merge (x:xs) [] = x:xs
merge (x:xs) (y:ys) | x <= y = x:(merge xs (y:ys))
                    | otherwise = y:(merge (x:xs) ys)
*)

Fixpoint merge (l1: list Z) {struct l1}: list Z -> list Z :=
  match l1 with
  | nil => fun (l2:list Z) => l2
  | cons x xs => fix merge' (l2:list Z) : list Z := 
                   match l2 with
                   | nil => (cons x xs)
                   | cons y ys => match Z_le_gt_dec x y with
                                  | left _ => cons x (merge xs (cons y ys))
                                  | right _ => cons y (merge' ys)
                                  end
                   end
  end.

(*********************************
  NON-STRUCTURAL RECURSION
**********************************)

(* Euclidean division in haskell:
div :: Int -> Int -> (Int,Int)
div n d | n < d = (0,n)
        | otherwise = let (q,r)=div (n-d) d
                      in (q+1,r)
*)

(* Exercise: define "div" with an additional structural argument which
  bounds recursion. Check the results for some inputs. *)


Require Import Recdef.

Function div (p:nat*nat) {measure fst} : nat*nat :=
  match p with
  | (_,0) => (0,0)
  | (a,b) => if le_lt_dec b a
             then let (x,y):=div (a-b,b) in (1+x,y)
             else (0,a)
  end.
intros.
simpl.
omega.
Qed.

Function merge2 (p:list Z*list Z)
{measure (fun p=>(length (fst p))+(length (snd p)))} : list Z :=
  match p with
  | (nil,l) => l
  | (l,nil) => l
  | (x::xs,y::ys) => if Z_lt_ge_dec x y
                     then x::(merge2 (xs,y::ys))
                     else y::(merge2 (x::xs,ys))
  end.
intros.
simpl; auto with arith.
intros.
simpl; auto with arith.
Qed.




(********************************************
  FUNCTIONAL CORRECTNESS - direct approach
*********************************************)


(*
Definition divRel (args:nat*nat) (res:nat*nat) : Prop :=
 let (n,d):=args in let (q,r):=res in q*d+r=n /\ r<d.

Definition divPre (args:nat*nat) : Prop := (snd args)<>0.
*)


Theorem div_correct : forall (p:nat*nat),  divPre p -> divRel p (div p).
unfold divPre, divRel.
intro p.
functional induction (div p); simpl.
intro H; elim H; reflexivity.
replace (div (a-b,b)) with (fst (div (a-b,b)),snd (div (a-b,b))) in IHp0.
simpl in *.
intro H; elim (IHp0 H); intros.
split.
change (b + (fst (x,y0)) * b + (snd (x,y0)) = a).
rewrite <- e1.
omega.
change (snd (x,y0)<b); rewrite <- e1; assumption.
symmetry; apply surjective_pairing.
auto.
Qed.

(** CAUTION **)
(* Sometimes, the coq simply loses the connections between the
   objects that compromises the proof-development...
As an example, consider the following formulation for div_correct
*)

Theorem div_correct' : forall n d q r, d<>0 -> (q,r)=div (n,d) ->
  q*d+r=n /\ r<d.
intros n d q r.
functional induction (div (n,d)); simpl.
(* AND NOW, IT IS IMPOSSIBLE TO PROVE!!! *)
Admitted.




(*********************************
  SPECIFICATION WITH TYPES
**********************************)

Print sig.

(* ...from the last lecture...*)
(* An inductive relation "x is the last element of list l" *)
Inductive last (A:Type) (x:A) : list A -> Prop :=
| last_base : last x (cons x nil)
| last_step : forall l y, last x l -> last x (cons y l).

Hint Constructors last.


Theorem lastCorrect : forall (A:Type) (l:list A), l<>nil -> { x:A | last x l }.
induction l.
intro H; elim H; reflexivity.
intros.
destruct l.
exists a; auto.
assert ((a0::l)<>nil).
discriminate.
elim (IHl H0).
intros r Hr; exists r; auto.
Qed.



Extraction Inline sig_rect.
Extraction lastCorrect.

(********************************************
  EXERCISES
*********************************************)



(* Exercise: *)
Theorem elemStrong : forall (x:Z) (l:list Z), {InL x l}+{~InL x l}.
intros x l.
elim (elem_correct_complete x l).
destruct (elem x l); auto.
intros; right; red; intro.
absurd (false=true); auto.
Qed.

Extraction Inline and_rect and_rec.
Extraction elemStrong.


(* Exercise: for the well known list functions "app" and "rev" provide:
    i) a (relational) specification for it;
    ii) prove the corresponding correctness assertion.
*)



(********************************************
  INSERTION SORT
*********************************************)

Open Scope Z_scope.

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 Constructors Sorted.


Fixpoint count (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 (count z l')
      | right _ => count z l'
      end
  end.

Definition Perm (l1 l2:list Z) : Prop :=
  forall z, count z l1 = count z l2.

(* AUXILIARY LEMMAS: *)

(* Exercise: *)
Lemma Perm_cons_cons :
  forall (x y:Z) (l:list Z), Perm (x::y::l) (y::x::l).
Proof.
unfold Perm; intros; simpl; elim (Z_eq_dec z x); elim (Z_eq_dec z y); auto with zarith. 
Qed.

(* Exercise:
  prove that Perm is an equivalence relation
*)
Theorem Perm_trans :
  forall (l1 l2 l3:list Z), Perm l1 l2 -> Perm l2 l3 -> Perm l1 l3.
Proof.
unfold Perm; intros.
apply trans_eq with (count z l2); auto.
Qed.

(* Functions definitions *)

Fixpoint insert (x:Z) (l:list Z) {struct l} : list Z :=
  match l with
    nil => cons x (@nil Z)
  | cons h t =>
        match Z_lt_ge_dec x h with
          left _ => cons x (cons h t)
        | right _ => cons h (insert x t)
        end
  end.

Fixpoint isort (l:list Z) : (list Z) :=
  match l with
    nil => nil
  | (x::xs) => insert x (isort xs)
  end.

(* MAIN LEMMAS *)

Lemma insert_Sorted : forall x l, Sorted l -> Sorted (insert x l).
intros x l H; elim H; simpl; auto with zarith.
intro z; elim (Z_lt_ge_dec x z); intros.
auto with zarith.
auto with zarith.
intros z1 z2 l0 H0 H1.
elim (Z_lt_ge_dec x z2); elim (Z_lt_ge_dec x z1); auto with zarith.
Qed.


Lemma insert_Perm : forall x l, Perm (x::l) (insert x l).
unfold Perm; induction l.
simpl; auto with zarith.
simpl insert; elim (Z_lt_ge_dec x a); auto with zarith. 
intros; rewrite Perm_cons_cons.
pattern (x::l); simpl count; elim (Z_eq_dec z a); intros.
rewrite IHl; reflexivity.
apply IHl.
Qed.

(* MAIN THEOREM *)

Theorem isort_correct : forall (l l':list Z),
  l'=isort l -> Perm l l' /\ Sorted l'.
induction l; intros.
unfold Perm; rewrite H; split; auto.
simpl in H.
rewrite H.
elim (IHl (isort l)); intros; split.
apply Perm_trans with (a::isort l).
unfold Perm; intro z; simpl; elim (Z_eq_dec z a); intros; auto with zarith.
apply insert_Perm.
apply insert_Sorted; auto.
Qed.
















Theorem lastCorrect : forall (A:Type) (l:list A), l<>nil -> { x:A | last x l }.
induction l.
intro H; elim H; reflexivity.
intros.
destruct l.
exists a; auto.
assert ((a0::l)<>nil).
discriminate.
elim (IHl H0).
intros r Hr; exists r; auto.
Qed.

Extraction Inline sig_rect.
Extraction lastCorrect.




(* INSERTION SORT *)

Open Scope Z_scope.

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 Constructors Sorted.


Inductive Sorted' : list Z -> Prop :=
  | sorted0' : Sorted' nil
  | sorted1' : forall (z:Z) (l:list Z),
        (forall x, (InL x l) -> z<=x) -> Sorted' l -> Sorted' (z :: l).

Hint Constructors Sorted'.