diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-25 22:52:18 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-25 22:52:18 +0000 |
commit | b2e0ec34cdd95017ce9ecec99b3431494b452d6c (patch) | |
tree | ccbc1c35da20152063cc5d094cc2e1b256fa4cf0 /theories/NArith/Ndigits.v | |
parent | 0274e797162cd62fe9145436a66027a61d727d64 (diff) |
Un gros coup de lifting pour IntMap:
* le type ad des adresses est maintenant un alias vers
le N de NArith, qui lui est isomorphe.
* toutes les operations sur ces adresses (p.ex. un xor
bit a bit) sont maintenant dans de nouveaux fichiers du
repertoire NArith.
* Intmap utilise maintenant le meme type option que le
reste du monde
* etc etc...
Tout ceci ne preserve pas forcement la compatibilite. Les 4 contribs
utilisant Intmap sont adaptees en consequence. Me demander si besoin
ma moulinette d'adaptation (incomplete).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8733 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/Ndigits.v')
-rw-r--r-- | theories/NArith/Ndigits.v | 698 |
1 files changed, 698 insertions, 0 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v new file mode 100644 index 000000000..f935a779d --- /dev/null +++ b/theories/NArith/Ndigits.v @@ -0,0 +1,698 @@ +(************************************************************************) +(* 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$ i*) + +Require Import Bool. +Require Import Bvector. +Require Import BinPos. +Require Import BinNat. + +(** Operation over bits of a [N] number. *) + +(** [xor] *) + +Fixpoint Pxor (p p2:positive) {struct p} : N := + match p with + | xH => + match p2 with + | xH => N0 + | xO p'2 => Npos (xI p'2) + | xI p'2 => Npos (xO p'2) + end + | xO p' => + match p2 with + | xH => Npos (xI p') + | xO p'2 => + match Pxor p' p'2 with + | N0 => N0 + | Npos p'' => Npos (xO p'') + end + | xI p'2 => + match Pxor p' p'2 with + | N0 => Npos 1 + | Npos p'' => Npos (xI p'') + end + end + | xI p' => + match p2 with + | xH => Npos (xO p') + | xO p'2 => + match Pxor p' p'2 with + | N0 => Npos 1 + | Npos p'' => Npos (xI p'') + end + | xI p'2 => + match Pxor p' p'2 with + | N0 => N0 + | Npos p'' => Npos (xO p'') + end + end + end. + +Definition Nxor (n n':N) := + match n with + | N0 => n' + | Npos p => match n' with + | N0 => n + | Npos p' => Pxor p p' + end + end. + +Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n. +Proof. + trivial. +Qed. + +Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n. +Proof. + destruct n; destruct n'; simpl; auto. + generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl; + auto. + destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial. + destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial. + destruct p0 as [p| p| ]; simpl; auto. +Qed. + +Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0. +Proof. + destruct n; trivial. + simpl. induction p as [p IHp| p IHp| ]; trivial. + simpl. rewrite IHp; reflexivity. + simpl. rewrite IHp; reflexivity. +Qed. + +(** Checking whether a particular bit is set on not *) + +Fixpoint Pbit (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' => Pbit p n' + end + | xI p => fun n:nat => match n with + | O => true + | S n' => Pbit p n' + end + end. + +Definition Nbit (a:N) := + match a with + | N0 => fun _ => false + | Npos p => Pbit p + end. + +(** Auxiliary results about streams of bits *) + +Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. + +Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. +Proof. + unfold eqf. intros. rewrite H. reflexivity. +Qed. + +Lemma eqf_refl : forall f:nat -> bool, eqf f f. +Proof. + unfold eqf. trivial. +Qed. + +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). +Qed. + +Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n). + +Lemma xorf_eq : + forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'. +Proof. + unfold eqf, xorf. intros. apply xorb_eq. apply H. +Qed. + +Lemma xorf_assoc : + forall f f' f'', + eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')). +Proof. + unfold eqf, xorf. intros. apply xorb_assoc. +Qed. + +Lemma eqf_xorf : + forall f f' f'' f''', + eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f'''). +Proof. + unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity. +Qed. + +(** End of auxilliary results *) + +(** This part is aimed at proving that if two numbers produce + the same stream of bits, then they are equal. *) + +Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a. +Proof. + destruct a. trivial. + induction p as [p IHp| p IHp| ]; intro H. + absurd (N0 = Npos p). discriminate. + exact (IHp (fun n => H (S n))). + absurd (N0 = Npos p). discriminate. + exact (IHp (fun n => H (S n))). + absurd (false = true). discriminate. + exact (H 0). +Qed. + +Lemma Nbit_faithful_2 : + forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a. +Proof. + destruct a. intros. absurd (true = false). discriminate. + exact (H 0). + destruct p. intro H. absurd (N0 = Npos p). discriminate. + exact (Nbit_faithful_1 (Npos p) (fun n:nat => H (S n))). + intros. absurd (true = false). discriminate. + exact (H 0). + trivial. +Qed. + +Lemma Nbit_faithful_3 : + forall (a:N) (p:positive), + (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> + eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a. +Proof. + destruct a. intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))). + intro. rewrite (Nbit_faithful_1 (Npos (xO p)) H1). reflexivity. + unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity. + case p. intros. absurd (false = true). discriminate. + exact (H0 0). + intros. rewrite (H p0 (fun n => H0 (S n))). reflexivity. + intros. absurd (false = true). discriminate. + exact (H0 0). +Qed. + +Lemma Nbit_faithful_4 : + forall (a:N) (p:positive), + (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> + eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a. +Proof. + destruct a. intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))). + intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity. + unfold eqf. 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 (N0 = Npos p0). discriminate. + cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))). + intro. exact (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))). + unfold eqf in *. intro. rewrite H0. reflexivity. +Qed. + +Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'. +Proof. + destruct a. exact Nbit_faithful_1. + induction p. intros a' H. apply Nbit_faithful_4. intros. cut (Npos p = Npos p'). + intro. inversion H1. reflexivity. + exact (IHp (Npos p') H0). + assumption. + intros. apply Nbit_faithful_3. intros. cut (Npos p = Npos p'). intro. inversion H1. reflexivity. + exact (IHp (Npos p') H0). + assumption. + exact Nbit_faithful_2. +Qed. + +(** We now describe the semantics of [Nxor] in terms of bit streams. *) + +Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0. +Proof. + trivial. +Qed. + +Lemma Nxor_sem_2 : + forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0). +Proof. + intro. case a'. trivial. + simpl. intro. + case p; trivial. +Qed. + +Lemma Nxor_sem_3 : + forall (p:positive) (a':N), + Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0. +Proof. + intros. case a'. trivial. + simpl. intro. + case p0; trivial. intro. + case (Pxor p p1); trivial. + intro. case (Pxor p p1); trivial. +Qed. + +Lemma Nxor_sem_4 : + forall (p:positive) (a':N), + Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0). +Proof. + intros. case a'. trivial. + simpl. intro. case p0; trivial. intro. + case (Pxor p p1); trivial. + intro. + case (Pxor p p1); trivial. +Qed. + +Lemma Nxor_sem_5 : + forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0. +Proof. + destruct a. intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial. + case p. exact Nxor_sem_4. + intros. change (Nbit (Nxor (Npos (xO p0)) a') 0 = xorb false (Nbit a' 0)). + rewrite false_xorb. apply Nxor_sem_3. exact Nxor_sem_2. +Qed. + +Lemma Nxor_sem_6 : + forall n:nat, + (forall a a':N, Nbit (Nxor a a') n = xorf (Nbit a) (Nbit a') n) -> + forall a a':N, + Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n). +Proof. + intros. + generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H. + unfold xorf in *. + case a. simpl Nbit; rewrite false_xorb. reflexivity. + case a'; intros. + simpl Nbit; rewrite xorb_false. reflexivity. + case p0. case p; intros; simpl Nbit in *. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite xorb_false. reflexivity. + case p; intros; simpl Nbit in *. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite xorb_false. reflexivity. + simpl Nbit. rewrite false_xorb. simpl. case p; trivial. +Qed. + +Lemma Nxor_semantics : + forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')). +Proof. + unfold eqf. intros. generalize a a'. elim n. exact Nxor_sem_5. + exact Nxor_sem_6. +Qed. + +(** Consequences: + - only equal numbers lead to a null xor + - xor is associative +*) + +Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'. +Proof. + intros. apply Nbit_faithful. apply xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')). + apply eqf_sym. apply Nxor_semantics. + rewrite H. unfold eqf. trivial. +Qed. + +Lemma Nxor_assoc : + forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a''). +Proof. + intros. apply Nbit_faithful. + apply eqf_trans with + (f' := xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')). + apply eqf_trans with (f' := xorf (Nbit (Nxor a a')) (Nbit a'')). + apply Nxor_semantics. + apply eqf_xorf. apply Nxor_semantics. + apply eqf_refl. + apply eqf_trans with + (f' := xorf (Nbit a) (xorf (Nbit a') (Nbit a''))). + apply xorf_assoc. + apply eqf_trans with (f' := xorf (Nbit a) (Nbit (Nxor a' a''))). + apply eqf_xorf. apply eqf_refl. + apply eqf_sym. apply Nxor_semantics. + apply eqf_sym. apply Nxor_semantics. +Qed. + +(** Checking whether a number is odd, i.e. + if its lower bit is set. *) + +Definition Nbit0 (n:N) := + match n with + | N0 => false + | Npos (xO _) => false + | _ => true + end. + +Definition Nodd (n:N) := Nbit0 n = true. +Definition Neven (n:N) := Nbit0 n = false. + +Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n. +Proof. + destruct n; trivial. + destruct p; trivial. +Qed. + +Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndouble_plus_one_bit0 : + forall n:N, Nbit0 (Ndouble_plus_one n) = true. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndiv2_double : + forall n:N, Neven n -> Ndouble (Ndiv2 n) = n. +Proof. + destruct n. trivial. destruct p. intro H. discriminate H. + intros. reflexivity. + intro H. discriminate H. +Qed. + +Lemma Ndiv2_double_plus_one : + forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n. +Proof. + destruct n. intro. discriminate H. + destruct p. intros. reflexivity. + intro H. discriminate H. + intro. reflexivity. +Qed. + +Lemma Ndiv2_correct : + forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit a (S n). +Proof. + destruct a; trivial. + destruct p; trivial. +Qed. + +Lemma Nxor_bit0 : + forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a'). +Proof. + intros. rewrite <- Nbit0_correct. rewrite (Nxor_semantics a a' 0). + unfold xorf. rewrite Nbit0_correct. rewrite Nbit0_correct. reflexivity. +Qed. + +Lemma Nxor_div2 : + forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a'). +Proof. + intros. apply Nbit_faithful. unfold eqf. intro. + rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n). + rewrite Ndiv2_correct. + rewrite (Nxor_semantics a a' (S n)). + unfold xorf. rewrite Ndiv2_correct. rewrite Ndiv2_correct. + reflexivity. +Qed. + +Lemma Nneg_bit0 : + forall a a':N, + Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). +Proof. + intros. rewrite <- true_xorb. rewrite <- H. rewrite Nxor_bit0. + rewrite xorb_assoc. rewrite xorb_nilpotent. rewrite xorb_false. reflexivity. +Qed. + +Lemma Nneg_bit0_1 : + forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 a'). +Proof. + intros. apply Nneg_bit0. rewrite H. reflexivity. +Qed. + +Lemma Nneg_bit0_2 : + forall (a a':N) (p:positive), + Nxor a a' = Npos (xI p) -> Nbit0 a = negb (Nbit0 a'). +Proof. + intros. apply Nneg_bit0. rewrite H. reflexivity. +Qed. + +Lemma Nsame_bit0 : + forall (a a':N) (p:positive), + Nxor a a' = Npos (xO p) -> Nbit0 a = Nbit0 a'. +Proof. + intros. rewrite <- (xorb_false (Nbit0 a)). cut (Nbit0 (Npos (xO p)) = false). + intro. rewrite <- H0. rewrite <- H. rewrite Nxor_bit0. rewrite <- xorb_assoc. + rewrite xorb_nilpotent. rewrite false_xorb. reflexivity. + reflexivity. +Qed. + +(** a lexicographic order on bits, starting from the lowest bit *) + +Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool := + match p with + | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p' + | _ => andb (negb (Nbit0 a)) (Nbit0 a') + end. + +Definition Nless (a a':N) := + match Nxor a a' with + | N0 => false + | Npos p => Nless_aux a a' p + end. + +Lemma Nbit0_less : + forall a a', + Nbit0 a = false -> Nbit0 a' = true -> Nless a a' = true. +Proof. + intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *. + rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5. + rewrite H in H5. rewrite H0 in H5. discriminate H5. + rewrite H4. reflexivity. + intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intro H1. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H2. + rewrite H in H2. rewrite H0 in H2. discriminate H2. + rewrite H1. reflexivity. +Qed. + +Lemma Nbit0_gt : + forall a a', + Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false. +Proof. + intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *. + rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5. + rewrite H in H5. rewrite H0 in H5. discriminate H5. + rewrite H4. reflexivity. + intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intro H1. unfold Nless in |- *. rewrite H1. reflexivity. +Qed. + +Lemma Nless_not_refl : forall a, Nless a a = false. +Proof. + intro. unfold Nless in |- *. rewrite (Nxor_nilpotent a). reflexivity. +Qed. + +Lemma Nless_def_1 : + forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'. +Proof. + simple induction a. simple induction a'. reflexivity. + trivial. + simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial. + unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity. + trivial. +Qed. + +Lemma Nless_def_2 : + forall a a', + Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'. +Proof. + simple induction a. simple induction a'. reflexivity. + trivial. + simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial. + unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity. + trivial. +Qed. + +Lemma Nless_def_3 : + forall a a', Nless (Ndouble a) (Ndouble_plus_one a') = true. +Proof. + intros. apply Nbit0_less. apply Ndouble_bit0. + apply Ndouble_plus_one_bit0. +Qed. + +Lemma Nless_def_4 : + forall a a', Nless (Ndouble_plus_one a) (Ndouble a') = false. +Proof. + intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0. + apply Ndouble_bit0. +Qed. + +Lemma Nless_z : forall a, Nless a N0 = false. +Proof. + simple induction a. reflexivity. + unfold Nless in |- *. intro. rewrite (Nxor_neutral_right (Npos p)). elim p; trivial. +Qed. + +Lemma N0_less_1 : + forall a, Nless N0 a = true -> {p : positive | a = Npos p}. +Proof. + simple induction a. intro. discriminate H. + intros. split with p. reflexivity. +Qed. + +Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0. +Proof. + simple induction a. trivial. + unfold Nless in |- *. simpl in |- *. + cut (forall p:positive, Nless_aux N0 (Npos p) p = false -> False). + intros. elim (H p H0). + simple induction p. intros. discriminate H0. + intros. exact (H H0). + intro. discriminate H. +Qed. + +Lemma Nless_trans : + forall a a' a'', + Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. +Proof. + intro a. pattern a; apply N_ind_double. + intros. case_eq (Nless N0 a''). trivial. + intro H1. rewrite (N0_less_2 a'' H1) in H0. rewrite (Nless_z a') in H0. discriminate H0. + intros a0 H a'. pattern a'; apply N_ind_double. + intros. rewrite (Nless_z (Ndouble a0)) in H0. discriminate H0. + intros a1 H0 a'' H1. rewrite (Nless_def_1 a0 a1) in H1. + pattern a''; apply N_ind_double; clear a''. + intro. rewrite (Nless_z (Ndouble a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_1 a1 a2) in H3. rewrite (Nless_def_1 a0 a2). + exact (H a1 a2 H1 H3). + intros. apply Nless_def_3. + intros a1 H0 a'' H1. pattern a''; apply N_ind_double. + intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3. + intros. apply Nless_def_3. + intros a0 H a'. pattern a'; apply N_ind_double. + intros. rewrite (Nless_z (Ndouble_plus_one a0)) in H0. discriminate H0. + intros. rewrite (Nless_def_4 a0 a1) in H1. discriminate H1. + intros a1 H0 a'' H1. pattern a''; apply N_ind_double. + intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3. + rewrite (Nless_def_2 a0 a1) in H1. intros. rewrite (Nless_def_2 a1 a2) in H3. + rewrite (Nless_def_2 a0 a2). exact (H a1 a2 H1 H3). +Qed. + +Lemma Nless_total : + forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. +Proof. + intro a. + pattern a; apply N_rec_double; clear a. + intro. case_eq (Nless N0 a'). intro H. left. left. auto. + intro H. right. rewrite (N0_less_2 a' H). reflexivity. + intros a0 H a'. + pattern a'; apply N_rec_double; clear a'. + case_eq (Nless N0 (Ndouble a0)). intro H0. left. right. auto. + intro H0. right. exact (N0_less_2 _ H0). + intros a1 H0. rewrite Nless_def_1. rewrite Nless_def_1. elim (H a1). intro H1. + left. assumption. + intro H1. right. rewrite H1. reflexivity. + intros a1 H0. left. left. apply Nless_def_3. + intros a0 H a'. + pattern a'; apply N_rec_double; clear a'. + left. right. case a0; reflexivity. + intros a1 H0. left. right. apply Nless_def_3. + intros a1 H0. rewrite Nless_def_2. rewrite Nless_def_2. elim (H a1). intro H1. + left. assumption. + intro H1. right. rewrite H1. reflexivity. +Qed. + +(** Number of digits in a number *) + +Fixpoint Psize (p:positive) : nat := + match p with + | xH => 1%nat + | xI p => S (Psize p) + | xO p => S (Psize p) + end. + +Definition Nsize (n:N) : nat := match n with + | N0 => 0%nat + | Npos p => Psize p + end. + + +(** conversions between N and bit vectors. *) + +Fixpoint P2Bv (p:positive) : Bvector (Psize p) := + match p return Bvector (Psize p) with + | xH => Bvect_true 1%nat + | xO p => Bcons false (Psize p) (P2Bv p) + | xI p => Bcons true (Psize p) (P2Bv p) + end. + +Definition N2Bv (n:N) : Bvector (Nsize n) := + match n as n0 return Bvector (Nsize n0) with + | N0 => Bnil + | Npos p => P2Bv p + end. + +Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N := + match bv with + | Vnil => N0 + | Vcons false n bv => Ndouble (Bv2N n bv) + | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) + end. + +Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. +Proof. +destruct n. +simpl; auto. +induction p; simpl in *; auto; rewrite IHp; simpl; auto. +Qed. + +(* how to formulate N2Bv_Bv2N, i.e. something like + Lemma N2Bv_Bv2N : forall n (bv:Bvector n), + exists p, Vextend _ _ _ (N2Bv (Bv2N n bv)) (Bvect_false p) = bv. +*) + +(* How to prove this ? +Lemma Nbit0_Blow : forall n (bv:Bvector (S n)), + Nbit0 (Bv2N _ bv) = Blow _ bv. +*) + +Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool. +Proof. + induction 1. + intros. + elimtype False; inversion H. + intros. + destruct p. + exact a. + apply (IHbv p); auto with arith. +Defined. + +Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), + Bnth _ bv p H = Nbit (Bv2N _ bv) p. +Proof. +induction bv; intros. +inversion H. +destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto. +Qed. + +Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false. +Proof. +destruct n as [|n]. +simpl; auto. +induction n; simpl in *; intros; destruct p; auto with arith. +inversion H. +inversion H. +Qed. + +Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H. +Proof. +destruct n as [|n]. +inversion H. +induction n; simpl in *; intros; destruct p; auto with arith. +inversion H; inversion H1. +Qed. + +(* How to prove this one ? +Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), + Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). +*) |