Library Coq.IntMap.Adalloc
Require Import Bool.
Require Import Sumbool.
Require Import Arith.
Require Import NArith.
Require Import Ndigits.
Require Import Ndec.
Require Import Nnat.
Require Import Map.
Require Import Fset.
Section AdAlloc.
Variable A : Set.
Allocator: returns an address not in the domain of
m.
This allocator is optimal in that it returns the lowest possible address,
in the usual ordering on integers. It is not the most efficient, however.
Fixpoint ad_alloc_opt (m:Map A) : ad :=
match m with
| M0 => N0
| M1 a _ => if Neqb a N0 then Npos 1 else N0
| M2 m1 m2 =>
Nmin (Ndouble (ad_alloc_opt m1))
(Ndouble_plus_one (ad_alloc_opt m2))
end.
Lemma ad_alloc_opt_allocates_1 :
forall m:Map A, MapGet A m (ad_alloc_opt m) = None.
Proof.
induction m as [| a| m0 H m1 H0]. reflexivity.
simpl in |- *. elim (sumbool_of_bool (Neqb a N0)). intro H. rewrite H.
rewrite (Neqb_complete _ _ H). reflexivity.
intro H. rewrite H. rewrite H. reflexivity.
intros. change
(ad_alloc_opt (M2 A m0 m1)) with (Nmin (Ndouble (ad_alloc_opt m0))
(Ndouble_plus_one (ad_alloc_opt m1)))
in |- *.
elim
(Nmin_choice (Ndouble (ad_alloc_opt m0))
(Ndouble_plus_one (ad_alloc_opt m1))).
intro H1. rewrite H1. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption.
apply Ndouble_bit0.
intro H1. rewrite H1. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2. assumption.
apply Ndouble_plus_one_bit0.
Qed.
Lemma ad_alloc_opt_allocates :
forall m:Map A, in_dom A (ad_alloc_opt m) m = false.
Proof.
unfold in_dom in |- *. intro. rewrite (ad_alloc_opt_allocates_1 m). reflexivity.
Qed.
Moreover, this is optimal: all addresses below
(ad_alloc_opt m)
are in dom m:
Lemma ad_alloc_opt_optimal_1 :
forall (m:Map A) (a:ad),
Nle (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = Some y}.
Proof.
induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold Nle in |- *. simpl in |- *. intros. discriminate H.
simpl in |- *. intros b H. elim (sumbool_of_bool (Neqb a N0)). intro H0. rewrite H0 in H.
unfold Nle in H. cut (N0 = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity.
rewrite <- (N_of_nat_of_N b).
rewrite <- (le_n_O_eq _ (le_S_n _ _ (leb_complete_conv _ _ H))). reflexivity.
intro H0. rewrite H0 in H. discriminate H.
intros. simpl in H1. elim (Ndouble_or_double_plus_un a). intro H2. elim H2. intros a0 H3.
rewrite H3 in H1. elim (H _ (Nlt_double_mono_conv _ _ (Nmin_lt_3 _ _ _ H1))). intros y H4.
split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite Ndouble_div2. assumption.
apply Ndouble_bit0.
intro H2. elim H2. intros a0 H3. rewrite H3 in H1.
elim (H0 _ (Nlt_double_plus_one_mono_conv _ _ (Nmin_lt_4 _ _ _ H1))). intros y H4.
split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite Ndouble_plus_one_div2.
assumption.
apply Ndouble_plus_one_bit0.
Qed.
Lemma ad_alloc_opt_optimal :
forall (m:Map A) (a:ad),
Nle (ad_alloc_opt m) a = false -> in_dom A a m = true.
Proof.
intros. unfold in_dom in |- *. elim (ad_alloc_opt_optimal_1 m a H). intros y H0. rewrite H0.
reflexivity.
Qed.
End AdAlloc.