diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 642 |
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. |