From 9764ebbb67edf73a147c536a3c4f4ed0f1a7ce9e Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 6 Dec 2010 15:47:32 +0000 Subject: Numbers and bitwise functions. See NatInt/NZBits.v for the common axiomatization of bitwise functions over naturals / integers. Some specs aren't pretty, but easier to prove, see alternate statements in property functors {N,Z}Bits. Negative numbers are considered via the two's complement convention. We provide implementations for N (in Ndigits.v), for nat (quite dummy, just for completeness), for Z (new file Zdigits_def), for BigN (for the moment partly by converting to N, to be improved soon) and for BigZ. NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in the reversed order (for consistency with the rest of the world): for instance BigN.shiftl 1 10 is 2^10. NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2) on negative numbers. For the moment I've kept it intact, and have just added a Zdiv2' which is truly equivalent to (Zdiv _ 2). To reorganize someday ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNat.v | 178 +++++++++++++++++---------- theories/NArith/Ndigits.v | 304 ++++++++++++++++++++++++++++++---------------- theories/NArith/Ndist.v | 2 +- 3 files changed, 317 insertions(+), 167 deletions(-) (limited to 'theories/NArith') diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 51c5b462b..81e2e06e4 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -27,6 +27,13 @@ Arguments Scope Npos [positive_scope]. Local Open Scope N_scope. +(** Some local ad-hoc notation, since no interpretation of numerical + constants is available yet. *) + +Local Notation "0" := N0 : N_scope. +Local Notation "1" := (Npos 1) : N_scope. +Local Notation "2" := (Npos 2) : N_scope. + Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. Proof. destruct n; auto. @@ -37,42 +44,59 @@ Defined. Definition Ndouble_plus_one x := match x with - | N0 => Npos 1 - | Npos p => Npos (xI p) + | 0 => Npos 1 + | Npos p => Npos p~1 end. (** Operation x -> 2*x *) Definition Ndouble n := match n with - | N0 => N0 - | Npos p => Npos (xO p) + | 0 => 0 + | Npos p => Npos p~0 end. (** Successor *) Definition Nsucc n := match n with - | N0 => Npos 1 + | 0 => Npos 1 | Npos p => Npos (Psucc p) end. (** Predecessor *) Definition Npred (n : N) := match n with -| N0 => N0 +| 0 => 0 | Npos p => match p with - | xH => N0 + | xH => 0 | _ => Npos (Ppred p) end end. +(** The successor of a N can be seen as a positive *) + +Definition Nsucc_pos (n : N) : positive := + match n with + | N0 => 1%positive + | Npos p => Psucc p + end. + +(** Similarly, the predecessor of a positive, seen as a N *) + +Definition Ppred_N (p:positive) : N := + match p with + | 1 => N0 + | p~1 => Npos (p~0) + | p~0 => Npos (Pdouble_minus_one p) + end%positive. + (** Addition *) Definition Nplus n m := match n, m with - | N0, _ => m - | _, N0 => n + | 0, _ => m + | _, 0 => n | Npos p, Npos q => Npos (p + q) end. @@ -82,12 +106,12 @@ Infix "+" := Nplus : N_scope. Definition Nminus (n m : N) := match n, m with -| N0, _ => N0 -| n, N0 => n +| 0, _ => 0 +| n, 0 => n | Npos n', Npos m' => match Pminus_mask n' m' with | IsPos p => Npos p - | _ => N0 + | _ => 0 end end. @@ -97,8 +121,8 @@ Infix "-" := Nminus : N_scope. Definition Nmult n m := match n, m with - | N0, _ => N0 - | _, N0 => N0 + | 0, _ => 0 + | _, 0 => 0 | Npos p, Npos q => Npos (p * q) end. @@ -108,7 +132,7 @@ Infix "*" := Nmult : N_scope. Definition Neqb n m := match n, m with - | N0, N0 => true + | 0, 0 => true | Npos n, Npos m => Peqb n m | _,_ => false end. @@ -117,9 +141,9 @@ Definition Neqb n m := Definition Ncompare n m := match n, m with - | N0, N0 => Eq - | N0, Npos m' => Lt - | Npos n', N0 => Gt + | 0, 0 => Eq + | 0, Npos m' => Lt + | Npos n', 0 => Gt | Npos n', Npos m' => (n' ?= m')%positive Eq end. @@ -162,7 +186,7 @@ Definition nat_of_N (a:N) := Definition N_of_nat (n:nat) := match n with - | O => N0 + | O => 0 | S n' => Npos (P_of_succ_nat n') end. @@ -178,43 +202,43 @@ Defined. Lemma N_ind_double : forall (a:N) (P:N -> Prop), - P N0 -> + P 0 -> (forall a, P a -> P (Ndouble a)) -> (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. - intros; elim a. trivial. - simple induction p. intros. - apply (H1 (Npos p0)); trivial. - intros; apply (H0 (Npos p0)); trivial. - intros; apply (H1 N0); assumption. + intros a P P0 P2 PS2. destruct a as [|p]. trivial. + induction p as [p IHp|p IHp| ]. + now apply (PS2 (Npos p)). + now apply (P2 (Npos p)). + now apply (PS2 0). Qed. Lemma N_rec_double : forall (a:N) (P:N -> Set), - P N0 -> + P 0 -> (forall a, P a -> P (Ndouble a)) -> (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. - intros; elim a. trivial. - simple induction p. intros. - apply (H1 (Npos p0)); trivial. - intros; apply (H0 (Npos p0)); trivial. - intros; apply (H1 N0); assumption. + intros a P P0 P2 PS2. destruct a as [|p]. trivial. + induction p as [p IHp|p IHp| ]. + now apply (PS2 (Npos p)). + now apply (P2 (Npos p)). + now apply (PS2 0). Qed. (** Peano induction on binary natural numbers *) Definition Nrect - (P : N -> Type) (a : P N0) + (P : N -> Type) (a : P 0) (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n := let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in let P' (p : positive) := P (Npos p) in match n return (P n) with -| N0 => a -| Npos p => Prect P' (f N0 a) f' p +| 0 => a +| Npos p => Prect P' (f 0 a) f' p end. -Theorem Nrect_base : forall P a f, Nrect P a f N0 = a. +Theorem Nrect_base : forall P a f, Nrect P a f 0 = a. Proof. intros P a f; simpl; reflexivity. Qed. @@ -229,7 +253,7 @@ Definition Nind (P : N -> Prop) := Nrect P. Definition Nrec (P : N -> Set) := Nrect P. -Theorem Nrec_base : forall P a f, Nrec P a f N0 = a. +Theorem Nrec_base : forall P a f, Nrec P a f 0 = a. Proof. intros P a f; unfold Nrec; apply Nrect_base. Qed. @@ -248,14 +272,43 @@ case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ). intro H; false_hyp H Psucc_not_one. Qed. +Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1). +Proof. + intros [|[p|p|]]; trivial. +Qed. + +Lemma Nsucc_pred : forall n, n<>0 -> Nsucc (Npred n) = n. +Proof. + intros [|n] H; (now destruct H) || clear H. + rewrite Npred_minus. simpl. destruct n; simpl; trivial. + f_equal; apply Psucc_o_double_minus_one_eq_xO. +Qed. + +(** Properties of mixed successor and predecessor. *) + +Lemma Ppred_N_spec : forall p, Ppred_N p = Npred (Npos p). +Proof. + now destruct p. +Qed. + +Lemma Nsucc_pos_spec : forall n, Npos (Nsucc_pos n) = Nsucc n. +Proof. + now destruct n. +Qed. + +Lemma Ppred_Nsucc : forall n, Ppred_N (Nsucc_pos n) = n. +Proof. + intros. now rewrite Ppred_N_spec, Nsucc_pos_spec, Npred_succ. +Qed. + (** Properties of addition *) -Theorem Nplus_0_l : forall n:N, N0 + n = n. +Theorem Nplus_0_l : forall n:N, 0 + n = n. Proof. reflexivity. Qed. -Theorem Nplus_0_r : forall n:N, n + N0 = n. +Theorem Nplus_0_r : forall n:N, n + 0 = n. Proof. destruct n; reflexivity. Qed. @@ -285,7 +338,7 @@ destruct n, m. simpl; rewrite Pplus_succ_permute_l; reflexivity. Qed. -Theorem Nsucc_0 : forall n : N, Nsucc n <> N0. +Theorem Nsucc_0 : forall n : N, Nsucc n <> 0. Proof. now destruct n. Qed. @@ -308,7 +361,7 @@ Qed. (** Properties of subtraction. *) -Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'. +Lemma Nminus_N0_Nle : forall n n' : N, n - n' = 0 <-> n <= n'. Proof. intros [| p] [| q]; unfold Nle; simpl; split; intro H; try easy. @@ -319,7 +372,7 @@ subst. now rewrite Pminus_mask_diag. now rewrite Pminus_mask_Lt. Qed. -Theorem Nminus_0_r : forall n : N, n - N0 = n. +Theorem Nminus_0_r : forall n : N, n - 0 = n. Proof. now destruct n. Qed. @@ -332,14 +385,9 @@ simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. now destruct (Pminus_mask p q) as [|[r|r|]|]. Qed. -Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1). -Proof. - intros [|[p|p|]]; trivial. -Qed. - (** Properties of multiplication *) -Theorem Nmult_0_l : forall n:N, N0 * n = N0. +Theorem Nmult_0_l : forall n:N, 0 * n = 0. Proof. reflexivity. Qed. @@ -386,7 +434,7 @@ Proof. intros. rewrite ! (Nmult_comm p); apply Nmult_plus_distr_r. Qed. -Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m. +Theorem Nmult_reg_r : forall n m p:N, p <> 0 -> n * p = m * p -> n = m. Proof. destruct p; intros Hp H. contradiction Hp; reflexivity. @@ -405,6 +453,11 @@ Qed. (** Properties of comparison *) +Lemma Nle_0 : forall n, 0<=n. +Proof. + now destruct n. +Qed. + Lemma Ncompare_refl : forall n, (n ?= n) = Eq. Proof. destruct n; simpl; auto. @@ -524,7 +577,7 @@ Qed. (** 0 is the least natural number *) -Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. +Theorem Ncompare_0 : forall n : N, Ncompare n 0 <> Lt. Proof. destruct n; discriminate. Qed. @@ -533,8 +586,8 @@ Qed. Definition Ndiv2 (n:N) := match n with - | N0 => N0 - | Npos 1 => N0 + | 0 => 0 + | Npos 1 => 0 | Npos (p~0) => Npos p | Npos (p~1) => Npos p end. @@ -565,14 +618,14 @@ Qed. Definition Npow n p := match p, n with - | N0, _ => Npos 1 - | _, N0 => N0 + | 0, _ => Npos 1 + | _, 0 => 0 | Npos p, Npos q => Npos (Ppow q p) end. Infix "^" := Npow : N_scope. -Lemma Npow_0_r : forall n, n ^ N0 = Npos 1. +Lemma Npow_0_r : forall n, n ^ 0 = Npos 1. Proof. reflexivity. Qed. Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p. @@ -585,13 +638,13 @@ Qed. Definition Nlog2 n := match n with - | N0 => N0 - | Npos 1 => N0 + | 0 => 0 + | Npos 1 => 0 | Npos (p~0) => Npos (Psize_pos p) | Npos (p~1) => Npos (Psize_pos p) end. -Lemma Nlog2_spec : forall n, N0 < n -> +Lemma Nlog2_spec : forall n, 0 < n -> (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)). Proof. intros [|[p|p|]] H; discriminate H || clear H; simpl; split. @@ -605,7 +658,7 @@ Proof. reflexivity. Qed. -Lemma Nlog2_nonpos : forall n, n<=N0 -> Nlog2 n = N0. +Lemma Nlog2_nonpos : forall n, n<=0 -> Nlog2 n = 0. Proof. intros [|n] Hn. reflexivity. now destruct Hn. Qed. @@ -614,19 +667,16 @@ Qed. Definition Neven n := match n with - | N0 => true + | 0 => true | Npos (xO _) => true | _ => false end. Definition Nodd n := negb (Neven n). -Local Notation "1" := (Npos 1) : N_scope. -Local Notation "2" := (Npos 2) : N_scope. - Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m. Proof. destruct n. - split. now exists N0. + split. now exists 0. trivial. destruct p; simpl; split; trivial; try discriminate. intros (m,H). now destruct m. @@ -642,5 +692,5 @@ Proof. destruct p; simpl; split; trivial; try discriminate. exists (Npos p). reflexivity. intros (m,H). now destruct m. - exists N0. reflexivity. + exists 0. reflexivity. Qed. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 98e88c6a2..0dd2fceaa 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -7,7 +7,7 @@ (************************************************************************) Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat - Pnat Nnat Ndiv_def. + Pnat Nnat Ndiv_def Compare_dec Lt Minus. Local Open Scope positive_scope. @@ -192,12 +192,79 @@ Proof. destruct a. trivial. apply Pbit_Ptestbit. Qed. +(** Correctness proof for [Ntestbit]. + + Ideally, we would say that (Ntestbit a n) is (a/2^n) mod 2 + but that requires results about division we don't have yet. + Instead, we use a longer but simplier specification, and + obtain the nice equation later as a derived property. +*) + +Lemma Nsuccdouble_bounds : forall n p, n

1+2*n<2*p. +Proof. + intros [|n] [|p] H; try easy. + change (n0 *) + destruct (IH (Npred (Npos p))) as (l & h & (_,H) & EQ). clear IH. + exists (1+2*l). exists h. + set (b := if Ntestbit (Npos a) (Npred (Npos p)) then 1 else 0) in EQ. + change (if Ntestbit _ _ then 1 else 0) with b. + rewrite <- (Nsucc_pred (Npos p)), Npow_succ_r by discriminate. + set (p' := Npred (Npos p)) in *. + split. split. apply Nle_0. now apply Nsuccdouble_bounds. + change (Npos a~1) with (1+2*(Npos a)). rewrite EQ. + rewrite <-Nplus_assoc. f_equal. + rewrite Nmult_plus_distr_l. f_equal. + now rewrite !Nmult_assoc, (Nmult_comm 2). + (* a~0 n=0 *) + exists 0. exists (Npos a). simpl. repeat split; now rewrite ?Pmult_1_r. + (* a~0 n>0 *) + destruct (IH (Npred (Npos p))) as (l & h & (_,H) & EQ). clear IH. + exists (2*l). exists h. + set (b := if Ntestbit (Npos a) (Npred (Npos p)) then 1 else 0) in EQ. + change (if Ntestbit _ _ then 1 else 0) with b. + rewrite <- (Nsucc_pred (Npos p)), !Npow_succ_r by discriminate. + set (p' := Npred (Npos p)) in *. + split. split. apply Nle_0. now destruct l, (2^p'). + change (Npos a~0) with (2*(Npos a)). rewrite EQ. + rewrite Nmult_plus_distr_l. f_equal. + now rewrite !Nmult_assoc, (Nmult_comm 2). + (* 1 n=0 *) + exists 0. exists 0. simpl. now repeat split. + (* 1 n>0 *) + exists 1. exists 0. simpl. repeat split. easy. now apply Ppow_gt_1. +Qed. + (** Equivalence of shifts, N and nat versions *) +Lemma Nshiftr_nat_S : forall a n, + Nshiftr_nat a (S n) = Ndiv2 (Nshiftr_nat a n). +Proof. + reflexivity. +Qed. + +Lemma Nshiftl_nat_S : forall a n, + Nshiftl_nat a (S n) = Ndouble (Nshiftl_nat a n). +Proof. + reflexivity. +Qed. + Lemma Nshiftr_nat_equiv : forall a n, Nshiftr_nat a (nat_of_N n) = Nshiftr a n. Proof. - intros a [|n]; simpl; unfold Nshiftr_nat. + intros a [|n]; simpl. unfold Nshiftr_nat. trivial. symmetry. apply iter_nat_of_P. Qed. @@ -224,166 +291,199 @@ Qed. (** Correctness proofs for shifts *) -Lemma Nshiftl_mult_pow : forall a n, Nshiftl a n = a * 2^n. +Lemma Nshiftr_nat_spec : forall a n m, + Nbit (Nshiftr_nat a n) m = Nbit a (m+n). Proof. - intros [|a] [|n]; simpl; trivial. - now rewrite Pmult_1_r. - f_equal. - set (f x := Pmult x a). - rewrite Pmult_comm. fold (f (2^n))%positive. - change a with (f xH). - unfold Ppow. symmetry. now apply iter_pos_swap_gen. + induction n; intros m. + now rewrite <- plus_n_O. + simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S. + destruct (Nshiftr_nat a n) as [|[p|p|]]; simpl; trivial. Qed. -(* -Lemma Nshiftr_div_pow : forall a n, Nshiftr a n = a / 2^n. -*) - -(** Equality over functional streams of bits *) +Lemma Nshiftr_spec : forall a n m, + Ntestbit (Nshiftr a n) m = Ntestbit a (m+n). +Proof. + intros. + rewrite <- Nshiftr_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nplus. + apply Nshiftr_nat_spec. +Qed. -Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. +Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> + Nbit (Nshiftl_nat a n) m = Nbit a (m-n). +Proof. + 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 (Nshiftl_nat a n) as [|[p|p|]]; simpl; trivial. +Qed. -Instance eqf_equiv : Equivalence eqf. +Lemma Nshiftl_spec_high : forall a n m, n<=m -> + Ntestbit (Nshiftl a n) m = Ntestbit a (m-n). Proof. - split; congruence. + intros. + rewrite <- Nshiftl_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nminus. + apply Nshiftl_nat_spec_high. + apply nat_compare_le. now rewrite <- nat_of_Ncompare. Qed. -Local Infix "==" := eqf (at level 70, no associativity). +Lemma Nshiftl_nat_spec_low : forall a n m, (m + Nbit (Nshiftl_nat a n) m = false. +Proof. + induction n; intros m H. inversion H. + rewrite Nshiftl_nat_S. + destruct m. + destruct (Nshiftl_nat a n); trivial. + specialize (IHn m (lt_S_n _ _ H)). + destruct (Nshiftl_nat a n); trivial. +Qed. -(** If two numbers produce the same stream of bits, they are equal. *) +Lemma Nshiftl_spec_low : forall a n m, m + Ntestbit (Nshiftl a n) m = false. +Proof. + intros. + rewrite <- Nshiftl_nat_equiv, <- Nbit_Ntestbit. + apply Nshiftl_nat_spec_low. + apply nat_compare_lt. now rewrite <- nat_of_Ncompare. +Qed. -Local Notation Step H := (fun n => H (S n)). +(** Semantics of bitwise operations *) -Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)). +Lemma Pxor_semantics : forall p p' n, + Nbit (Pxor p p') n = xorb (Pbit p n) (Pbit p' n). Proof. - induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). - apply (IHp (Step H)). + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) || + now destruct Pbit. Qed. -Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'. +Lemma Nxor_semantics : forall a a' n, + Nbit (Nxor a a') n = xorb (Nbit a n) (Nbit a' n). Proof. - 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)). + intros [|p] [|p'] n; simpl; trivial. + now destruct Pbit. + now destruct Pbit. + apply Pxor_semantics. Qed. -Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'. +Lemma Nxor_spec : forall a a' n, + Ntestbit (Nxor a a') n = xorb (Ntestbit a n) (Ntestbit a' n). Proof. - intros [|p] [|p'] H; trivial. - symmetry in H. destruct (Pbit_faithful_0 _ H). - destruct (Pbit_faithful_0 _ H). - f_equal. apply Pbit_faithful, H. + intros. rewrite <- !Nbit_Ntestbit. apply Nxor_semantics. Qed. -Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'. +Lemma Por_semantics : forall p p' n, + Pbit (Por p p') n = (Pbit p n) || (Pbit p' n). Proof. - split. apply Nbit_faithful. intros; now subst. + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; + apply (IHp p' n) || now rewrite orb_false_r. Qed. - -(** Bit operations for functional streams of bits *) - -Definition orf (f g:nat -> bool) (n:nat) := (f n) || (g n). -Definition andf (f g:nat -> bool) (n:nat) := (f n) && (g n). -Definition difff (f g:nat -> bool) (n:nat) := (f n) && negb (g n). -Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n). - -Instance eqf_orf : Proper (eqf==>eqf==>eqf) orf. +Lemma Nor_semantics : forall a a' n, + Nbit (Nor a a') n = (Nbit a n) || (Nbit a' n). Proof. - unfold orf. congruence. + intros [|p] [|p'] n; simpl; trivial. + now rewrite orb_false_r. + apply Por_semantics. Qed. -Instance eqf_andf : Proper (eqf==>eqf==>eqf) andf. +Lemma Nor_spec : forall a a' n, + Ntestbit (Nor a a') n = (Ntestbit a n) || (Ntestbit a' n). Proof. - unfold andf. congruence. + intros. rewrite <- !Nbit_Ntestbit. apply Nor_semantics. Qed. -Instance eqf_difff : Proper (eqf==>eqf==>eqf) difff. +Lemma Pand_semantics : forall p p' n, + Nbit (Pand p p') n = (Pbit p n) && (Pbit p' n). Proof. - unfold difff. congruence. + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) || + now rewrite andb_false_r. Qed. -Instance eqf_xorf : Proper (eqf==>eqf==>eqf) xorf. +Lemma Nand_semantics : forall a a' n, + Nbit (Nand a a') n = (Nbit a n) && (Nbit a' n). Proof. - unfold xorf. congruence. + intros [|p] [|p'] n; simpl; trivial. + now rewrite andb_false_r. + apply Pand_semantics. Qed. -(** We now describe the semantics of [Nxor] and other bitwise - operations in terms of bit streams. *) - -Lemma Pxor_semantics : forall p p', - Nbit (Pxor p p') == xorf (Pbit p) (Pbit p'). +Lemma Nand_spec : forall a a' n, + Ntestbit (Nand a a') n = (Ntestbit a n) && (Ntestbit a' n). Proof. - induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; - (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) || - (unfold xorf; now rewrite ?xorb_false_l, ?xorb_false_r). + intros. rewrite <- !Nbit_Ntestbit. apply Nand_semantics. Qed. -Lemma Nxor_semantics : forall a a', - Nbit (Nxor a a') == xorf (Nbit a) (Nbit a'). +Lemma Pdiff_semantics : forall p p' n, + Nbit (Pdiff p p') n = (Pbit p n) && negb (Pbit p' n). Proof. - intros [|p] [|p'] n; simpl; unfold xorf; trivial. - now rewrite xorb_false_l. - now rewrite xorb_false_r. - apply Pxor_semantics. + induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) || + now rewrite andb_true_r. Qed. -Lemma Por_semantics : forall p p', - Pbit (Por p p') == orf (Pbit p) (Pbit p'). +Lemma Ndiff_semantics : forall a a' n, + Nbit (Ndiff a a') n = (Nbit a n) && negb (Nbit a' n). Proof. - induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; - unfold orf; apply (IHp p' n) || now rewrite orb_false_r. + intros [|p] [|p'] n; simpl; trivial. + simpl. now rewrite andb_true_r. + apply Pdiff_semantics. Qed. -Lemma Nor_semantics : forall a a', - Nbit (Nor a a') == orf (Nbit a) (Nbit a'). +Lemma Ndiff_spec : forall a a' n, + Ntestbit (Ndiff a a') n = (Ntestbit a n) && negb (Ntestbit a' n). Proof. - intros [|p] [|p'] n; simpl; unfold orf; trivial. - now rewrite orb_false_r. - apply Por_semantics. + intros. rewrite <- !Nbit_Ntestbit. apply Ndiff_semantics. Qed. -Lemma Pand_semantics : forall p p', - Nbit (Pand p p') == andf (Pbit p) (Pbit p'). + +(** 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. - induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; - (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) || - (unfold andf; now rewrite andb_false_r). + induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). + apply (IHp (Step H)). Qed. -Lemma Nand_semantics : forall a a', - Nbit (Nand a a') == andf (Nbit a) (Nbit a'). +Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'. Proof. - intros [|p] [|p'] n; simpl; unfold andf; trivial. - now rewrite andb_false_r. - apply Pand_semantics. + 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 Pdiff_semantics : forall p p', - Nbit (Pdiff p p') == difff (Pbit p) (Pbit p'). +Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'. Proof. - induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl; - (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) || - (unfold difff; simpl; now rewrite andb_true_r). + 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 Ndiff_semantics : forall a a', - Nbit (Ndiff a a') == difff (Nbit a) (Nbit a'). +Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'. Proof. - intros [|p] [|p'] n; simpl; unfold difff; trivial. - simpl. now rewrite andb_true_r. - apply Pdiff_semantics. + split. apply Nbit_faithful. intros; now subst. Qed. Hint Rewrite Nxor_semantics Nor_semantics Nand_semantics Ndiff_semantics : bitwise_semantics. Ltac bitwise_semantics := - apply Nbit_faithful; autorewrite with bitwise_semantics; - intro n; unfold xorf, orf, andf, difff. + apply Nbit_faithful; intro n; autorewrite with bitwise_semantics. (** Now, we can easily deduce properties of [Nxor] and others from properties of [xorb] and others. *) @@ -391,7 +491,7 @@ Ltac bitwise_semantics := Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'. Proof. intros a a' H. bitwise_semantics. apply xorb_eq. - rewrite <- Nbit_faithful_iff, Nxor_semantics in H. apply H. + now rewrite <- Nxor_semantics, H. Qed. Lemma Nxor_nilpotent : forall a, Nxor a a = 0. @@ -593,7 +693,7 @@ 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' O). - unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity. + rewrite Nbit0_correct, Nbit0_correct. reflexivity. Qed. Lemma Nxor_div2 : @@ -601,7 +701,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. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 0b61718f8..9d399f5cd 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -301,7 +301,7 @@ Proof. cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false). intros. apply H1. reflexivity. intro a''. case a''. intro. reflexivity. - intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). unfold xorf in |- *. + intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) (refl_equal (Nplength (Npos p))) k H0). -- cgit v1.2.3