Require Import Arith.
Require Import ZArith.
Set Implicit Arguments.
Require Import List.

Definition adr := option Z.
Definition null : adr := None.

Record node : Type 
  := mknode { value : nat ; next : adr}.

Definition heap := Z -> option node.

Definition val (h : heap) (a : adr) : option node
  := match a with None => None | Some z => h z end.

Lemma val_simpl_some : forall h z, val h (Some z) = h z.
trivial.
Qed.

(** Using type classes to hide the argument that the adress
    is allocated *)
Definition is_alloc A (a:option A) : Prop 
 := match a with Some _ => True | None  => False end.

Class alloc {A} (a:option A) := Alloc : is_alloc a.

(** Access as a partial function *)
Definition access (h:heap) (a:adr) 
  : forall p : alloc (val h a), node 
  := match (val h a) as x return alloc x -> node
     with None   => fun (H:False) => False_rect _ H
        | Some n => fun (H:True)  => n
     end.

Implicit Arguments access [[p]].

Lemma access_val (h:heap) (a:adr) {p:alloc (val h a)} : 
      forall z, val h a = Some z -> access h a = z.
unfold access; intros.
generalize p; rewrite H; trivial.
Save.

Lemma alloc_val (h:heap) (a:adr) 
  : forall z, val h a = Some z -> alloc (val h a).
intros z H; rewrite H; simpl; trivial.
Save.


(** an address corresponds to a linked lists if when not a null address, 
   it is allocated in the heap and the next address is itself a linked list
*)

Inductive LList (h : heap) (a:adr) :  Prop := 
  mkLL : forall (LLa : alloc a -> alloc (val h a)),
  (forall (p:alloc a), LList h (next (access h a)))
   -> LList h a.

Lemma LL_null : forall h, LList h null.
  intro.
  assert (LLa:alloc null -> alloc (val h null)); trivial. 
  apply mkLL with (LLa:=LLa); contradiction.
Save.

Lemma LL_cons : forall h a {q:alloc (val h a)},
      LList h (next (access h a)) -> LList h a.
intros;
apply mkLL with (LLa:=fun _ => q); auto.
Save.

Instance LL_alloc_val {h} {a} (L:LList h a) {p:alloc a}
   : alloc (val h a).
destruct L; auto.
Defined.

Lemma LL_next : forall h a (L:LList h a) {p:alloc a}, 
         LList h (next (access h a (p:=LL_alloc_val L))).
unfold LL_alloc_val; destruct L; trivial.
Defined.

Definition nullp (a:adr) : {a=null}+{alloc a}.
destruct a; simpl; auto.
Defined.


Section IsLLlist_rec.
Variable h : heap.
Variable P : adr -> Type.
Variable Pnull : forall a, a=null -> P a.
Variable Pnext : forall a (q:alloc (val h a)), 
                 P (next (access h a)) -> P a.
Implicit Arguments Pnext [[q]].

Fixpoint LL_rec (a:adr) (La : LList h a) : P a :=
    match nullp a with 
       left  p => Pnull p
     | right p => Pnext a (LL_rec (LL_next La))
    end.

(* Implicit Arguments LL_rec []. *)

Lemma LL_rec_eq : forall (a:adr) (La : LList h a),
     LL_rec La = match nullp a with 
       left  p => Pnull p
     | right p => Pnext a (LL_rec (LL_next La))
    end.
destruct La; trivial.
Qed.

End IsLLlist_rec.
Implicit Arguments LL_rec [].

Section LinearSearch.
Variable h : heap.

Fixpoint LL_list (a:adr) (La: LList h a) : list nat := 
     match nullp a with 
       left  p => nil
     | right p => value (access h a (p:=LL_alloc_val La))
                  ::LL_list (LL_next La)
     end.


Fixpoint LL_linear (a:adr) (La: LList h a) (n:nat) : option nat := 
   match nullp a with 
       left  p => None
     | right p => if zerop (value (access h a (p:=LL_alloc_val La))) 
                     then Some n 
                     else LL_linear (LL_next La) (S n)
   end.

Lemma LL_list_eq : forall (a:adr) (La: LList h a), 
      LL_list La = match nullp a with 
       left  p => nil
     | right p => value (access h a (p:=LL_alloc_val La))
                  ::LL_list (LL_next La)
     end.
destruct La; trivial.
Qed.

Lemma LL_linear_eq : forall (a:adr) (La: LList h a) (n:nat), 
   LL_linear La n = match nullp a with 
       left  p => None
     | right p => if zerop (value (access h a (p:=LL_alloc_val La))) 
                     then Some n 
                     else LL_linear (LL_next La) (S n)
   end.
