summaryrefslogtreecommitdiff
path: root/theories/NArith/Ndigits.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /theories/NArith/Ndigits.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'theories/NArith/Ndigits.v')
-rw-r--r--theories/NArith/Ndigits.v642
1 files changed, 283 insertions, 359 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 6b490dfc..4ea8e1d4 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -1,343 +1,276 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Ndigits.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
+Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
+ Pnat Nnat Compare_dec Lt Minus.
-Require Import Bool.
-Require Import Bvector.
-Require Import BinPos.
-Require Import BinNat.
+Local Open Scope N_scope.
-(** Operation over bits of a [N] number. *)
+(** This file is mostly obsolete, see directly [BinNat] now. *)
-(** [xor] *)
+(** Compatibility names for some bitwise operations *)
-Fixpoint Pxor (p1 p2:positive) : 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.
+Notation Pxor := Pos.lxor (compat "8.3").
+Notation Nxor := N.lxor (compat "8.3").
+Notation Pbit := Pos.testbit_nat (compat "8.3").
+Notation Nbit := N.testbit_nat (compat "8.3").
-Definition Nxor (n n':N) :=
- match n, n' with
- | N0, _ => n'
- | _, N0 => n
- | Npos p, Npos p' => Pxor p p'
- end.
+Notation Nxor_eq := N.lxor_eq (compat "8.3").
+Notation Nxor_comm := N.lxor_comm (compat "8.3").
+Notation Nxor_assoc := N.lxor_assoc (compat "8.3").
+Notation Nxor_neutral_left := N.lxor_0_l (compat "8.3").
+Notation Nxor_neutral_right := N.lxor_0_r (compat "8.3").
+Notation Nxor_nilpotent := N.lxor_nilpotent (compat "8.3").
-Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n.
+(** Equivalence of bit-testing functions,
+ either with index in [N] or in [nat]. *)
+
+Lemma Ptestbit_Pbit :
+ forall p n, Pos.testbit p (N.of_nat n) = Pos.testbit_nat p n.
Proof.
- trivial.
+ induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial;
+ rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite Nat2N.inj_pred.
Qed.
-Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n.
+Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = N.testbit_nat a n.
Proof.
- destruct n; trivial.
+ destruct a. trivial. apply Ptestbit_Pbit.
Qed.
-Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n.
+Lemma Pbit_Ptestbit :
+ forall p n, Pos.testbit_nat p (N.to_nat n) = Pos.testbit p n.
Proof.
- destruct n; destruct n'; simpl; auto.
- generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl;
- auto.
- destruct p0; trivial; rewrite Hrecp; trivial.
- destruct p0; trivial; rewrite Hrecp; trivial.
- destruct p0 as [p| p| ]; simpl; auto.
+ intros; now rewrite <- Ptestbit_Pbit, N2Nat.id.
Qed.
-Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0.
+Lemma Nbit_Ntestbit :
+ forall a n, N.testbit_nat a (N.to_nat n) = N.testbit a n.
Proof.
- destruct n; trivial.
- simpl. induction p as [p IHp| p IHp| ]; trivial.
- simpl. rewrite IHp; reflexivity.
- simpl. rewrite IHp; reflexivity.
+ destruct a. trivial. apply Pbit_Ptestbit.
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.
+(** Equivalence of shifts, index in [N] or [nat] *)
-Definition Nbit (a:N) :=
- match a with
- | N0 => fun _ => false
- | Npos p => Pbit p
- end.
+Lemma Nshiftr_nat_S : forall a n,
+ N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n).
+Proof.
+ reflexivity.
+Qed.
-(** Auxiliary results about streams of bits *)
+Lemma Nshiftl_nat_S : forall a n,
+ N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n).
+Proof.
+ reflexivity.
+Qed.
-Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
+Lemma Nshiftr_nat_equiv :
+ forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n.
+Proof.
+ intros a [|n]; simpl. unfold N.shiftr_nat.
+ trivial.
+ symmetry. apply Pos2Nat.inj_iter.
+Qed.
-Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f.
+Lemma Nshiftr_equiv_nat :
+ forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n.
Proof.
- unfold eqf. intros. rewrite H. reflexivity.
+ intros. now rewrite <- Nshiftr_nat_equiv, Nat2N.id.
Qed.
-Lemma eqf_refl : forall f:nat -> bool, eqf f f.
+Lemma Nshiftl_nat_equiv :
+ forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n.
Proof.
- unfold eqf. trivial.
+ intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial.
+ apply nat_iter_invariant; intros; now subst.
+ rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen.
Qed.
-Lemma eqf_trans :
- forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''.
+Lemma Nshiftl_equiv_nat :
+ forall a n, N.shiftl a (N.of_nat n) = N.shiftl_nat a n.
Proof.
- unfold eqf. intros. rewrite H. exact (H0 n).
+ intros. now rewrite <- Nshiftl_nat_equiv, Nat2N.id.
Qed.
-Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n).
+(** Correctness proofs for shifts, nat version *)
-Lemma xorf_eq :
- forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'.
+Lemma Nshiftr_nat_spec : forall a n m,
+ N.testbit_nat (N.shiftr_nat a n) m = N.testbit_nat a (m+n).
Proof.
- unfold eqf, xorf. intros. apply xorb_eq, H.
+ induction n; intros m.
+ now rewrite <- plus_n_O.
+ simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S.
+ destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.
-Lemma xorf_assoc :
- forall f f' f'',
- eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')).
+Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
+ N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n).
Proof.
- unfold eqf, xorf. intros. apply xorb_assoc.
+ induction n; intros m H.
+ now rewrite <- minus_n_O.
+ destruct m. inversion H. apply le_S_n in H.
+ simpl. rewrite <- IHn, Nshiftl_nat_S; trivial.
+ destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial.
Qed.
-Lemma eqf_xorf :
- forall f f' f'' f''',
- eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f''').
+Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
+ N.testbit_nat (N.shiftl_nat a n) m = false.
Proof.
- unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity.
+ induction n; intros m H. inversion H.
+ rewrite Nshiftl_nat_S.
+ destruct m.
+ destruct (N.shiftl_nat a n); trivial.
+ specialize (IHn m (lt_S_n _ _ H)).
+ destruct (N.shiftl_nat a n); trivial.
Qed.
-(** End of auxilliary results *)
+(** A left shift for positive numbers (used in BigN) *)
+
+Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p.
+Proof. reflexivity. Qed.
-(** This part is aimed at proving that if two numbers produce
- the same stream of bits, then they are equal. *)
+Lemma Pshiftl_nat_S :
+ forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n).
+Proof. reflexivity. Qed.
-Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a.
+Lemma Pshiftl_nat_N :
+ forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n.
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).
+ unfold Pos.shiftl_nat, N.shiftl_nat.
+ induction n; simpl; auto. now rewrite <- IHn.
Qed.
-Lemma Nbit_faithful_2 :
- forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a.
+Lemma Pshiftl_nat_plus : forall n m p,
+ Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m.
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.
+ induction m; simpl; intros. reflexivity.
+ rewrite 2 Pshiftl_nat_S. now f_equal.
+Qed.
+
+(** Semantics of bitwise operations with respect to [N.testbit_nat] *)
+
+Lemma Pxor_semantics p p' n :
+ N.testbit_nat (Pos.lxor p p') n = xorb (Pos.testbit_nat p n) (Pos.testbit_nat p' n).
+Proof.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec.
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.
+Lemma Nxor_semantics a a' n :
+ N.testbit_nat (N.lxor a a') n = xorb (N.testbit_nat a n) (N.testbit_nat a' n).
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.
- destruct p. discriminate (H0 O).
- rewrite (H p (fun n => H0 (S n))). reflexivity.
- discriminate (H0 0).
+ rewrite <- !Ntestbit_Nbit. apply N.lxor_spec.
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.
+Lemma Por_semantics p p' n :
+ Pos.testbit_nat (Pos.lor p p') n = (Pos.testbit_nat p n) || (Pos.testbit_nat p' n).
Proof.
- destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))).
- intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity.
- intro. rewrite H0. reflexivity.
- destruct p. rewrite (H p (fun n:nat => H0 (S n))). reflexivity.
- discriminate (H0 0).
- cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))).
- intro. discriminate (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))).
- intro. rewrite H0. reflexivity.
+ rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec.
Qed.
-Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'.
+Lemma Nor_semantics a a' n :
+ N.testbit_nat (N.lor a a') n = (N.testbit_nat a n) || (N.testbit_nat a' n).
Proof.
- destruct a. exact Nbit_faithful_1.
- induction p. intros a' H. apply Nbit_faithful_4. intros.
- assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
- inversion H1. reflexivity.
- assumption.
- intros. apply Nbit_faithful_3. intros.
- assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
- inversion H1. reflexivity.
- assumption.
- exact Nbit_faithful_2.
+ rewrite <- !Ntestbit_Nbit. apply N.lor_spec.
Qed.
-(** We now describe the semantics of [Nxor] in terms of bit streams. *)
+Lemma Pand_semantics p p' n :
+ N.testbit_nat (Pos.land p p') n = (Pos.testbit_nat p n) && (Pos.testbit_nat p' n).
+Proof.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec.
+Qed.
-Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0.
+Lemma Nand_semantics a a' n :
+ N.testbit_nat (N.land a a') n = (N.testbit_nat a n) && (N.testbit_nat a' n).
Proof.
- trivial.
+ rewrite <- !Ntestbit_Nbit. apply N.land_spec.
Qed.
-Lemma Nxor_sem_2 :
- forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0).
+Lemma Pdiff_semantics p p' n :
+ N.testbit_nat (Pos.ldiff p p') n = (Pos.testbit_nat p n) && negb (Pos.testbit_nat p' n).
Proof.
- intro. destruct a'. trivial.
- destruct p; trivial.
+ rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec.
+Qed.
+
+Lemma Ndiff_semantics a a' n :
+ N.testbit_nat (N.ldiff a a') n = (N.testbit_nat a n) && negb (N.testbit_nat a' n).
+Proof.
+ rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec.
Qed.
-Lemma Nxor_sem_3 :
- forall (p:positive) (a':N),
- Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0.
+(** Equality over functional streams of bits *)
+
+Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
+
+Program Instance eqf_equiv : Equivalence eqf.
+
+Local Infix "==" := eqf (at level 70, no associativity).
+
+(** If two numbers produce the same stream of bits, they are equal. *)
+
+Local Notation Step H := (fun n => H (S n)).
+
+Lemma Pbit_faithful_0 : forall p, ~(Pos.testbit_nat p == (fun _ => false)).
Proof.
- intros. destruct a'. trivial.
- simpl. destruct p0; trivial.
- destruct (Pxor p p0); trivial.
- destruct (Pxor p p0); trivial.
+ induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
+ apply (IHp (Step H)).
Qed.
-Lemma Nxor_sem_4 :
- forall (p:positive) (a':N),
- Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0).
+Lemma Pbit_faithful : forall p p', Pos.testbit_nat p == Pos.testbit_nat p' -> p = p'.
Proof.
- intros. destruct a'. trivial.
- simpl. destruct p0; trivial.
- destruct (Pxor p p0); trivial.
- destruct (Pxor p p0); trivial.
+ induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial;
+ try discriminate (H O).
+ f_equal. apply (IHp _ (Step H)).
+ destruct (Pbit_faithful_0 _ (Step H)).
+ f_equal. apply (IHp _ (Step H)).
+ symmetry in H. destruct (Pbit_faithful_0 _ (Step H)).
Qed.
-Lemma Nxor_sem_5 :
- forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0.
+Lemma Nbit_faithful : forall n n', N.testbit_nat n == N.testbit_nat n' -> n = n'.
Proof.
- destruct a; intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial.
- destruct p. apply Nxor_sem_4.
- change (Nbit (Nxor (Npos (xO p)) a') 0 = xorb false (Nbit a' 0)).
- rewrite false_xorb. apply Nxor_sem_3. apply Nxor_sem_2.
+ intros [|p] [|p'] H; trivial.
+ symmetry in H. destruct (Pbit_faithful_0 _ H).
+ destruct (Pbit_faithful_0 _ H).
+ f_equal. apply Pbit_faithful, H.
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).
+Lemma Nbit_faithful_iff : forall n n', N.testbit_nat n == N.testbit_nat n' <-> n = n'.
Proof.
- intros.
-(* pose proof (fun p1 p2 => H (Npos p1) (Npos p2)) as H'. clear H. rename H' into H.*)
- generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H.
- unfold xorf in *.
- destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity.
- destruct a' as [|p0].
- simpl Nbit; rewrite xorb_false. reflexivity.
- destruct p. destruct p0; simpl Nbit in *.
- rewrite <- H; simpl; case (Pxor p p0); trivial.
- rewrite <- H; simpl; case (Pxor p p0); trivial.
- rewrite xorb_false. reflexivity.
- destruct p0; simpl Nbit in *.
- rewrite <- H; simpl; case (Pxor p p0); trivial.
- rewrite <- H; simpl; case (Pxor p p0); trivial.
- rewrite xorb_false. reflexivity.
- simpl Nbit. rewrite false_xorb. destruct p0; 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'. induction n.
- apply Nxor_sem_5. apply Nxor_sem_6; assumption.
-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, xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')).
- apply eqf_sym, 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 (xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')).
- apply eqf_trans with (xorf (Nbit (Nxor a a')) (Nbit a'')).
- apply Nxor_semantics.
- apply eqf_xorf. apply Nxor_semantics.
- apply eqf_refl.
- apply eqf_trans with (xorf (Nbit a) (xorf (Nbit a') (Nbit a''))).
- apply xorf_assoc.
- apply eqf_trans with (xorf (Nbit a) (Nbit (Nxor a' a''))).
- apply eqf_xorf. apply eqf_refl.
- apply eqf_sym, Nxor_semantics.
- apply eqf_sym, Nxor_semantics.
+ split. apply Nbit_faithful. intros; now subst.
Qed.
+Local Close Scope N_scope.
+
(** 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.
+Notation Nbit0 := N.odd (compat "8.3").
-Definition Nodd (n:N) := Nbit0 n = true.
-Definition Neven (n:N) := Nbit0 n = false.
+Definition Nodd (n:N) := N.odd n = true.
+Definition Neven (n:N) := N.odd n = false.
-Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n.
+Lemma Nbit0_correct : forall n:N, N.testbit_nat n 0 = N.odd n.
Proof.
destruct n; trivial.
destruct p; trivial.
Qed.
-Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false.
+Lemma Ndouble_bit0 : forall n:N, N.odd (N.double n) = false.
Proof.
destruct n; trivial.
Qed.
Lemma Ndouble_plus_one_bit0 :
- forall n:N, Nbit0 (Ndouble_plus_one n) = true.
+ forall n:N, N.odd (N.succ_double n) = true.
Proof.
destruct n; trivial.
Qed.
Lemma Ndiv2_double :
- forall n:N, Neven n -> Ndouble (Ndiv2 n) = n.
+ forall n:N, Neven n -> N.double (N.div2 n) = n.
Proof.
destruct n. trivial. destruct p. intro H. discriminate H.
intros. reflexivity.
@@ -345,7 +278,7 @@ Proof.
Qed.
Lemma Ndiv2_double_plus_one :
- forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n.
+ forall n:N, Nodd n -> N.succ_double (N.div2 n) = n.
Proof.
destruct n. intro. discriminate H.
destruct p. intros. reflexivity.
@@ -354,134 +287,136 @@ Proof.
Qed.
Lemma Ndiv2_correct :
- forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit a (S n).
+ forall (a:N) (n:nat), N.testbit_nat (N.div2 a) n = N.testbit_nat 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').
+ forall a a':N, N.odd (N.lxor a a') = xorb (N.odd a) (N.odd a').
Proof.
- intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' 0).
- unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity.
+ intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O).
+ rewrite Nbit0_correct, Nbit0_correct. reflexivity.
Qed.
Lemma Nxor_div2 :
- forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a').
+ forall a a':N, N.div2 (N.lxor a a') = N.lxor (N.div2 a) (N.div2 a').
Proof.
intros. apply Nbit_faithful. unfold eqf. intro.
- rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
- unfold xorf. rewrite 2! Ndiv2_correct.
+ rewrite (Nxor_semantics (N.div2 a) (N.div2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
+ rewrite 2! Ndiv2_correct.
reflexivity.
Qed.
Lemma Nneg_bit0 :
forall a a':N,
- Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a').
+ N.odd (N.lxor a a') = true -> N.odd a = negb (N.odd a').
Proof.
intros.
- rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false.
+ rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc,
+ xorb_nilpotent, xorb_false.
reflexivity.
Qed.
Lemma Nneg_bit0_1 :
- forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 a').
+ forall a a':N, N.lxor a a' = Npos 1 -> N.odd a = negb (N.odd 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').
+ N.lxor a a' = Npos (xI p) -> N.odd a = negb (N.odd 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'.
+ N.lxor a a' = Npos (xO p) -> N.odd a = N.odd a'.
Proof.
- intros. rewrite <- (xorb_false (Nbit0 a)).
- assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity.
- rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity.
+ intros. rewrite <- (xorb_false (N.odd a)).
+ assert (H0: N.odd (Npos (xO p)) = false) by reflexivity.
+ rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb.
+ reflexivity.
Qed.
(** a lexicographic order on bits, starting from the lowest bit *)
Fixpoint Nless_aux (a a':N) (p:positive) : bool :=
match p with
- | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p'
- | _ => andb (negb (Nbit0 a)) (Nbit0 a')
+ | xO p' => Nless_aux (N.div2 a) (N.div2 a') p'
+ | _ => andb (negb (N.odd a)) (N.odd a')
end.
Definition Nless (a a':N) :=
- match Nxor a a' with
+ match N.lxor 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.
+ N.odd a = false -> N.odd a' = true -> Nless a a' = true.
Proof.
- intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+ intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
- assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+ assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
simpl. rewrite H, H0. reflexivity.
- assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+ assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
Qed.
Lemma Nbit0_gt :
forall a a',
- Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false.
+ N.odd a = true -> N.odd a' = false -> Nless a a' = false.
Proof.
- intros. destruct (Ndiscr (Nxor a a')) as [(p,H2)|H1]. unfold Nless.
+ intros. destruct (N.discr (N.lxor a a')) as [(p,H2)|H1]. unfold Nless.
rewrite H2. destruct p. simpl. rewrite H, H0. reflexivity.
- assert (H1: Nbit0 (Nxor a a') = false) by (rewrite H2; reflexivity).
+ assert (H1: N.odd (N.lxor a a') = false) by (rewrite H2; reflexivity).
rewrite (Nxor_bit0 a a'), H, H0 in H1. discriminate H1.
simpl. rewrite H, H0. reflexivity.
- assert (H2: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity).
+ assert (H2: N.odd (N.lxor a a') = false) by (rewrite H1; reflexivity).
rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2.
Qed.
Lemma Nless_not_refl : forall a, Nless a a = false.
Proof.
- intro. unfold Nless. rewrite (Nxor_nilpotent a). reflexivity.
+ intro. unfold Nless. rewrite (N.lxor_nilpotent a). reflexivity.
Qed.
Lemma Nless_def_1 :
- forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'.
+ forall a a', Nless (N.double a) (N.double a') = Nless a a'.
Proof.
destruct a; destruct a'. reflexivity.
trivial.
unfold Nless. simpl. destruct p; trivial.
- unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+ unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
trivial.
Qed.
Lemma Nless_def_2 :
forall a a',
- Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'.
+ Nless (N.succ_double a) (N.succ_double a') = Nless a a'.
Proof.
destruct a; destruct a'. reflexivity.
trivial.
unfold Nless. simpl. destruct p; trivial.
- unfold Nless. simpl. destruct (Pxor p p0). reflexivity.
+ unfold Nless. simpl. destruct (Pos.lxor p p0). reflexivity.
trivial.
Qed.
Lemma Nless_def_3 :
- forall a a', Nless (Ndouble a) (Ndouble_plus_one a') = true.
+ forall a a', Nless (N.double a) (N.succ_double 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.
+ forall a a', Nless (N.succ_double a) (N.double a') = false.
Proof.
intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0.
apply Ndouble_bit0.
@@ -490,7 +425,7 @@ Qed.
Lemma Nless_z : forall a, Nless a N0 = false.
Proof.
induction a. reflexivity.
- unfold Nless. rewrite (Nxor_neutral_right (Npos p)). induction p; trivial.
+ unfold Nless. rewrite (N.lxor_0_r (Npos p)). induction p; trivial.
Qed.
Lemma N0_less_1 :
@@ -510,26 +445,26 @@ Lemma Nless_trans :
forall a a' a'',
Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true.
Proof.
- induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0.
- destruct (Nless N0 a'') as []_eqn:Heqb. trivial.
- rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0.
- induction a' as [|a' _|a' _] using N_ind_double.
- rewrite (Nless_z (Ndouble a)) in H. discriminate H.
+ induction a as [|a IHa|a IHa] using N.binary_ind; intros a' a'' H H0.
+ case_eq (Nless N0 a'') ; intros Heqn. trivial.
+ rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0.
+ induction a' as [|a' _|a' _] using N.binary_ind.
+ rewrite (Nless_z (N.double a)) in H. discriminate H.
rewrite (Nless_def_1 a a') in H.
- induction a'' using N_ind_double.
- rewrite (Nless_z (Ndouble a')) in H0. discriminate H0.
+ induction a'' using N.binary_ind.
+ rewrite (Nless_z (N.double a')) in H0. discriminate H0.
rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a'').
exact (IHa _ _ H H0).
apply Nless_def_3.
- induction a'' as [|a'' _|a'' _] using N_ind_double.
- rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+ induction a'' as [|a'' _|a'' _] using N.binary_ind.
+ rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
apply Nless_def_3.
- induction a' as [|a' _|a' _] using N_ind_double.
- rewrite (Nless_z (Ndouble_plus_one a)) in H. discriminate H.
+ induction a' as [|a' _|a' _] using N.binary_ind.
+ rewrite (Nless_z (N.succ_double a)) in H. discriminate H.
rewrite (Nless_def_4 a a') in H. discriminate H.
- induction a'' using N_ind_double.
- rewrite (Nless_z (Ndouble_plus_one a')) in H0. discriminate H0.
+ induction a'' using N.binary_ind.
+ rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0.
rewrite (Nless_def_4 a' a'') in H0. discriminate H0.
rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H.
rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0).
@@ -538,17 +473,17 @@ Qed.
Lemma Nless_total :
forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}.
Proof.
- induction a using N_rec_double; intro a'.
- destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto.
+ induction a using N.binary_rec; intro a'.
+ case_eq (Nless N0 a') ; intros Heqb. left. left. auto.
right. rewrite (N0_less_2 a' Heqb). reflexivity.
- induction a' as [|a' _|a' _] using N_rec_double.
- destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto.
+ induction a' as [|a' _|a' _] using N.binary_rec.
+ case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto.
right. exact (N0_less_2 _ Heqb).
rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->].
left. assumption.
right. reflexivity.
left. left. apply Nless_def_3.
- induction a' as [|a' _|a' _] using N_rec_double.
+ induction a' as [|a' _|a' _] using N.binary_rec.
left. right. destruct a; reflexivity.
left. right. apply Nless_def_3.
rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->].
@@ -558,32 +493,28 @@ Qed.
(** Number of digits in a number *)
-Definition Nsize (n:N) : nat := match n with
- | N0 => 0%nat
- | Npos p => Psize p
- end.
-
+Notation Nsize := N.size_nat (compat "8.3").
(** conversions between N and bit vectors. *)
-Fixpoint P2Bv (p:positive) : Bvector (Psize p) :=
- match p return Bvector (Psize p) with
+Fixpoint P2Bv (p:positive) : Bvector (Pos.size_nat p) :=
+ match p return Bvector (Pos.size_nat p) with
| xH => Bvect_true 1%nat
- | xO p => Bcons false (Psize p) (P2Bv p)
- | xI p => Bcons true (Psize p) (P2Bv p)
+ | xO p => Bcons false (Pos.size_nat p) (P2Bv p)
+ | xI p => Bcons true (Pos.size_nat p) (P2Bv p)
end.
-Definition N2Bv (n:N) : Bvector (Nsize n) :=
- match n as n0 return Bvector (Nsize n0) with
+Definition N2Bv (n:N) : Bvector (N.size_nat n) :=
+ match n as n0 return Bvector (N.size_nat n0) with
| N0 => Bnil
| Npos p => P2Bv p
end.
Fixpoint Bv2N (n:nat)(bv:Bvector n) : N :=
match bv with
- | Vnil => N0
- | Vcons false n bv => Ndouble (Bv2N n bv)
- | Vcons true n bv => Ndouble_plus_one (Bv2N n bv)
+ | Vector.nil => N0
+ | Vector.cons false n bv => N.double (Bv2N n bv)
+ | Vector.cons true n bv => N.succ_double (Bv2N n bv)
end.
Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n.
@@ -597,15 +528,14 @@ Qed.
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.
+Lemma Bv2N_Nsize : forall n (bv:Bvector n), N.size_nat (Bv2N n bv) <= n.
Proof.
-induction n; intros.
-rewrite (V0_eq _ bv); simpl; auto.
-rewrite (VSn_eq _ _ bv); simpl.
-specialize IHn with (Vtail _ _ bv).
-destruct (Vhead _ _ bv);
- destruct (Bv2N n (Vtail bool n bv));
- simpl; auto with arith.
+induction bv; intros.
+auto.
+simpl.
+destruct h;
+ destruct (Bv2N n bv);
+ simpl ; auto with arith.
Qed.
(** In the previous lemma, we can only replace the inequality by
@@ -613,17 +543,12 @@ Qed.
Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)),
Bsign _ bv = true <->
- Nsize (Bv2N _ bv) = (S n).
+ N.size_nat (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.
+apply Vector.rectS ; intros ; simpl.
+destruct a ; compute ; split ; intros x ; now inversion x.
+ destruct a, (Bv2N (S n) v) ;
+ simpl ;intuition ; try discriminate.
Qed.
(** To state nonetheless a second result about composition of
@@ -642,7 +567,7 @@ Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n :=
(** 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.
+Lemma N2Bv_N2Bv_gen : forall (a:N), N2Bv a = N2Bv_gen (N.size_nat a) a.
Proof.
destruct a; simpl.
auto.
@@ -653,7 +578,7 @@ Qed.
[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).
+ N2Bv_gen (N.size_nat a + k) a = Vector.append (N2Bv a) (Bvect_false k).
Proof.
destruct a; simpl.
destruct k; simpl; auto.
@@ -665,49 +590,43 @@ Qed.
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.
+induction bv; intros.
+auto.
+simpl.
+generalize IHbv; clear IHbv.
unfold Bcons.
-destruct (Bv2N _ (Vtail _ _ bv));
- destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial;
+destruct (Bv2N _ bv);
+ destruct h; 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.
+ N.odd (Bv2N _ bv) = Blow _ bv.
Proof.
+apply Vector.caseS.
intros.
unfold Blow.
-rewrite (VSn_eq _ _ bv) at 1.
simpl.
-destruct (Bv2N n (Vtail bool n bv)); simpl;
- destruct (Vhead bool n bv); auto.
+destruct (Bv2N n t); simpl;
+ destruct h; auto.
Qed.
-Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool.
-Proof.
- induction bv in p |- *.
- intros.
- exfalso; inversion H.
- intros.
- destruct p.
- exact a.
- apply (IHbv p); auto with arith.
-Defined.
+Notation Bnth := (@Vector.nth_order bool).
Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n),
- Bnth _ bv p H = Nbit (Bv2N _ bv) p.
+ Bnth bv H = N.testbit_nat (Bv2N _ bv) p.
Proof.
induction bv; intros.
inversion H.
-destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto.
+destruct p ; simpl.
+ destruct (Bv2N n bv); destruct h; simpl in *; auto.
+ specialize IHbv with p (lt_S_n _ _ H).
+ simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto.
Qed.
-Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false.
+Lemma Nbit_Nsize : forall n p, N.size_nat n <= p -> N.testbit_nat n p = false.
Proof.
destruct n as [|n].
simpl; auto.
@@ -716,26 +635,31 @@ inversion H.
inversion H.
Qed.
-Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H.
+Lemma Nbit_Bth: forall n p (H:p < N.size_nat n),
+ N.testbit_nat n p = Bnth (N2Bv n) H.
Proof.
destruct n as [|n].
inversion H.
-induction n; simpl in *; intros; destruct p; auto with arith.
-inversion H; inversion H1.
+induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto.
+intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)).
Qed.
-(** Xor is the same in the two worlds. *)
+(** Binary bitwise operations are the same in the two worlds. *)
Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
- Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
+ Bv2N _ (BVxor _ bv bv') = N.lxor (Bv2N _ bv) (Bv2N _ bv').
Proof.
-induction n.
-intros.
-rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
-intros.
-rewrite (VSn_eq _ _ bv), (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.
+apply Vector.rect2 ; intros.
+now simpl.
+simpl.
+destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl.
Qed.
+Lemma Nand_BVand : forall n (bv bv' : Bvector n),
+ Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv').
+Proof.
+refine (@Vector.rect2 _ _ _ _ _); simpl; intros; auto.
+rewrite H.
+destruct a, b, (Bv2N n v1), (Bv2N n v2);
+ simpl; auto.
+Qed.