diff options
Diffstat (limited to 'theories7/IntMap/Addec.v')
| -rw-r--r-- | theories7/IntMap/Addec.v | 179 |
1 files changed, 179 insertions, 0 deletions
diff --git a/theories7/IntMap/Addec.v b/theories7/IntMap/Addec.v new file mode 100644 index 00000000..50dc1480 --- /dev/null +++ b/theories7/IntMap/Addec.v @@ -0,0 +1,179 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Addec.v,v 1.1.2.1 2004/07/16 19:31:26 herbelin Exp $ i*) + +(** 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. + NewDestruct a; Trivial. + NewInduction p; Trivial. +Qed. + +Lemma ad_eq_complete : (a,a':ad) (ad_eq a a')=true -> a=a'. +Proof. + NewDestruct a. NewDestruct a'; Trivial. NewDestruct p. + Discriminate 1. + Discriminate 1. + Discriminate 1. + NewDestruct a'. Intros. Discriminate H. + Unfold ad_eq. Intros. Cut p=p0. Intros. Rewrite H0. Reflexivity. + Generalize Dependent p0. + NewInduction p as [p IHp|p IHp|]. NewDestruct p0; Intro H. + Rewrite (IHp p0). Reflexivity. + Exact H. + Discriminate H. + Discriminate H. + NewDestruct p0; Intro H. Discriminate H. + Rewrite (IHp p0 H). Reflexivity. + Discriminate H. + NewDestruct p0; Intro H. Discriminate H. + Discriminate H. + 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. + NewDestruct 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. + NewDestruct 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. NewDestruct n. + Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Assumption. + 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. |