Ajout lemmes arithmetiques

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

1 files changed, 164 insertions, 0 deletions

diff --git a/theories/IntMap/Addec.v b/theories/IntMap/Addec.v
new file mode 100644
index 0000000000..889c38d950
--- /dev/null
+++ b/theories/IntMap/Addec.v
@@ -0,0 +1,164 @@
+
+(*s Equality on adresses *)
+Require Bool.
+Require Sumbool.
+Require ZArith.
+Require Addr.
+
+Fixpoint ad_eq_1 [p1,p2:positive] : bool :=
+  Cases p1 p2 of
+      xH xH => true
+    | (xO p'1) (xO p'2) => (ad_eq_1 p'1 p'2)
+    | (xI p'1) (xI p'2) => (ad_eq_1 p'1 p'2)
+    | _ _ => false
+  end.
+
+Definition ad_eq := [a,a':ad]
+  Cases a a' of
+      ad_z ad_z => true
+    | (ad_x p) (ad_x p') => (ad_eq_1 p p')
+    | _ _ => false
+  end.
+
+Lemma ad_eq_correct : (a:ad) (ad_eq a a)=true.
+Proof.
+  Induction a; Trivial.
+  Induction p; Trivial.
+Qed.
+
+Lemma ad_eq_complete : (a,a':ad) (ad_eq a a')=true -> a=a'.
+Proof.
+  Induction a. Induction a'; Trivial. Induction p. Intros. Discriminate H0.
+  Intros. Discriminate H0.
+  Intros. Discriminate H.
+  Induction a'. Intros. Discriminate H.
+  Unfold ad_eq. Intros. Cut p=p0. Intros. Rewrite H0. Reflexivity.
+  Generalize p0 H. Elim p. Induction p2. Intros. 
+  Rewrite (H0 p3). Reflexivity.
+  Exact H2.
+  Intros. Discriminate H2.
+  Intros. Discriminate H1.
+  Induction p2. Intros. Discriminate H2.
+  Intros. Rewrite (H0 p3 H2). Reflexivity.
+  Intros. Discriminate H1.
+  Induction p1. Intros. Discriminate H1.
+  Intros. Discriminate H1.
+  Trivial.
+Qed.
+
+Lemma ad_eq_comm : (a,a':ad) (ad_eq a a')=(ad_eq a' a).
+Proof.
+  Intros. Cut (b,b':bool)(ad_eq a a')=b->(ad_eq a' a)=b'->b=b'.
+  Intros. Apply H. Reflexivity.
+  Reflexivity.
+  Induction b. Intros. Cut a=a'.
+  Intro. Rewrite H1 in H0. Rewrite (ad_eq_correct a') in H0. Exact H0.
+  Apply ad_eq_complete. Exact H.
+  Induction b'. Intros. Cut a'=a.
+  Intro. Rewrite H1 in H. Rewrite H1 in H0. Rewrite <- H. Exact H0.
+  Apply ad_eq_complete. Exact H0.
+  Trivial.
+Qed.
+
+Lemma ad_xor_eq_true : (a,a':ad) (ad_xor a a')=ad_z -> (ad_eq a a')=true.
+Proof.
+  Intros. Rewrite (ad_xor_eq a a' H). Apply ad_eq_correct.
+Qed.
+
+Lemma ad_xor_eq_false : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x p) -> (ad_eq a a')=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0.
+  Rewrite (ad_eq_complete a a' H0) in H. Rewrite (ad_xor_nilpotent a') in H. Discriminate H.
+  Trivial.
+Qed.
+
+Lemma ad_bit_0_1_not_double : (a:ad) (ad_bit_0 a)=true ->
+      (a0:ad) (ad_eq (ad_double a0) a)=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq (ad_double a0) a)). Intro H0.
+  Rewrite <- (ad_eq_complete ? ? H0) in H. Rewrite (ad_double_bit_0 a0) in H. Discriminate H.
+  Trivial.
+Qed.
+
+Lemma ad_not_div_2_not_double : (a,a0:ad) (ad_eq (ad_div_2 a) a0)=false ->
+      (ad_eq a (ad_double a0))=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq (ad_double a0) a)). Intro H0.
+  Rewrite <- (ad_eq_complete ? ? H0) in H. Rewrite (ad_double_div_2 a0) in H.
+  Rewrite (ad_eq_correct a0) in H. Discriminate H.
+  Intro. Rewrite ad_eq_comm. Assumption.
+Qed.
+
+Lemma ad_bit_0_0_not_double_plus_un : (a:ad) (ad_bit_0 a)=false ->
+      (a0:ad) (ad_eq (ad_double_plus_un a0) a)=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq (ad_double_plus_un a0) a)). Intro H0.
+  Rewrite <- (ad_eq_complete ? ? H0) in H. Rewrite (ad_double_plus_un_bit_0 a0) in H.
+  Discriminate H.
+  Trivial.
+Qed.
+
+Lemma ad_not_div_2_not_double_plus_un : (a,a0:ad) (ad_eq (ad_div_2 a) a0)=false ->
+      (ad_eq (ad_double_plus_un a0) a)=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq a (ad_double_plus_un a0))). Intro H0.
+  Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_double_plus_un_div_2 a0) in H.
+  Rewrite (ad_eq_correct a0) in H. Discriminate H.
+  Intro H0. Rewrite ad_eq_comm. Assumption.
+Qed.
+
+Lemma ad_bit_0_neq : (a,a':ad) (ad_bit_0 a)=false -> (ad_bit_0 a')=true -> (ad_eq a a')=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H1. Rewrite (ad_eq_complete ? ? H1) in H.
+  Rewrite H in H0. Discriminate H0.
+  Trivial.
+Qed.
+
+Lemma ad_div_eq : (a,a':ad) (ad_eq a a')=true -> (ad_eq (ad_div_2 a) (ad_div_2 a'))=true.
+Proof.
+  Intros. Cut a=a'. Intros. Rewrite H0. Apply ad_eq_correct.
+  Apply ad_eq_complete. Exact H.
+Qed.
+
+Lemma ad_div_neq : (a,a':ad) (ad_eq (ad_div_2 a) (ad_div_2 a'))=false -> (ad_eq a a')=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq a a')). Intro H0.
+  Rewrite (ad_eq_complete ? ? H0) in H. Rewrite (ad_eq_correct (ad_div_2 a')) in H. Discriminate H.
+  Trivial.
+Qed.
+
+Lemma ad_div_bit_eq : (a,a':ad) (ad_bit_0 a)=(ad_bit_0 a') ->
+    (ad_div_2 a)=(ad_div_2 a') -> a=a'.
+Proof.
+  Intros. Apply ad_faithful. Unfold eqf. Induction n.
+  Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Assumption.
+  Intros. Rewrite <- ad_div_2_correct. Rewrite <- ad_div_2_correct.
+  Rewrite H0. Reflexivity.
+Qed.
+
+Lemma ad_div_bit_neq : (a,a':ad) (ad_eq a a')=false -> (ad_bit_0 a)=(ad_bit_0 a') ->
+    (ad_eq (ad_div_2 a) (ad_div_2 a'))=false.
+Proof.
+  Intros. Elim (sumbool_of_bool (ad_eq (ad_div_2 a) (ad_div_2 a'))). Intro H1.
+  Rewrite (ad_div_bit_eq ? ? H0 (ad_eq_complete ? ? H1)) in H.
+  Rewrite (ad_eq_correct a') in H. Discriminate H.
+  Trivial.
+Qed.
+
+Lemma ad_neq : (a,a':ad) (ad_eq a a')=false ->
+    (ad_bit_0 a)=(negb (ad_bit_0 a')) \/ (ad_eq (ad_div_2 a) (ad_div_2 a'))=false.
+Proof.
+  Intros. Cut (ad_bit_0 a)=(ad_bit_0 a')\/(ad_bit_0 a)=(negb (ad_bit_0 a')).
+  Intros. Elim H0. Intro. Right . Apply ad_div_bit_neq. Assumption.
+  Assumption.
+  Intro. Left . Assumption.
+  Case (ad_bit_0 a); Case (ad_bit_0 a'); Auto.
+Qed.
+
+Lemma ad_double_or_double_plus_un : (a:ad)
+    {a0:ad | a=(ad_double a0)}+{a1:ad | a=(ad_double_plus_un a1)}.
+Proof.
+  Intro. Elim (sumbool_of_bool (ad_bit_0 a)). Intro H. Right . Split with (ad_div_2 a).
+  Rewrite (ad_div_2_double_plus_un a H). Reflexivity.
+  Intro H. Left . Split with (ad_div_2 a). Rewrite (ad_div_2_double a H). Reflexivity.
+Qed.