From 157bee13827f9a616b6c82be4af110c8f2464c64 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:23 +0000 Subject: Modularization of BinNat + fixes of stdlib A sub-module N in BinNat now contains functions add (ex-Nplus), mul (ex-Nmult), ... and properties. In particular, this sub-module N directly instantiates NAxiomsSig and includes all derived properties NProp. Files Ndiv_def and co are now obsolete and kept only for compat git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/NArith/BinNat.v | 1402 +++++++++++++++++++++++++++++++++---------- theories/NArith/NArith.v | 5 - theories/NArith/Ndigits.v | 463 +++----------- theories/NArith/Ndiv_def.v | 161 +---- theories/NArith/Ngcd_def.v | 85 +-- theories/NArith/Nsqrt_def.v | 48 +- 6 files changed, 1185 insertions(+), 979 deletions(-) (limited to 'theories/NArith') diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 3a4250566..b1d62d776 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -7,7 +7,8 @@ (************************************************************************) Require Export BinNums. -Require Import BinPos. +Require Import BinPos RelationClasses Morphisms Setoid + Equalities GenericMinMax Wf_nat Bool NAxioms NProperties. (**********************************************************************) (** * Binary natural numbers, operations and properties *) @@ -16,25 +17,35 @@ Require Import BinPos. (** The type [N] and its constructors [N0] and [Npos] are now defined in [BinNums.v] *) +(** Every definitions and early properties about binary natural numbers + are placed in a module [N] for qualification purpose. *) + Local Open Scope N_scope. -Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. -Proof. - destruct n; auto. - left; exists p; auto. -Defined. +(** Every definitions and early properties about positive numbers + are placed in a module [N] for qualification purpose. *) + +Module N + <: NAxiomsMiniSig + <: UsualOrderedTypeFull + <: UsualDecidableTypeFull + <: TotalOrder. + +Definition t := N. +Definition eq := @Logic.eq t. +Definition eq_equiv := @eq_equivalence t. -(** Operation x -> 2*x+1 *) +(** Operation [x -> 2*x+1] *) -Definition Ndouble_plus_one x := +Definition succ_double x := match x with | 0 => Npos 1 | Npos p => Npos p~1 end. -(** Operation x -> 2*x *) +(** Operation [x -> 2*x] *) -Definition Ndouble n := +Definition double n := match n with | 0 => 0 | Npos p => Npos p~0 @@ -42,88 +53,68 @@ Definition Ndouble n := (** Successor *) -Definition Nsucc n := +Definition succ n := match n with - | 0 => Npos 1 - | Npos p => Npos (Psucc p) + | 0 => 1 + | Npos p => Npos (Pos.succ p) end. (** Predecessor *) -Definition Npred (n : N) := match n with -| 0 => 0 -| Npos p => match p with - | xH => 0 - | _ => Npos (Ppred p) - end -end. +Definition pred n := + match n with + | 0 => 0 + | Npos p => Pos.pred_N p + end. (** The successor of a N can be seen as a positive *) -Definition Nsucc_pos (n : N) : positive := +Definition succ_pos (n : N) : positive := match n with | N0 => 1%positive - | Npos p => Psucc p + | Npos p => Pos.succ 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 := +Definition add n m := match n, m with | 0, _ => m | _, 0 => n | Npos p, Npos q => Npos (p + q) end. -Infix "+" := Nplus : N_scope. +Infix "+" := add : N_scope. (** Subtraction *) -Definition Nminus (n m : N) := +Definition sub n m := match n, m with | 0, _ => 0 | n, 0 => n | Npos n', Npos m' => - match Pminus_mask n' m' with + match Pos.sub_mask n' m' with | IsPos p => Npos p | _ => 0 end end. -Infix "-" := Nminus : N_scope. +Infix "-" := sub : N_scope. (** Multiplication *) -Definition Nmult n m := +Definition mul n m := match n, m with | 0, _ => 0 | _, 0 => 0 | Npos p, Npos q => Npos (p * q) end. -Infix "*" := Nmult : N_scope. - -(** Boolean Equality *) - -Definition Neqb n m := - match n, m with - | 0, 0 => true - | Npos n, Npos m => Peqb n m - | _,_ => false - end. +Infix "*" := mul : N_scope. (** Order *) -Definition Ncompare n m := +Definition compare n m := match n, m with | 0, 0 => Eq | 0, Npos m' => Lt @@ -131,64 +122,299 @@ Definition Ncompare n m := | Npos n', Npos m' => (n' ?= m')%positive end. -Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +Infix "?=" := compare (at level 70, no associativity) : N_scope. -Definition Nlt (x y:N) := (x ?= y) = Lt. -Definition Ngt (x y:N) := (x ?= y) = Gt. -Definition Nle (x y:N) := (x ?= y) <> Gt. -Definition Nge (x y:N) := (x ?= y) <> Lt. +Definition lt x y := (x ?= y) = Lt. +Definition gt x y := (x ?= y) = Gt. +Definition le x y := (x ?= y) <> Gt. +Definition ge x y := (x ?= y) <> Lt. -Infix "<=" := Nle : N_scope. -Infix "<" := Nlt : N_scope. -Infix ">=" := Nge : N_scope. -Infix ">" := Ngt : N_scope. +Infix "<=" := le : N_scope. +Infix "<" := lt : N_scope. +Infix ">=" := ge : N_scope. +Infix ">" := gt : N_scope. Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope. Notation "x <= y < z" := (x <= y /\ y < z) : N_scope. Notation "x < y < z" := (x < y /\ y < z) : N_scope. Notation "x < y <= z" := (x < y /\ y <= z) : N_scope. +(** Boolean equality and comparison *) + +(** Nota: this [eqb] is not convertible with the generated [N_beq], + since the underlying [Pos.eqb] differs from [positive_beq] + (cf BinIntDef). *) + +Fixpoint eqb n m := + match n, m with + | 0, 0 => true + | Npos p, Npos q => Pos.eqb p q + | _, _ => false + end. + +Definition leb x y := + match x ?= y with Gt => false | _ => true end. + +Definition ltb x y := + match x ?= y with Lt => true | _ => false end. + +Infix "=?" := eqb (at level 70, no associativity) : N_scope. +Infix "<=?" := leb (at level 70, no associativity) : N_scope. +Infix " n | Gt => n' end. -Definition Nmax (n n' : N) := match Ncompare n n' with +Definition max n n' := match n ?= n' with | Lt | Eq => n' | Gt => n end. +(** Dividing by 2 *) + +Definition div2 n := + match n with + | 0 => 0 + | Npos 1 => 0 + | Npos (p~0) => Npos p + | Npos (p~1) => Npos p + end. + +(** Parity *) + +Definition even n := + match n with + | 0 => true + | Npos (xO _) => true + | _ => false + end. + +Definition odd n := negb (even n). + +(** Power *) + +Definition pow n p := + match p, n with + | 0, _ => Npos 1 + | _, 0 => 0 + | Npos p, Npos q => Npos (q^p) + end. + +Infix "^" := pow : N_scope. + +(** Base-2 logarithm *) + +Definition log2 n := + match n with + | 0 => 0 + | Npos 1 => 0 + | Npos (p~0) => Npos (Pos.size p) + | Npos (p~1) => Npos (Pos.size p) + end. + +(** How many digits in a number ? + Number 0 is said to have no digits at all. +*) + +Definition size n := + match n with + | 0 => 0 + | Npos p => Npos (Pos.size p) + end. + +Definition size_nat n := + match n with + | 0 => O + | Npos p => Pos.size_nat p + end. + +(** Euclidean division *) + +Fixpoint pos_div_eucl (a:positive)(b:N) : N * N := + match a with + | xH => + match b with 1 => (1,0) | _ => (0,1) end + | xO a' => + let (q, r) := pos_div_eucl a' b in + let r' := double r in + if b <=? r' then (succ_double q, r' - b) + else (double q, r') + | xI a' => + let (q, r) := pos_div_eucl a' b in + let r' := succ_double r in + if b <=? r' then (succ_double q, r' - b) + else (double q, r') + end. + +Definition div_eucl (a b:N) : N * N := + match a, b with + | 0, _ => (0, 0) + | _, 0 => (0, a) + | Npos na, _ => pos_div_eucl na b + end. + +Definition div a b := fst (div_eucl a b). +Definition modulo a b := snd (div_eucl a b). + +Infix "/" := div : N_scope. +Infix "mod" := modulo (at level 40, no associativity) : N_scope. + +(** Greatest common divisor *) + +Definition divide p q := exists r, p*r = q. + +Notation "( p | q )" := (divide p q) (at level 0) : N_scope. + +Definition gcd a b := + match a, b with + | 0, _ => b + | _, 0 => a + | Npos p, Npos q => Npos (Pos.gcd p q) + end. + +(** Generalized Gcd, also computing rests of [a] and [b] after + division by gcd. *) + +Definition ggcd a b := + match a, b with + | 0, _ => (b,(0,1)) + | _, 0 => (a,(1,0)) + | Npos p, Npos q => + let '(g,(aa,bb)) := Pos.ggcd p q in + (Npos g, (Npos aa, Npos bb)) + end. + +(** Square root *) + +Definition sqrtrem n := + match n with + | 0 => (0, 0) + | Npos p => + match Pos.sqrtrem p with + | (s, IsPos r) => (Npos s, Npos r) + | (s, _) => (Npos s, 0) + end + end. + +Definition sqrt n := + match n with + | 0 => 0 + | Npos p => Npos (Pos.sqrt p) + end. + +(** Operation over bits of a [N] number. *) + +(** Logical [or] *) + +Definition lor n m := + match n, m with + | 0, _ => m + | _, 0 => n + | Npos p, Npos q => Npos (Pos.lor p q) + end. + +(** Logical [and] *) + +Definition land n m := + match n, m with + | 0, _ => 0 + | _, 0 => 0 + | Npos p, Npos q => Pos.land p q + end. + +(** Logical [diff] *) + +Fixpoint ldiff n m := + match n, m with + | 0, _ => 0 + | _, 0 => n + | Npos p, Npos q => Pos.ldiff p q + end. + +(** [xor] *) + +Definition lxor n m := + match n, m with + | 0, _ => m + | _, 0 => n + | Npos p, Npos q => Pos.lxor p q + end. + +(** Shifts *) + +Definition shiftl_nat (a:N)(n:nat) := iter_nat n _ double a. + +Definition shiftr_nat (a:N)(n:nat) := iter_nat n _ div2 a. + +Definition shiftl a n := + match a with + | 0 => 0 + | Npos a => Npos (Pos.shiftl a n) + end. + +Definition shiftr a n := + match n with + | 0 => a + | Npos p => Pos.iter p div2 a + end. + +(** Checking whether a particular bit is set or not *) + +Definition testbit_nat (a:N) := + match a with + | 0 => fun _ => false + | Npos p => Pos.testbit_nat p + end. + +(** Same, but with index in N *) + +Definition testbit a n := + match a with + | 0 => false + | Npos p => Pos.testbit p n + end. + (** Translation from [N] to [nat] and back. *) -Definition nat_of_N (a:N) := +Definition to_nat (a:N) := match a with | N0 => O - | Npos p => nat_of_P p + | Npos p => Pos.to_nat p end. -Definition N_of_nat (n:nat) := +Definition of_nat (n:nat) := match n with | O => 0 - | S n' => Npos (P_of_succ_nat n') + | S n' => Npos (Pos.of_succ_nat n') end. (** Decidability of equality. *) -Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }. +Definition eq_dec : forall n m : N, { n = m } + { n <> m }. Proof. decide equality. - apply positive_eq_dec. + apply Pos.eq_dec. Defined. -(** convenient induction principles *) +(** Discrimination principle *) -Lemma N_ind_double : +Definition discr n : { p:positive | n = Npos p } + { n = N0 }. +Proof. + destruct n; auto. + left; exists p; auto. +Defined. + +(** Convenient induction principles *) + +Lemma binary_ind : forall (a:N) (P:N -> Prop), P 0 -> - (forall a, P a -> P (Ndouble a)) -> - (forall a, P a -> P (Ndouble_plus_one a)) -> P a. + (forall a, P a -> P (double a)) -> + (forall a, P a -> P (succ_double a)) -> P a. Proof. intros a P P0 P2 PS2. destruct a as [|p]. trivial. induction p as [p IHp|p IHp| ]. @@ -197,11 +423,11 @@ Proof. now apply (PS2 0). Qed. -Lemma N_rec_double : +Lemma binary_rec : forall (a:N) (P:N -> Set), P 0 -> - (forall a, P a -> P (Ndouble a)) -> - (forall a, P a -> P (Ndouble_plus_one a)) -> P a. + (forall a, P a -> P (double a)) -> + (forall a, P a -> P (succ_double a)) -> P a. Proof. intros a P P0 P2 PS2. destruct a as [|p]. trivial. induction p as [p IHp|p IHp| ]. @@ -212,478 +438,996 @@ Qed. (** Peano induction on binary natural numbers *) -Definition Nrect +Definition peano_rect (P : N -> Type) (a : P 0) - (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n := + (f : forall n : N, P n -> P (succ 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 | 0 => a -| Npos p => Prect P' (f 0 a) f' p +| Npos p => Pos.peano_rect P' (f 0 a) f' p end. -Theorem Nrect_base : forall P a f, Nrect P a f 0 = a. +Theorem peano_rect_base P a f : peano_rect P a f 0 = a. Proof. -intros P a f; simpl; reflexivity. +reflexivity. Qed. -Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n). +Theorem peano_rect_succ P a f n : + peano_rect P a f (succ n) = f n (peano_rect P a f n). Proof. -intros P a f; destruct n as [| p]; simpl; -[rewrite Prect_base | rewrite Prect_succ]; reflexivity. +destruct n; simpl; +[rewrite Pos.peano_rect_base | rewrite Pos.peano_rect_succ]; reflexivity. Qed. -Definition Nind (P : N -> Prop) := Nrect P. +Definition peano_ind (P : N -> Prop) := peano_rect P. -Definition Nrec (P : N -> Set) := Nrect P. +Definition peano_rec (P : N -> Set) := peano_rect P. -Theorem Nrec_base : forall P a f, Nrec P a f 0 = a. +Theorem peano_rec_base P a f : peano_rec P a f 0 = a. Proof. -intros P a f; unfold Nrec; apply Nrect_base. +apply peano_rect_base. Qed. -Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n). +Theorem peano_rec_succ P a f n : + peano_rec P a f (succ n) = f n (peano_rec P a f n). Proof. -intros P a f; unfold Nrec; apply Nrect_step. +apply peano_rect_succ. Qed. -(** Properties of successor and predecessor *) +(** Properties of double *) -Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n. +Lemma double_spec n : double n = 2 * n. Proof. -intros [| p]; simpl. reflexivity. -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. + reflexivity. Qed. -Lemma Nsucc_pred : forall n, n<>0 -> Nsucc (Npred n) = n. +Lemma succ_double_spec n : succ_double n = 2 * n + 1. 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. + now destruct n. Qed. (** Properties of mixed successor and predecessor. *) -Lemma Ppred_N_spec : forall p, Ppred_N p = Npred (Npos p). +Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p). Proof. now destruct p. Qed. -Lemma Nsucc_pos_spec : forall n, Npos (Nsucc_pos n) = Nsucc n. +Lemma succ_pos_spec n : Npos (succ_pos n) = succ n. Proof. now destruct n. Qed. -Lemma Ppred_Nsucc : forall n, Ppred_N (Nsucc_pos n) = n. +Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n. Proof. - intros. now rewrite Ppred_N_spec, Nsucc_pos_spec, Npred_succ. + destruct n. trivial. apply Pos.pred_N_succ. Qed. -(** Properties of addition *) - -Theorem Nplus_0_l : forall n:N, 0 + n = n. +Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p. Proof. -reflexivity. + destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double. Qed. -Theorem Nplus_0_r : forall n:N, n + 0 = n. +(** Properties of successor and predecessor *) + +Theorem pred_succ n : pred (succ n) = n. Proof. -destruct n; reflexivity. +destruct n; trivial. simpl. apply Pos.pred_N_succ. Qed. -Theorem Nplus_comm : forall n m:N, n + m = m + n. +Theorem pred_sub n : pred n = sub n 1. Proof. -intros. -destruct n; destruct m; simpl; try reflexivity. -rewrite Pplus_comm; reflexivity. + now destruct n as [|[p|p|]]. Qed. -Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p. +Theorem succ_0_discr n : succ n <> 0. Proof. -intros. -destruct n; try reflexivity. -destruct m; try reflexivity. -destruct p; try reflexivity. -simpl; rewrite Pplus_assoc; reflexivity. +now destruct n. Qed. -Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m). +(** Specification of addition *) + +Theorem add_0_l n : 0 + n = n. Proof. -destruct n, m. - simpl; reflexivity. - unfold Nsucc, Nplus; rewrite <- Pplus_one_succ_l; reflexivity. - simpl; reflexivity. - simpl; rewrite Pplus_succ_permute_l; reflexivity. +reflexivity. Qed. -Theorem Nsucc_0 : forall n : N, Nsucc n <> 0. +Theorem add_succ_l n m : succ n + m = succ (n + m). Proof. -now destruct n. +destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l. Qed. -Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m. +(** Specification of subtraction. *) + +Theorem sub_0_r n : n - 0 = n. Proof. -intros [|p] [|q] H; simpl in *; trivial; injection H; clear H; intro H. - now elim (Psucc_not_one q). - now elim (Psucc_not_one p). - apply Psucc_inj in H. now f_equal. +now destruct n. Qed. -Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p. +Theorem sub_succ_r n m : n - succ m = pred (n - m). Proof. - induction n using Nind. - trivial. - intros m p H; rewrite 2 Nplus_succ in H. - apply Nsucc_inj in H. now apply IHn. +destruct n as [|p], m as [|q]; trivial. +now destruct p. +simpl. rewrite Pos.sub_mask_succ_r, Pos.sub_mask_carry_spec. +now destruct (Pos.sub_mask p q) as [|[r|r|]|]. Qed. -(** Properties of subtraction. *) +(** Specification of multiplication *) -Lemma Nminus_N0_Nle : forall n n' : N, n - n' = 0 <-> n <= n'. +Theorem mul_0_l n : 0 * n = 0. Proof. -intros [| p] [| q]; unfold Nle; simpl; -split; intro H; try easy. -now elim H. -contradict H. now destruct (Pminus_mask_Gt _ _ H) as (h & -> & _). -destruct (Pcompare_spec p q); try now elim H. -subst. now rewrite Pminus_mask_diag. -now rewrite Pminus_mask_Lt. +reflexivity. Qed. -Theorem Nminus_0_r : forall n : N, n - 0 = n. +Theorem mul_succ_l n m : (succ n) * m = n * m + m. Proof. -now destruct n. +destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm. +apply Pos.mul_succ_l. Qed. -Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m). +(** Properties of comparison *) + +Lemma compare_refl n : (n ?= n) = Eq. Proof. -intros [|p] [|q]; trivial. -now destruct p. -simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. -now destruct (Pminus_mask p q) as [|[r|r|]|]. +destruct n; simpl; trivial. apply Pos.compare_refl. Qed. -(** Properties of multiplication *) +Theorem compare_eq n m : (n ?= m) = Eq -> n = m. +Proof. +destruct n, m; simpl; try easy. intros. f_equal. +now apply Pos.compare_eq. +Qed. -Theorem Nmult_0_l : forall n:N, 0 * n = 0. +Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m. Proof. -reflexivity. +split; intros. now apply compare_eq. subst; now apply compare_refl. Qed. -Theorem Nmult_1_l : forall n:N, Npos 1 * n = n. +Lemma compare_antisym n m : CompOpp (n ?= m) = (m ?= n). Proof. -destruct n; reflexivity. +destruct n, m; simpl; trivial. +symmetry. apply Pos.compare_antisym. (* TODO : quel sens ? *) Qed. -Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. +(** Specification of lt and le *) + +Theorem lt_irrefl n : ~ n < n. Proof. -intros [|n] [|m]; simpl; trivial. now rewrite Pmult_Sn_m. +unfold lt. now rewrite compare_refl. Qed. -Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n. +Lemma lt_eq_cases n m : n <= m <-> n < m \/ n=m. Proof. -intros [|n]; simpl; trivial. now rewrite Pmult_1_r. +unfold le, lt. rewrite <- compare_eq_iff. +destruct (n ?= m); now intuition. Qed. -Theorem Nmult_comm : forall n m:N, n * m = m * n. +Lemma lt_succ_r n m : n < succ m <-> n<=m. Proof. -intros [|n] [|m]; simpl; trivial. now rewrite Pmult_comm. +destruct n as [|p], m as [|q]; simpl; try easy'. +split. now destruct p. now destruct 1. +apply Pos.lt_succ_r. Qed. -Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p. +Lemma compare_spec n m : CompareSpec (n=m) (n n=m. Proof. -intros. -destruct n; try reflexivity. -destruct m; destruct p; try reflexivity. -simpl; rewrite Pmult_plus_distr_r; reflexivity. +destruct n as [|n], m as [|m]; simpl; try easy'. +rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H. Qed. -Theorem Nmult_plus_distr_l : forall n m p:N, p * (n + m) = p * n + p * m. +Lemma ltb_lt n m : (n n < m. Proof. -intros. rewrite ! (Nmult_comm p); apply Nmult_plus_distr_r. + unfold ltb, lt. destruct compare; easy'. Qed. -Theorem Nmult_reg_r : forall n m p:N, p <> 0 -> n * p = m * p -> n = m. +Lemma leb_le n m : (n <=? m) = true <-> n <= m. Proof. -destruct p; intros Hp H. -contradiction Hp; reflexivity. -destruct n; destruct m; reflexivity || (try discriminate H). -injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity. + unfold leb, le. destruct compare; easy'. Qed. -(** Properties of boolean order. *) +Lemma leb_spec n m : BoolSpec (n<=m) (m n=m. +Lemma ltb_spec n m : BoolSpec (n n = m. Proof. - now destruct n. +destruct n as [|p], m as [|q]; intro H; simpl in *; trivial; destr_eq H. + now destruct (Pos.succ_not_1 q). + now destruct (Pos.succ_not_1 p). + f_equal. now apply Pos.succ_inj. Qed. -Lemma Ncompare_refl : forall n, (n ?= n) = Eq. +Theorem add_0_r n : n + 0 = n. Proof. -destruct n; simpl; auto. -apply Pcompare_refl. +now destruct n. Qed. -Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m. +Theorem add_comm n m : n + m = m + n. Proof. -destruct n as [| n]; destruct m as [| m]; simpl; intro H; - reflexivity || (try discriminate H). - rewrite (Pcompare_Eq_eq n m H); reflexivity. +destruct n, m; simpl; try reflexivity. simpl. f_equal. apply Pos.add_comm. Qed. -Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m. +Theorem add_assoc n m p : n + (m + p) = n + m + p. Proof. -split; intros; - [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ]. +destruct n; try reflexivity. +destruct m; try reflexivity. +destruct p; try reflexivity. +simpl. f_equal. apply Pos.add_assoc. Qed. -Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n). +Lemma sub_add n m : n <= m -> m - n + n = m. Proof. -destruct n; destruct m; simpl; auto. -exact (Pcompare_antisym p p0 Eq). + destruct n as [|p], m as [|q]; simpl; try easy'. + unfold le, compare. rewrite Pos.compare_antisym. intros H. + assert (H1 := Pos.sub_mask_compare q p). + assert (H2 := Pos.sub_mask_add q p). + destruct Pos.sub_mask as [|r|]; simpl in *; f_equal. + symmetry. now apply Pos.compare_eq. + rewrite Pos.add_comm. now apply H2. + rewrite <- H1 in H. now destruct H. Qed. -Lemma Ngt_Nlt : forall n m, n > m -> m < n. +Theorem mul_1_l n : 1 * n = n. Proof. -unfold Ngt, Nlt; intros n m GT. -rewrite <- Ncompare_antisym, GT; reflexivity. +now destruct n. Qed. -Theorem Nlt_irrefl : forall n : N, ~ n < n. +Theorem mul_comm n m : n * m = m * n. Proof. -intro n; unfold Nlt; now rewrite Ncompare_refl. +destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm. Qed. -Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q. +Theorem mul_assoc n m p : n * (m * p) = n * m * p. Proof. -destruct n; - destruct m; try discriminate; - destruct q; try discriminate; auto. -eapply Plt_trans; eauto. +destruct n; try reflexivity. +destruct m; try reflexivity. +destruct p; try reflexivity. +simpl. f_equal. apply Pos.mul_assoc. Qed. -Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m. +Theorem mul_add_distr_r n m p : (n + m) * p = n * p + m * p. Proof. - intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto. +destruct n; try reflexivity. +destruct m, p; try reflexivity. +simpl. f_equal. apply Pos.mul_add_distr_r. Qed. -Theorem Ncompare_n_Sm : - forall n m : N, (n ?= Nsucc m) = Lt <-> (n ?= m) = Lt \/ n = m. +Theorem mul_add_distr_l n m p : n * (m + p) = n * m + n * p. Proof. -intros [|p] [|q]; simpl; split; intros H; auto. -destruct p; discriminate. -destruct H; discriminate. -apply Plt_succ_r, Ple_lteq in H. destruct H; subst; auto. -apply Plt_succ_r, Ple_lteq. destruct H; [left|right]; congruence. +rewrite !(mul_comm n); apply mul_add_distr_r. Qed. -Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y. +Lemma le_0_l n : 0<=n. Proof. -unfold Nle, Nlt; intros. -generalize (Ncompare_eq_correct x y). -destruct (x ?= y); intuition; discriminate. +now destruct n. Qed. -Lemma Nlt_succ_r : forall n m, n < Nsucc m <-> n<=m. +Theorem lt_trans n m q : n < m -> m < q -> n < q. Proof. -intros n m. -eapply iff_trans. apply Ncompare_n_Sm. apply iff_sym, Nle_lteq. +destruct n, m, q; try easy. eapply Pos.lt_trans; eauto. Qed. -Lemma Nle_trans : forall n m p, n<=m -> m<=p -> n<=p. +Lemma le_trans n m p : n<=m -> m<=p -> n<=p. Proof. - intros n m p H H'. - apply Nle_lteq. apply Nle_lteq in H. apply Nle_lteq in H'. - destruct H, H'; subst; auto. - left; now apply Nlt_trans with m. + rewrite 3 lt_eq_cases. intros [H|H] [H'|H']; subst; + (now right) || left; trivial. + now apply lt_trans with m. Qed. -Lemma Nle_succ_l : forall n m, Nsucc n <= m <-> n < m. +Lemma add_lt_cancel_l n m p : p+n < p+m -> n min n m = n. Proof. -intros. -destruct (Ncompare x y) as [ ]_eqn; constructor; auto. -apply Ncompare_Eq_eq; auto. -apply Ngt_Nlt; auto. +unfold min, le. case compare; trivial. now destruct 1. Qed. -(** Order and operations *) +Theorem min_r n m : m <= n -> min n m = m. +Proof. +unfold min, le. rewrite <- compare_antisym. +case compare_spec; trivial. now destruct 2. +Qed. -(** NB : Many more results will come from NBinary, the Number instantiation. - The next lemmas are useful for proving the correctness of - advanced functions. -*) +Theorem max_l n m : m <= n -> max n m = n. +Proof. +unfold max, le. rewrite <- compare_antisym. +case compare_spec; auto. now destruct 2. +Qed. -Lemma Nplus_lt_cancel_l : forall n m p, p+n < p+m -> n max n m = m. Proof. - intros. destruct p. simpl; auto. - destruct n; destruct m. - elim (Nlt_irrefl _ H). - red; auto. - rewrite Nplus_0_r in H. simpl in H. - red in H. simpl in H. - elim (Plt_not_plus_l _ _ H). - now apply (Pplus_lt_mono_l p). +unfold max, le. case compare; trivial. now destruct 1. Qed. (** 0 is the least natural number *) -Theorem Ncompare_0 : forall n : N, Ncompare n 0 <> Lt. +Theorem compare_0_r n : (n ?= 0) <> Lt. Proof. -destruct n; discriminate. +now destruct n. Qed. (** Dividing by 2 *) -Definition Ndiv2 (n:N) := - match n with - | 0 => 0 - | Npos 1 => 0 - | Npos (p~0) => Npos p - | Npos (p~1) => Npos p - end. - -Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. +Lemma div2_double n : div2 (double n) = n. Proof. - destruct n; trivial. +now destruct n. Qed. -Lemma Ndouble_plus_one_div2 : - forall n:N, Ndiv2 (Ndouble_plus_one n) = n. +Lemma div2_succ_double n : div2 (succ_double n) = n. Proof. - destruct n; trivial. +now destruct n. Qed. -Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m. +Lemma double_inj n m : double n = double m -> n = m. Proof. - intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2. +intro H. rewrite <- (div2_double n), H. apply div2_double. Qed. -Lemma Ndouble_plus_one_inj : - forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m. +Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m. Proof. - intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. +intro H. rewrite <- (div2_succ_double n), H. apply div2_succ_double. Qed. -(** Power *) - -Definition Npow n p := - match p, n with - | 0, _ => Npos 1 - | _, 0 => 0 - | Npos p, Npos q => Npos (Ppow q p) - end. - -Infix "^" := Npow : N_scope. +(** Speficications of power *) -Lemma Npow_0_r : forall n, n ^ 0 = Npos 1. +Lemma pow_0_r n : n ^ 0 = 1. Proof. reflexivity. Qed. -Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p. +Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p. Proof. - intros [|q] [|p]; simpl; trivial; f_equal. - apply Ppow_succ_r. + intros _. + destruct n, p; simpl; trivial; f_equal. apply Pos.pow_succ_r. Qed. -(** Base-2 logarithm *) +Lemma pow_neg_r n p : p<0 -> n^p = 0. +Proof. + now destruct p. +Qed. -Definition Nlog2 n := - match n with - | 0 => 0 - | Npos 1 => 0 - | Npos (p~0) => Npos (Psize_pos p) - | Npos (p~1) => Npos (Psize_pos p) - end. +(** Specification of Base-2 logarithm *) -Lemma Nlog2_spec : forall n, 0 < n -> - (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)). +Lemma log2_spec n : 0 < n -> + 2^(log2 n) <= n < 2^(succ (log2 n)). Proof. - intros [|[p|p|]] H; discriminate H || clear H; simpl; split. - eapply Nle_trans with (Npos (p~0)). - apply Psize_pos_le. - apply Nle_lteq; left. exact (Pcompare_p_Sp (p~0)). - apply Psize_pos_gt. - apply Psize_pos_le. - apply Psize_pos_gt. + destruct n as [|[p|p|]]; discriminate || intros _; simpl; split. + eapply le_trans with (Npos (p~0)). + apply Pos.size_le. + apply lt_eq_cases; left. apply Pos.lt_succ_diag_r. + apply Pos.size_gt. + apply Pos.size_le. + apply Pos.size_gt. discriminate. reflexivity. Qed. -Lemma Nlog2_nonpos : forall n, n<=0 -> Nlog2 n = 0. +Lemma log2_nonpos n : n<=0 -> log2 n = 0. Proof. - intros [|n] Hn. reflexivity. now destruct Hn. + destruct n; intros Hn. reflexivity. now destruct Hn. Qed. -(** Parity *) +Lemma size_log2 n : n<>0 -> size n = succ (log2 n). +Proof. + destruct n as [|[n|n| ]]; trivial. now destruct 1. +Qed. -Definition Neven n := - match n with - | 0 => true - | Npos (xO _) => true - | _ => false - end. -Definition Nodd n := negb (Neven n). +Lemma size_gt n : n < 2^(size n). +Proof. + destruct n. reflexivity. simpl. apply Pos.size_gt. +Qed. -Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m. +Lemma size_le n : 2^(size n) <= succ_double n. +Proof. + destruct n. discriminate. + simpl. apply le_trans with (Npos (p~0)). + apply Pos.size_le. + apply lt_eq_cases. left. apply Pos.lt_succ_diag_r. +Qed. + +(** Specification of parity functions *) + +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. + +Lemma even_spec n : even n = true <-> Even n. Proof. destruct n. split. now exists 0. trivial. - destruct p; simpl; split; trivial; try discriminate. + destruct p; simpl; split; try easy. intros (m,H). now destruct m. now exists (Npos p). intros (m,H). now destruct m. Qed. -Lemma Nodd_spec : forall n, Nodd n = true <-> exists m, n=2*m+1. +Lemma odd_spec n : odd n = true <-> Odd n. Proof. destruct n. split. discriminate. intros (m,H). now destruct m. - destruct p; simpl; split; trivial; try discriminate. - exists (Npos p). reflexivity. + destruct p; simpl; split; try easy. + now exists (Npos p). intros (m,H). now destruct m. - exists 0. reflexivity. + now exists 0. +Qed. + +(** Specification of the euclidean division *) + +Theorem pos_div_eucl_spec (a:positive)(b:N) : + let (q,r) := pos_div_eucl a b in Npos a = q * b + r. +Proof. + induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. + (* a~1 *) + destruct pos_div_eucl as (q,r). + assert (Npos a~1 = (double q)*b + succ_double r). + rewrite succ_double_spec, double_spec. + now rewrite add_assoc, <- mul_assoc, <- mul_add_distr_l, <- IHa. + case leb_spec; intros H'; trivial. + rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec, + mul_1_l, <- add_assoc. + now rewrite (add_comm b), sub_add. + (* a~0 *) + destruct pos_div_eucl as (q,r). + assert (Npos a~0 = (double q)*b + double r). + rewrite (double_spec q), (double_spec r). (* BUG: !double_spec *) + now rewrite <- mul_assoc, <- mul_add_distr_l, <- IHa. + case leb_spec; intros H'; trivial. + rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec, + mul_1_l, <- add_assoc. + now rewrite (add_comm b), sub_add. + (* 1 *) + now destruct b as [|[ | | ]]. +Qed. + +Theorem div_eucl_spec a b : + let (q,r) := div_eucl a b in a = b * q + r. +Proof. + destruct a as [|a], b as [|b]; unfold div_eucl; trivial. + generalize (pos_div_eucl_spec a (Npos b)). + destruct pos_div_eucl. now rewrite mul_comm. +Qed. + +Theorem div_mod' a b : a = b * (a/b) + (a mod b). +Proof. + generalize (div_eucl_spec a b). + unfold div, modulo. now destruct div_eucl. +Qed. + +Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b). +Proof. + intros _. apply div_mod'. +Qed. + +Lemma succ_double_lt n m : n succ_double n < double m. +Proof. + destruct n as [|n], m as [|m]; intros H; try easy. + unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H. +Qed. + +Theorem pos_div_eucl_remainder (a:positive) (b:N) : + b<>0 -> snd (pos_div_eucl a b) < b. +Proof. + intros Hb. + induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. + (* a~1 *) + destruct pos_div_eucl as (q,r); simpl in *. + case leb_spec; intros H; simpl; trivial. + apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial. + destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. + apply (succ_double_lt _ _ IHa). + (* a~0 *) + destruct pos_div_eucl as (q,r); simpl in *. + case leb_spec; intros H; simpl; trivial. + apply add_lt_cancel_l with b. rewrite add_comm, sub_add by trivial. + destruct b as [|b]; [now destruct Hb| simpl; rewrite Pos.add_diag ]. + now destruct r. + (* 1 *) + destruct b as [|[ | | ]]; easy || (now destruct Hb). +Qed. + +Theorem mod_lt a b : b<>0 -> a mod b < b. +Proof. + destruct b as [ |b]. now destruct 1. + destruct a as [ |a]. reflexivity. + unfold modulo. simpl. apply pos_div_eucl_remainder. +Qed. + +Theorem mod_bound_pos a b : 0<=a -> 0 0 <= a mod b < b. +Proof. + intros _ H. split. apply le_0_l. apply mod_lt. now destruct b. +Qed. + +(** Specification of square root *) + +Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n. +Proof. + destruct n. reflexivity. + unfold sqrtrem, sqrt, Pos.sqrt. + destruct (Pos.sqrtrem p) as (s,r). now destruct r. +Qed. + +Lemma sqrtrem_spec n : + let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s. +Proof. + destruct n. now split. + generalize (Pos.sqrtrem_spec p). simpl. + destruct 1; simpl; subst; now split. +Qed. + +Lemma sqrt_spec n : 0<=n -> + let s := sqrt n in s*s <= n < (succ s)*(succ s). +Proof. + intros _. destruct n. now split. apply (Pos.sqrt_spec p). +Qed. + +Lemma sqrt_neg n : n<0 -> sqrt n = 0. +Proof. + now destruct n. +Qed. + +(** Specification of gcd *) + +(** The first component of ggcd is gcd *) + +Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. +Proof. + destruct a as [|p], b as [|q]; simpl; auto. + assert (H := Pos.ggcd_gcd p q). + destruct Pos.ggcd as (g,(aa,bb)); simpl; now f_equal. +Qed. + +(** The other components of ggcd are indeed the correct factors. *) + +Lemma ggcd_correct_divisors a b : + let '(g,(aa,bb)) := ggcd a b in + a=g*aa /\ b=g*bb. +Proof. + destruct a as [|p], b as [|q]; simpl; auto. + now rewrite Pos.mul_1_r. + now rewrite Pos.mul_1_r. + generalize (Pos.ggcd_correct_divisors p q). + destruct Pos.ggcd as (g,(aa,bb)); simpl. + destruct 1; split; now f_equal. +Qed. + +(** We can use this fact to prove a part of the gcd correctness *) + +Lemma gcd_divide_l a b : (gcd a b | a). +Proof. + rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). + destruct ggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto. +Qed. + +Lemma gcd_divide_r a b : (gcd a b | b). +Proof. + rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto. +Qed. + +(** We now prove directly that gcd is the greatest amongst common divisors *) + +Lemma gcd_greatest a b c : (c|a) -> (c|b) -> (c|gcd a b). +Proof. + destruct a as [ |p], b as [ |q]; simpl; trivial. + destruct c as [ |r]. intros (s,H). discriminate. + intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. + destruct (Pos.gcd_greatest p q r) as (u,H). + exists s. now inversion Hs. + exists t. now inversion Ht. + exists (Npos u). simpl; now f_equal. +Qed. + +Lemma gcd_nonneg a b : 0 <= gcd a b. +Proof. apply le_0_l. Qed. + +(** Specification of bitwise functions *) + +(** Correctness proofs for [testbit]. *) + +Lemma testbit_even_0 a : testbit (2*a) 0 = false. +Proof. + now destruct a. Qed. +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. +Proof. + now destruct a. +Qed. + +Lemma testbit_succ_r_div2 a n : 0<=n -> + testbit a (succ n) = testbit (div2 a) n. +Proof. + intros _. destruct a as [|[a|a| ]], n as [|n]; simpl; trivial; + f_equal; apply Pos.pred_N_succ. +Qed. + +Lemma testbit_odd_succ a n : 0<=n -> + testbit (2*a+1) (succ n) = testbit a n. +Proof. + intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a. +Qed. + +Lemma testbit_even_succ a n : 0<=n -> + testbit (2*a) (succ n) = testbit a n. +Proof. + intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a. +Qed. + +Lemma testbit_neg_r a n : n<0 -> testbit a n = false. +Proof. + now destruct n. +Qed. + +(** Correctness proofs for shifts *) + +Lemma shiftr_succ_r a n : + shiftr a (succ n) = div2 (shiftr a n). +Proof. + destruct n; simpl; trivial. apply Pos.iter_succ. +Qed. + +Lemma shiftl_succ_r a n : + shiftl a (succ n) = double (shiftl a n). +Proof. + destruct n, a; simpl; trivial. f_equal. apply Pos.iter_succ. +Qed. + +Lemma shiftr_spec a n m : 0<=m -> + testbit (shiftr a n) m = testbit a (m+n). +Proof. + intros _. revert a m. + induction n using peano_ind; intros a m. now rewrite add_0_r. + rewrite add_comm, add_succ_l, add_comm, <- add_succ_l. + now rewrite <- IHn, testbit_succ_r_div2, shiftr_succ_r by apply le_0_l. +Qed. + +Lemma shiftl_spec_high a n m : 0<=m -> n<=m -> + testbit (shiftl a n) m = testbit a (m-n). +Proof. + intros _ H. + rewrite <- (sub_add n m H) at 1. + set (m' := m-n). clearbody m'. clear H m. revert a m'. + induction n using peano_ind; intros a m. + rewrite add_0_r; now destruct a. + rewrite shiftl_succ_r. + rewrite add_comm, add_succ_l, add_comm. + now rewrite testbit_succ_r_div2, div2_double by apply le_0_l. +Qed. + +Lemma shiftl_spec_low a n m : m + testbit (shiftl a n) m = false. +Proof. + revert a m. + induction n using peano_ind; intros a m H. + elim (le_0_l m). now rewrite <- compare_antisym, H. + rewrite shiftl_succ_r. + destruct m. now destruct (shiftl a n). + rewrite <- (succ_pos_pred p), testbit_succ_r_div2, div2_double by apply le_0_l. + apply IHn. + apply add_lt_cancel_l with 1. rewrite 2 (add_succ_l 0). simpl. + now rewrite succ_pos_pred. +Qed. + +Definition div2_spec a : div2 a = shiftr a 1. +Proof. + reflexivity. +Qed. + +(** Semantics of bitwise operations *) + +Lemma pos_lxor_spec p p' n : + testbit (Pos.lxor p p') n = xorb (Pos.testbit p n) (Pos.testbit p' n). +Proof. + revert p' n. + induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IH p'); destruct Pos.lxor; trivial; now rewrite <-IH) || + (now destruct Pos.testbit). +Qed. + +Lemma lxor_spec a a' n : + testbit (lxor a a') n = xorb (testbit a n) (testbit a' n). +Proof. + destruct a, a'; simpl; trivial. + now destruct Pos.testbit. + now destruct Pos.testbit. + apply pos_lxor_spec. +Qed. + +Lemma pos_lor_spec p p' n : + Pos.testbit (Pos.lor p p') n = (Pos.testbit p n) || (Pos.testbit p' n). +Proof. + revert p' n. + induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; + apply IH || now rewrite orb_false_r. +Qed. + +Lemma lor_spec a a' n : + testbit (lor a a') n = (testbit a n) || (testbit a' n). +Proof. + destruct a, a'; simpl; trivial. + now rewrite orb_false_r. + apply pos_lor_spec. +Qed. + +Lemma pos_land_spec p p' n : + testbit (Pos.land p p') n = (Pos.testbit p n) && (Pos.testbit p' n). +Proof. + revert p' n. + induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IH p'); destruct Pos.land; trivial; now rewrite <-IH) || + (now rewrite andb_false_r). +Qed. + +Lemma land_spec a a' n : + testbit (land a a') n = (testbit a n) && (testbit a' n). +Proof. + destruct a, a'; simpl; trivial. + now rewrite andb_false_r. + apply pos_land_spec. +Qed. + +Lemma pos_ldiff_spec p p' n : + testbit (Pos.ldiff p p') n = (Pos.testbit p n) && negb (Pos.testbit p' n). +Proof. + revert p' n. + induction p as [p IH|p IH|]; intros [p'|p'|] [|n]; trivial; simpl; + (specialize (IH p'); destruct Pos.ldiff; trivial; now rewrite <-IH) || + (now rewrite andb_true_r). +Qed. + +Lemma ldiff_spec a a' n : + testbit (ldiff a a') n = (testbit a n) && negb (testbit a' n). +Proof. + destruct a, a'; simpl; trivial. + now rewrite andb_true_r. + apply pos_ldiff_spec. +Qed. + +(** Some constants *) + +Definition zero := 0. +Definition one := 1. +Definition two := 2. + +Lemma one_succ : 1 = succ 0. +Proof. reflexivity. Qed. + +Lemma two_succ : 2 = succ 1. +Proof. reflexivity. Qed. + +Definition pred_0 : pred 0 = 0. +Proof. reflexivity. Qed. + +(** Proof of morphisms, obvious since eq is Leibniz *) + +Local Obligation Tactic := simpl_relation. +Program Definition succ_wd : Proper (eq==>eq) succ := _. +Program Definition pred_wd : Proper (eq==>eq) pred := _. +Program Definition add_wd : Proper (eq==>eq==>eq) add := _. +Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _. +Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _. +Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _. +Program Definition div_wd : Proper (eq==>eq==>eq) div := _. +Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _. +Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. +Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. + +(** Generic induction / recursion *) + +Theorem bi_induction : + forall A : N -> Prop, Proper (Logic.eq==>iff) A -> + A N0 -> (forall n, A n <-> A (succ n)) -> forall n : N, A n. +Proof. +intros A A_wd A0 AS. apply peano_rect. assumption. intros; now apply -> AS. +Qed. + +Definition recursion {A} : A -> (N -> A -> A) -> N -> A := + peano_rect (fun _ => A). + +Instance recursion_wd {A} (Aeq : relation A) : + Proper (Aeq==>(Logic.eq==>Aeq==>Aeq)==>Logic.eq==>Aeq) recursion. +Proof. +intros a a' Ea f f' Ef x x' Ex. subst x'. +induction x using peano_ind. +trivial. +unfold recursion in *. rewrite 2 peano_rect_succ. now apply Ef. +Qed. + +Theorem recursion_0 {A} (a:A) (f:N->A->A) : recursion a f 0 = a. +Proof. reflexivity. Qed. + +Theorem recursion_succ {A} (Aeq : relation A) (a : A) (f : N -> A -> A): + Aeq a a -> Proper (Logic.eq==>Aeq==>Aeq) f -> + forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)). +Proof. +unfold recursion; intros a_wd f_wd n. induction n using peano_ind. +rewrite peano_rect_succ. now apply f_wd. +rewrite !peano_rect_succ in *. now apply f_wd. +Qed. + +(** Instantiation of generic properties of natural numbers *) + +Include !NProp + <+ !UsualMinMaxLogicalProperties <+ !UsualMinMaxDecProperties. + +(* TODO : avoir un inlining selectif : t eq zero one two *) + +End N. + +(** Exportation of notations *) + +Infix "+" := N.add : N_scope. +Infix "-" := N.sub : N_scope. +Infix "*" := N.mul : N_scope. +Infix "^" := N.pow : N_scope. + +Infix "?=" := N.compare (at level 70, no associativity) : N_scope. + +Infix "<=" := N.le : N_scope. +Infix "<" := N.lt : N_scope. +Infix ">=" := N.ge : N_scope. +Infix ">" := N.gt : N_scope. + +Notation "x <= y <= z" := (x <= y /\ y <= z) : N_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : N_scope. +Notation "x < y < z" := (x < y /\ y < z) : N_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : N_scope. + +Infix "=?" := N.eqb (at level 70, no associativity) : N_scope. +Infix "<=?" := N.leb (at level 70, no associativity) : N_scope. +Infix " m = p. +Proof (proj1 (N.add_cancel_l m p n)). +Lemma Nmult_Sn_m n m : N.succ n * m = m + n * m. +Proof (eq_trans (N.mul_succ_l n m) (N.add_comm _ _)). +Lemma Nmult_plus_distr_l n m p : p * (n + m) = p * n + p * m. +Proof (N.mul_add_distr_l p n m). +Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m. +Proof (fun H => proj1 (N.mul_cancel_r n m p H)). + +Lemma Ngt_Nlt n m : n > m -> m < n. +Proof. +unfold Ngt, Nlt; intro H. now rewrite <- N.compare_antisym, H. +Qed. + +(** Not kept : Ncompare_n_Sm Nplus_lt_cancel_l *) diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 6bfc323d6..4a5f4ee1d 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -17,11 +17,6 @@ Require Export Nsqrt_def. Require Export Ngcd_def. Require Export Ndigits. Require Export NArithRing. -Require NBinary. - -Module N. - Include NBinary.N. -End N. (** [N] contains an [order] tactic for natural numbers *) diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 94432a7cf..e13d6ac51 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -7,172 +7,38 @@ (************************************************************************) Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat - Pnat Nnat Ndiv_def Compare_dec Lt Minus. + Pnat Nnat Compare_dec Lt Minus. -Local Open Scope positive_scope. - -(** Operation over bits of a [N] number. *) - -(** Logical [or] *) - -Fixpoint Por (p q : positive) : positive := - match p, q with - | 1, q~0 => q~1 - | 1, _ => q - | p~0, 1 => p~1 - | _, 1 => p - | p~0, q~0 => (Por p q)~0 - | p~0, q~1 => (Por p q)~1 - | p~1, q~0 => (Por p q)~1 - | p~1, q~1 => (Por p q)~1 - end. - -Definition Nor n m := - match n, m with - | N0, _ => m - | _, N0 => n - | Npos p, Npos q => Npos (Por p q) - end. - -(** Logical [and] *) - -Fixpoint Pand (p q : positive) : N := - match p, q with - | 1, q~0 => N0 - | 1, _ => Npos 1 - | p~0, 1 => N0 - | _, 1 => Npos 1 - | p~0, q~0 => Ndouble (Pand p q) - | p~0, q~1 => Ndouble (Pand p q) - | p~1, q~0 => Ndouble (Pand p q) - | p~1, q~1 => Ndouble_plus_one (Pand p q) - end. - -Definition Nand n m := - match n, m with - | N0, _ => N0 - | _, N0 => N0 - | Npos p, Npos q => Pand p q - end. - -(** Logical [diff] *) - -Fixpoint Pdiff (p q:positive) : N := - match p, q with - | 1, q~0 => Npos 1 - | 1, _ => N0 - | _~0, 1 => Npos p - | p~1, 1 => Npos (p~0) - | p~0, q~0 => Ndouble (Pdiff p q) - | p~0, q~1 => Ndouble (Pdiff p q) - | p~1, q~1 => Ndouble (Pdiff p q) - | p~1, q~0 => Ndouble_plus_one (Pdiff p q) - end. - -Fixpoint Ndiff n m := - match n, m with - | N0, _ => N0 - | _, N0 => n - | Npos p, Npos q => Pdiff p q - end. - -(** [xor] *) - -Fixpoint Pxor (p q:positive) : N := - match p, q with - | 1, 1 => N0 - | 1, q~0 => Npos (q~1) - | 1, q~1 => Npos (q~0) - | p~0, 1 => Npos (p~1) - | p~0, q~0 => Ndouble (Pxor p q) - | p~0, q~1 => Ndouble_plus_one (Pxor p q) - | p~1, 1 => Npos (p~0) - | p~1, q~0 => Ndouble_plus_one (Pxor p q) - | p~1, q~1 => Ndouble (Pxor p q) - end. - -Definition Nxor (n m:N) := - match n, m with - | N0, _ => m - | _, N0 => n - | Npos p, Npos q => Pxor p q - end. - -(** For proving properties of these operations, we will use - an equivalence with functional streams of bit, cf [eqf] below *) - -(** Shift *) - -Definition Nshiftl_nat (a:N)(n:nat) := iter_nat n _ Ndouble a. - -Definition Nshiftr_nat (a:N)(n:nat) := iter_nat n _ Ndiv2 a. - -Definition Nshiftr a n := - match n with - | N0 => a - | Npos p => iter_pos p _ Ndiv2 a - end. - -Definition Nshiftl a n := - match a, n with - | _, N0 => a - | N0, _ => a - | Npos p, Npos q => Npos (iter_pos q _ xO p) - end. - -(** Checking whether a particular bit is set on not *) - -Fixpoint Pbit (p:positive) : nat -> bool := - match p with - | 1 => fun n => match n with - | O => true - | S _ => false - end - | p~0 => fun n => match n with - | O => false - | S n' => Pbit p n' - end - | p~1 => fun n => 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. - -(** Same, but with index in N *) +Local Open Scope N_scope. -Fixpoint Ptestbit p n := - match p, n with - | p~0, N0 => false - | _, N0 => true - | 1, _ => false - | p~0, _ => Ptestbit p (Npred n) - | p~1, _ => Ptestbit p (Npred n) - end. +(** This file is mostly obsolete, see directly [BinNat] now. *) -Definition Ntestbit a n := - match a with - | N0 => false - | Npos p => Ptestbit p n - end. +(** Operation over bits of a [N] number. *) -Local Close Scope positive_scope. -Local Open Scope N_scope. +Notation Por := Pos.lor (only parsing). +Notation Nor := N.lor (only parsing). +Notation Pand := Pos.land (only parsing). +Notation Nand := N.land (only parsing). +Notation Pdiff := Pos.ldiff (only parsing). +Notation Ndiff := N.ldiff (only parsing). +Notation Pxor := Pos.lxor (only parsing). +Notation Nxor := N.lxor (only parsing). +Notation Nshiftl_nat := N.shiftl_nat (only parsing). +Notation Nshiftr_nat := N.shiftr_nat (only parsing). +Notation Nshiftl := N.shiftl (only parsing). +Notation Nshiftr := N.shiftr (only parsing). +Notation Pbit := Pos.testbit_nat (only parsing). +Notation Nbit := N.testbit_nat (only parsing). +Notation Ptestbit := Pos.testbit (only parsing). +Notation Ntestbit := N.testbit (only parsing). (** Equivalence of Pbit and Ptestbit *) Lemma Ptestbit_Pbit : forall p n, Ptestbit p (N_of_nat n) = Pbit p n. Proof. - induction p as [p IH|p IH| ]; intros n; simpl. - rewrite <- N_of_pred, IH; destruct n; trivial. - rewrite <- N_of_pred, IH; destruct n; trivial. - destruct n; trivial. + induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial; + rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred. Qed. Lemma Ntestbit_Nbit : forall a n, Ntestbit a (N_of_nat n) = Nbit a n. @@ -192,32 +58,6 @@ Proof. destruct a. trivial. apply Pbit_Ptestbit. Qed. -(** Correctness proofs for [Ntestbit]. *) - -Lemma Ntestbit_odd_0 a : Ntestbit (2*a+1) 0 = true. -Proof. - now destruct a. -Qed. - -Lemma Ntestbit_even_0 a : Ntestbit (2*a) 0 = false. -Proof. - now destruct a. -Qed. - -Lemma Ntestbit_odd_succ a n : - Ntestbit (2*a+1) (Nsucc n) = Ntestbit a n. -Proof. - destruct a. simpl. now destruct n. - simpl. rewrite Npred_succ. now destruct n. -Qed. - -Lemma Ntestbit_even_succ a n : - Ntestbit (2*a) (Nsucc n) = Ntestbit a n. -Proof. - destruct a. trivial. - simpl. rewrite Npred_succ. now destruct n. -Qed. - (** Equivalence of shifts, N and nat versions *) Lemma Nshiftr_nat_S : forall a n, @@ -260,7 +100,7 @@ Proof. intros. now rewrite <- Nshiftl_nat_equiv, nat_of_N_of_nat. Qed. -(** Correctness proofs for shifts *) +(** Correctness proofs for shifts, nat version *) Lemma Nshiftr_nat_spec : forall a n m, Nbit (Nshiftr_nat a n) m = Nbit a (m+n). @@ -271,14 +111,6 @@ Proof. destruct (Nshiftr_nat a n) as [|[p|p|]]; simpl; trivial. Qed. -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. - Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> Nbit (Nshiftl_nat a n) m = Nbit a (m-n). Proof. @@ -289,15 +121,6 @@ Proof. destruct (Nshiftl_nat a n) as [|[p|p|]]; simpl; trivial. Qed. -Lemma Nshiftl_spec_high : forall a n m, n<=m -> - Ntestbit (Nshiftl a n) m = Ntestbit a (m-n). -Proof. - 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. - Lemma Nshiftl_nat_spec_low : forall a n m, (m Nbit (Nshiftl_nat a n) m = false. Proof. @@ -309,18 +132,9 @@ Proof. destruct (Nshiftl_nat a n); trivial. Qed. -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. - (** A left shift for positive numbers (used in BigN) *) -Definition Pshiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p. +Notation Pshiftl_nat := Pos.shiftl_nat (only parsing). Lemma Pshiftl_nat_0 : forall p, Pshiftl_nat p 0 = p. Proof. reflexivity. Qed. @@ -343,7 +157,7 @@ Proof. rewrite 2 Pshiftl_nat_S. now f_equal. Qed. -(** Semantics of bitwise operations *) +(** Semantics of bitwise operations with respect to [Nbit] *) Lemma Pxor_semantics : forall p p' n, Nbit (Pxor p p') n = xorb (Pbit p n) (Pbit p' n). @@ -362,12 +176,6 @@ Proof. apply Pxor_semantics. Qed. -Lemma Nxor_spec : forall a a' n, - Ntestbit (Nxor a a') n = xorb (Ntestbit a n) (Ntestbit a' n). -Proof. - intros. rewrite <- !Nbit_Ntestbit. apply Nxor_semantics. -Qed. - Lemma Por_semantics : forall p p' n, Pbit (Por p p') n = (Pbit p n) || (Pbit p' n). Proof. @@ -383,12 +191,6 @@ Proof. apply Por_semantics. Qed. -Lemma Nor_spec : forall a a' n, - Ntestbit (Nor a a') n = (Ntestbit a n) || (Ntestbit a' n). -Proof. - intros. rewrite <- !Nbit_Ntestbit. apply Nor_semantics. -Qed. - Lemma Pand_semantics : forall p p' n, Nbit (Pand p p') n = (Pbit p n) && (Pbit p' n). Proof. @@ -405,12 +207,6 @@ Proof. apply Pand_semantics. Qed. -Lemma Nand_spec : forall a a' n, - Ntestbit (Nand a a') n = (Ntestbit a n) && (Ntestbit a' n). -Proof. - intros. rewrite <- !Nbit_Ntestbit. apply Nand_semantics. -Qed. - Lemma Pdiff_semantics : forall p p' n, Nbit (Pdiff p p') n = (Pbit p n) && negb (Pbit p' n). Proof. @@ -427,12 +223,6 @@ Proof. apply Pdiff_semantics. Qed. -Lemma Ndiff_spec : forall a a' n, - Ntestbit (Ndiff a a') n = (Ntestbit a n) && negb (Ntestbit a' n). -Proof. - intros. rewrite <- !Nbit_Ntestbit. apply Ndiff_semantics. -Qed. - (** Equality over functional streams of bits *) @@ -484,162 +274,67 @@ Ltac bitwise_semantics := (** Now, we can easily deduce properties of [Nxor] and others from properties of [xorb] and others. *) -Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'. -Proof. - intros a a' H. bitwise_semantics. apply xorb_eq. - now rewrite <- Nxor_semantics, H. -Qed. +Definition Nxor_eq : forall a a', Nxor a a' = 0 -> a = a' := N.lxor_eq. +Definition Nxor_nilpotent : forall a, Nxor a a = 0 := N.lxor_nilpotent. +Definition Nxor_0_l : forall n, Nxor 0 n = n := N.lxor_0_l. +Definition Nxor_0_r : forall n, Nxor n 0 = n := N.lxor_0_r. -Lemma Nxor_nilpotent : forall a, Nxor a a = 0. -Proof. - intros. bitwise_semantics. apply xorb_nilpotent. -Qed. - -Lemma Nxor_0_l : forall n, Nxor 0 n = n. -Proof. - trivial. -Qed. Notation Nxor_neutral_left := Nxor_0_l (only parsing). - -Lemma Nxor_0_r : forall n, Nxor n 0 = n. -Proof. - destruct n; trivial. -Qed. Notation Nxor_neutral_right := Nxor_0_r (only parsing). -Lemma Nxor_comm : forall a a', Nxor a a' = Nxor a' a. -Proof. - intros. bitwise_semantics. apply xorb_comm. -Qed. - -Lemma Nxor_assoc : - forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a''). -Proof. - intros. bitwise_semantics. apply xorb_assoc. -Qed. - -Lemma Nor_0_l : forall n, Nor 0 n = n. -Proof. - trivial. -Qed. - -Lemma Nor_0_r : forall n, Nor n 0 = n. -Proof. - destruct n; trivial. -Qed. - -Lemma Nor_comm : forall a a', Nor a a' = Nor a' a. -Proof. - intros. bitwise_semantics. apply orb_comm. -Qed. - -Lemma Nor_assoc : - forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''. -Proof. - intros. bitwise_semantics. apply orb_assoc. -Qed. - -Lemma Nor_diag : forall a, Nor a a = a. -Proof. - intros. bitwise_semantics. apply orb_diag. -Qed. - -Lemma Nand_0_l : forall n, Nand 0 n = 0. -Proof. - trivial. -Qed. - -Lemma Nand_0_r : forall n, Nand n 0 = 0. -Proof. - destruct n; trivial. -Qed. - -Lemma Nand_comm : forall a a', Nand a a' = Nand a' a. -Proof. - intros. bitwise_semantics. apply andb_comm. -Qed. - -Lemma Nand_assoc : - forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''. -Proof. - intros. bitwise_semantics. apply andb_assoc. -Qed. - -Lemma Nand_diag : forall a, Nand a a = a. -Proof. - intros. bitwise_semantics. apply andb_diag. -Qed. - -Lemma Ndiff_0_l : forall n, Ndiff 0 n = 0. -Proof. - trivial. -Qed. - -Lemma Ndiff_0_r : forall n, Ndiff n 0 = n. -Proof. - destruct n; trivial. -Qed. - -Lemma Ndiff_diag : forall a, Ndiff a a = 0. -Proof. - intros. bitwise_semantics. apply andb_negb_r. -Qed. - -Lemma Nor_and_distr_l : forall a b c, - Nor (Nand a b) c = Nand (Nor a c) (Nor b c). -Proof. - intros. bitwise_semantics. apply orb_andb_distrib_l. -Qed. - -Lemma Nor_and_distr_r : forall a b c, - Nor a (Nand b c) = Nand (Nor a b) (Nor a c). -Proof. - intros. bitwise_semantics. apply orb_andb_distrib_r. -Qed. - -Lemma Nand_or_distr_l : forall a b c, - Nand (Nor a b) c = Nor (Nand a c) (Nand b c). -Proof. - intros. bitwise_semantics. apply andb_orb_distrib_l. -Qed. - -Lemma Nand_or_distr_r : forall a b c, - Nand a (Nor b c) = Nor (Nand a b) (Nand a c). -Proof. - intros. bitwise_semantics. apply andb_orb_distrib_r. -Qed. - -Lemma Ndiff_diff_l : forall a b c, - Ndiff (Ndiff a b) c = Ndiff a (Nor b c). -Proof. - intros. bitwise_semantics. now rewrite negb_orb, andb_assoc. -Qed. - -Lemma Nor_diff_and : forall a b, - Nor (Ndiff a b) (Nand a b) = a. -Proof. - intros. bitwise_semantics. - now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r. -Qed. - -Lemma Nand_diff : forall a b, - Nand (Ndiff a b) b = 0. -Proof. - intros. bitwise_semantics. - now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r. -Qed. +Definition Nxor_comm : forall a a', Nxor a a' = Nxor a' a := N.lxor_comm. + +Definition Nxor_assoc : + forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'') + := N.lxor_assoc. + +Definition Nor_0_l : forall n, Nor 0 n = n := N.lor_0_l. +Definition Nor_0_r : forall n, Nor n 0 = n := N.lor_0_r. +Definition Nor_comm : forall a a', Nor a a' = Nor a' a := N.lor_comm. +Definition Nor_assoc : + forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a'' + := N.lor_assoc. +Definition Nor_diag : forall a, Nor a a = a := N.lor_diag. + +Definition Nand_0_l : forall n, Nand 0 n = 0 := N.land_0_l. +Definition Nand_0_r : forall n, Nand n 0 = 0 := N.land_0_r. +Definition Nand_comm : forall a a', Nand a a' = Nand a' a := N.land_comm. +Definition Nand_assoc : + forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a'' + := N.land_assoc. +Definition Nand_diag : forall a, Nand a a = a := N.land_diag. + +Definition Ndiff_0_l : forall n, Ndiff 0 n = 0 := N.ldiff_0_l. +Definition Ndiff_0_r : forall n, Ndiff n 0 = n := N.ldiff_0_r. +Definition Ndiff_diag : forall a, Ndiff a a = 0 := N.ldiff_diag. +Definition Nor_and_distr_l : forall a b c, + Nor (Nand a b) c = Nand (Nor a c) (Nor b c) + := N.lor_land_distr_l. +Definition Nor_and_distr_r : forall a b c, + Nor a (Nand b c) = Nand (Nor a b) (Nor a c) + := N.lor_land_distr_r. +Definition Nand_or_distr_l : forall a b c, + Nand (Nor a b) c = Nor (Nand a c) (Nand b c) + := N.land_lor_distr_l. +Definition Nand_or_distr_r : forall a b c, + Nand a (Nor b c) = Nor (Nand a b) (Nand a c) + := N.land_lor_distr_r. +Definition Ndiff_diff_l : forall a b c, + Ndiff (Ndiff a b) c = Ndiff a (Nor b c) + := N.ldiff_ldiff_l. +Definition Nor_diff_and : forall a b, + Nor (Ndiff a b) (Nand a b) = a + := N.lor_ldiff_and. +Definition Nand_diff : forall a b, + Nand (Ndiff a b) b = 0 + := N.land_ldiff. Local Close Scope N_scope. (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Definition Nbit0 (n:N) := - match n with - | N0 => false - | Npos (_~0) => false - | _ => true - end. +Notation Nbit0 := N.odd (only parsing). Definition Nodd (n:N) := Nbit0 n = true. Definition Neven (n:N) := Nbit0 n = false. @@ -885,11 +580,7 @@ Qed. (** Number of digits in a number *) -Definition Nsize (n:N) : nat := match n with - | N0 => O - | Npos p => Psize p - end. - +Notation Nsize := N.size_nat (only parsing). (** conversions between N and bit vectors. *) diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 0850a631e..559f01f16 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -6,155 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -Require Import BinPos BinNat. - +Require Import BinNat. Local Open Scope N_scope. -Definition NPgeb (a:N)(b:positive) := - match a with - | 0 => false - | Npos na => match Pos.compare na b with Lt => false | _ => true end - end. - -Local Notation "a >=? b" := (NPgeb a b) (at level 70). - -Fixpoint Pdiv_eucl (a b:positive) : N * N := - match a with - | xH => - match b with xH => (1, 0) | _ => (0, 1) end - | xO a' => - let (q, r) := Pdiv_eucl a' b in - let r' := 2 * r in - if r' >=? b then (2 * q + 1, r' - Npos b) - else (2 * q, r') - | xI a' => - let (q, r) := Pdiv_eucl a' b in - let r' := 2 * r + 1 in - if r' >=? b then (2 * q + 1, r' - Npos b) - else (2 * q, r') - end. - -Definition Ndiv_eucl (a b:N) : N * N := - match a, b with - | 0, _ => (0, 0) - | _, 0 => (0, a) - | Npos na, Npos nb => Pdiv_eucl na nb - end. - -Definition Ndiv a b := fst (Ndiv_eucl a b). -Definition Nmod a b := snd (Ndiv_eucl a b). - -Infix "/" := Ndiv : N_scope. -Infix "mod" := Nmod (at level 40, no associativity) : N_scope. - -(** Auxiliary Results about [NPgeb] *) +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) -Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b. -Proof. - destruct a; simpl; intros. - discriminate. - unfold Nge, Ncompare. now destruct Pos.compare. -Qed. +Definition Pdiv_eucl a b := N.pos_div_eucl a (Npos b). -Lemma NPgeb_lt : forall a b, NPgeb a b = false -> a < Npos b. -Proof. - destruct a; simpl; intros. red; auto. - unfold Nlt, Ncompare. now destruct Pos.compare. -Qed. +Definition Pdiv_eucl_correct a b : + let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r + := N.pos_div_eucl_spec a (Npos b). -Theorem NPgeb_correct: forall (a:N)(b:positive), - if NPgeb a b then a = a - Npos b + Npos b else True. -Proof. - destruct a as [|a]; simpl; intros b; auto. - case Pos.compare_spec; intros; subst; auto. - now rewrite Pminus_mask_diag. - destruct (Pminus_mask_Gt a b (Pos.lt_gt _ _ H)) as [d [H2 [H3 _]]]. - rewrite H2. rewrite <- H3. - simpl; f_equal; apply Pplus_comm. -Qed. - -Lemma NPgeb_ineq0 : forall a p, a < Npos p -> NPgeb (2*a) p = true -> - 2*a - Npos p < Npos p. -Proof. -intros a p LT GE. -apply Nplus_lt_cancel_l with (Npos p). -rewrite Nplus_comm. -generalize (NPgeb_correct (2*a) p). rewrite GE. intros <-. -rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r. -destruct a; auto. -Qed. - -Lemma NPgeb_ineq1 : forall a p, a < Npos p -> NPgeb (2*a+1) p = true -> - (2*a+1) - Npos p < Npos p. -Proof. -intros a p LT GE. -apply Nplus_lt_cancel_l with (Npos p). -rewrite Nplus_comm. -generalize (NPgeb_correct (2*a+1) p). rewrite GE. intros <-. -rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r. -destruct a; auto. -red; simpl. apply Pcompare_Gt_Lt; auto. -Qed. - -(* Proofs of specifications for these euclidean divisions. *) - -Theorem Pdiv_eucl_correct: forall a b, - let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + r. -Proof. - induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hq1. - assert (Npos a~1 = 2*q1*Npos b + (2*r1+1)) - by now rewrite Nplus_assoc, <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1. - generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H'; auto. - rewrite Nmult_plus_distr_r, Nmult_1_l. - rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hq1. - assert (Npos a~0 = 2*q1*Npos b + 2*r1) - by now rewrite <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1. - generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H'; auto. - rewrite Nmult_plus_distr_r, Nmult_1_l. - rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto. - destruct b; auto. -Qed. - -Theorem Ndiv_eucl_correct: forall a b, - let (q,r) := Ndiv_eucl a b in a = b * q + r. -Proof. - destruct a as [|a]; destruct b as [|b]; simpl; auto. - generalize (Pdiv_eucl_correct a b); case Pdiv_eucl; intros q r. - destruct q. simpl; auto. rewrite Nmult_comm. intro EQ; exact EQ. -Qed. - -Theorem Ndiv_mod_eq : forall a b, - a = b * (a/b) + (a mod b). -Proof. - intros; generalize (Ndiv_eucl_correct a b). - unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl; auto. -Qed. - -Theorem Pdiv_eucl_remainder : forall a b:positive, +Lemma Pdiv_eucl_remainder a b : snd (Pdiv_eucl a b) < Npos b. -Proof. - induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hr1; simpl in Hr1. - case_eq (NPgeb (2*r1+1) b); intros; unfold snd. - apply NPgeb_ineq1; auto. - apply NPgeb_lt; auto. - intros b; generalize (IHa b); case Pdiv_eucl. - intros q1 r1 Hr1; simpl in Hr1. - case_eq (NPgeb (2*r1) b); intros; unfold snd. - apply NPgeb_ineq0; auto. - apply NPgeb_lt; auto. - destruct b; simpl; reflexivity. -Qed. +Proof. now apply (N.pos_div_eucl_remainder a (Npos b)). Qed. + +Notation Ndiv_eucl := N.div_eucl (only parsing). +Notation Ndiv := N.div (only parsing). +Notation Nmod := N.modulo (only parsing). -Theorem Nmod_lt : forall (a b:N), b<>0 -> a mod b < b. -Proof. - destruct b as [ |b]; intro H; try solve [elim H;auto]. - destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl. - generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; auto. -Qed. +Notation Ndiv_eucl_correct := N.div_eucl_spec (only parsing). +Notation Ndiv_mod_eq := N.div_mod' (only parsing). +Notation Nmod_lt := N.mod_lt (only parsing). diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index c25af8717..13211f467 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -7,79 +7,16 @@ (************************************************************************) Require Import BinPos BinNat. - Local Open Scope N_scope. -(** * Divisibility *) - -Definition Ndivide p q := exists r, p*r = q. -Notation "( p | q )" := (Ndivide p q) (at level 0) : N_scope. - -(** * Definition of a Pgcd function for binary natural numbers *) - -Definition Ngcd (a b : N) := - match a, b with - | 0, _ => b - | _, 0 => a - | Npos p, Npos q => Npos (Pos.gcd p q) - end. - -(** * Generalized Gcd, also computing rests of a and b after - division by gcd. *) - -Definition Nggcd (a b : N) := - match a, b with - | 0, _ => (b,(0,1)) - | _, 0 => (a,(1,0)) - | Npos p, Npos q => - let '(g,(aa,bb)) := Pos.ggcd p q in - (Npos g, (Npos aa, Npos bb)) - end. - -(** The first component of Nggcd is Ngcd *) - -Lemma Nggcd_gcd : forall a b, fst (Nggcd a b) = Ngcd a b. -Proof. - intros [ |p] [ |q]; simpl; auto. - generalize (Pos.ggcd_gcd p q). destruct Pos.ggcd as (g,(aa,bb)); simpl; congruence. -Qed. - -(** The other components of Nggcd are indeed the correct factors. *) - -Lemma Nggcd_correct_divisors : forall a b, - let '(g,(aa,bb)) := Nggcd a b in - a=g*aa /\ b=g*bb. -Proof. - intros [ |p] [ |q]; simpl; auto. - now rewrite Pmult_1_r. - now rewrite Pmult_1_r. - generalize (Pos.ggcd_correct_divisors p q). - destruct Pos.ggcd as (g,(aa,bb)); simpl. destruct 1; split; congruence. -Qed. - -(** We can use this fact to prove a part of the gcd correctness *) - -Lemma Ngcd_divide_l : forall a b, (Ngcd a b | a). -Proof. - intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b). - destruct Nggcd as (g,(aa,bb)); simpl. intros (H,_). exists aa; auto. -Qed. - -Lemma Ngcd_divide_r : forall a b, (Ngcd a b | b). -Proof. - intros a b. rewrite <- Nggcd_gcd. generalize (Nggcd_correct_divisors a b). - destruct Nggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb; auto. -Qed. - -(** We now prove directly that gcd is the greatest amongst common divisors *) - -Lemma Ngcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|Ngcd a b). -Proof. - intros [ |p] [ |q]; simpl; auto. - intros [ |r]. intros (s,H). discriminate. - intros ([ |s],Hs) ([ |t],Ht); try discriminate; simpl in *. - destruct (Pos.gcd_greatest p q r) as (u,H). - exists s. now inversion Hs. - exists t. now inversion Ht. - exists (Npos u). simpl; now f_equal. -Qed. +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) + +Notation Ndivide := N.divide (only parsing). +Notation Ngcd := N.gcd (only parsing). +Notation Nggcd := N.ggcd (only parsing). +Notation Nggcd_gcd := N.ggcd_gcd (only parsing). +Notation Nggcd_correct_divisors := N.ggcd_correct_divisors (only parsing). +Notation Ngcd_divide_l := N.gcd_divide_l (only parsing). +Notation Ngcd_divide_r := N.gcd_divide_r (only parsing). +Notation Ngcd_greatest := N.gcd_greatest (only parsing). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 375ed0f90..edb6b2895 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -6,45 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Definition of a square root function for N. *) +Require Import BinNat. -Require Import BinPos BinNat. +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) -Local Open Scope N_scope. - -Definition Nsqrtrem n := - match n with - | N0 => (N0, N0) - | Npos p => - match Pos.sqrtrem p with - | (s, IsPos r) => (Npos s, Npos r) - | (s, _) => (Npos s, N0) - end - end. - -Definition Nsqrt n := - match n with - | N0 => N0 - | Npos p => Npos (Pos.sqrt p) - end. - -Lemma Nsqrtrem_spec : forall n, - let (s,r) := Nsqrtrem n in n = s*s + r /\ r <= 2*s. -Proof. - destruct n. now split. - generalize (Pos.sqrtrem_spec p). simpl. - destruct 1; simpl; subst; now split. -Qed. - -Lemma Nsqrt_spec : forall n, - let s := Nsqrt n in s*s <= n < (Nsucc s)*(Nsucc s). -Proof. - destruct n. now split. apply (Pos.sqrt_spec p). -Qed. - -Lemma Nsqrtrem_sqrt : forall n, fst (Nsqrtrem n) = Nsqrt n. -Proof. - destruct n. reflexivity. - unfold Nsqrtrem, Nsqrt, Pos.sqrt. - destruct (Pos.sqrtrem p) as (s,r). now destruct r. -Qed. \ No newline at end of file +Notation Nsqrtrem := N.sqrtrem (only parsing). +Notation Nsqrt := N.sqrt (only parsing). +Notation Nsqrtrem_spec := N.sqrtrem_spec (only parsing). +Notation Nsqrt_spec := (fun n => N.sqrt_spec n (N.le_0_l n)) (only parsing). +Notation Nsqrtrem_sqrt := N.sqrtrem_sqrt (only parsing). -- cgit v1.2.3