diff options
Diffstat (limited to 'theories7/IntMap/Addr.v')
| -rw-r--r-- | theories7/IntMap/Addr.v | 456 |
1 files changed, 456 insertions, 0 deletions
diff --git a/theories7/IntMap/Addr.v b/theories7/IntMap/Addr.v new file mode 100644 index 00000000..9f362772 --- /dev/null +++ b/theories7/IntMap/Addr.v @@ -0,0 +1,456 @@ +(************************************************************************) +(* 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: Addr.v,v 1.1.2.1 2004/07/16 19:31:27 herbelin Exp $ i*) + +(** Representation of adresses by the [positive] type of binary numbers *) + +Require Bool. +Require ZArith. + +Inductive ad : Set := + ad_z : ad + | ad_x : positive -> ad. + +Lemma ad_sum : (a:ad) {p:positive | a=(ad_x p)}+{a=ad_z}. +Proof. + NewDestruct a; Auto. + Left; Exists p; Trivial. +Qed. + +Fixpoint p_xor [p:positive] : positive -> ad := + [p2] Cases p of + xH => Cases p2 of + xH => ad_z + | (xO p'2) => (ad_x (xI p'2)) + | (xI p'2) => (ad_x (xO p'2)) + end + | (xO p') => Cases p2 of + xH => (ad_x (xI p')) + | (xO p'2) => Cases (p_xor p' p'2) of + ad_z => ad_z + | (ad_x p'') => (ad_x (xO p'')) + end + | (xI p'2) => Cases (p_xor p' p'2) of + ad_z => (ad_x xH) + | (ad_x p'') => (ad_x (xI p'')) + end + end + | (xI p') => Cases p2 of + xH => (ad_x (xO p')) + | (xO p'2) => Cases (p_xor p' p'2) of + ad_z => (ad_x xH) + | (ad_x p'') => (ad_x (xI p'')) + end + | (xI p'2) => Cases (p_xor p' p'2) of + ad_z => ad_z + | (ad_x p'') => (ad_x (xO p'')) + end + end + end. + +Definition ad_xor := [a,a':ad] + Cases a of + ad_z => a' + | (ad_x p) => Cases a' of + ad_z => a + | (ad_x p') => (p_xor p p') + end + end. + +Lemma ad_xor_neutral_left : (a:ad) (ad_xor ad_z a)=a. +Proof. + Trivial. +Qed. + +Lemma ad_xor_neutral_right : (a:ad) (ad_xor a ad_z)=a. +Proof. + NewDestruct a; Trivial. +Qed. + +Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a). +Proof. + NewDestruct a; NewDestruct a'; Simpl; Auto. + Generalize p0; Clear p0; NewInduction p as [p Hrecp|p Hrecp|]; Simpl; Auto. + NewDestruct p0; Simpl; Trivial; Intros. + Rewrite Hrecp; Trivial. + Rewrite Hrecp; Trivial. + NewDestruct p0; Simpl; Trivial; Intros. + Rewrite Hrecp; Trivial. + Rewrite Hrecp; Trivial. + NewDestruct p0; Simpl; Auto. +Qed. + +Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z. +Proof. + NewDestruct a; Trivial. + Simpl. NewInduction p as [p IHp|p IHp|]; Trivial. + Simpl. Rewrite IHp; Reflexivity. + Simpl. Rewrite IHp; Reflexivity. +Qed. + +Fixpoint ad_bit_1 [p:positive] : nat -> bool := + Cases p of + xH => [n:nat] Cases n of + O => true + | (S _) => false + end + | (xO p) => [n:nat] Cases n of + O => false + | (S n') => (ad_bit_1 p n') + end + | (xI p) => [n:nat] Cases n of + O => true + | (S n') => (ad_bit_1 p n') + end + end. + +Definition ad_bit := [a:ad] + Cases a of + ad_z => [_:nat] false + | (ad_x p) => (ad_bit_1 p) + end. + +Definition eqf := [f,g:nat->bool] (n:nat) (f n)=(g n). + +Lemma ad_faithful_1 : (a:ad) (eqf (ad_bit ad_z) (ad_bit a)) -> ad_z=a. +Proof. + NewDestruct a. Trivial. + NewInduction p as [p IHp|p IHp|];Intro H. Absurd ad_z=(ad_x p). Discriminate. + Exact (IHp [n:nat](H (S n))). + Absurd ad_z=(ad_x p). Discriminate. + Exact (IHp [n:nat](H (S n))). + Absurd false=true. Discriminate. + Exact (H O). +Qed. + +Lemma ad_faithful_2 : (a:ad) (eqf (ad_bit (ad_x xH)) (ad_bit a)) -> (ad_x xH)=a. +Proof. + NewDestruct a. Intros. Absurd true=false. Discriminate. + Exact (H O). + NewDestruct p. Intro H. Absurd ad_z=(ad_x p). Discriminate. + Exact (ad_faithful_1 (ad_x p) [n:nat](H (S n))). + Intros. Absurd true=false. Discriminate. + Exact (H O). + Trivial. +Qed. + +Lemma ad_faithful_3 : + (a:ad) (p:positive) + ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') -> + (eqf (ad_bit (ad_x (xO p))) (ad_bit a)) -> + (ad_x (xO p))=a. +Proof. + NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xO p)))). + Intro. Rewrite (ad_faithful_1 (ad_x (xO p)) H1). Reflexivity. + Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity. + Case p. Intros. Absurd false=true. Discriminate. + Exact (H0 O). + Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity. + Intros. Absurd false=true. Discriminate. + Exact (H0 O). +Qed. + +Lemma ad_faithful_4 : + (a:ad) (p:positive) + ((p':positive) (eqf (ad_bit (ad_x p)) (ad_bit (ad_x p'))) -> p=p') -> + (eqf (ad_bit (ad_x (xI p))) (ad_bit a)) -> + (ad_x (xI p))=a. +Proof. + NewDestruct a. Intros. Cut (eqf (ad_bit ad_z) (ad_bit (ad_x (xI p)))). + Intro. Rewrite (ad_faithful_1 (ad_x (xI p)) H1). Reflexivity. + Unfold eqf. Intro. Unfold eqf in H0. Rewrite H0. Reflexivity. + Case p. Intros. Rewrite (H p0 [n:nat](H0 (S n))). Reflexivity. + Intros. Absurd true=false. Discriminate. + Exact (H0 O). + Intros. Absurd ad_z=(ad_x p0). Discriminate. + Cut (eqf (ad_bit (ad_x xH)) (ad_bit (ad_x (xI p0)))). + Intro. Exact (ad_faithful_1 (ad_x p0) [n:nat](H1 (S n))). + Unfold eqf. Unfold eqf in H0. Intro. Rewrite H0. Reflexivity. +Qed. + +Lemma ad_faithful : (a,a':ad) (eqf (ad_bit a) (ad_bit a')) -> a=a'. +Proof. + NewDestruct a. Exact ad_faithful_1. + NewInduction p. Intros a' H. Apply ad_faithful_4. Intros. Cut (ad_x p)=(ad_x p'). + Intro. Inversion H1. Reflexivity. + Exact (IHp (ad_x p') H0). + Assumption. + Intros. Apply ad_faithful_3. Intros. Cut (ad_x p)=(ad_x p'). Intro. Inversion H1. Reflexivity. + Exact (IHp (ad_x p') H0). + Assumption. + Exact ad_faithful_2. +Qed. + +Definition adf_xor := [f,g:nat->bool; n:nat] (xorb (f n) (g n)). + +Lemma ad_xor_sem_1 : (a':ad) (ad_bit (ad_xor ad_z a') O)=(ad_bit a' O). +Proof. + Trivial. +Qed. + +Lemma ad_xor_sem_2 : (a':ad) (ad_bit (ad_xor (ad_x xH) a') O)=(negb (ad_bit a' O)). +Proof. + Intro. Case a'. Trivial. + Simpl. Intro. + Case p; Trivial. +Qed. + +Lemma ad_xor_sem_3 : + (p:positive) (a':ad) (ad_bit (ad_xor (ad_x (xO p)) a') O)=(ad_bit a' O). +Proof. + Intros. Case a'. Trivial. + Simpl. Intro. + Case p0; Trivial. Intro. + Case (p_xor p p1); Trivial. + Intro. Case (p_xor p p1); Trivial. +Qed. + +Lemma ad_xor_sem_4 : (p:positive) (a':ad) + (ad_bit (ad_xor (ad_x (xI p)) a') O)=(negb (ad_bit a' O)). +Proof. + Intros. Case a'. Trivial. + Simpl. Intro. Case p0; Trivial. Intro. + Case (p_xor p p1); Trivial. + Intro. + Case (p_xor p p1); Trivial. +Qed. + +Lemma ad_xor_sem_5 : + (a,a':ad) (ad_bit (ad_xor a a') O)=(adf_xor (ad_bit a) (ad_bit a') O). +Proof. + NewDestruct a. Intro. Change (ad_bit a' O)=(xorb false (ad_bit a' O)). Rewrite false_xorb. Trivial. + Case p. Exact ad_xor_sem_4. + Intros. Change (ad_bit (ad_xor (ad_x (xO p0)) a') O)=(xorb false (ad_bit a' O)). + Rewrite false_xorb. Apply ad_xor_sem_3. Exact ad_xor_sem_2. +Qed. + +Lemma ad_xor_sem_6 : (n:nat) + ((a,a':ad) (ad_bit (ad_xor a a') n)=(adf_xor (ad_bit a) (ad_bit a') n)) -> + (a,a':ad) (ad_bit (ad_xor a a') (S n))=(adf_xor (ad_bit a) (ad_bit a') (S n)). +Proof. + Intros. Case a. Unfold adf_xor. Unfold 2 ad_bit. Rewrite false_xorb. Reflexivity. + Case a'. Unfold adf_xor. Unfold 3 ad_bit. Intro. Rewrite xorb_false. Reflexivity. + Intros. Case p0. Case p. Intros. + Change (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xI p1))) (S n)) + =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n). + Rewrite <- H. Simpl. + Case (p_xor p2 p1); Trivial. + Intros. + Change (ad_bit (ad_xor (ad_x (xI p2)) (ad_x (xO p1))) (S n)) + =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n). + Rewrite <- H. Simpl. + Case (p_xor p2 p1); Trivial. + Intro. Unfold adf_xor. Unfold 3 ad_bit. Unfold ad_bit_1. Rewrite xorb_false. Reflexivity. + Case p. Intros. + Change (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xI p1))) (S n)) + =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n). + Rewrite <- H. Simpl. + Case (p_xor p2 p1); Trivial. + Intros. + Change (ad_bit (ad_xor (ad_x (xO p2)) (ad_x (xO p1))) (S n)) + =(adf_xor (ad_bit (ad_x p2)) (ad_bit (ad_x p1)) n). + Rewrite <- H. Simpl. + Case (p_xor p2 p1); Trivial. + Intro. Unfold adf_xor. Unfold 3 ad_bit. Unfold ad_bit_1. Rewrite xorb_false. Reflexivity. + Unfold adf_xor. Unfold 2 ad_bit. Unfold ad_bit_1. Rewrite false_xorb. Simpl. Case p; Trivial. +Qed. + +Lemma ad_xor_semantics : + (a,a':ad) (eqf (ad_bit (ad_xor a a')) (adf_xor (ad_bit a) (ad_bit a'))). +Proof. + Unfold eqf. Intros. Generalize a a'. Elim n. Exact ad_xor_sem_5. + Exact ad_xor_sem_6. +Qed. + +Lemma eqf_sym : (f,f':nat->bool) (eqf f f') -> (eqf f' f). +Proof. + Unfold eqf. Intros. Rewrite H. Reflexivity. +Qed. + +Lemma eqf_refl : (f:nat->bool) (eqf f f). +Proof. + Unfold eqf. Trivial. +Qed. + +Lemma eqf_trans : (f,f',f'':nat->bool) (eqf f f') -> (eqf f' f'') -> (eqf f f''). +Proof. + Unfold eqf. Intros. Rewrite H. Exact (H0 n). +Qed. + +Lemma adf_xor_eq : (f,f':nat->bool) (eqf (adf_xor f f') [n:nat] false) -> (eqf f f'). +Proof. + Unfold eqf. Unfold adf_xor. Intros. Apply xorb_eq. Apply H. +Qed. + +Lemma ad_xor_eq : (a,a':ad) (ad_xor a a')=ad_z -> a=a'. +Proof. + Intros. Apply ad_faithful. Apply adf_xor_eq. Apply eqf_trans with f':=(ad_bit (ad_xor a a')). + Apply eqf_sym. Apply ad_xor_semantics. + Rewrite H. Unfold eqf. Trivial. +Qed. + +Lemma adf_xor_assoc : (f,f',f'':nat->bool) + (eqf (adf_xor (adf_xor f f') f'') (adf_xor f (adf_xor f' f''))). +Proof. + Unfold eqf. Unfold adf_xor. Intros. Apply xorb_assoc. +Qed. + +Lemma eqf_xor_1 : (f,f',f'',f''':nat->bool) (eqf f f') -> (eqf f'' f''') -> + (eqf (adf_xor f f'') (adf_xor f' f''')). +Proof. + Unfold eqf. Intros. Unfold adf_xor. Rewrite H. Rewrite H0. Reflexivity. +Qed. + +Lemma ad_xor_assoc : + (a,a',a'':ad) (ad_xor (ad_xor a a') a'')=(ad_xor a (ad_xor a' a'')). +Proof. + Intros. Apply ad_faithful. + Apply eqf_trans with f':=(adf_xor (adf_xor (ad_bit a) (ad_bit a')) (ad_bit a'')). + Apply eqf_trans with f':=(adf_xor (ad_bit (ad_xor a a')) (ad_bit a'')). + Apply ad_xor_semantics. + Apply eqf_xor_1. Apply ad_xor_semantics. + Apply eqf_refl. + Apply eqf_trans with f':=(adf_xor (ad_bit a) (adf_xor (ad_bit a') (ad_bit a''))). + Apply adf_xor_assoc. + Apply eqf_trans with f':=(adf_xor (ad_bit a) (ad_bit (ad_xor a' a''))). + Apply eqf_xor_1. Apply eqf_refl. + Apply eqf_sym. Apply ad_xor_semantics. + Apply eqf_sym. Apply ad_xor_semantics. +Qed. + +Definition ad_double := [a:ad] + Cases a of + ad_z => ad_z + | (ad_x p) => (ad_x (xO p)) + end. + +Definition ad_double_plus_un := [a:ad] + Cases a of + ad_z => (ad_x xH) + | (ad_x p) => (ad_x (xI p)) + end. + +Definition ad_div_2 := [a:ad] + Cases a of + ad_z => ad_z + | (ad_x xH) => ad_z + | (ad_x (xO p)) => (ad_x p) + | (ad_x (xI p)) => (ad_x p) + end. + +Lemma ad_double_div_2 : (a:ad) (ad_div_2 (ad_double a))=a. +Proof. + NewDestruct a; Trivial. +Qed. + +Lemma ad_double_plus_un_div_2 : (a:ad) (ad_div_2 (ad_double_plus_un a))=a. +Proof. + NewDestruct a; Trivial. +Qed. + +Lemma ad_double_inj : (a0,a1:ad) (ad_double a0)=(ad_double a1) -> a0=a1. +Proof. + Intros. Rewrite <- (ad_double_div_2 a0). Rewrite H. Apply ad_double_div_2. +Qed. + +Lemma ad_double_plus_un_inj : + (a0,a1:ad) (ad_double_plus_un a0)=(ad_double_plus_un a1) -> a0=a1. +Proof. + Intros. Rewrite <- (ad_double_plus_un_div_2 a0). Rewrite H. Apply ad_double_plus_un_div_2. +Qed. + +Definition ad_bit_0 := [a:ad] + Cases a of + ad_z => false + | (ad_x (xO _)) => false + | _ => true + end. + +Lemma ad_double_bit_0 : (a:ad) (ad_bit_0 (ad_double a))=false. +Proof. + NewDestruct a; Trivial. +Qed. + +Lemma ad_double_plus_un_bit_0 : (a:ad) (ad_bit_0 (ad_double_plus_un a))=true. +Proof. + NewDestruct a; Trivial. +Qed. + +Lemma ad_div_2_double : (a:ad) (ad_bit_0 a)=false -> (ad_double (ad_div_2 a))=a. +Proof. + NewDestruct a. Trivial. NewDestruct p. Intro H. Discriminate H. + Intros. Reflexivity. + Intro H. Discriminate H. +Qed. + +Lemma ad_div_2_double_plus_un : + (a:ad) (ad_bit_0 a)=true -> (ad_double_plus_un (ad_div_2 a))=a. +Proof. + NewDestruct a. Intro. Discriminate H. + NewDestruct p. Intros. Reflexivity. + Intro H. Discriminate H. + Intro. Reflexivity. +Qed. + +Lemma ad_bit_0_correct : (a:ad) (ad_bit a O)=(ad_bit_0 a). +Proof. + NewDestruct a; Trivial. + NewDestruct p; Trivial. +Qed. + +Lemma ad_div_2_correct : (a:ad) (n:nat) (ad_bit (ad_div_2 a) n)=(ad_bit a (S n)). +Proof. + NewDestruct a; Trivial. + NewDestruct p; Trivial. +Qed. + +Lemma ad_xor_bit_0 : + (a,a':ad) (ad_bit_0 (ad_xor a a'))=(xorb (ad_bit_0 a) (ad_bit_0 a')). +Proof. + Intros. Rewrite <- ad_bit_0_correct. Rewrite (ad_xor_semantics a a' O). + Unfold adf_xor. Rewrite ad_bit_0_correct. Rewrite ad_bit_0_correct. Reflexivity. +Qed. + +Lemma ad_xor_div_2 : + (a,a':ad) (ad_div_2 (ad_xor a a'))=(ad_xor (ad_div_2 a) (ad_div_2 a')). +Proof. + Intros. Apply ad_faithful. Unfold eqf. Intro. + Rewrite (ad_xor_semantics (ad_div_2 a) (ad_div_2 a') n). + Rewrite ad_div_2_correct. + Rewrite (ad_xor_semantics a a' (S n)). + Unfold adf_xor. Rewrite ad_div_2_correct. Rewrite ad_div_2_correct. + Reflexivity. +Qed. + +Lemma ad_neg_bit_0 : (a,a':ad) (ad_bit_0 (ad_xor a a'))=true -> + (ad_bit_0 a)=(negb (ad_bit_0 a')). +Proof. + Intros. Rewrite <- true_xorb. Rewrite <- H. Rewrite ad_xor_bit_0. + Rewrite xorb_assoc. Rewrite xorb_nilpotent. Rewrite xorb_false. Reflexivity. +Qed. + +Lemma ad_neg_bit_0_1 : + (a,a':ad) (ad_xor a a')=(ad_x xH) -> (ad_bit_0 a)=(negb (ad_bit_0 a')). +Proof. + Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity. +Qed. + +Lemma ad_neg_bit_0_2 : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x (xI p)) -> + (ad_bit_0 a)=(negb (ad_bit_0 a')). +Proof. + Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity. +Qed. + +Lemma ad_same_bit_0 : (a,a':ad) (p:positive) (ad_xor a a')=(ad_x (xO p)) -> + (ad_bit_0 a)=(ad_bit_0 a'). +Proof. + Intros. Rewrite <- (xorb_false (ad_bit_0 a)). Cut (ad_bit_0 (ad_x (xO p)))=false. + Intro. Rewrite <- H0. Rewrite <- H. Rewrite ad_xor_bit_0. Rewrite <- xorb_assoc. + Rewrite xorb_nilpotent. Rewrite false_xorb. Reflexivity. + Reflexivity. +Qed. |