diff options
Diffstat (limited to 'theories/NArith/Ndigits.v')
-rw-r--r-- | theories/NArith/Ndigits.v | 108 |
1 files changed, 54 insertions, 54 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index fb32274e..b6c18e9b 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndigits.v 11735 2009-01-02 17:22:31Z herbelin $ i*) +(*i $Id$ i*) Require Import Bool. Require Import Bvector. @@ -17,7 +17,7 @@ Require Import BinNat. (** [xor] *) -Fixpoint Pxor (p1 p2:positive) {struct p1} : N := +Fixpoint Pxor (p1 p2:positive) : N := match p1, p2 with | xH, xH => N0 | xH, xO p2 => Npos (xI p2) @@ -27,7 +27,7 @@ Fixpoint Pxor (p1 p2:positive) {struct p1} : N := | 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) + | xI p1, xI p2 => Ndouble (Pxor p1 p2) end. Definition Nxor (n n':N) := @@ -65,7 +65,7 @@ Proof. simpl. rewrite IHp; reflexivity. Qed. -(** Checking whether a particular bit is set on not *) +(** Checking whether a particular bit is set on not *) Fixpoint Pbit (p:positive) : nat -> bool := match p with @@ -134,13 +134,13 @@ Qed. (** End of auxilliary results *) -(** This part is aimed at proving that if two numbers produce +(** 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. + 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. @@ -196,7 +196,7 @@ Proof. assert (Npos p = Npos p') by exact (IHp (Npos p') H0). inversion H1. reflexivity. assumption. - intros. apply Nbit_faithful_3. intros. + intros. apply Nbit_faithful_3. intros. assert (Npos p = Npos p') by exact (IHp (Npos p') H0). inversion H1. reflexivity. assumption. @@ -257,7 +257,7 @@ Proof. 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]. + 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. @@ -273,13 +273,13 @@ 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. + unfold eqf. intros; generalize a, a'. induction n. apply Nxor_sem_5. apply Nxor_sem_6; assumption. Qed. -(** Consequences: +(** Consequences: - only equal numbers lead to a null xor - - xor is associative + - xor is associative *) Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'. @@ -306,7 +306,7 @@ Proof. apply eqf_sym, Nxor_semantics. Qed. -(** Checking whether a number is odd, i.e. +(** Checking whether a number is odd, i.e. if its lower bit is set. *) Definition Nbit0 (n:N) := @@ -380,8 +380,8 @@ Lemma Nneg_bit0 : forall a a':N, Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). Proof. - intros. - rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. + intros. + rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. reflexivity. Qed. @@ -402,14 +402,14 @@ 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)). + 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. Qed. (** a lexicographic order on bits, starting from the lowest bit *) -Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool := +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') @@ -430,7 +430,7 @@ Proof. assert (H1: Nbit0 (Nxor 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: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. @@ -443,7 +443,7 @@ Proof. assert (H1: Nbit0 (Nxor 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: Nbit0 (Nxor a a') = false) by (rewrite H1; reflexivity). rewrite (Nxor_bit0 a a'), H, H0 in H2. discriminate H2. Qed. @@ -496,14 +496,14 @@ Qed. Lemma N0_less_1 : forall a, Nless N0 a = true -> {p : positive | a = Npos p}. Proof. - destruct a. intros. discriminate. + destruct a. discriminate. intros. exists p. reflexivity. Qed. Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0. Proof. induction a as [|p]; intro H. trivial. - elimtype False. induction p as [|p IHp|]; discriminate || simpl; auto using IHp. + exfalso. induction p as [|p IHp|]; discriminate || simpl; auto using IHp. Qed. Lemma Nless_trans : @@ -534,7 +534,7 @@ Proof. 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). Qed. - + Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. @@ -558,7 +558,7 @@ Qed. (** Number of digits in a number *) -Definition Nsize (n:N) : nat := match n with +Definition Nsize (n:N) : nat := match n with | N0 => 0%nat | Npos p => Psize p end. @@ -566,35 +566,35 @@ Definition Nsize (n:N) : nat := match n with (** 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 (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 + 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 +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) + | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. -Proof. +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 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. @@ -603,16 +603,16 @@ 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)); +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 <-> +Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), + Bsign _ bv = true <-> Nsize (Bv2N _ bv) = (S n). Proof. induction n; intro. @@ -621,18 +621,18 @@ 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)); +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 : *) +(** 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 +Fixpoint N2Bv_gen (n:nat)(a:N) : Bvector n := + match n return Bvector n with | 0 => Bnil - | S n => match a with + | 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)) @@ -649,10 +649,10 @@ auto. induction p; simpl; intros; auto; congruence. Qed. -(** In fact, if [k] is large enough, [N2Bv_gen k a] contains all digits of +(** 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), +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. @@ -662,7 +662,7 @@ Qed. (** Here comes now the second composition result. *) -Lemma N2Bv_Bv2N : forall n (bv:Bvector n), +Lemma N2Bv_Bv2N : forall n (bv:Bvector n), N2Bv_gen n (Bv2N n bv) = bv. Proof. induction n; intros. @@ -670,36 +670,36 @@ 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; +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)), +Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), Nbit0 (Bv2N _ bv) = Blow _ bv. Proof. intros. unfold Blow. rewrite (VSn_eq _ _ bv) at 1. simpl. -destruct (Bv2N n (Vtail bool n 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. + induction bv in p |- *. intros. - elimtype False; inversion H. + exfalso; 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), +Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), Bnth _ bv p H = Nbit (Bv2N _ bv) p. Proof. induction bv; intros. @@ -726,7 +726,7 @@ Qed. (** Xor is the same in the two worlds. *) -Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), +Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). Proof. induction n. @@ -735,7 +735,7 @@ 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 (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. |