Library Coq.NArith.Ndigits


Require Import Bool.

Require Import Bvector.

Require Import BinPos.

Require Import BinNat.

Operation over bits of a N number.

xor





Fixpoint Pxor (p1 p2:positive) {struct p1} : N :=

  match p1, p2 with

  | xH, xH => N0

  | xH, xO p2 => Npos (xI p2)

  | xH, xI p2 => Npos (xO p2)

  | xO p1, xH => Npos (xI p1)

  | xO p1, xO p2 => Ndouble (Pxor p1 p2)

  | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2)

  | xI p1, xH => Npos (xO p1)

  | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2)

  | xI p1, xI p2 => Ndouble (Pxor p1 p2) 

  end.




Definition Nxor (n n':N) :=

  match n, n' with

  | N0, _ => n'

  | _, N0 => n

  | Npos p, Npos p' => Pxor p p'

  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.

The opposite composition is not so simple: if the considered bit vector has some zeros on its right, they will disappear during the return Bv2N translation:





Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n.

Proof.

induction n; intros.

rewrite (V0_eq _ bv); simpl; auto.

rewrite (VSn_eq _ _ bv); simpl.

generalize (IHn (Vtail _ _ bv)); clear IHn.

destruct (Vhead _ _ bv); 

 destruct (Bv2N n (Vtail bool n bv)); 

  simpl; auto with arith.

Qed.

In the previous lemma, we can only replace the inequality by an equality whenever the highest bit is non-null.





Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), 

  Bsign _ bv = true <-> 

  Nsize (Bv2N _ bv) = (S n).

Proof.

induction n; intro.

rewrite (VSn_eq _ _ bv); simpl.

rewrite (V0_eq _ (Vtail _ _ bv)); simpl.

destruct (Vhead _ _ bv); simpl; intuition; try discriminate.

rewrite (VSn_eq _ _ bv); simpl.

generalize (IHn (Vtail _ _ bv)); clear IHn.

destruct (Vhead _ _ bv); 

 destruct (Bv2N (S n) (Vtail bool (S n) bv)); 

  simpl; intuition; try discriminate.

Qed.

To state nonetheless a second result about composition of conversions, we define a conversion on a given number of bits :





Fixpoint N2Bv_gen (n:nat)(a:N) { struct n } : Bvector n := 

 match n return Bvector n with 

   | 0 => Bnil

   | S n => match a with 

       | N0 => Bvect_false (S n)

       | Npos xH => Bcons true _ (Bvect_false n)

       | Npos (xO p) => Bcons false _ (N2Bv_gen n (Npos p))

       | Npos (xI p) => Bcons true _ (N2Bv_gen n (Npos p))

      end

  end.

The first N2Bv is then a special case of N2Bv_gen





Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (Nsize a) a.

Proof.

destruct a; simpl.

auto.

induction p; simpl; intros; auto; congruence.

Qed.

In fact, if k is large enough, N2Bv_gen k a contains all digits of a plus some zeros.





Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), 

 N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k).

Proof.

destruct a; simpl.

destruct k; simpl; auto.

induction p; simpl; intros;unfold Bcons; f_equal; auto.

Qed.

Here comes now the second composition result.





Lemma N2Bv_Bv2N : forall n (bv:Bvector n), 

   N2Bv_gen n (Bv2N n bv) = bv.

Proof.

induction n; intros.

rewrite (V0_eq _ bv); simpl; auto.

rewrite (VSn_eq _ _ bv); simpl.

generalize (IHn (Vtail _ _ bv)); clear IHn.

unfold Bcons.

destruct (Bv2N _ (Vtail _ _ bv)); 

 destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; 

  induction n; simpl; auto.

Qed.

accessing some precise bits.





Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), 

  Nbit0 (Bv2N _ bv) = Blow _ bv.

Proof.

intros.

unfold Blow.

pattern bv at 1; rewrite (VSn_eq _ _ bv).

simpl.

destruct (Bv2N n (Vtail bool n bv)); simpl; 

 destruct (Vhead bool n bv); auto.

Qed.




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.

Xor is the same in the two worlds.





Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), 

  Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').

Proof.

induction n.

intros.

rewrite (V0_eq _ bv); rewrite (V0_eq _ bv'); simpl; auto.

intros.

rewrite (VSn_eq _ _ bv); rewrite (VSn_eq _ _ bv'); simpl; auto.

rewrite IHn.

destruct (Vhead bool n bv); destruct (Vhead bool n bv'); 

 destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto.

Qed.