diff options
Diffstat (limited to 'theories/IntMap/Addr.v')
| -rw-r--r-- | theories/IntMap/Addr.v | 637 |
1 files changed, 336 insertions, 301 deletions
diff --git a/theories/IntMap/Addr.v b/theories/IntMap/Addr.v index cff8936b6f..fcab8b565c 100644 --- a/theories/IntMap/Addr.v +++ b/theories/IntMap/Addr.v @@ -9,448 +9,483 @@ (** Representation of adresses by the [positive] type of binary numbers *) -Require Bool. -Require ZArith. +Require Import Bool. +Require Import ZArith. Inductive ad : Set := - ad_z : ad + | 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 +Lemma ad_sum : forall a:ad, {p : positive | a = ad_x p} + {a = ad_z}. +Proof. + destruct a; auto. + left; exists p; trivial. +Qed. + +Fixpoint p_xor (p p2:positive) {struct p} : ad := + match p with + | xH => + match p2 with + | xH => ad_z + | xO p'2 => ad_x (xI p'2) + | xI p'2 => ad_x (xO p'2) + end + | xO p' => + match p2 with + | xH => ad_x (xI p') + | xO p'2 => + match p_xor p' p'2 with + | ad_z => ad_z + | ad_x p'' => ad_x (xO p'') + end + | xI p'2 => + match p_xor p' p'2 with + | ad_z => ad_x 1 + | ad_x p'' => ad_x (xI p'') + end + end + | xI p' => + match p2 with + | xH => ad_x (xO p') + | xO p'2 => + match p_xor p' p'2 with + | ad_z => ad_x 1 + | ad_x p'' => ad_x (xI p'') + end + | xI p'2 => + match p_xor p' p'2 with + | 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 +Definition ad_xor (a a':ad) := + match a with + | ad_z => a' + | ad_x p => match a' with + | 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. +Lemma ad_xor_neutral_left : forall a:ad, ad_xor ad_z a = a. Proof. - Trivial. + trivial. Qed. -Lemma ad_xor_neutral_right : (a:ad) (ad_xor a ad_z)=a. +Lemma ad_xor_neutral_right : forall a:ad, ad_xor a ad_z = a. Proof. - NewDestruct a; Trivial. + destruct a; trivial. Qed. -Lemma ad_xor_comm : (a,a':ad) (ad_xor a a')=(ad_xor a' a). +Lemma ad_xor_comm : forall 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. + destruct a; destruct a'; simpl in |- *; auto. + generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl in |- *; + auto. + destruct p0; simpl in |- *; trivial; intros. + rewrite Hrecp; trivial. + rewrite Hrecp; trivial. + destruct p0; simpl in |- *; trivial; intros. + rewrite Hrecp; trivial. + rewrite Hrecp; trivial. + destruct p0 as [p| p| ]; simpl in |- *; auto. Qed. -Lemma ad_xor_nilpotent : (a:ad) (ad_xor a a)=ad_z. +Lemma ad_xor_nilpotent : forall 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. + destruct a; trivial. + simpl in |- *. induction p as [p IHp| p IHp| ]; trivial. + simpl in |- *. rewrite IHp; reflexivity. + simpl in |- *. 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 +Fixpoint ad_bit_1 (p:positive) : nat -> bool := + match p with + | xH => fun n:nat => match n with + | O => true + | S _ => false + end + | xO p => + fun n:nat => match n with + | O => false + | S n' => ad_bit_1 p n' + end + | xI p => fun n:nat => match n with + | 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) +Definition ad_bit (a:ad) := + match a with + | ad_z => fun _:nat => false + | ad_x p => ad_bit_1 p end. -Definition eqf := [f,g:nat->bool] (n:nat) (f n)=(g n). +Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. -Lemma ad_faithful_1 : (a:ad) (eqf (ad_bit ad_z) (ad_bit a)) -> ad_z=a. +Lemma ad_faithful_1 : forall 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). + destruct a. trivial. + induction p as [p IHp| p IHp| ]; intro H. absurd (ad_z = ad_x p). discriminate. + exact (IHp (fun n:nat => H (S n))). + absurd (ad_z = ad_x p). discriminate. + exact (IHp (fun n:nat => H (S n))). + absurd (false = true). discriminate. + exact (H 0). Qed. -Lemma ad_faithful_2 : (a:ad) (eqf (ad_bit (ad_x xH)) (ad_bit a)) -> (ad_x xH)=a. +Lemma ad_faithful_2 : + forall a:ad, eqf (ad_bit (ad_x 1)) (ad_bit a) -> ad_x 1 = 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. + destruct a. intros. absurd (true = false). discriminate. + exact (H 0). + destruct p. intro H. absurd (ad_z = ad_x p). discriminate. + exact (ad_faithful_1 (ad_x p) (fun n:nat => H (S n))). + intros. absurd (true = false). discriminate. + exact (H 0). + 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. + forall (a:ad) (p:positive), + (forall 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). + destruct 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 in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity. + case p. intros. absurd (false = true). discriminate. + exact (H0 0). + intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity. + intros. absurd (false = true). discriminate. + exact (H0 0). 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. + forall (a:ad) (p:positive), + (forall 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. + destruct 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 in |- *. intro. unfold eqf in H0. rewrite H0. reflexivity. + case p. intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity. + intros. absurd (true = false). discriminate. + exact (H0 0). + intros. absurd (ad_z = ad_x p0). discriminate. + cut (eqf (ad_bit (ad_x 1)) (ad_bit (ad_x (xI p0)))). + intro. exact (ad_faithful_1 (ad_x p0) (fun n:nat => H1 (S n))). + unfold eqf in |- *. unfold eqf in H0. intro. rewrite H0. reflexivity. Qed. -Lemma ad_faithful : (a,a':ad) (eqf (ad_bit a) (ad_bit a')) -> a=a'. +Lemma ad_faithful : forall 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. + destruct a. exact ad_faithful_1. + induction 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)). +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). +Lemma ad_xor_sem_1 : forall a':ad, ad_bit (ad_xor ad_z a') 0 = ad_bit a' 0. Proof. - Trivial. + trivial. Qed. -Lemma ad_xor_sem_2 : (a':ad) (ad_bit (ad_xor (ad_x xH) a') O)=(negb (ad_bit a' O)). +Lemma ad_xor_sem_2 : + forall a':ad, ad_bit (ad_xor (ad_x 1) a') 0 = negb (ad_bit a' 0). Proof. - Intro. Case a'. Trivial. - Simpl. Intro. - Case p; Trivial. + intro. case a'. trivial. + simpl in |- *. 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). + forall (p:positive) (a':ad), + ad_bit (ad_xor (ad_x (xO p)) a') 0 = ad_bit a' 0. Proof. - Intros. Case a'. Trivial. - Simpl. Intro. - Case p0; Trivial. Intro. - Case (p_xor p p1); Trivial. - Intro. Case (p_xor p p1); Trivial. + intros. case a'. trivial. + simpl in |- *. 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)). +Lemma ad_xor_sem_4 : + forall (p:positive) (a':ad), + ad_bit (ad_xor (ad_x (xI p)) a') 0 = negb (ad_bit a' 0). Proof. - Intros. Case a'. Trivial. - Simpl. Intro. Case p0; Trivial. Intro. - Case (p_xor p p1); Trivial. - Intro. - Case (p_xor p p1); Trivial. + intros. case a'. trivial. + simpl in |- *. 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. + forall a a':ad, ad_bit (ad_xor a a') 0 = adf_xor (ad_bit a) (ad_bit a') 0. +Proof. + destruct a. intro. change (ad_bit a' 0 = xorb false (ad_bit a' 0)) in |- *. rewrite false_xorb. trivial. + case p. exact ad_xor_sem_4. + intros. change (ad_bit (ad_xor (ad_x (xO p0)) a') 0 = xorb false (ad_bit a' 0)) + in |- *. + rewrite false_xorb. apply ad_xor_sem_3. exact ad_xor_sem_2. +Qed. + +Lemma ad_xor_sem_6 : + forall n:nat, + (forall a a':ad, ad_bit (ad_xor a a') n = adf_xor (ad_bit a) (ad_bit a') n) -> + forall 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 in |- *. unfold ad_bit at 2 in |- *. rewrite false_xorb. reflexivity. + case a'. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. 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) + in |- *. + rewrite <- H. simpl in |- *. + 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) + in |- *. + rewrite <- H. simpl in |- *. + case (p_xor p2 p1); trivial. + intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. 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) + in |- *. + rewrite <- H. simpl in |- *. + 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) + in |- *. + rewrite <- H. simpl in |- *. + case (p_xor p2 p1); trivial. + intro. unfold adf_xor in |- *. unfold ad_bit at 3 in |- *. unfold ad_bit_1 in |- *. rewrite xorb_false. reflexivity. + unfold adf_xor in |- *. unfold ad_bit at 2 in |- *. unfold ad_bit_1 in |- *. rewrite false_xorb. simpl in |- *. 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'))). + forall 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. + unfold eqf in |- *. 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). +Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. Proof. - Unfold eqf. Intros. Rewrite H. Reflexivity. + unfold eqf in |- *. intros. rewrite H. reflexivity. Qed. -Lemma eqf_refl : (f:nat->bool) (eqf f f). +Lemma eqf_refl : forall f:nat -> bool, eqf f f. Proof. - Unfold eqf. Trivial. + unfold eqf in |- *. trivial. Qed. -Lemma eqf_trans : (f,f',f'':nat->bool) (eqf f f') -> (eqf f' f'') -> (eqf f f''). +Lemma eqf_trans : + forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''. Proof. - Unfold eqf. Intros. Rewrite H. Exact (H0 n). + unfold eqf in |- *. 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'). +Lemma adf_xor_eq : + forall f f':nat -> bool, eqf (adf_xor f f') (fun n:nat => false) -> eqf f f'. Proof. - Unfold eqf. Unfold adf_xor. Intros. Apply xorb_eq. Apply H. + unfold eqf in |- *. unfold adf_xor in |- *. intros. apply xorb_eq. apply H. Qed. -Lemma ad_xor_eq : (a,a':ad) (ad_xor a a')=ad_z -> a=a'. +Lemma ad_xor_eq : forall 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. + 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 in |- *. 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''))). +Lemma adf_xor_assoc : + forall 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. + unfold eqf in |- *. unfold adf_xor in |- *. 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''')). +Lemma eqf_xor_1 : + forall 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. + unfold eqf in |- *. intros. unfold adf_xor in |- *. 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)) + forall 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) := + match a with + | 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)) +Definition ad_double_plus_un (a:ad) := + match a with + | ad_z => ad_x 1 + | 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) +Definition ad_div_2 (a:ad) := + match a with + | 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. +Lemma ad_double_div_2 : forall a:ad, ad_div_2 (ad_double a) = a. Proof. - NewDestruct a; Trivial. + destruct a; trivial. Qed. -Lemma ad_double_plus_un_div_2 : (a:ad) (ad_div_2 (ad_double_plus_un a))=a. +Lemma ad_double_plus_un_div_2 : + forall a:ad, ad_div_2 (ad_double_plus_un a) = a. Proof. - NewDestruct a; Trivial. + destruct a; trivial. Qed. -Lemma ad_double_inj : (a0,a1:ad) (ad_double a0)=(ad_double a1) -> a0=a1. +Lemma ad_double_inj : forall 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. + 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. + forall 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. + 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 +Definition ad_bit_0 (a:ad) := + match a with + | ad_z => false + | ad_x (xO _) => false + | _ => true end. -Lemma ad_double_bit_0 : (a:ad) (ad_bit_0 (ad_double a))=false. +Lemma ad_double_bit_0 : forall a:ad, ad_bit_0 (ad_double a) = false. Proof. - NewDestruct a; Trivial. + destruct a; trivial. Qed. -Lemma ad_double_plus_un_bit_0 : (a:ad) (ad_bit_0 (ad_double_plus_un a))=true. +Lemma ad_double_plus_un_bit_0 : + forall a:ad, ad_bit_0 (ad_double_plus_un a) = true. Proof. - NewDestruct a; Trivial. + destruct a; trivial. Qed. -Lemma ad_div_2_double : (a:ad) (ad_bit_0 a)=false -> (ad_double (ad_div_2 a))=a. +Lemma ad_div_2_double : + forall 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. + destruct a. trivial. destruct 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. + forall 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. + destruct a. intro. discriminate H. + destruct 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). +Lemma ad_bit_0_correct : forall a:ad, ad_bit a 0 = ad_bit_0 a. Proof. - NewDestruct a; Trivial. - NewDestruct p; Trivial. + destruct a; trivial. + destruct p; trivial. Qed. -Lemma ad_div_2_correct : (a:ad) (n:nat) (ad_bit (ad_div_2 a) n)=(ad_bit a (S n)). +Lemma ad_div_2_correct : + forall (a:ad) (n:nat), ad_bit (ad_div_2 a) n = ad_bit a (S n). Proof. - NewDestruct a; Trivial. - NewDestruct p; Trivial. + destruct a; trivial. + destruct 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')). + forall 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. + intros. rewrite <- ad_bit_0_correct. rewrite (ad_xor_semantics a a' 0). + unfold adf_xor in |- *. 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')). + forall 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. + intros. apply ad_faithful. unfold eqf in |- *. 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 in |- *. 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')). +Lemma ad_neg_bit_0 : + forall 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. + 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')). + forall a a':ad, ad_xor a a' = ad_x 1 -> ad_bit_0 a = negb (ad_bit_0 a'). Proof. - Intros. Apply ad_neg_bit_0. Rewrite H. Reflexivity. + 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')). +Lemma ad_neg_bit_0_2 : + forall (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. + 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'). +Lemma ad_same_bit_0 : + forall (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. + 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.
\ No newline at end of file |