diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
| -rw-r--r-- | theories/NArith/Ndigits.v | 517 |
1 files changed, 220 insertions, 297 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 6b490dfc..b0c33595 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -1,320 +1,253 @@ (************************************************************************) (* 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-2010 *) (* \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 (only parsing). +Notation Nxor := N.lxor (only parsing). +Notation Pbit := Pos.testbit_nat (only parsing). +Notation Nbit := N.testbit_nat (only parsing). -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 (only parsing). +Notation Nxor_comm := N.lxor_comm (only parsing). +Notation Nxor_assoc := N.lxor_assoc (only parsing). +Notation Nxor_neutral_left := N.lxor_0_l (only parsing). +Notation Nxor_neutral_right := N.lxor_0_r (only parsing). +Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). -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) = Pbit 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 N_of_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) = Nbit 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, Pbit 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, Nbit 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 iter_nat_of_P. +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, + Nbit (N.shiftr_nat a n) m = Nbit 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 -> + Nbit (N.shiftl_nat a n) m = Nbit 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 -> + Nbit (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 [Nbit] *) + +Lemma Pxor_semantics p p' n : + Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit 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 : + Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit 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 : + Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit 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 : + Nbit (N.lor a a') n = (Nbit a n) || (Nbit 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 : + Nbit (Pos.land p p') n = (Pbit p n) && (Pbit 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 : + Nbit (N.land a a') n = (Nbit a n) && (Nbit 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 : + Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit 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 : + Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit 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, ~(Pbit 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', Pbit p == Pbit 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', Nbit n == Nbit 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', Nbit n == Nbit 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 (only parsing). Definition Nodd (n:N) := Nbit0 n = true. Definition Neven (n:N) := Nbit0 n = false. @@ -363,8 +296,8 @@ Qed. Lemma Nxor_bit0 : forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 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 : @@ -372,7 +305,7 @@ Lemma Nxor_div2 : 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 2! Ndiv2_correct. reflexivity. Qed. @@ -381,7 +314,8 @@ Lemma Nneg_bit0 : Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 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. @@ -404,7 +338,8 @@ Lemma Nsame_bit0 : 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. + rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. + reflexivity. Qed. (** a lexicographic order on bits, starting from the lowest bit *) @@ -511,8 +446,8 @@ Lemma Nless_trans : 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. + 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_ind_double. rewrite (Nless_z (Ndouble a)) in H. discriminate H. rewrite (Nless_def_1 a a') in H. @@ -539,10 +474,10 @@ 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. + 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. + case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto. right. exact (N0_less_2 _ Heqb). rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. left. assumption. @@ -558,11 +493,7 @@ 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 (only parsing). (** conversions between N and bit vectors. *) @@ -581,9 +512,9 @@ Definition N2Bv (n:N) : Bvector (Nsize n) := 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 => Ndouble (Bv2N n bv) + | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. @@ -599,13 +530,12 @@ Qed. 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. -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 @@ -615,15 +545,10 @@ 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. +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 @@ -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 (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k). Proof. destruct a; simpl. destruct k; simpl; auto. @@ -665,13 +590,13 @@ 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. @@ -680,31 +605,25 @@ Qed. Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), Nbit0 (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 = Nbit (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. @@ -716,26 +635,30 @@ 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 < Nsize n), Nbit 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'). 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. |