Library LinkedLists
Require Import Arith.
Require Import ZArith.
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.
Require Import ZArith.
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.
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.
:= 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.
Lemma alloc_val (h:heap) (a:adr)
: forall z, val h a = Some z -> alloc (val h a).
: 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.
Lemma alloc_val (h:heap) (a:adr)
: forall z, val h a = Some z -> alloc (val h a).
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.
Lemma LL_cons : forall h a {q:alloc (val h a)},
LList h (next (access h a)) -> LList h a.
Instance LL_alloc_val {h} {a} (L:LList h a) {p:alloc a}
: alloc (val h a).
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))).
Definition nullp (a:adr) : {a=null}+{alloc a}.
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.
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.
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.
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.
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)).
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}.
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).
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.
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).
Instance eq_val_alloc h1 h2 a {p1:alloc (val h1 a)} : val h1 a = val h2 a
-> alloc (val h2 a).
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.
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).
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.
alloc (val h c) -> alloc (val (upd_heap_next h a b) c).
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.
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).
Instance eq_val_alloc h1 h2 a {p1:alloc (val h1 a)} : val h1 a = val h2 a
-> alloc (val h2 a).
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.
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).
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.