destruct La; trivial.
Qed.

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.

Scheme LList_indd := Induction for LList Sort Prop.

Lemma linear_correct : forall a (La:LList h a) n k, 
      LL_linear La n = Some k <-> (n <= k /\ correct (k-n) (LL_list La)).
induction La using LList_indd; simpl; intros.
case (nullp a); intros.
split; intros; try discriminate.
destruct H0 as (_,H0); inversion H0.
destruct (zerop (value (access h a))).
split;[intro H1; injection H1; intro; subst n; split; auto | intros (H1,H2)].
replace (k-k) with 0; auto with arith.
inversion H2; subst.
assert (n=k); try omega; f_equal; trivial.
contradiction.
destruct (H a0 (S n) k) as (Hl,Hr).
split;[intro H1| intros (H1,H2)].
destruct (Hl H1) as (Hle,Hc); clear Hl Hr.
split; auto with arith.
replace (k - n) with (S (k - (S n))); auto with zarith.
inversion H2; subst.
exfalso; omega.
assert (S n <= k); try omega.
assert (n0 = k - S n); try omega.
subst n0; auto with arith.
Qed.

End LinearSearch.
Extraction LL_linear.

Definition upd_node_val n v := mknode v (next n).
Definition upd_node_next n a := mknode (value n) a.

Definition upd_heap (h:heap) a n : heap := 
    match a with None => h 
               | Some za => fun z => if Z_eq_dec z za then n else h z
    end.

Definition adr_eq_dec : forall (a b:adr), {a=b}+{~a=b}.
destruct a; destruct b; auto; try (right; discriminate).
case (Z_eq_dec z z0); intros; try subst; auto.
right; intro Hs; apply n; injection Hs; trivial.
Defined.

Definition upd_heap_val (h:heap) a v {p : alloc (val h a)} : heap := 
    fun z => if adr_eq_dec (Some z) a then Some (upd_node_val (access h a) v) else h z.

Definition upd_heap_next (h:heap) a b {p : alloc (val h a)} : heap := 
    fun z => if adr_eq_dec (Some z) a then Some (upd_node_next (access h a) b) else h z.

(** Every allocated address stays allocated **)
Lemma upd_heap_next_alloc (h:heap) a b {p : alloc (val h a)} (c:adr) : 
      alloc (val h c) -> alloc (val (upd_heap_next h a b) c).
unfold upd_heap_next,val.
destruct c; trivial.
destruct (adr_eq_dec (Some z) a); simpl; auto.
Defined.

Lemma upd_heap_next_diff (h:heap) a b {p : alloc (val h a)} (c:adr) : 
      c<>a ->
      val (upd_heap_next h a b) c = val h c.
unfold upd_heap_next; intros.
destruct c; trivial.
unfold val.
case (adr_eq_dec (Some z) a); auto || contradiction.
Qed.

Lemma upd_heap_next_eq (h:heap) a b {p : alloc (val h a)} : 
      val (upd_heap_next h a b) a = Some (mknode (value (access h a)) b).
unfold upd_heap_next; intros.
destruct a.
rewrite val_simpl_some.
destruct (adr_eq_dec (Some z) (Some z)); simpl; auto.
destruct n; trivial.
destruct p.
Qed.

Instance eq_val_alloc h1 h2 a {p1:alloc (val h1 a)} : val h1 a = val h2 a 
     -> alloc (val h2 a).
intros H; destruct H; trivial.
Defined.

Lemma eq_val_access_gen
  : forall h1 h2 a (_:val h1 a = val h2 a) 
    {Hp:alloc (val h1 a)} {Hq : alloc (val h2 a)},
    access h1 a = access h2 a.
unfold access; destruct 1.
destruct (val h1 a); auto.
destruct Hp.
Qed.

Lemma eq_val_access : 
  forall h1 h2 a (Hv:val h1 a = val h2 a) 
  {Hp:alloc (val h1 a)},
  access h1 a = access h2 a (p:=eq_val_alloc h1 h2 a Hv).
intros; apply eq_val_access_gen; trivial.
Save.

Lemma upd_heap_next_access (h:heap) a b 
      {p : alloc (val h a)}
      {q:alloc (val (upd_heap_next h a b) a)} : 
      next (access (upd_heap_next h a b) a) = b.
intros; rewrite access_val 
  with (z:=mknode (value (access h a)) b); auto.
apply upd_heap_next_eq.
Save.