diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 89 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 412 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 767 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 338 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 177 |
5 files changed, 1778 insertions, 5 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index b4582d51..78353145 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinNat.v 8685 2006-04-06 13:22:02Z letouzey $ i*) +(*i $Id: BinNat.v 8771 2006-04-29 11:55:57Z letouzey $ i*) Require Import BinPos. Unset Boxed Definitions. @@ -29,6 +29,12 @@ Arguments Scope Npos [positive_scope]. Open Local Scope N_scope. +Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. +Proof. + destruct n; auto. + left; exists p; auto. +Defined. + (** Operation x -> 2*x+1 *) Definition Ndouble_plus_one x := @@ -39,10 +45,11 @@ Definition Ndouble_plus_one x := (** Operation x -> 2*x *) -Definition Ndouble n := match n with - | N0 => N0 - | Npos p => Npos (xO p) - end. +Definition Ndouble n := + match n with + | N0 => N0 + | Npos p => Npos (xO p) + end. (** Successor *) @@ -86,6 +93,34 @@ Definition Ncompare n m := Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +(** convenient induction principles *) + +Lemma N_ind_double : + forall (a:N) (P:N -> Prop), + P N0 -> + (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. +Qed. + +Lemma N_rec_double : + forall (a:N) (P:N -> Set), + P N0 -> + (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. +Qed. + (** Peano induction on binary natural numbers *) Theorem Nind : @@ -211,3 +246,47 @@ destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H; reflexivity || (try discriminate H). rewrite (Pcompare_Eq_eq n m H); reflexivity. Qed. + +Lemma Ncompare_refl : forall n, (n ?= n) = Eq. +Proof. +destruct n; simpl; auto. +apply Pcompare_refl. +Qed. + +Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n). +Proof. +destruct n; destruct m; simpl; auto. +exact (Pcompare_antisym p p0 Eq). +Qed. + +(** Dividing by 2 *) + +Definition Ndiv2 (n:N) := + match n with + | N0 => N0 + | Npos 1 => N0 + | Npos (xO p) => Npos p + | Npos (xI p) => Npos p + end. + +Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndouble_plus_one_div2 : + forall n:N, Ndiv2 (Ndouble_plus_one n) = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m. +Proof. + intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2. +Qed. + +Lemma Ndouble_plus_one_inj : + forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m. +Proof. + intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. +Qed. diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v new file mode 100644 index 00000000..df2da25b --- /dev/null +++ b/theories/NArith/Ndec.v @@ -0,0 +1,412 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Ndec.v 8733 2006-04-25 22:52:18Z letouzey $ i*) + +Require Import Bool. +Require Import Sumbool. +Require Import Arith. +Require Import BinPos. +Require Import BinNat. +Require Import Pnat. +Require Import Nnat. +Require Import Ndigits. + +(** A boolean equality over [N] *) + +Fixpoint Peqb (p1 p2:positive) {struct p2} : bool := + match p1, p2 with + | xH, xH => true + | xO p'1, xO p'2 => Peqb p'1 p'2 + | xI p'1, xI p'2 => Peqb p'1 p'2 + | _, _ => false + end. + +Lemma Peqb_correct : forall p, Peqb p p = true. +Proof. +induction p; auto. +Qed. + +Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq. +Proof. + induction p; destruct p'; simpl; intros; try discriminate; auto. +Qed. + +Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. +Proof. +intros; rewrite <- (Pcompare_Eq_eq _ _ H). +apply Peqb_correct. +Qed. + +Definition Neqb (a a':N) := + match a, a' with + | N0, N0 => true + | Npos p, Npos p' => Peqb p p' + | _, _ => false + end. + +Lemma Neqb_correct : forall n, Neqb n n = true. +Proof. + destruct n; trivial. + simpl; apply Peqb_correct. +Qed. + +Lemma Neqb_Ncompare : forall n n', Neqb n n' = true -> Ncompare n n' = Eq. +Proof. + destruct n; destruct n'; simpl; intros; try discriminate; auto; apply Peqb_Pcompare; auto. +Qed. + +Lemma Ncompare_Neqb : forall n n', Ncompare n n' = Eq -> Neqb n n' = true. +Proof. +intros; rewrite <- (Ncompare_Eq_eq _ _ H). +apply Neqb_correct. +Qed. + +Lemma Neqb_complete : forall a a', Neqb a a' = true -> a = a'. +Proof. + intros. + apply Ncompare_Eq_eq. + apply Neqb_Ncompare; auto. +Qed. + +Lemma Neqb_comm : forall a a', Neqb a a' = Neqb a' a. +Proof. + intros; apply bool_1; split; intros. + rewrite (Neqb_complete _ _ H); apply Neqb_correct. + rewrite (Neqb_complete _ _ H); apply Neqb_correct. +Qed. + +Lemma Nxor_eq_true : + forall a a', Nxor a a' = N0 -> Neqb a a' = true. +Proof. + intros. rewrite (Nxor_eq a a' H). apply Neqb_correct. +Qed. + +Lemma Nxor_eq_false : + forall a a' p, Nxor a a' = Npos p -> Neqb a a' = false. +Proof. + intros. elim (sumbool_of_bool (Neqb a a')). intro H0. + rewrite (Neqb_complete a a' H0) in H. rewrite (Nxor_nilpotent a') in H. discriminate H. + trivial. +Qed. + +Lemma Nodd_not_double : + forall a, + Nodd a -> forall a0, Neqb (Ndouble a0) a = false. +Proof. + intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0. + rewrite <- (Neqb_complete _ _ H0) in H. + unfold Nodd in H. + rewrite (Ndouble_bit0 a0) in H. discriminate H. + trivial. +Qed. + +Lemma Nnot_div2_not_double : + forall a a0, + Neqb (Ndiv2 a) a0 = false -> Neqb a (Ndouble a0) = false. +Proof. + intros. elim (sumbool_of_bool (Neqb (Ndouble a0) a)). intro H0. + rewrite <- (Neqb_complete _ _ H0) in H. rewrite (Ndouble_div2 a0) in H. + rewrite (Neqb_correct a0) in H. discriminate H. + intro. rewrite Neqb_comm. assumption. +Qed. + +Lemma Neven_not_double_plus_one : + forall a, + Neven a -> forall a0, Neqb (Ndouble_plus_one a0) a = false. +Proof. + intros. elim (sumbool_of_bool (Neqb (Ndouble_plus_one a0) a)). intro H0. + rewrite <- (Neqb_complete _ _ H0) in H. + unfold Neven in H. + rewrite (Ndouble_plus_one_bit0 a0) in H. + discriminate H. + trivial. +Qed. + +Lemma Nnot_div2_not_double_plus_one : + forall a a0, + Neqb (Ndiv2 a) a0 = false -> Neqb (Ndouble_plus_one a0) a = false. +Proof. + intros. elim (sumbool_of_bool (Neqb a (Ndouble_plus_one a0))). intro H0. + rewrite (Neqb_complete _ _ H0) in H. rewrite (Ndouble_plus_one_div2 a0) in H. + rewrite (Neqb_correct a0) in H. discriminate H. + intro H0. rewrite Neqb_comm. assumption. +Qed. + +Lemma Nbit0_neq : + forall a a', + Nbit0 a = false -> Nbit0 a' = true -> Neqb a a' = false. +Proof. + intros. elim (sumbool_of_bool (Neqb a a')). intro H1. rewrite (Neqb_complete _ _ H1) in H. + rewrite H in H0. discriminate H0. + trivial. +Qed. + +Lemma Ndiv2_eq : + forall a a', Neqb a a' = true -> Neqb (Ndiv2 a) (Ndiv2 a') = true. +Proof. + intros. cut (a = a'). intros. rewrite H0. apply Neqb_correct. + apply Neqb_complete. exact H. +Qed. + +Lemma Ndiv2_neq : + forall a a', + Neqb (Ndiv2 a) (Ndiv2 a') = false -> Neqb a a' = false. +Proof. + intros. elim (sumbool_of_bool (Neqb a a')). intro H0. + rewrite (Neqb_complete _ _ H0) in H. rewrite (Neqb_correct (Ndiv2 a')) in H. discriminate H. + trivial. +Qed. + +Lemma Ndiv2_bit_eq : + forall a a', + Nbit0 a = Nbit0 a' -> Ndiv2 a = Ndiv2 a' -> a = a'. +Proof. + intros. apply Nbit_faithful. unfold eqf in |- *. destruct n. + rewrite Nbit0_correct. rewrite Nbit0_correct. assumption. + rewrite <- Ndiv2_correct. rewrite <- Ndiv2_correct. + rewrite H0. reflexivity. +Qed. + +Lemma Ndiv2_bit_neq : + forall a a', + Neqb a a' = false -> + Nbit0 a = Nbit0 a' -> Neqb (Ndiv2 a) (Ndiv2 a') = false. +Proof. + intros. elim (sumbool_of_bool (Neqb (Ndiv2 a) (Ndiv2 a'))). intro H1. + rewrite (Ndiv2_bit_eq _ _ H0 (Neqb_complete _ _ H1)) in H. + rewrite (Neqb_correct a') in H. discriminate H. + trivial. +Qed. + +Lemma Nneq_elim : + forall a a', + Neqb a a' = false -> + Nbit0 a = negb (Nbit0 a') \/ + Neqb (Ndiv2 a) (Ndiv2 a') = false. +Proof. + intros. cut (Nbit0 a = Nbit0 a' \/ Nbit0 a = negb (Nbit0 a')). + intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption. + assumption. + intro. left. assumption. + case (Nbit0 a); case (Nbit0 a'); auto. +Qed. + +Lemma Ndouble_or_double_plus_un : + forall a, + {a0 : N | a = Ndouble a0} + {a1 : N | a = Ndouble_plus_one a1}. +Proof. + intro. elim (sumbool_of_bool (Nbit0 a)). intro H. right. split with (Ndiv2 a). + rewrite (Ndiv2_double_plus_one a H). reflexivity. + intro H. left. split with (Ndiv2 a). rewrite (Ndiv2_double a H). reflexivity. +Qed. + +(** A boolean order on [N] *) + +Definition Nle (a b:N) := leb (nat_of_N a) (nat_of_N b). + +Lemma Nle_Ncompare : forall a b, Nle a b = true <-> Ncompare a b <> Gt. +Proof. + intros; rewrite nat_of_Ncompare. + unfold Nle; apply leb_compare. +Qed. + +Lemma Nle_refl : forall a, Nle a a = true. +Proof. + intro. unfold Nle in |- *. apply leb_correct. apply le_n. +Qed. + +Lemma Nle_antisym : + forall a b, Nle a b = true -> Nle b a = true -> a = b. +Proof. + unfold Nle in |- *. intros. rewrite <- (N_of_nat_of_N a). rewrite <- (N_of_nat_of_N b). + rewrite (le_antisym _ _ (leb_complete _ _ H) (leb_complete _ _ H0)). reflexivity. +Qed. + +Lemma Nle_trans : + forall a b c, Nle a b = true -> Nle b c = true -> Nle a c = true. +Proof. + unfold Nle in |- *. intros. apply leb_correct. apply le_trans with (m := nat_of_N b). + apply leb_complete. assumption. + apply leb_complete. assumption. +Qed. + +Lemma Nle_lt_trans : + forall a b c, + Nle a b = true -> Nle c b = false -> Nle c a = false. +Proof. + unfold Nle in |- *. intros. apply leb_correct_conv. apply le_lt_trans with (m := nat_of_N b). + apply leb_complete. assumption. + apply leb_complete_conv. assumption. +Qed. + +Lemma Nlt_le_trans : + forall a b c, + Nle b a = false -> Nle b c = true -> Nle c a = false. +Proof. + unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_le_trans with (m := nat_of_N b). + apply leb_complete_conv. assumption. + apply leb_complete. assumption. +Qed. + +Lemma Nlt_trans : + forall a b c, + Nle b a = false -> Nle c b = false -> Nle c a = false. +Proof. + unfold Nle in |- *. intros. apply leb_correct_conv. apply lt_trans with (m := nat_of_N b). + apply leb_complete_conv. assumption. + apply leb_complete_conv. assumption. +Qed. + +Lemma Nlt_le_weak : forall a b:N, Nle b a = false -> Nle a b = true. +Proof. + unfold Nle in |- *. intros. apply leb_correct. apply lt_le_weak. + apply leb_complete_conv. assumption. +Qed. + +Lemma Nle_double_mono : + forall a b, + Nle a b = true -> Nle (Ndouble a) (Ndouble b) = true. +Proof. + unfold Nle in |- *. intros. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. apply leb_correct. + simpl in |- *. apply plus_le_compat. apply leb_complete. assumption. + apply plus_le_compat. apply leb_complete. assumption. + apply le_n. +Qed. + +Lemma Nle_double_plus_one_mono : + forall a b, + Nle a b = true -> + Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true. +Proof. + unfold Nle in |- *. intros. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + apply leb_correct. apply le_n_S. simpl in |- *. apply plus_le_compat. apply leb_complete. + assumption. + apply plus_le_compat. apply leb_complete. assumption. + apply le_n. +Qed. + +Lemma Nle_double_mono_conv : + forall a b, + Nle (Ndouble a) (Ndouble b) = true -> Nle a b = true. +Proof. + unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble. rewrite nat_of_Ndouble. intro. + apply leb_correct. apply (mult_S_le_reg_l 1). apply leb_complete. assumption. +Qed. + +Lemma Nle_double_plus_one_mono_conv : + forall a b, + Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = true -> + Nle a b = true. +Proof. + unfold Nle in |- *. intros a b. rewrite nat_of_Ndouble_plus_one. rewrite nat_of_Ndouble_plus_one. + intro. apply leb_correct. apply (mult_S_le_reg_l 1). apply le_S_n. apply leb_complete. + assumption. +Qed. + +Lemma Nlt_double_mono : + forall a b, + Nle a b = false -> Nle (Ndouble a) (Ndouble b) = false. +Proof. + intros. elim (sumbool_of_bool (Nle (Ndouble a) (Ndouble b))). intro H0. + rewrite (Nle_double_mono_conv _ _ H0) in H. discriminate H. + trivial. +Qed. + +Lemma Nlt_double_plus_one_mono : + forall a b, + Nle a b = false -> + Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false. +Proof. + intros. elim (sumbool_of_bool (Nle (Ndouble_plus_one a) (Ndouble_plus_one b))). intro H0. + rewrite (Nle_double_plus_one_mono_conv _ _ H0) in H. discriminate H. + trivial. +Qed. + +Lemma Nlt_double_mono_conv : + forall a b, + Nle (Ndouble a) (Ndouble b) = false -> Nle a b = false. +Proof. + intros. elim (sumbool_of_bool (Nle a b)). intro H0. rewrite (Nle_double_mono _ _ H0) in H. + discriminate H. + trivial. +Qed. + +Lemma Nlt_double_plus_one_mono_conv : + forall a b, + Nle (Ndouble_plus_one a) (Ndouble_plus_one b) = false -> + Nle a b = false. +Proof. + intros. elim (sumbool_of_bool (Nle a b)). intro H0. + rewrite (Nle_double_plus_one_mono _ _ H0) in H. discriminate H. + trivial. +Qed. + +(* A [min] function over [N] *) + +Definition Nmin (a b:N) := if Nle a b then a else b. + +Lemma Nmin_choice : forall a b, {Nmin a b = a} + {Nmin a b = b}. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. left. rewrite H. + reflexivity. + intro H. right. rewrite H. reflexivity. +Qed. + +Lemma Nmin_le_1 : forall a b, Nle (Nmin a b) a = true. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. + apply Nle_refl. + intro H. rewrite H. apply Nlt_le_weak. assumption. +Qed. + +Lemma Nmin_le_2 : forall a b, Nle (Nmin a b) b = true. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle a b)). intro H. rewrite H. assumption. + intro H. rewrite H. apply Nle_refl. +Qed. + +Lemma Nmin_le_3 : + forall a b c, Nle a (Nmin b c) = true -> Nle a b = true. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + assumption. + intro H0. rewrite H0 in H. apply Nlt_le_weak. apply Nle_lt_trans with (b := c); assumption. +Qed. + +Lemma Nmin_le_4 : + forall a b c, Nle a (Nmin b c) = true -> Nle a c = true. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + apply Nle_trans with (b := b); assumption. + intro H0. rewrite H0 in H. assumption. +Qed. + +Lemma Nmin_le_5 : + forall a b c, + Nle a b = true -> Nle a c = true -> Nle a (Nmin b c) = true. +Proof. + intros. elim (Nmin_choice b c). intro H1. rewrite H1. assumption. + intro H1. rewrite H1. assumption. +Qed. + +Lemma Nmin_lt_3 : + forall a b c, Nle (Nmin b c) a = false -> Nle b a = false. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + assumption. + intro H0. rewrite H0 in H. apply Nlt_trans with (b := c); assumption. +Qed. + +Lemma Nmin_lt_4 : + forall a b c, Nle (Nmin b c) a = false -> Nle c a = false. +Proof. + unfold Nmin in |- *. intros. elim (sumbool_of_bool (Nle b c)). intro H0. rewrite H0 in H. + apply Nlt_le_trans with (b := b); assumption. + intro H0. rewrite H0 in H. assumption. +Qed. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v new file mode 100644 index 00000000..ed8ced5b --- /dev/null +++ b/theories/NArith/Ndigits.v @@ -0,0 +1,767 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Ndigits.v 8736 2006-04-26 21:18:44Z letouzey $ i*) + +Require Import Bool. +Require Import Bvector. +Require Import BinPos. +Require Import BinNat. + +(** Operation over bits of a [N] number. *) + +(** [xor] *) + +Fixpoint Pxor (p1 p2:positive) {struct p1} : 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. + +Definition Nxor (n n':N) := + match n, n' with + | N0, _ => n' + | _, N0 => n + | Npos p, Npos p' => Pxor p p' + end. + +Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n. +Proof. + trivial. +Qed. + +Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n. +Proof. + destruct n; trivial. +Qed. + +Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n. +Proof. + destruct n; destruct n'; simpl; auto. + generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl; + auto. + destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial. + destruct p0; simpl; trivial; intros; rewrite Hrecp; trivial. + destruct p0 as [p| p| ]; simpl; auto. +Qed. + +Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0. +Proof. + destruct n; trivial. + simpl. induction p as [p IHp| p IHp| ]; trivial. + simpl. rewrite IHp; reflexivity. + simpl. rewrite IHp; reflexivity. +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. + +Definition Nbit (a:N) := + match a with + | N0 => fun _ => false + | Npos p => Pbit p + end. + +(** Auxiliary results about streams of bits *) + +Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. + +Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. +Proof. + unfold eqf. intros. rewrite H. reflexivity. +Qed. + +Lemma eqf_refl : forall f:nat -> bool, eqf f f. +Proof. + unfold eqf. trivial. +Qed. + +Lemma eqf_trans : + forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''. +Proof. + unfold eqf. intros. rewrite H. exact (H0 n). +Qed. + +Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n). + +Lemma xorf_eq : + forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'. +Proof. + unfold eqf, xorf. intros. apply xorb_eq. apply H. +Qed. + +Lemma xorf_assoc : + forall f f' f'', + eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')). +Proof. + unfold eqf, xorf. intros. apply xorb_assoc. +Qed. + +Lemma eqf_xorf : + forall f f' f'' f''', + eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f'''). +Proof. + unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity. +Qed. + +(** End of auxilliary results *) + +(** 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. + 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). +Qed. + +Lemma Nbit_faithful_2 : + forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a. +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. +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. +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. + case p. intros. absurd (false = true). discriminate. + exact (H0 0). + intros. rewrite (H p0 (fun n => H0 (S n))). reflexivity. + intros. absurd (false = true). discriminate. + exact (H0 0). +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. +Proof. + destruct a. intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))). + intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity. + unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity. + case p. intros. rewrite (H p0 (fun n:nat => H0 (S n))). reflexivity. + intros. absurd (true = false). discriminate. + exact (H0 0). + intros. absurd (N0 = Npos p0). discriminate. + cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))). + intro. exact (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))). + unfold eqf in *. intro. rewrite H0. reflexivity. +Qed. + +Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'. +Proof. + destruct a. exact Nbit_faithful_1. + induction p. intros a' H. apply Nbit_faithful_4. intros. cut (Npos p = Npos p'). + intro. inversion H1. reflexivity. + exact (IHp (Npos p') H0). + assumption. + intros. apply Nbit_faithful_3. intros. cut (Npos p = Npos p'). intro. inversion H1. reflexivity. + exact (IHp (Npos p') H0). + assumption. + exact Nbit_faithful_2. +Qed. + +(** We now describe the semantics of [Nxor] in terms of bit streams. *) + +Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0. +Proof. + trivial. +Qed. + +Lemma Nxor_sem_2 : + forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0). +Proof. + intro. case a'. trivial. + simpl. intro. + case p; trivial. +Qed. + +Lemma Nxor_sem_3 : + forall (p:positive) (a':N), + Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0. +Proof. + intros. case a'. trivial. + simpl. intro. + case p0; trivial. intro. + case (Pxor p p1); trivial. + intro. case (Pxor p p1); trivial. +Qed. + +Lemma Nxor_sem_4 : + forall (p:positive) (a':N), + Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0). +Proof. + intros. case a'. trivial. + simpl. intro. case p0; trivial. intro. + case (Pxor p p1); trivial. + intro. + case (Pxor p p1); trivial. +Qed. + +Lemma Nxor_sem_5 : + forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0. +Proof. + destruct a. intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial. + case p. exact Nxor_sem_4. + intros. change (Nbit (Nxor (Npos (xO p0)) a') 0 = xorb false (Nbit a' 0)). + rewrite false_xorb. apply Nxor_sem_3. exact Nxor_sem_2. +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). +Proof. + intros. + generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H. + unfold xorf in *. + case a. simpl Nbit; rewrite false_xorb. reflexivity. + case a'; intros. + simpl Nbit; rewrite xorb_false. reflexivity. + case p0. case p; intros; simpl Nbit in *. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite xorb_false. reflexivity. + case p; intros; simpl Nbit in *. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite <- H; simpl; case (Pxor p2 p1); trivial. + rewrite xorb_false. reflexivity. + simpl Nbit. rewrite false_xorb. simpl. case p; 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'. elim n. exact Nxor_sem_5. + exact Nxor_sem_6. +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. apply xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')). + apply eqf_sym. apply 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 + (f' := xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')). + apply eqf_trans with (f' := xorf (Nbit (Nxor a a')) (Nbit a'')). + apply Nxor_semantics. + apply eqf_xorf. apply Nxor_semantics. + apply eqf_refl. + apply eqf_trans with + (f' := xorf (Nbit a) (xorf (Nbit a') (Nbit a''))). + apply xorf_assoc. + apply eqf_trans with (f' := xorf (Nbit a) (Nbit (Nxor a' a''))). + apply eqf_xorf. apply eqf_refl. + apply eqf_sym. apply Nxor_semantics. + apply eqf_sym. apply Nxor_semantics. +Qed. + +(** 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. + +Definition Nodd (n:N) := Nbit0 n = true. +Definition Neven (n:N) := Nbit0 n = false. + +Lemma Nbit0_correct : forall n:N, Nbit n 0 = Nbit0 n. +Proof. + destruct n; trivial. + destruct p; trivial. +Qed. + +Lemma Ndouble_bit0 : forall n:N, Nbit0 (Ndouble n) = false. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndouble_plus_one_bit0 : + forall n:N, Nbit0 (Ndouble_plus_one n) = true. +Proof. + destruct n; trivial. +Qed. + +Lemma Ndiv2_double : + forall n:N, Neven n -> Ndouble (Ndiv2 n) = n. +Proof. + destruct n. trivial. destruct p. intro H. discriminate H. + intros. reflexivity. + intro H. discriminate H. +Qed. + +Lemma Ndiv2_double_plus_one : + forall n:N, Nodd n -> Ndouble_plus_one (Ndiv2 n) = n. +Proof. + destruct n. intro. discriminate H. + destruct p. intros. reflexivity. + intro H. discriminate H. + intro. reflexivity. +Qed. + +Lemma Ndiv2_correct : + forall (a:N) (n:nat), Nbit (Ndiv2 a) n = Nbit 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'). +Proof. + intros. rewrite <- Nbit0_correct. rewrite (Nxor_semantics a a' 0). + unfold xorf. rewrite Nbit0_correct. rewrite Nbit0_correct. reflexivity. +Qed. + +Lemma Nxor_div2 : + forall a a':N, Ndiv2 (Nxor a a') = Nxor (Ndiv2 a) (Ndiv2 a'). +Proof. + intros. apply Nbit_faithful. unfold eqf. intro. + rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n). + rewrite Ndiv2_correct. + rewrite (Nxor_semantics a a' (S n)). + unfold xorf. rewrite Ndiv2_correct. rewrite Ndiv2_correct. + reflexivity. +Qed. + +Lemma Nneg_bit0 : + forall a a':N, + Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). +Proof. + intros. rewrite <- true_xorb. rewrite <- H. rewrite Nxor_bit0. + rewrite xorb_assoc. rewrite xorb_nilpotent. rewrite xorb_false. reflexivity. +Qed. + +Lemma Nneg_bit0_1 : + forall a a':N, Nxor a a' = Npos 1 -> Nbit0 a = negb (Nbit0 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'). +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'. +Proof. + intros. rewrite <- (xorb_false (Nbit0 a)). cut (Nbit0 (Npos (xO p)) = false). + intro. rewrite <- H0. rewrite <- H. rewrite Nxor_bit0. rewrite <- xorb_assoc. + rewrite xorb_nilpotent. rewrite false_xorb. reflexivity. + reflexivity. +Qed. + +(** a lexicographic order on bits, starting from the lowest bit *) + +Fixpoint Nless_aux (a a':N) (p:positive) {struct p} : bool := + match p with + | xO p' => Nless_aux (Ndiv2 a) (Ndiv2 a') p' + | _ => andb (negb (Nbit0 a)) (Nbit0 a') + end. + +Definition Nless (a a':N) := + match Nxor 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. +Proof. + intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *. + rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5. + rewrite H in H5. rewrite H0 in H5. discriminate H5. + rewrite H4. reflexivity. + intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intro H1. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H2. + rewrite H in H2. rewrite H0 in H2. discriminate H2. + rewrite H1. reflexivity. +Qed. + +Lemma Nbit0_gt : + forall a a', + Nbit0 a = true -> Nbit0 a' = false -> Nless a a' = false. +Proof. + intros. elim (Ndiscr (Nxor a a')). intro H1. elim H1. intros p H2. unfold Nless in |- *. + rewrite H2. generalize H2. elim p. intros. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intros. cut (Nbit0 (Nxor a a') = false). intro. rewrite (Nxor_bit0 a a') in H5. + rewrite H in H5. rewrite H0 in H5. discriminate H5. + rewrite H4. reflexivity. + intro. simpl in |- *. rewrite H. rewrite H0. reflexivity. + intro H1. unfold Nless in |- *. rewrite H1. reflexivity. +Qed. + +Lemma Nless_not_refl : forall a, Nless a a = false. +Proof. + intro. unfold Nless in |- *. rewrite (Nxor_nilpotent a). reflexivity. +Qed. + +Lemma Nless_def_1 : + forall a a', Nless (Ndouble a) (Ndouble a') = Nless a a'. +Proof. + simple induction a. simple induction a'. reflexivity. + trivial. + simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial. + unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity. + trivial. +Qed. + +Lemma Nless_def_2 : + forall a a', + Nless (Ndouble_plus_one a) (Ndouble_plus_one a') = Nless a a'. +Proof. + simple induction a. simple induction a'. reflexivity. + trivial. + simple induction a'. unfold Nless in |- *. simpl in |- *. elim p; trivial. + unfold Nless in |- *. simpl in |- *. intro. case (Pxor p p0). reflexivity. + trivial. +Qed. + +Lemma Nless_def_3 : + forall a a', Nless (Ndouble a) (Ndouble_plus_one 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. +Proof. + intros. apply Nbit0_gt. apply Ndouble_plus_one_bit0. + apply Ndouble_bit0. +Qed. + +Lemma Nless_z : forall a, Nless a N0 = false. +Proof. + simple induction a. reflexivity. + unfold Nless in |- *. intro. rewrite (Nxor_neutral_right (Npos p)). elim p; trivial. +Qed. + +Lemma N0_less_1 : + forall a, Nless N0 a = true -> {p : positive | a = Npos p}. +Proof. + simple induction a. intro. discriminate H. + intros. split with p. reflexivity. +Qed. + +Lemma N0_less_2 : forall a, Nless N0 a = false -> a = N0. +Proof. + simple induction a. trivial. + unfold Nless in |- *. simpl in |- *. + cut (forall p:positive, Nless_aux N0 (Npos p) p = false -> False). + intros. elim (H p H0). + simple induction p. intros. discriminate H0. + intros. exact (H H0). + intro. discriminate H. +Qed. + +Lemma Nless_trans : + forall a a' a'', + Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. +Proof. + intro a. pattern a; apply N_ind_double. + intros. case_eq (Nless N0 a''). trivial. + intro H1. rewrite (N0_less_2 a'' H1) in H0. rewrite (Nless_z a') in H0. discriminate H0. + intros a0 H a'. pattern a'; apply N_ind_double. + intros. rewrite (Nless_z (Ndouble a0)) in H0. discriminate H0. + intros a1 H0 a'' H1. rewrite (Nless_def_1 a0 a1) in H1. + pattern a''; apply N_ind_double; clear a''. + intro. rewrite (Nless_z (Ndouble a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_1 a1 a2) in H3. rewrite (Nless_def_1 a0 a2). + exact (H a1 a2 H1 H3). + intros. apply Nless_def_3. + intros a1 H0 a'' H1. pattern a''; apply N_ind_double. + intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3. + intros. apply Nless_def_3. + intros a0 H a'. pattern a'; apply N_ind_double. + intros. rewrite (Nless_z (Ndouble_plus_one a0)) in H0. discriminate H0. + intros. rewrite (Nless_def_4 a0 a1) in H1. discriminate H1. + intros a1 H0 a'' H1. pattern a''; apply N_ind_double. + intro. rewrite (Nless_z (Ndouble_plus_one a1)) in H2. discriminate H2. + intros. rewrite (Nless_def_4 a1 a2) in H3. discriminate H3. + rewrite (Nless_def_2 a0 a1) in H1. intros. rewrite (Nless_def_2 a1 a2) in H3. + rewrite (Nless_def_2 a0 a2). exact (H a1 a2 H1 H3). +Qed. + +Lemma Nless_total : + forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. +Proof. + intro a. + pattern a; apply N_rec_double; clear a. + intro. case_eq (Nless N0 a'). intro H. left. left. auto. + intro H. right. rewrite (N0_less_2 a' H). reflexivity. + intros a0 H a'. + pattern a'; apply N_rec_double; clear a'. + case_eq (Nless N0 (Ndouble a0)). intro H0. left. right. auto. + intro H0. right. exact (N0_less_2 _ H0). + intros a1 H0. rewrite Nless_def_1. rewrite Nless_def_1. elim (H a1). intro H1. + left. assumption. + intro H1. right. rewrite H1. reflexivity. + intros a1 H0. left. left. apply Nless_def_3. + intros a0 H a'. + pattern a'; apply N_rec_double; clear a'. + left. right. case a0; reflexivity. + intros a1 H0. left. right. apply Nless_def_3. + intros a1 H0. rewrite Nless_def_2. rewrite Nless_def_2. elim (H a1). intro H1. + left. assumption. + intro H1. right. rewrite H1. reflexivity. +Qed. + +(** Number of digits in a number *) + +Fixpoint Psize (p:positive) : nat := + match p with + | xH => 1%nat + | xI p => S (Psize p) + | xO p => S (Psize p) + end. + +Definition Nsize (n:N) : nat := match n with + | N0 => 0%nat + | Npos p => Psize p + end. + + +(** conversions between N and bit vectors. *) + +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 + | N0 => Bnil + | Npos p => P2Bv p + end. + +Fixpoint Bv2N (n:nat)(bv:Bvector n) {struct bv} : N := + match bv with + | Vnil => N0 + | Vcons false n bv => Ndouble (Bv2N n bv) + | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) + end. + +Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. +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 return [Bv2N] translation: *) + +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. +generalize (IHn (Vtail _ _ bv)); clear IHn. +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 <-> + 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. +Qed. + +(** 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 + | 0 => Bnil + | 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)) + | Npos (xI p) => Bcons true _ (N2Bv_gen n (Npos p)) + end + end. + +(** 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. +Proof. +destruct a; simpl. +auto. +induction p; simpl; intros; auto; congruence. +Qed. + +(** 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), + N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k). +Proof. +destruct a; simpl. +destruct k; simpl; auto. +induction p; simpl; intros;unfold Bcons; f_equal; auto. +Qed. + +(** Here comes now the second composition result. *) + +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. +unfold Bcons. +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)), + Nbit0 (Bv2N _ bv) = Blow _ bv. +Proof. +intros. +unfold Blow. +pattern bv at 1; rewrite (VSn_eq _ _ 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. + intros. + elimtype False; 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), + Bnth _ bv p H = Nbit (Bv2N _ bv) p. +Proof. +induction bv; intros. +inversion H. +destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto. +Qed. + +Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false. +Proof. +destruct n as [|n]. +simpl; auto. +induction n; simpl in *; intros; destruct p; auto with arith. +inversion H. +inversion H. +Qed. + +Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H. +Proof. +destruct n as [|n]. +inversion H. +induction n; simpl in *; intros; destruct p; auto with arith. +inversion H; inversion H1. +Qed. + +(** Xor is 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); rewrite (V0_eq _ bv'); simpl; auto. +intros. +rewrite (VSn_eq _ _ bv); rewrite (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. +Qed. + diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v new file mode 100644 index 00000000..d5bfc15c --- /dev/null +++ b/theories/NArith/Ndist.v @@ -0,0 +1,338 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(*i $Id: Ndist.v 8733 2006-04-25 22:52:18Z letouzey $ i*) + +Require Import Arith. +Require Import Min. +Require Import BinPos. +Require Import BinNat. +Require Import Ndigits. + +(** An ultrametric distance over [N] numbers *) + +Inductive natinf : Set := + | infty : natinf + | ni : nat -> natinf. + +Fixpoint Pplength (p:positive) : nat := + match p with + | xH => 0 + | xI _ => 0 + | xO p' => S (Pplength p') + end. + +Definition Nplength (a:N) := + match a with + | N0 => infty + | Npos p => ni (Pplength p) + end. + +Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0. +Proof. + simple induction a; trivial. + unfold Nplength in |- *; intros; discriminate H. +Qed. + +Lemma Nplength_zeros : + forall (a:N) (n:nat), + Nplength a = ni n -> forall k:nat, k < n -> Nbit a k = false. +Proof. + simple induction a; trivial. + simple induction p. simple induction n. intros. inversion H1. + simple induction k. simpl in H1. discriminate H1. + intros. simpl in H1. discriminate H1. + simple induction k. trivial. + generalize H0. case n. intros. inversion H3. + intros. simpl in |- *. unfold Nbit in H. apply (H n0). simpl in H1. inversion H1. reflexivity. + exact (lt_S_n n1 n0 H3). + simpl in |- *. intros n H. inversion H. intros. inversion H0. +Qed. + +Lemma Nplength_one : + forall (a:N) (n:nat), Nplength a = ni n -> Nbit a n = true. +Proof. + simple induction a. intros. inversion H. + simple induction p. intros. simpl in H0. inversion H0. reflexivity. + intros. simpl in H0. inversion H0. simpl in |- *. unfold Nbit in H. apply H. reflexivity. + intros. simpl in H. inversion H. reflexivity. +Qed. + +Lemma Nplength_first_one : + forall (a:N) (n:nat), + (forall k:nat, k < n -> Nbit a k = false) -> + Nbit a n = true -> Nplength a = ni n. +Proof. + simple induction a. intros. simpl in H0. discriminate H0. + simple induction p. intros. generalize H0. case n. intros. reflexivity. + intros. absurd (Nbit (Npos (xI p0)) 0 = false). trivial with bool. + auto with bool arith. + intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. + intros. simpl in |- *. unfold Nplength in H. + cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity. + apply H. intros. change (Nbit (Npos (xO p0)) (S k) = false) in |- *. apply H2. apply lt_n_S. exact H4. + exact H3. + intro. case n. trivial. + intros. simpl in H0. discriminate H0. +Qed. + +Definition ni_min (d d':natinf) := + match d with + | infty => d' + | ni n => match d' with + | infty => d + | ni n' => ni (min n n') + end + end. + +Lemma ni_min_idemp : forall d:natinf, ni_min d d = d. +Proof. + simple induction d; trivial. + unfold ni_min in |- *. + simple induction n; trivial. + intros. + simpl in |- *. + inversion H. + rewrite H1. + rewrite H1. + reflexivity. +Qed. + +Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d. +Proof. + simple induction d. simple induction d'; trivial. + simple induction d'; trivial. elim n. simple induction n0; trivial. + intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). + intro. unfold ni_min in |- *. simpl in |- *. rewrite H1. reflexivity. + cut (ni (min n0 n2) = ni (min n2 n0)). intros. + inversion H1; trivial. + exact (H n2). +Qed. + +Lemma ni_min_assoc : + forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d''). +Proof. + simple induction d; trivial. simple induction d'; trivial. + simple induction d''; trivial. + unfold ni_min in |- *. intro. cut (min (min n n0) n1 = min n (min n0 n1)). + intro. rewrite H. reflexivity. + generalize n0 n1. elim n; trivial. + simple induction n3; trivial. simple induction n5; trivial. + intros. simpl in |- *. auto. +Qed. + +Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0. +Proof. + simple induction d; trivial. +Qed. + +Lemma ni_min_O_r : forall d:natinf, ni_min d (ni 0) = ni 0. +Proof. + intros. rewrite ni_min_comm. apply ni_min_O_l. +Qed. + +Lemma ni_min_inf_l : forall d:natinf, ni_min infty d = d. +Proof. + trivial. +Qed. + +Lemma ni_min_inf_r : forall d:natinf, ni_min d infty = d. +Proof. + simple induction d; trivial. +Qed. + +Definition ni_le (d d':natinf) := ni_min d d' = d. + +Lemma ni_le_refl : forall d:natinf, ni_le d d. +Proof. + exact ni_min_idemp. +Qed. + +Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'. +Proof. + unfold ni_le in |- *. intros d d'. rewrite ni_min_comm. intro H. rewrite H. trivial. +Qed. + +Lemma ni_le_trans : + forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''. +Proof. + unfold ni_le in |- *. intros. rewrite <- H. rewrite ni_min_assoc. rewrite H0. reflexivity. +Qed. + +Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d. +Proof. + unfold ni_le in |- *. intros. rewrite (ni_min_comm d d'). rewrite ni_min_assoc. + rewrite ni_min_idemp. reflexivity. +Qed. + +Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'. +Proof. + unfold ni_le in |- *. intros. rewrite ni_min_assoc. rewrite ni_min_idemp. reflexivity. +Qed. + +Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. +Proof. + simple induction d. intro. right. exact (ni_min_inf_l d'). + simple induction d'. left. exact (ni_min_inf_r (ni n)). + unfold ni_min in |- *. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). + intros. case (H n0). intro. left. rewrite H0. reflexivity. + intro. right. rewrite H0. reflexivity. + elim n. intro. left. reflexivity. + simple induction n1. right. reflexivity. + intros. case (H n2). intro. left. simpl in |- *. rewrite H1. reflexivity. + intro. right. simpl in |- *. rewrite H1. reflexivity. +Qed. + +Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. +Proof. + unfold ni_le in |- *. intros. rewrite (ni_min_comm d' d). apply ni_min_case. +Qed. + +Lemma ni_le_min_induc : + forall d d' dm:natinf, + ni_le dm d -> + ni_le dm d' -> + (forall d'':natinf, ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) -> + ni_min d d' = dm. +Proof. + intros. case (ni_min_case d d'). intro. rewrite H2. + apply ni_le_antisym. apply H1. apply ni_le_refl. + exact H2. + exact H. + intro. rewrite H2. apply ni_le_antisym. apply H1. unfold ni_le in |- *. rewrite ni_min_comm. exact H2. + apply ni_le_refl. + exact H0. +Qed. + +Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). +Proof. + cut (forall m n:nat, m <= n -> min m n = m). + intros. unfold ni_le, ni_min in |- *. rewrite (H m n H0). reflexivity. + simple induction m. trivial. + simple induction n0. intro. inversion H0. + intros. simpl in |- *. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. +Qed. + +Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. +Proof. + unfold ni_le in |- *. unfold ni_min in |- *. intros. inversion H. apply le_min_r. +Qed. + +Lemma Nplength_lb : + forall (a:N) (n:nat), + (forall k:nat, k < n -> Nbit a k = false) -> ni_le (ni n) (Nplength a). +Proof. + simple induction a. intros. exact (ni_min_inf_r (ni n)). + intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt n (Pplength p)). trivial. + intro. absurd (Nbit (Npos p) (Pplength p) = false). + rewrite + (Nplength_one (Npos p) (Pplength p) + (refl_equal (Nplength (Npos p)))). + discriminate. + apply H. exact H0. +Qed. + +Lemma Nplength_ub : + forall (a:N) (n:nat), Nbit a n = true -> ni_le (Nplength a) (ni n). +Proof. + simple induction a. intros. discriminate H. + intros. unfold Nplength in |- *. apply le_ni_le. case (le_or_lt (Pplength p) n). trivial. + intro. absurd (Nbit (Npos p) n = true). + rewrite + (Nplength_zeros (Npos p) (Pplength p) + (refl_equal (Nplength (Npos p))) n H0). + discriminate. + exact H. +Qed. + + +(** We define an ultrametric distance between [N] numbers: + $d(a,a')=1/2^pd(a,a')$, + where $pd(a,a')$ is the number of identical bits at the beginning + of $a$ and $a'$ (infinity if $a=a'$). + Instead of working with $d$, we work with $pd$, namely + [Npdist]: *) + +Definition Npdist (a a':N) := Nplength (Nxor a a'). + +(** d is a distance, so $d(a,a')=0$ iff $a=a'$; this means that + $pd(a,a')=infty$ iff $a=a'$: *) + +Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty. +Proof. + intros. unfold Npdist in |- *. rewrite Nxor_nilpotent. reflexivity. +Qed. + +Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'. +Proof. + intros. apply Nxor_eq. apply Nplength_infty. exact H. +Qed. + +(** $d$ is a distance, so $d(a,a')=d(a',a)$: *) + +Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a. +Proof. + unfold Npdist in |- *. intros. rewrite Nxor_comm. reflexivity. +Qed. + +(** $d$ is an ultrametric distance, that is, not only $d(a,a')\leq + d(a,a'')+d(a'',a')$, + but in fact $d(a,a')\leq max(d(a,a''),d(a'',a'))$. + This means that $min(pd(a,a''),pd(a'',a'))<=pd(a,a')$ (lemma [Npdist_ultra] below). + This follows from the fact that $a ~Ra~|a| = 1/2^{\texttt{Nplength}}(a))$ + is an ultrametric norm, i.e. that $|a-a'| \leq max (|a-a''|, |a''-a'|)$, + or equivalently that $|a+b|<=max(|a|,|b|)$, i.e. that + min $(\texttt{Nplength}(a), \texttt{Nplength}(b)) \leq + \texttt{Nplength} (a~\texttt{xor}~ b)$ + (lemma [Nplength_ultra]). +*) + +Lemma Nplength_ultra_1 : + forall a a':N, + ni_le (Nplength a) (Nplength a') -> + ni_le (Nplength a) (Nplength (Nxor a a')). +Proof. + simple induction a. intros. unfold ni_le in H. unfold Nplength at 1 3 in H. + rewrite (ni_min_inf_l (Nplength a')) in H. + rewrite (Nplength_infty a' H). simpl in |- *. apply ni_le_refl. + intros. unfold Nplength at 1 in |- *. apply Nplength_lb. intros. + 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 |- *. + rewrite + (Nplength_zeros (Npos p) (Pplength p) + (refl_equal (Nplength (Npos p))) k H0). + generalize H. case a'. trivial. + intros. cut (Nbit (Npos p1) k = false). intros. rewrite H3. reflexivity. + apply Nplength_zeros with (n := Pplength p1). reflexivity. + apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0. + apply ni_le_le. exact H2. +Qed. + +Lemma Nplength_ultra : + forall a a':N, + ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (Nxor a a')). +Proof. + intros. case (ni_le_total (Nplength a) (Nplength a')). intro. + cut (ni_min (Nplength a) (Nplength a') = Nplength a). + intro. rewrite H0. apply Nplength_ultra_1. exact H. + exact H. + intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a'). + intro. rewrite H0. rewrite Nxor_comm. apply Nplength_ultra_1. exact H. + rewrite ni_min_comm. exact H. +Qed. + +Lemma Npdist_ultra : + forall a a' a'':N, + ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a'). +Proof. + intros. unfold Npdist in |- *. cut (Nxor (Nxor a a'') (Nxor a'' a') = Nxor a a'). + intro. rewrite <- H. apply Nplength_ultra. + rewrite Nxor_assoc. rewrite <- (Nxor_assoc a'' a'' a'). rewrite Nxor_nilpotent. + rewrite Nxor_neutral_left. reflexivity. +Qed.
\ No newline at end of file diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v new file mode 100644 index 00000000..6ba6ca3d --- /dev/null +++ b/theories/NArith/Nnat.v @@ -0,0 +1,177 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: Nnat.v 8733 2006-04-25 22:52:18Z letouzey $ i*) + +Require Import Arith. +Require Import Compare_dec. +Require Import Sumbool. +Require Import Div2. +Require Import BinPos. +Require Import BinNat. +Require Import Pnat. + +(** Translation from [N] to [nat] and back. *) + +Definition nat_of_N (a:N) := + match a with + | N0 => 0%nat + | Npos p => nat_of_P p + end. + +Definition N_of_nat (n:nat) := + match n with + | O => N0 + | S n' => Npos (P_of_succ_nat n') + end. + +Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a. +Proof. + destruct a as [| p]. reflexivity. + simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *. + rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H. + rewrite nat_of_P_inj with (1 := H). reflexivity. +Qed. + +Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n. +Proof. + induction n. trivial. + intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ. +Qed. + +(** Interaction of this translation and usual operations. *) + +Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a). +Proof. + destruct a; simpl nat_of_N; auto. + apply nat_of_P_xO. +Qed. + +Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + rewrite <- nat_of_Ndouble. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Ndouble_plus_one : + forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)). +Proof. + destruct a; simpl nat_of_N; auto. + apply nat_of_P_xI. +Qed. + +Lemma N_of_double_plus_one : + forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + rewrite <- nat_of_Ndouble_plus_one. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a). +Proof. + destruct a; simpl. + apply nat_of_P_xH. + apply nat_of_P_succ_morphism. +Qed. + +Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + rewrite <- nat_of_Nsucc. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nplus : + forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a'). +Proof. + destruct a; destruct a'; simpl; auto. + apply nat_of_P_plus_morphism. +Qed. + +Lemma N_of_plus : + forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nplus. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Nmult : + forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a'). +Proof. + destruct a; destruct a'; simpl; auto. + apply nat_of_P_mult_morphism. +Qed. + +Lemma N_of_mult : + forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + rewrite <- nat_of_Nmult. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Ndiv2 : + forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a). +Proof. + destruct a; simpl in *; auto. + destruct p; auto. + rewrite nat_of_P_xI. + rewrite div2_double_plus_one; auto. + rewrite nat_of_P_xO. + rewrite div2_double; auto. +Qed. + +Lemma N_of_div2 : + forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + rewrite <- nat_of_Ndiv2. + apply N_of_nat_of_N. +Qed. + +Lemma nat_of_Ncompare : + forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). +Proof. + destruct a; destruct a'; simpl. + compute; auto. + generalize (lt_O_nat_of_P p). + unfold nat_compare. + destruct (lt_eq_lt_dec 0 (nat_of_P p)) as [[H|H]|H]; auto. + rewrite <- H; inversion 1. + intros; generalize (lt_trans _ _ _ H0 H); inversion 1. + generalize (lt_O_nat_of_P p). + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_P p) 0) as [[H|H]|H]; auto. + intros; generalize (lt_trans _ _ _ H0 H); inversion 1. + rewrite H; inversion 1. + unfold nat_compare. + destruct (lt_eq_lt_dec (nat_of_P p) (nat_of_P p0)) as [[H|H]|H]; auto. + apply nat_of_P_lt_Lt_compare_complement_morphism; auto. + rewrite (nat_of_P_inj _ _ H); apply Pcompare_refl. + apply nat_of_P_gt_Gt_compare_complement_morphism; auto. +Qed. + +Lemma N_of_nat_compare : + forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n'). +Proof. + intros. + pattern n at 1; rewrite <- (nat_of_N_of_nat n). + pattern n' at 1; rewrite <- (nat_of_N_of_nat n'). + symmetry; apply nat_of_Ncompare. +Qed.
\ No newline at end of file |