(* -*- coq-prog-args: ("-emacs-U") -*- *)
Require Import Coq.Program.Program.
Require Export Coq.Lists.List.

Set Implicit Arguments.

Notation " [] " := nil.
Notation " [ x ] " := (cons x nil).
Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..).

Section Accessors.
  Variable A : Type.

  Obligations Tactic := idtac.

  Program Definition head : forall (l : list A | length l <> 0), A :=  
    fun l =>
      match l with
        | nil => !
        | hd :: tl => hd
      end.

  Next Obligation.
  Proof.
    intros ; destruct l as [l Hl] ; subst ; simpl in *.
    subst.
    apply Hl.
    simpl.
    reflexivity.
  Qed.
    
  Obligations Tactic := program_simpl.

  Program Definition tail (l : list A | length l <> 0) : list A :=
    match l with
      | nil => !
      | hd :: tl => tl
    end.

  Program Definition test_tail_nil : list A := tail nil.
  Admit Obligations.

  Program Fixpoint last (l : list A | l <> nil) {measure length} : A :=
    match l with 
      | nil => !
      | hd :: nil => hd
      | hd :: tl => last tl
    end.

  Next Obligation.
  Proof.
    clear last.
    red ; intros.
    subst.
    apply (H hd) ; auto.
  Qed.

  Program Fixpoint liat (l : list A | length l <> 0) {measure length} : list A :=
    match l with 
      | nil => !
      | hd :: nil => nil
      | hd :: (_ :: _) as tl => hd :: liat tl
    end.

End Accessors.

Program Definition test_hd : nat := head (cons 1 nil).
Eval compute in test_hd.

Extraction head.
Extraction tail.
Extraction last.

Program Definition test_liat : list nat := liat ([1 ; 3 ; 5]).
Eval lazy in test_liat.

Program Definition test_tail : list nat := tail ([1 ; 3 ; 5]).
Eval lazy in test_tail.


Section app.
  Variable A : Type.

  Program Fixpoint app (l : list A) (l' : list A) { struct l } :
    { r : list A | length r = length l + length l' } :=
    match l with
      | nil => l'
      | hd :: tl => hd :: (tl ++ l')
    end 
    where "x ++ y" := (app x y).

  Next Obligation.
    intros.
    destruct_call app ; program_simpl.
  Defined.
  
  Program Lemma app_id_l : forall l : list A, l = nil ++ l.
  Proof.
    simpl ; auto.
  Qed.
  
  Program Lemma app_id_r : forall l : list A, l = l ++ nil.
  Proof.
    induction l ; simpl ; auto.
    rewrite <- IHl ; auto.
  Qed.

End app.

Section Nth.

  Variable A : Type.

  Program Fixpoint nth (l : list A) (n : nat | n < length l) { struct l } : A := 
    match n, l with
      | 0, hd :: _ => hd
      | S n', _ :: tl => nth tl n'
      | _, nil => !
    end.

  Next Obligation.
  Proof.
    inversion H.
  Defined.
End Nth.

Section Tip.
  Variable A : Type.
  Program Definition tip (a : A) : { l : list A | l <> nil } := (cons a nil).
End Tip.

Section Fold_Left.
  Variable (A B : Type).
  Variable (P : list A -> B -> Prop).
  
  Program Fixpoint fold_left_aux (s : list A) (s' : list A)
    (f : forall (e : { e : A | In e s }) (s' : list A), sig (P s') -> sig (P (s' ++ [e])))
    (i : sig (P s')) { struct s } : sig (P (s' ++ s)) :=
    match s with
      | [] => i
      | hd :: tl => fold_left_aux tl  (fun e s' acc => f e s' acc) (f hd s' i)
    end.
  
  Next Obligation.
  Proof.
    intros.
    simpl_list.
    assumption.
  Qed.
    
  Next Obligation.
  Proof.
    intros.
    destruct_call fold_left_aux ; clear fold_left_aux.
    simpl in *.
    rewrite <- Heq_s.
    rewrite app_ass in p.
    simpl in p.
    assumption.
  Defined.

  Program Definition fold_left
    (s : list A)
    (f : forall (e : { e : A | In e s }) (s' : list A), sig (P s') -> sig (P (s' ++ [e])))
    (i : sig (P [])) : sig (P s) :=
    @fold_left_aux s [] f i.

End Fold_Left.

Section Fold_Right.
  Variable (A B : Type).
  Variable (P : list A -> B -> Prop).

  Program Fixpoint fold_right (s : list A)
    (f : forall (s' : list A), sig (P s') -> forall (e : { e : A | In e s }), sig (P (e :: s')))
    (i : sig (P [])) { struct s } : sig (P s) :=
    match s with
      | [] => i
      | hd :: tl => f tl (fold_right tl (fun e s' acc => f e s' acc) i) hd
    end.
    
  Next Obligation.
  Proof.
    intros.
    destruct_call f ; clear fold_right.
    simpl in *.
    rewrite <- Heq_s ; assumption.
  Defined.
  
End Fold_Right.

(*Section Map.
  Variable A B : Type.
  Variable l : list A.
  Variable f : { x : A | In x l } -> B.

  Definition sub_list (A : Type) (l' l : list A) := (forall v, In v l' -> In v l) /\ length l' <= length l.
  
  Lemma sub_list_tl : forall A : Type, forall x (l l' : list A), sub_list (x :: l) l' -> sub_list l l'.
  Proof.
    intros.
    inversion H.
    split.
    intros.
    apply H0.
    auto with datatypes.
    auto with arith.
  Qed.

  Obligations Tactic := unfold sub_list in * ; 
    program_simpl.

  Program Fixpoint map_rec ( l' : list A | sub_list l' l )
    { measure length l' } : { r : list B | 
      length r = length l' /\
      forall { x : A | In x l' }, In (f x) r } :=
    match l' with
      | nil => nil
      | cons x tl => let tl' := map_rec tl in f x :: tl'
    end.

  Solve Obligations using unfold sub_list in * ; program_simpl ; intuition.
    
  Next Obligation.
  Proof.
    intros.
    split ; intros ; auto.
    destruct x.
    inversion i.
  Qed.

  Next Obligation.
  Proof.
    intros.
    destruct_call map_rec.
    simpl in *.
    program_simpl.
    split.
    rewrite <- Heq_l'.
    simpl ; auto.

    intro.
    destruct x1.
    simpl.
    assert(j:=i).
    rewrite <- Heq_l' in j.
    destruct j ; subst*.
    left ; auto.
    f_equal ; f_equal ; apply proof_irrelevance.

    right.
    pose (H1 (exist _ x1 H2)).
    simpl in i0.
    
    (* Really need PI *)

    rewrite (proof_irrelevance _ i).
    
    intuition.


    intros l'.
    intros.
    intros x.
  Admitted.
    destruct x.
    destruct l'.

    destruct_call map_rec.
    simpl in *.
    subst l'.
    simpl ; auto with arith.
  Qed.
      
  Program Definition map : list V := map_rec l.
    
End Map_DependentRecursor.

*)