Require Import Bool.
Require Import Sumbool.
Require Import ZArith.
Require Import Arith.
Require Import Addr.
Require Import Adist.
Require Import Addec.
Require Import Map.
Require Import Fset.
Section AdAlloc.
Variable A : Set.
Definition nat_of_ad (a:ad) :=
match a with
| ad_z => 0
| ad_x p => nat_of_P p
end.
Fixpoint nat_le (m:nat) : nat -> bool :=
match m with
| O => fun _:nat => true
| S m' =>
fun n:nat => match n with
| O => false
| S n' => nat_le m' n'
end
end.
Lemma nat_le_correct : forall m n:nat, m <= n -> nat_le m n = true.
Proof.
induction m as [| m IHm]. trivial.
destruct n. intro H. elim (le_Sn_O _ H).
intros. simpl in |- *. apply IHm. apply le_S_n. assumption.
Qed.
Lemma nat_le_complete : forall m n:nat, nat_le m n = true -> m <= n.
Proof.
induction m. trivial with arith.
destruct n. intro H. discriminate H.
auto with arith.
Qed.
Lemma nat_le_correct_conv : forall m n:nat, m < n -> nat_le n m = false.
Proof.
intros. elim (sumbool_of_bool (nat_le n m)). intro H0.
elim (lt_irrefl _ (lt_le_trans _ _ _ H (nat_le_complete _ _ H0))).
trivial.
Qed.
Lemma nat_le_complete_conv : forall m n:nat, nat_le n m = false -> m < n.
Proof.
intros. elim (le_or_lt n m). intro. conditional trivial rewrite nat_le_correct in H. discriminate H.
trivial.
Qed.
Definition ad_of_nat (n:nat) :=
match n with
| O => ad_z
| S n' => ad_x (P_of_succ_nat n')
end.
Lemma ad_of_nat_of_ad : forall a:ad, ad_of_nat (nat_of_ad a) = a.
Proof.
destruct a as [| p]. reflexivity.
simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H.
rewrite nat_of_P_inj with (1 := H). reflexivity.
Qed.
Lemma nat_of_ad_of_nat : forall n:nat, nat_of_ad (ad_of_nat n) = n.
Proof.
induction n. trivial.
intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.
Definition ad_le (a b:ad) := nat_le (nat_of_ad a) (nat_of_ad b).
Lemma ad_le_refl : forall a:ad, ad_le a a = true.
Proof.
intro. unfold ad_le in |- *. apply nat_le_correct. apply le_n.
Qed.
Lemma ad_le_antisym :
forall a b:ad, ad_le a b = true -> ad_le b a = true -> a = b.
Proof.
unfold ad_le in |- *. intros. rewrite <- (ad_of_nat_of_ad a). rewrite <- (ad_of_nat_of_ad b).
rewrite (le_antisym _ _ (nat_le_complete _ _ H) (nat_le_complete _ _ H0)). reflexivity.
Qed.
Lemma ad_le_trans :
forall a b c:ad, ad_le a b = true -> ad_le b c = true -> ad_le a c = true.
Proof.
unfold ad_le in |- *. intros. apply nat_le_correct. apply le_trans with (m:= nat_of_ad b).
apply nat_le_complete. assumption.
apply nat_le_complete. assumption.
Qed.
Lemma ad_le_lt_trans :
forall a b c:ad,
ad_le a b = true -> ad_le c b = false -> ad_le c a = false.
Proof.
unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply le_lt_trans with (m:= nat_of_ad b).
apply nat_le_complete. assumption.
apply nat_le_complete_conv. assumption.
Qed.
Lemma ad_lt_le_trans :
forall a b c:ad,
ad_le b a = false -> ad_le b c = true -> ad_le c a = false.
Proof.
unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply lt_le_trans with (m:= nat_of_ad b).
apply nat_le_complete_conv. assumption.
apply nat_le_complete. assumption.
Qed.
Lemma ad_lt_trans :
forall a b c:ad,
ad_le b a = false -> ad_le c b = false -> ad_le c a = false.
Proof.
unfold ad_le in |- *. intros. apply nat_le_correct_conv. apply lt_trans with (m:= nat_of_ad b).
apply nat_le_complete_conv. assumption.
apply nat_le_complete_conv. assumption.
Qed.
Lemma ad_lt_le_weak : forall a b:ad, ad_le b a = false -> ad_le a b = true.
Proof.
unfold ad_le in |- *. intros. apply nat_le_correct. apply lt_le_weak.
apply nat_le_complete_conv. assumption.
Qed.
Definition ad_min (a b:ad) := if ad_le a b then a else b.
Lemma ad_min_choice : forall a b:ad, {ad_min a b = a} + {ad_min a b = b}.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. left. rewrite H.
reflexivity.
intro H. right. rewrite H. reflexivity.
Qed.
Lemma ad_min_le_1 : forall a b:ad, ad_le (ad_min a b) a = true.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. rewrite H.
apply ad_le_refl.
intro H. rewrite H. apply ad_lt_le_weak. assumption.
Qed.
Lemma ad_min_le_2 : forall a b:ad, ad_le (ad_min a b) b = true.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le a b)). intro H. rewrite H. assumption.
intro H. rewrite H. apply ad_le_refl.
Qed.
Lemma ad_min_le_3 :
forall a b c:ad, ad_le a (ad_min b c) = true -> ad_le a b = true.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H.
assumption.
intro H0. rewrite H0 in H. apply ad_lt_le_weak. apply ad_le_lt_trans with (b:= c); assumption.
Qed.
Lemma ad_min_le_4 :
forall a b c:ad, ad_le a (ad_min b c) = true -> ad_le a c = true.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H.
apply ad_le_trans with (b:= b); assumption.
intro H0. rewrite H0 in H. assumption.
Qed.
Lemma ad_min_le_5 :
forall a b c:ad,
ad_le a b = true -> ad_le a c = true -> ad_le a (ad_min b c) = true.
Proof.
intros. elim (ad_min_choice b c). intro H1. rewrite H1. assumption.
intro H1. rewrite H1. assumption.
Qed.
Lemma ad_min_lt_3 :
forall a b c:ad, ad_le (ad_min b c) a = false -> ad_le b a = false.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H.
assumption.
intro H0. rewrite H0 in H. apply ad_lt_trans with (b:= c); assumption.
Qed.
Lemma ad_min_lt_4 :
forall a b c:ad, ad_le (ad_min b c) a = false -> ad_le c a = false.
Proof.
unfold ad_min in |- *. intros. elim (sumbool_of_bool (ad_le b c)). intro H0. rewrite H0 in H.
apply ad_lt_le_trans with (b:= b); assumption.
intro H0. rewrite H0 in H. assumption.
Qed.
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 => ad_z
| M1 a _ => if ad_eq a ad_z then ad_x 1 else ad_z
| M2 m1 m2 =>
ad_min (ad_double (ad_alloc_opt m1))
(ad_double_plus_un (ad_alloc_opt m2))
end.
Lemma ad_alloc_opt_allocates_1 :
forall m:Map A, MapGet A m (ad_alloc_opt m) = NONE A.
Proof.
induction m as [| a| m0 H m1 H0]. reflexivity.
simpl in |- *. elim (sumbool_of_bool (ad_eq a ad_z)). intro H. rewrite H.
rewrite (ad_eq_complete _ _ H). reflexivity.
intro H. rewrite H. rewrite H. reflexivity.
intros. change
(ad_alloc_opt (M2 A m0 m1)) with (ad_min (ad_double (ad_alloc_opt m0))
(ad_double_plus_un (ad_alloc_opt m1)))
in |- *.
elim
(ad_min_choice (ad_double (ad_alloc_opt m0))
(ad_double_plus_un (ad_alloc_opt m1))).
intro H1. rewrite H1. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption.
apply ad_double_bit_0.
intro H1. rewrite H1. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2. assumption.
apply ad_double_plus_un_bit_0.
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 nat_of_ad_double :
forall a:ad, nat_of_ad (ad_double a) = 2 * nat_of_ad a.
Proof.
destruct a as [| p]. trivial.
exact (nat_of_P_xO p).
Qed.
Lemma nat_of_ad_double_plus_un :
forall a:ad, nat_of_ad (ad_double_plus_un a) = S (2 * nat_of_ad a).
Proof.
destruct a as [| p]. trivial.
exact (nat_of_P_xI p).
Qed.
Lemma ad_le_double_mono :
forall a b:ad,
ad_le a b = true -> ad_le (ad_double a) (ad_double b) = true.
Proof.
unfold ad_le in |- *. intros. rewrite nat_of_ad_double. rewrite nat_of_ad_double. apply nat_le_correct.
simpl in |- *. apply plus_le_compat. apply nat_le_complete. assumption.
apply plus_le_compat. apply nat_le_complete. assumption.
apply le_n.
Qed.
Lemma ad_le_double_plus_un_mono :
forall a b:ad,
ad_le a b = true ->
ad_le (ad_double_plus_un a) (ad_double_plus_un b) = true.
Proof.
unfold ad_le in |- *. intros. rewrite nat_of_ad_double_plus_un. rewrite nat_of_ad_double_plus_un.
apply nat_le_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply nat_le_complete.
assumption.
apply plus_le_compat. apply nat_le_complete. assumption.
apply le_n.
Qed.
Lemma ad_le_double_mono_conv :
forall a b:ad,
ad_le (ad_double a) (ad_double b) = true -> ad_le a b = true.
Proof.
unfold ad_le in |- *. intros a b. rewrite nat_of_ad_double. rewrite nat_of_ad_double. intro.
apply nat_le_correct. apply (mult_S_le_reg_l 1). apply nat_le_complete. assumption.
Qed.
Lemma ad_le_double_plus_un_mono_conv :
forall a b:ad,
ad_le (ad_double_plus_un a) (ad_double_plus_un b) = true ->
ad_le a b = true.
Proof.
unfold ad_le in |- *. intros a b. rewrite nat_of_ad_double_plus_un. rewrite nat_of_ad_double_plus_un.
intro. apply nat_le_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply nat_le_complete.
assumption.
Qed.
Lemma ad_lt_double_mono :
forall a b:ad,
ad_le a b = false -> ad_le (ad_double a) (ad_double b) = false.
Proof.
intros. elim (sumbool_of_bool (ad_le (ad_double a) (ad_double b))). intro H0.
rewrite (ad_le_double_mono_conv _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma ad_lt_double_plus_un_mono :
forall a b:ad,
ad_le a b = false ->
ad_le (ad_double_plus_un a) (ad_double_plus_un b) = false.
Proof.
intros. elim (sumbool_of_bool (ad_le (ad_double_plus_un a) (ad_double_plus_un b))). intro H0.
rewrite (ad_le_double_plus_un_mono_conv _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma ad_lt_double_mono_conv :
forall a b:ad,
ad_le (ad_double a) (ad_double b) = false -> ad_le a b = false.
Proof.
intros. elim (sumbool_of_bool (ad_le a b)). intro H0. rewrite (ad_le_double_mono _ _ H0) in H.
discriminate H.
trivial.
Qed.
Lemma ad_lt_double_plus_un_mono_conv :
forall a b:ad,
ad_le (ad_double_plus_un a) (ad_double_plus_un b) = false ->
ad_le a b = false.
Proof.
intros. elim (sumbool_of_bool (ad_le a b)). intro H0.
rewrite (ad_le_double_plus_un_mono _ _ H0) in H. discriminate H.
trivial.
Qed.
Lemma ad_alloc_opt_optimal_1 :
forall (m:Map A) (a:ad),
ad_le (ad_alloc_opt m) a = false -> {y : A | MapGet A m a = SOME A y}.
Proof.
induction m as [| a y| m0 H m1 H0]. simpl in |- *. unfold ad_le in |- *. simpl in |- *. intros. discriminate H.
simpl in |- *. intros b H. elim (sumbool_of_bool (ad_eq a ad_z)). intro H0. rewrite H0 in H.
unfold ad_le in H. cut (ad_z = b). intro. split with y. rewrite <- H1. rewrite H0. reflexivity.
rewrite <- (ad_of_nat_of_ad b).
rewrite <- (le_n_O_eq _ (le_S_n _ _ (nat_le_complete_conv _ _ H))). reflexivity.
intro H0. rewrite H0 in H. discriminate H.
intros. simpl in H1. elim (ad_double_or_double_plus_un a). intro H2. elim H2. intros a0 H3.
rewrite H3 in H1. elim (H _ (ad_lt_double_mono_conv _ _ (ad_min_lt_3 _ _ _ H1))). intros y H4.
split with y. rewrite H3. rewrite MapGet_M2_bit_0_0. rewrite ad_double_div_2. assumption.
apply ad_double_bit_0.
intro H2. elim H2. intros a0 H3. rewrite H3 in H1.
elim (H0 _ (ad_lt_double_plus_un_mono_conv _ _ (ad_min_lt_4 _ _ _ H1))). intros y H4.
split with y. rewrite H3. rewrite MapGet_M2_bit_0_1. rewrite ad_double_plus_un_div_2.
assumption.
apply ad_double_plus_un_bit_0.
Qed.
Lemma ad_alloc_opt_optimal :
forall (m:Map A) (a:ad),
ad_le (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.