Library ListChallenges

Require Import ZArith.
Require Import List.
Import Datatypes.
Open Scope Z_scope.

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.
Hint Resolve Zlength_pos : zarith.

Definition is_nil : forall A (l:list A), {l=nil}+{l<>nil}.
Defined.

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)).

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)).

Lemma sum_max_prop : forall l, sum l <= Zlength l * max l.

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.

Require Import Coq.Program.Program.

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.

Extraction max2.

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

Lemma zmax2_spec : forall l, is_max l (zmax2 l).

Lemma ismax_prop : forall l m, is_max l m -> sum l <= Zlength l * m.

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.

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).

Lemma linear_search_correct : forall l k,
      linear_search l = Some k <-> correct k l.


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.
Hint Resolve skip_length.
Require Export Program.

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.

Lemma decrease_skip : forall n l, decrease l -> decrease (skipn n l).

Lemma decrease_correct_skip :
      forall l, decrease l ->
         forall m n, n <= hd 0 l ->
                correct m (skipn n l) -> correct (n+m) l.

Lemma skip_correct
   : forall n l, correct n l -> forall m, m <= n -> correct (n-m) (skipn m l).
Hint Resolve skip_correct.

Lemma correct_decrease_le : forall k l, correct k l -> decrease l -> hd 0 l <= k.

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.