Set Implicit Arguments.
Require Import ZArith.
Require Import List.
Import Datatypes.
Open Scope Z_scope.

Fixpoint sum (l : list Z) : Z :=  
   match l with nil => 0 | a::m => a + sum m end.

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

(** max nil = 0 
    max a::m = if m=nil then a else max a (max m)
*)

Definition is_nil 
  : forall A (l:list A), { l = nil }+{ l <> nil }.
destruct l; auto.
right; discriminate.
Defined.

Fixpoint max (l : list Z) : Z :=  
   match l with 
     nil   => 0 
   | a::m   => if is_nil m then a 
               else Zmax a (max m) 
   end.

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

Fixpoint Zlength (l : list Z) : Z :=  
   match l with nil   => 0 
             | a::m   => Zlength m + 1
   end.

Lemma Zlength_pos : forall l, 0 <= Zlength l.
induction l; simpl.
auto with zarith.
auto with zarith.
Save.
Hint Resolve Zlength_pos : zarith.


Lemma sum_max_prop : forall l, sum l <= Zlength l * max l.
induction l; simpl; auto with zarith.
destruct (is_nil l).
subst l; auto with zarith.
apply Zle_trans with ((Zlength l * max l) + a); auto with zarith.
destruct (Zmax_spec a (max l)) as [(Hge,He)|(Hlt,He)].
rewrite He.
ring_simplify.
auto with zarith.
rewrite He.
ring_simplify.
auto with zarith.
Qed.

(** Introducing the property in post-condition *)

Definition maxs1 (l : list Z) : { z : Z | sum l <= Zlength l * z}.
induction l.
simpl.
exists 0; auto with zarith.
destruct IHl as (maxl,H); simpl.
destruct (is_nil l) as [Hn|Hn].
exists a; rewrite Hn; auto with zarith.
exists (Zmax a maxl).
apply Zle_trans with (Zlength l * maxl + a); 
      auto with zarith.
destruct (Zmax_spec a maxl) as [(Hge,He)|(Hlt,He)]; 
  rewrite He; ring_simplify; auto with zarith.
Defined.

Extraction maxs1.

Eval compute in 
(let (m,_) := maxs1 (2::5::3::4::nil) in m).

(** Using Program to develop the term with proofs *)
 
Require Import Program.

Program Fixpoint maxs (l : list Z) 
   : {z:Z | sum l <= Zlength l * z} :=  
   match l with 
      nil   => 0 
    | a::m  => if is_nil m then a else Zmax a (maxs m) 
   end.
Next Obligation.
simpl; auto with zarith.
Defined.
Next Obligation.
apply Zle_trans with (Zlength m * x + a); 
      auto with zarith.
destruct (Zmax_spec a x) as [(Hge,He)|(Hlt,He)]; 
  rewrite He; ring_simplify; auto with zarith.
Defined.
Extraction maxs.
Eval compute in 
     (let (m,_) := maxs (2::5::3::4::nil) in m).

(** Getting a complete specification *)

Inductive is_max : list Z -> Z -> Prop := 
  is_max0 : is_max nil 0
| is_max1 : forall a, is_max (a::nil) a
| is_maxconsle : forall a b m, m <> nil -> is_max m b -> a <= b -> is_max (a::m) b
| is_maxconsgt : forall a b m, m <> nil -> is_max m b -> a > b -> is_max (a::m) a.

Hint Constructors is_max.


Program Fixpoint max2 (l : list Z) : {z:Z | is_max l z} :=  
   match l with nil   => 0 
             | a::m   => if is_nil m then a else Zmax a (max2 m) 
   end.
Next Obligation.
assert (a <= x \/ a > x) as [Hle|Hlt]; try omega.
rewrite Zmax_right; auto with zarith.
rewrite Zmax_left; auto with zarith.
apply is_maxconsgt with x; auto with zarith.
Defined.

Extraction max2.

Definition zmax2 (l : list Z) : Z := let (m,_) := max2 l in m.

Lemma zmax2_spec : forall l, is_max l (zmax2 l).
intros; unfold zmax2.
destruct (max2 l) as (m,H).
trivial.
Save.

Lemma ismax_prop 
    : forall l m, is_max l m -> sum l <= Zlength l * m.
induction 1; simpl sum; simpl Zlength; ring_simplify; auto with zarith.
apply Zle_trans with (Zlength m * b + a); ring_simplify; auto with zarith. 
Save.



(* 2.2 : linear search *)
Open Scope nat_scope.

Fixpoint linear (n:nat) (l:list nat) : option nat := 
  match l with 
      nil => None
    | a::m => if zerop a then Some n else linear (S n) m 
  end.

Definition linear_search := linear 0.

Inductive correct : nat -> list nat -> Prop := 
   correct_hd : forall a l, a=0 -> correct 0 (a::l)
 | correct_tl : forall a l n, a<>0 
             -> correct n l -> correct (S n) (a::l).
Hint Constructors correct.

Lemma linear_correct : forall l n k, 
      linear n l = Some k <-> (n <= k /\ correct (k-n) l).
