diff options
Diffstat (limited to 'theories7/IntMap/Addec.v')
| -rw-r--r-- | theories7/IntMap/Addec.v | 179 |
1 files changed, 0 insertions, 179 deletions
diff --git a/theories7/IntMap/Addec.v b/theories7/IntMap/Addec.v deleted file mode 100644 index 50dc1480..00000000 --- a/theories7/IntMap/Addec.v +++ /dev/null @@ -1,179 +0,0 @@ -(************************************************************************) -(* 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. |