(* A purely functional version of random access lists *)
(* From Chris Okasaki's book *)
(* Explanations given in series_advanced2_ralist.pdf *)

Definition TO_BE_REMOVED {T: Type} : T. Admitted.

Arguments minus n m : simpl nomatch.

Fixpoint leb m n :=
  match m, n with
  | O, _ => true
  | S _, O => false
  | S m, S n => leb m n
  end.

Arguments leb m n : simpl nomatch.

Fixpoint eqb m n :=
  match m, n with
  | O, O => true
  | S m, S n => eqb m n
  | _, _ => false
  end.

Arguments eqb m n : simpl nomatch.

Lemma eqb_correct :
  forall m n,
  if eqb m n then m = n else m <> n.
Proof.
Admitted.

(* The following lines turn Boolean statements into Prop *)
Notation "m <= n" := (leb m n).
Notation "m < n" := (leb (S m) n).
Notation "m == n" := (eqb m n) (at level 70, no associativity).
Coercion is_true : bool >-> Sortclass.
Print is_true.

Lemma lt_le_neq :
  forall m n, m <= n -> m <> n -> m < n.
Proof.
Admitted.

Lemma le_lt :
  forall m n, m < n -> m <= n.
Proof.
Admitted.

Lemma le_refl :
  forall n, n <= n.
Proof.
Admitted.

Lemma le_trans :
  forall m n p, m <= n -> n <= p -> m <= p.
Proof.
Admitted.

Lemma le_S :
  forall m, m <= S m.
Proof.
Admitted.

Lemma plus_0_r :
  forall m, m + 0 = m.
Proof.
Admitted.

Lemma minus_0_r :
  forall m, m - 0 = m.
Proof.
Admitted.

Lemma lt_plus :
  forall m n p, m < p -> m < n + p.
Proof.
Admitted.

Lemma lt_minus :
  forall m n p, (n <= m) -> (m - n < p) = (m < n + p).
Proof.
Admitted.

Lemma minus_plus :
  forall m n p, m - (n + p) = m - n - p.
Proof.
Admitted.

Lemma le_not_lt :
  forall m n, (m <= n) = negb (n < m).
Proof.
Admitted.

Require Import List.

Section StandardList.

Definition head {T : Type} (l : list T) : option T :=
  match l with
  | nil => None
  | cons h _ => Some h
  end.

Definition tail {T : Type} (l : list T) : list T :=
  match l with
  | nil => nil
  | cons h q => q
  end.

Fixpoint get {T : Type} (l : list T) (n : nat) {struct l} : option T :=
  match l with
  | nil => None
  | cons h q =>
    if n == 0 then Some h else get q (n - 1)
  end.

Fixpoint set {T : Type} (l : list T) (n : nat) (v : T) {struct l} : list T :=
  match l with
  | nil => l
  | cons h q =>
    if n == 0 then cons v q else cons h (set q (n - 1) v)
  end.

End StandardList.

Section RandomAccessList.

Variable T : Type.

Inductive tree :=
  | Leaf : T -> tree
  | Node : T -> tree -> tree -> tree.

Fixpoint height t :=
  match t with
  | Leaf _ => O
  | Node _ t1 _ => 1 + height t1
  end.

Fixpoint balanced t :=
  match t with
  | Leaf _ => True
  | Node _ t1 t2 =>
    height t1 = height t2 /\ balanced t1 /\ balanced t2
  end.

Inductive ralist :=
  | raNil : ralist
  | raCons : tree -> nat -> ralist -> ralist.

Fixpoint abs_tree (t : tree) {struct t} : list T :=
  match t with
  | Leaf x => cons x nil
  | Node x t1 t2 => cons x (app (abs_tree t1) (abs_tree t2))
  end.

Fixpoint abs (l : ralist) {struct l} : list T :=
  match l with
  | raNil => nil
  | raCons t _ q => app (abs_tree t) (abs q)
  end.

Definition rahead (l : ralist) : option T :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma rahead_correct :
  forall l : ralist,
  rahead l = head (abs l).
Proof.
Admitted.

Definition racons (x : T) (l : ralist) : ralist :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma racons_correct :
  forall (x : T) (l : ralist),
  abs (racons x l) = cons x (abs l).
Proof.
Admitted.

Definition ratail (l : ralist) : ralist :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma ratail_correct :
  forall l : ralist,
  abs (ratail l) = tail (abs l).
Proof.
Admitted.

Lemma head_cons :
  forall l (x:T),
  head (cons x l) = Some x.
Proof.
Admitted.

Lemma tail_cons :
  forall l (x:T),
  tail (cons x l) = l.
Proof.
Admitted.

Fixpoint structured_aux l h :=
  match l with
  | raNil => True
  | raCons t h' q =>
    balanced t /\ height t = h' /\ h <= h' /\
    structured_aux q (1 + h')
  end.

Definition structured l :=
  match l with
  | raNil => True
  | raCons t h q =>
    balanced t /\ height t = h /\
    structured_aux q h
  end.

Lemma structured_aux_le :
  forall l h1 h2,
  h2 <= h1 ->
  structured_aux l h1 ->
  structured_aux l h2.
Proof.
Admitted.

Lemma structured_structured_aux :
  forall l h,
  structured_aux l h ->
  structured l.
Proof.
Admitted.

Lemma structured_cons :
  forall l (x:T),
  structured l ->
  structured (racons x l).
Proof.
Admitted.

Lemma structured_tail :
  forall l,
  structured l ->
  structured (ratail l).
Proof.
Admitted.

Fixpoint height2size h :=
  match h with
  | O => 1
  | S h' => let s' := height2size h' in 1 + (s' + s')
  end.

Fixpoint tree_get t h n :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Fixpoint raget l n :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma get_tail :
  forall l n,
  structured l ->
  raget l (1 + n) = raget (ratail l) n.
Proof.
Admitted.

Fixpoint size l :=
  match l with
  | raNil => 0
  | raCons t h q => height2size h + size q
  end.

Fixpoint tree_set t h n v :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma tree_get_set_eq :
  forall t n v,
  n < height2size (height t) ->
  balanced t ->
  tree_get (tree_set t (height t) n v) (height t) n = Some v.
Proof.
Admitted.

Fixpoint raset l n v :=
  (* FILL IN HERE *) TO_BE_REMOVED.

Lemma get_set_eq :
  forall l n v,
  structured l ->
  n < size l ->
  raget (raset l n v) n = Some v.
Proof.
Admitted.

End RandomAccessList.

Extract Inductive bool => "bool" [ "true" "false" ].

Extract Inductive option => "option" [ "Some" "None" ].

Extract Inductive nat => "int" [ "0" "succ" ]
  "(fun fO fS n -> if n=0 then fO () else fS (n-1))".

Extract Inlined Constant plus => "(+)".
Extract Inlined Constant minus => "(-)".
Extract Inlined Constant leb => "(<=)".
Extract Inlined Constant eqb => "(==)".

Recursive Extraction raget.