induction l; simpl;intros.
split.
discriminate.
intros (_,H); inversion H.
destruct (zerop a).
split.
intro H; injection H; intro neq.
subst n.
replace (k-k) with 0; auto with zarith.
intros (H1,H2).
assert (k = n)%nat.
inversion H2; try omega.
f_equal; auto.
destruct (IHl (S n) k) as (Hd,Hf); clear IHl.
split.
intro HS; destruct Hd as (H1,H2); clear Hf; trivial.
split; auto with arith.
replace (k - n) with (S (k - (S n)))%nat; auto with zarith.
intros (H1,H2).
assert (S n <= k).
assert (~ k - n = O)%nat.
intro Hkn; rewrite Hkn in H2; inversion H2; auto with zarith.
omega.
apply Hf; split; auto with zarith.
assert (Hkn:k - n = S (k - (S n))); try omega.
rewrite Hkn in H2; inversion H2; auto.
Qed.

Lemma linear_search_correct : forall l k, 
      linear_search l = Some k <-> correct k l.
intros; unfold linear_search.
rewrite (linear_correct l 0 k).
rewrite <- minus_n_O; intuition.
Save.

(* [decrease l] if successive elements 
   do not decrease by more than one *)

Inductive decrease : list nat -> Prop := 
   decrease_nil : decrease nil
 | decrease_cons : forall a b l, 
     decrease (b::l) -> a <= S b -> decrease (a::b::l).
Hint Constructors decrease.


Lemma skip_length : forall A n (l:list A), 
      length (skipn n l) <= length l.
induction n; simpl; auto.
destruct l; auto.
apply le_trans with (length l); simpl;auto.
Qed.
Hint Resolve skip_length.

(** Proving termination *)
Program Fixpoint 
  linear2 (n : nat) (l : list nat) {measure (length l)} 
  : option nat := 
      match l with 
          nil => None
        | a::m => if zerop a then Some n 
                  else linear2 (a+n) (skipn (a-1) m)
      end.
Next Obligation.
intros.
apply le_lt_trans with (length m); simpl; auto with arith.
Defined.

(** Proving functional correctness *)

Lemma decrease_skip 
  : forall n l, decrease l -> decrease (skipn n l).
induction n; auto.
intros l H; inversion H; auto.
simpl skipn; auto.
Qed.


Lemma decrease_correct_skip : 
      forall l, decrease l -> 
      forall m n, n <= hd 0 l -> 
             correct m (skipn n l) -> correct (n+m) l.
induction 1; simpl in *; intros.
assert (n=0); try subst n; auto with arith.
destruct n; auto.
assert (a <> 0); try omega.
simpl skipn in H2.
simpl plus; auto with zarith.
Qed.

Lemma skip_correct 
   : forall n l, correct n l -> 
     forall m, m <= n -> correct (n-m) (skipn m l).
induction 1.
intros; simpl; assert (m = 0); 
  try subst m; simpl; auto with arith.
intros.
destruct m; simpl; auto with arith.
Qed. 
Hint Resolve skip_correct.

Lemma correct_decrease_le : 
   forall k l, correct k l -> decrease l -> hd 0 l <= k.
induction 1; simpl hd in *; intros.
subst; auto.
inversion H1; subst; simpl hd in *; auto with arith.
apply le_trans with (S b); auto with arith.
Qed. 


Program Fixpoint linear3 (n : nat) (l : list nat) 
 { measure (length l) } : 
 { res : option nat | decrease l -> 
   forall k, res = Some k <-> (n <= k /\ correct (k-n) l) }
 := match l with 
           nil  => None
         | a::m => if zerop a then Some n 
                   else linear3 (a+n) (skipn (a-1) m)
              end.
Next Obligation.
split; intro H1.
discriminate H1.
destruct H1 as (_,H1).
inversion H1.
Qed.
Next Obligation.
split; intro H1.
injection H1; intro Heq; subst n; split; auto with arith.
replace (k-k) with 0; auto with arith.
destruct H1 as (H1,H2).
inversion H2.
replace k with n; auto with zarith.
destruct H5; trivial.
Qed.
Next Obligation.
apply le_lt_trans with (length m); simpl; auto with arith.
Qed.
Next Obligation.
destruct 
    (linear3 (a + n) (skipn (a - 1) m))
as (res,Hres); clear linear3; simpl.
assert (Hd : decrease (skipn (a - 1) m)).
apply (decrease_skip (S (a-1)) (l:=a::m)); auto.
destruct Hres with (k:=k) as (H1,H2); clear Hres; trivial.
split; intros.
destruct H1 as (Hle,Hc); clear H2; trivial; split; auto with zarith.
replace (k - n) with (a + (k - (a + n))); try omega.
apply (decrease_correct_skip (l:=a::m)) with (n:=a); auto with arith.
assert (Ha:a = S (a - 1)); try omega.
rewrite Ha at 2; trivial.
destruct H3 as (H4,H5).
assert (a + n <= k).
assert (a <= k - n); auto with zarith.
apply (correct_decrease_le (k:=k-n) (l:=a::m)); auto.
apply H2; split; auto.
change (correct (k - (a + n)) (skipn (S (a-1)) (a:: m))).
replace (S (a-1)) with a; auto with arith.
replace (k - (a + n)) with ((k - n) - a); auto with arith.
apply skip_correct; auto with zarith.
omega.
omega.
Qed.