Ajout lemmes arithmetiques

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1557 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 363 insertions, 0 deletions

diff --git a/theories/IntMap/Adalloc.v b/theories/IntMap/Adalloc.v
new file mode 100644
index 000000000..58d02676e
--- /dev/null
+++ b/theories/IntMap/Adalloc.v
@@ -0,0 +1,363 @@
+
+Require Bool.
+Require Sumbool.
+Require ZArith.
+Require Arith.
+Require Addr.
+Require Adist.
+Require Addec.
+Require Map.
+Require Fset.
+
+Section AdAlloc.
+
+  Variable A : Set.
+
+  Definition nat_of_ad := [a:ad] Cases a of
+                                     ad_z => O
+				   | (ad_x p) => (convert p)
+			         end.
+
+  Fixpoint nat_le [m:nat] : nat -> bool :=
+    Cases m of
+        O => [_:nat] true
+      | (S m') => [n:nat] Cases n of
+                              O => false
+			    | (S n') => (nat_le m' n')
+			  end
+    end.
+
+  Lemma nat_le_correct : (m,n:nat) (le m n) -> (nat_le m n)=true.
+  Proof.
+    Induction m. Trivial.
+    Induction n0. Intro. Elim (le_Sn_O ? H0).
+    Intros. Simpl. Apply H. Apply le_S_n. Assumption.
+  Qed.
+
+  Lemma nat_le_complete : (m,n:nat) (nat_le m n)=true -> (le m n).
+  Proof.
+    Induction m. Trivial with arith.
+    Induction n0. Intro. Discriminate H0.
+    Auto with arith.
+  Qed.
+
+  Lemma nat_le_correct_conv : (m,n:nat) (lt m n) -> (nat_le n m)=false.
+  Proof.
+    Intros. Elim (sumbool_of_bool (nat_le n m)). Intro H0.
+    Elim (lt_n_n ? (lt_le_trans ? ? ? H (nat_le_complete ? ? H0))).
+    Trivial.
+  Qed.
+
+  Lemma nat_le_complete_conv : (m,n:nat) (nat_le n m)=false -> (lt m n).
+  Proof.
+    Intros. Elim (le_or_lt n m). Intro. Rewrite (nat_le_correct ? ? H0) in H. Discriminate H.
+    Trivial.
+  Qed.
+
+  Definition ad_of_nat := [n:nat] Cases n of
+                                      O => ad_z
+				    | (S n') => (ad_x (anti_convert n'))
+				  end.
+
+  Lemma ad_of_nat_of_ad : (a:ad) (ad_of_nat (nat_of_ad a))=a.
+  Proof.
+    Induction a. Reflexivity.
+    Intro. Simpl. Elim (ZL4 p). Intros p' H. Rewrite H. Simpl. Rewrite <- (bij1 p') in H.
+    Rewrite (convert_intro ? ? H). Reflexivity.
+  Qed.
+
+  Lemma nat_of_ad_of_nat : (n:nat) (nat_of_ad (ad_of_nat n))=n.
+  Proof.
+    Induction n. Trivial.
+    Intros. Simpl. Apply bij1.
+  Qed.
+
+  Definition ad_le := [a,b:ad] (nat_le (nat_of_ad a) (nat_of_ad b)).
+
+  Lemma ad_le_refl : (a:ad) (ad_le a a)=true.
+  Proof.
+    Intro. Unfold ad_le. Apply nat_le_correct. Apply le_n.
+  Qed.
+
+  Lemma ad_le_antisym : (a,b:ad) (ad_le a b)=true -> (ad_le b a)=true -> a=b.
+  Proof.
+    Unfold ad_le. 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 : (a,b,c:ad) (ad_le a b)=true -> (ad_le b c)=true -> (ad_le a c)=true.
+  Proof.
+    Unfold ad_le. 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 : (a,b,c:ad) (ad_le a b)=true -> (ad_le c b)=false -> (ad_le c a)=false.
+  Proof.
+    Unfold ad_le. 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 : (a,b,c:ad) (ad_le b a)=false -> (ad_le b c)=true -> (ad_le c a)=false.
+  Proof.
+    Unfold ad_le. 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 : (a,b,c:ad) (ad_le b a)=false -> (ad_le c b)=false -> (ad_le c a)=false.
+  Proof.
+    Unfold ad_le. 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 : (a,b:ad) (ad_le b a)=false -> (ad_le a b)=true.
+  Proof.
+    Unfold ad_le. 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 : (a,b:ad) {(ad_min a b)=a}+{(ad_min a b)=b}.
+  Proof.
+    Unfold ad_min. 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 : (a,b:ad) (ad_le (ad_min a b) a)=true.
+  Proof.
+    Unfold ad_min. 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 : (a,b:ad) (ad_le (ad_min a b) b)=true.
+  Proof.
+    Unfold ad_min. 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 : (a,b,c:ad) (ad_le a (ad_min b c))=true -> (ad_le a b)=true.
+  Proof.
+    Unfold ad_min. 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 : (a,b,c:ad) (ad_le a (ad_min b c))=true -> (ad_le a c)=true.
+  Proof.
+    Unfold ad_min. 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 : (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 : (a,b,c:ad) (ad_le (ad_min b c) a)=false -> (ad_le b a)=false.
+  Proof.
+    Unfold ad_min. 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 : (a,b,c:ad) (ad_le (ad_min b c) a)=false -> (ad_le c a)=false.
+  Proof.
+    Unfold ad_min. 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 :=
+    Cases m of
+        M0 => ad_z
+      | (M1 a _) => if (ad_eq a ad_z)
+                    then (ad_x xH)
+		    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 : (m:(Map A)) (MapGet A m (ad_alloc_opt m))=(NONE A).
+  Proof.
+    Induction m. Reflexivity.
+    Simpl. Intros. 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 (MapGet A (M2 A m0 m1)
+         (ad_min (ad_double (ad_alloc_opt m0)) (ad_double_plus_un (ad_alloc_opt m1))))=(NONE A).
+    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 : (m:(Map A)) (in_dom A (ad_alloc_opt m) m)=false.
+  Proof.
+    Unfold in_dom. 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 convert_xH : (convert xH)=(1).
+  Proof.
+    Reflexivity.
+  Qed.
+
+  Lemma positive_to_nat_mult : (p:positive) (n,m:nat)
+      (positive_to_nat p (mult m n))=(mult m (positive_to_nat p n)).
+  Proof.
+    Induction p. Intros. Simpl. Rewrite mult_plus_distr_r. Rewrite <- (mult_plus_distr_r m n n).
+    Rewrite (H (plus n n) m). Reflexivity.
+    Intros. Simpl. Rewrite <- (mult_plus_distr_r m n n). Apply H.
+    Trivial.
+  Qed.
+
+  Lemma positive_to_nat_2 : (p:positive)
+      (positive_to_nat p (2))=(mult (2) (positive_to_nat p (1))).
+  Proof.
+    Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+  Qed.
+
+  Lemma positive_to_nat_4 : (p:positive)
+      (positive_to_nat p (4))=(mult (2) (positive_to_nat p (2))).
+  Proof.
+    Intros. Rewrite <- positive_to_nat_mult. Reflexivity.
+  Qed.
+
+  Lemma convert_xO : (p:positive) (convert (xO p))=(mult (2) (convert p)).
+  Proof.
+    Induction p. Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2.
+    Rewrite positive_to_nat_4. Rewrite H. Simpl. Rewrite <- plus_Snm_nSm. Reflexivity.
+    Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+    Rewrite H. Reflexivity.
+    Reflexivity.
+  Qed.
+
+  Lemma convert_xI : (p:positive) (convert (xI p))=(S (mult (2) (convert p))).
+  Proof.
+    Induction p. Unfold convert. Simpl. Intro p0. Intro. Rewrite positive_to_nat_2.
+    Rewrite positive_to_nat_4. Inversion H. Rewrite H1. Rewrite <- plus_Snm_nSm. Reflexivity.
+    Unfold convert. Simpl. Intros. Rewrite positive_to_nat_2. Rewrite positive_to_nat_4.
+    Inversion H. Rewrite H1. Reflexivity.
+    Reflexivity.
+  Qed.
+
+  Lemma nat_of_ad_double : (a:ad) (nat_of_ad (ad_double a))=(mult (2) (nat_of_ad a)).
+  Proof.
+    Induction a. Trivial.
+    Exact convert_xO.
+  Qed.
+
+  Lemma nat_of_ad_double_plus_un : (a:ad)
+      (nat_of_ad (ad_double_plus_un a))=(S (mult (2) (nat_of_ad a))).
+  Proof.
+    Induction a. Trivial.
+    Exact convert_xI.
+  Qed.
+
+  Lemma ad_le_double_mono : (a,b:ad) (ad_le a b)=true -> (ad_le (ad_double a) (ad_double b))=true.
+  Proof.
+    Unfold ad_le. Intros. Rewrite nat_of_ad_double. Rewrite nat_of_ad_double. Apply nat_le_correct.
+    Simpl. Apply le_plus_plus. Apply nat_le_complete. Assumption.
+    Apply le_plus_plus. Apply nat_le_complete. Assumption.
+    Apply le_n.
+  Qed.
+
+  Lemma ad_le_double_plus_un_mono : (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. Intros. Rewrite nat_of_ad_double_plus_un. Rewrite nat_of_ad_double_plus_un.
+    Apply nat_le_correct. Apply le_n_S. Simpl. Apply le_plus_plus. Apply nat_le_complete.
+    Assumption.
+    Apply le_plus_plus. Apply nat_le_complete. Assumption.
+    Apply le_n.
+  Qed.
+
+  Lemma ad_le_double_mono_conv : (a,b:ad) (ad_le (ad_double a) (ad_double b))=true ->
+      (ad_le a b)=true.
+  Proof.
+    Unfold ad_le. Intros a b. Rewrite nat_of_ad_double. Rewrite nat_of_ad_double. Intro.
+    Apply nat_le_correct. Apply (mult_le_conv_1 (1)). Apply nat_le_complete. Assumption.
+  Qed.
+
+  Lemma ad_le_double_plus_un_mono_conv : (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. Intros a b. Rewrite nat_of_ad_double_plus_un. Rewrite nat_of_ad_double_plus_un.
+    Intro. Apply nat_le_correct. Apply (mult_le_conv_1 (1)). Apply le_S_n. Apply nat_le_complete.
+    Assumption.
+  Qed.
+
+  Lemma ad_lt_double_mono : (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 : (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 : (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 : (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 : (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. Simpl. Unfold ad_le. Simpl. Intros. Discriminate H.
+    Simpl. Intros a y 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 : (m:(Map A)) (a:ad) (ad_le (ad_alloc_opt m) a)=false ->
+      (in_dom A a m)=true.
+  Proof.
+    Intros. Unfold in_dom. Elim (ad_alloc_opt_optimal_1 m a H). Intros y H0. Rewrite H0.
+    Reflexivity.
+  Qed.
+
+End AdAlloc.