diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 1235 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 381 | ||||
| -rw-r--r-- | theories/NArith/BinPos.v | 1172 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 23 | ||||
| -rw-r--r-- | theories/NArith/NOrderedType.v | 60 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 12 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 517 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 8 | ||||
| -rw-r--r-- | theories/NArith/Ndiv_def.v | 31 | ||||
| -rw-r--r-- | theories/NArith/Ngcd_def.v | 22 | ||||
| -rw-r--r-- | theories/NArith/Nminmax.v | 126 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 450 | ||||
| -rw-r--r-- | theories/NArith/Nsqrt_def.v | 18 | ||||
| -rw-r--r-- | theories/NArith/POrderedType.v | 60 | ||||
| -rw-r--r-- | theories/NArith/Pminmax.v | 126 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 462 | ||||
| -rw-r--r-- | theories/NArith/intro.tex | 2 | ||||
| -rw-r--r-- | theories/NArith/vo.itarget | 10 |
18 files changed, 1789 insertions, 2926 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 8695acca..30e35f50 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1,500 +1,1123 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: BinNat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import BinPos. -Unset Boxed Definitions. +Require Export BinNums. +Require Import BinPos RelationClasses Morphisms Setoid + Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties. +Require BinNatDef. (**********************************************************************) -(** Binary natural numbers *) +(** * Binary natural numbers, operations and properties *) +(**********************************************************************) -Inductive N : Set := - | N0 : N - | Npos : positive -> N. +(** The type [N] and its constructors [N0] and [Npos] are now + defined in [BinNums.v] *) -(** Declare binding key for scope positive_scope *) +(** Every definitions and properties about binary natural numbers + are placed in a module [N] for qualification purpose. *) -Delimit Scope N_scope with N. +Local Open Scope N_scope. -(** Automatically open scope positive_scope for the constructors of N *) +(** Every definitions and early properties about positive numbers + are placed in a module [N] for qualification purpose. *) -Bind Scope N_scope with N. -Arguments Scope Npos [positive_scope]. +Module N + <: NAxiomsSig + <: UsualOrderedTypeFull + <: UsualDecidableTypeFull + <: TotalOrder. -Open Local Scope N_scope. +(** Definitions of operations, now in a separate file *) -Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. -Proof. - destruct n; auto. - left; exists p; auto. -Defined. +Include BinNatDef.N. -(** Operation x -> 2*x+1 *) +(** When including property functors, only inline t eq zero one two *) -Definition Ndouble_plus_one x := - match x with - | N0 => Npos 1 - | Npos p => Npos (xI p) - end. +Set Inline Level 30. -(** Operation x -> 2*x *) +(** Logical predicates *) -Definition Ndouble n := - match n with - | N0 => N0 - | Npos p => Npos (xO p) - end. +Definition eq := @Logic.eq N. +Definition eq_equiv := @eq_equivalence N. -(** Successor *) +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. -Definition Nsucc n := - match n with - | N0 => Npos 1 - | Npos p => Npos (Psucc p) - end. +Infix "<=" := le : N_scope. +Infix "<" := lt : N_scope. +Infix ">=" := ge : N_scope. +Infix ">" := gt : N_scope. -(** Predecessor *) +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. -Definition Npred (n : N) := match n with -| N0 => N0 -| Npos p => match p with - | xH => N0 - | _ => Npos (Ppred p) - end -end. +Definition divide p q := exists r, q = r*p. +Notation "( p | q )" := (divide p q) (at level 0) : N_scope. -(** Addition *) +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. -Definition Nplus n m := - match n, m with - | N0, _ => m - | _, N0 => n - | Npos p, Npos q => Npos (p + q) - end. +(** Decidability of equality. *) -Infix "+" := Nplus : N_scope. +Definition eq_dec : forall n m : N, { n = m } + { n <> m }. +Proof. + decide equality. + apply Pos.eq_dec. +Defined. -(** Subtraction *) +(** Discrimination principle *) -Definition Nminus (n m : N) := -match n, m with -| N0, _ => N0 -| n, N0 => n -| Npos n', Npos m' => - match Pminus_mask n' m' with - | IsPos p => Npos p - | _ => N0 - end -end. +Definition discr n : { p:positive | n = Npos p } + { n = N0 }. +Proof. + destruct n; auto. + left; exists p; auto. +Defined. -Infix "-" := Nminus : N_scope. +(** Convenient induction principles *) + +Definition binary_rect (P:N -> Type) (f0 : P 0) + (f2 : forall n, P n -> P (double n)) + (fS2 : forall n, P n -> P (succ_double n)) (n : N) : P n := + let P' p := P (Npos p) in + let f2' p := f2 (Npos p) in + let fS2' p := fS2 (Npos p) in + match n with + | 0 => f0 + | Npos p => positive_rect P' fS2' f2' (fS2 0 f0) p + end. -(** Multiplication *) +Definition binary_rec (P:N -> Set) := binary_rect P. +Definition binary_ind (P:N -> Prop) := binary_rect P. -Definition Nmult n m := - match n, m with - | N0, _ => N0 - | _, N0 => N0 - | Npos p, Npos q => Npos (p * q) - end. +(** Peano induction on binary natural numbers *) -Infix "*" := Nmult : N_scope. +Definition peano_rect + (P : N -> Type) (f0 : P 0) + (f : forall n : N, P n -> P (succ n)) (n : N) : P n := +let P' p := P (Npos p) in +let f' p := f (Npos p) in +match n with +| 0 => f0 +| Npos p => Pos.peano_rect P' (f 0 f0) f' p +end. -(** Boolean Equality *) +Theorem peano_rect_base P a f : peano_rect P a f 0 = a. +Proof. +reflexivity. +Qed. -Definition Neqb n m := - match n, m with - | N0, N0 => true - | Npos n, Npos m => Peqb n m - | _,_ => false - end. +Theorem peano_rect_succ P a f n : + peano_rect P a f (succ n) = f n (peano_rect P a f n). +Proof. +destruct n; simpl. +trivial. +now rewrite Pos.peano_rect_succ. +Qed. -(** Order *) +Definition peano_ind (P : N -> Prop) := peano_rect P. -Definition Ncompare n m := - match n, m with - | N0, N0 => Eq - | N0, Npos m' => Lt - | Npos n', N0 => Gt - | Npos n', Npos m' => (n' ?= m')%positive Eq - end. +Definition peano_rec (P : N -> Set) := peano_rect P. -Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. +Theorem peano_rec_base P a f : peano_rec P a f 0 = a. +Proof. +apply peano_rect_base. +Qed. -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. +Theorem peano_rec_succ P a f n : + peano_rec P a f (succ n) = f n (peano_rec P a f n). +Proof. +apply peano_rect_succ. +Qed. -Infix "<=" := Nle : N_scope. -Infix "<" := Nlt : N_scope. -Infix ">=" := Nge : N_scope. -Infix ">" := Ngt : N_scope. +(** Properties of mixed successor and predecessor. *) -(** Min and max *) +Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p). +Proof. + now destruct p. +Qed. -Definition Nmin (n n' : N) := match Ncompare n n' with - | Lt | Eq => n - | Gt => n' - end. +Lemma succ_pos_spec n : Npos (succ_pos n) = succ n. +Proof. + now destruct n. +Qed. -Definition Nmax (n n' : N) := match Ncompare n n' with - | Lt | Eq => n' - | Gt => n - end. +Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n. +Proof. + destruct n. trivial. apply Pos.pred_N_succ. +Qed. -(** Decidability of equality. *) +Lemma succ_pos_pred p : succ (Pos.pred_N p) = Npos p. +Proof. + destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double. +Qed. + +(** Properties of successor and predecessor *) -Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }. +Theorem pred_succ n : pred (succ n) = n. Proof. - decide equality. - apply positive_eq_dec. -Defined. +destruct n; trivial. simpl. apply Pos.pred_N_succ. +Qed. -(** convenient induction principles *) +Theorem pred_sub n : pred n = sub n 1. +Proof. + now destruct n as [|[p|p|]]. +Qed. -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. +Theorem succ_0_discr n : succ n <> 0. 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. +now destruct n. 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. +(** Specification of addition *) + +Theorem add_0_l n : 0 + n = n. 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. +reflexivity. Qed. -(** Peano induction on binary natural numbers *) +Theorem add_succ_l n m : succ n + m = succ (n + m). +Proof. +destruct n, m; unfold succ, add; now rewrite ?Pos.add_1_l, ?Pos.add_succ_l. +Qed. -Definition Nrect - (P : N -> Type) (a : P N0) - (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n := -let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in -let P' (p : positive) := P (Npos p) in -match n return (P n) with -| N0 => a -| Npos p => Prect P' (f N0 a) f' p -end. +(** Specification of subtraction. *) -Theorem Nrect_base : forall P a f, Nrect P a f N0 = a. +Theorem sub_0_r n : n - 0 = n. Proof. -intros P a f; simpl; reflexivity. +now destruct n. Qed. -Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n). +Theorem sub_succ_r n m : n - succ m = pred (n - m). Proof. -intros P a f; destruct n as [| p]; simpl; -[rewrite Prect_base | rewrite Prect_succ]; reflexivity. +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. -Definition Nind (P : N -> Prop) := Nrect P. +(** Specification of multiplication *) -Definition Nrec (P : N -> Set) := Nrect P. +Theorem mul_0_l n : 0 * n = 0. +Proof. +reflexivity. +Qed. -Theorem Nrec_base : forall P a f, Nrec P a f N0 = a. +Theorem mul_succ_l n m : (succ n) * m = n * m + m. Proof. -intros P a f; unfold Nrec; apply Nrect_base. +destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm. +apply Pos.mul_succ_l. Qed. -Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n). +(** Specification of boolean comparisons. *) + +Lemma eqb_eq n m : eqb n m = true <-> n=m. Proof. -intros P a f; unfold Nrec; apply Nrect_step. +destruct n as [|n], m as [|m]; simpl; try easy'. +rewrite Pos.eqb_eq. split; intro H. now subst. now destr_eq H. Qed. -(** Properties of successor and predecessor *) +Lemma ltb_lt n m : (n <? m) = true <-> n < m. +Proof. + unfold ltb, lt. destruct compare; easy'. +Qed. -Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n. +Lemma leb_le n m : (n <=? m) = true <-> n <= m. Proof. -destruct n as [| 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. + unfold leb, le. destruct compare; easy'. Qed. -(** Properties of addition *) +(** Basic properties of comparison *) + +Theorem compare_eq_iff n m : (n ?= m) = Eq <-> n = m. +Proof. +destruct n, m; simpl; rewrite ?Pos.compare_eq_iff; split; congruence. +Qed. -Theorem Nplus_0_l : forall n:N, N0 + n = n. +Theorem compare_lt_iff n m : (n ?= m) = Lt <-> n < m. Proof. reflexivity. Qed. -Theorem Nplus_0_r : forall n:N, n + N0 = n. +Theorem compare_le_iff n m : (n ?= m) <> Gt <-> n <= m. Proof. -destruct n; reflexivity. +reflexivity. Qed. -Theorem Nplus_comm : forall n m:N, n + m = m + n. +Theorem compare_antisym n m : (m ?= n) = CompOpp (n ?= m). Proof. -intros. -destruct n; destruct m; simpl in |- *; try reflexivity. -rewrite Pplus_comm; reflexivity. +destruct n, m; simpl; trivial. apply Pos.compare_antisym. +Qed. + +(** Some more advanced properties of comparison and orders, + including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *) + +Include BoolOrderFacts. + +(** We regroup here some results used for proving the correctness + of more advanced functions. These results will also be provided + by the generic functor of properties about natural numbers + instantiated at the end of the file. *) + +Module Import Private_BootStrap. + +Theorem add_0_r n : n + 0 = n. +Proof. +now destruct n. Qed. -Theorem Nplus_assoc : forall n m p:N, n + (m + p) = n + m + p. +Theorem add_comm n m : n + m = m + n. +Proof. +destruct n, m; simpl; try reflexivity. simpl. f_equal. apply Pos.add_comm. +Qed. + +Theorem add_assoc n m p : n + (m + p) = n + m + p. Proof. -intros. destruct n; try reflexivity. destruct m; try reflexivity. destruct p; try reflexivity. -simpl in |- *; rewrite Pplus_assoc; reflexivity. +simpl. f_equal. apply Pos.add_assoc. +Qed. + +Lemma sub_add n m : n <= m -> m - n + n = m. +Proof. + destruct n as [|p], m as [|q]; simpl; try easy'. intros H. + case Pos.sub_mask_spec; intros; simpl; subst; trivial. + now rewrite Pos.add_comm. + apply Pos.le_nlt in H. elim H. apply Pos.lt_add_r. +Qed. + +Theorem mul_comm n m : n * m = m * n. +Proof. +destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm. +Qed. + +Lemma le_0_l n : 0<=n. +Proof. +now destruct n. +Qed. + +Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m). +Proof. + unfold le, lt, leb. rewrite (compare_antisym n m). + case compare; now constructor. +Qed. + +Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m. +Proof. + intro H. destruct p. simpl; auto. + destruct n; destruct m. + elim (Pos.lt_irrefl _ H). + red; auto. + rewrite add_0_r in H. simpl in H. + red in H. simpl in H. + elim (Pos.lt_not_add_l _ _ H). + now apply (Pos.add_lt_mono_l p). +Qed. + +End Private_BootStrap. + +(** Specification of lt and le. *) + +Lemma lt_succ_r n m : n < succ m <-> n<=m. +Proof. +destruct n as [|p], m as [|q]; simpl; try easy'. +split. now destruct p. now destruct 1. +apply Pos.lt_succ_r. Qed. -Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m). +(** Properties of [double] and [succ_double] *) + +Lemma double_spec n : double n = 2 * n. Proof. -destruct n; destruct m. - simpl in |- *; reflexivity. - unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity. - simpl in |- *; reflexivity. - simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. + reflexivity. Qed. -Theorem Nsucc_0 : forall n : N, Nsucc n <> N0. +Lemma succ_double_spec n : succ_double n = 2 * n + 1. Proof. -intro n; elim n; simpl Nsucc; intros; discriminate. + now destruct n. Qed. -Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m. +Lemma double_add n m : double (n+m) = double n + double m. Proof. -destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H; - clear H; intro H. - symmetry in H; contradiction Psucc_not_one with p. - contradiction Psucc_not_one with p. - rewrite Psucc_inj with (1 := H); reflexivity. + now destruct n, m. Qed. -Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p. +Lemma succ_double_add n m : succ_double (n+m) = double n + succ_double m. Proof. -intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *. - trivial. - intros n IHn m p H0; do 2 rewrite Nplus_succ in H0. - apply IHn; apply Nsucc_inj; assumption. + now destruct n, m. Qed. -(** Properties of subtraction. *) +Lemma double_mul n m : double (n*m) = double n * m. +Proof. + now destruct n, m. +Qed. -Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'. +Lemma succ_double_mul n m : + succ_double n * m = double n * m + m. Proof. -destruct n as [| p]; destruct n' as [| q]; unfold Nle; simpl; -split; intro H; try discriminate; try reflexivity. -now elim H. -intro H1; apply Pminus_mask_Gt in H1. destruct H1 as [h [H1 _]]. -rewrite H1 in H; discriminate. -case_eq (Pcompare p q Eq); intro H1; rewrite H1 in H; try now elim H. -assert (H2 : p = q); [now apply Pcompare_Eq_eq |]. now rewrite H2, Pminus_mask_diag. -now rewrite Pminus_mask_Lt. + destruct n; simpl; destruct m; trivial. + now rewrite Pos.add_comm. Qed. -Theorem Nminus_0_r : forall n : N, n - N0 = n. +Lemma div2_double n : div2 (double n) = n. Proof. now destruct n. Qed. -Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m). +Lemma div2_succ_double n : div2 (succ_double n) = n. Proof. -destruct n as [| p]; destruct m as [| q]; try reflexivity. -now destruct p. -simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. -now destruct (Pminus_mask p q) as [| r |]; [| destruct r |]. +now destruct n. Qed. -(** Properties of multiplication *) +Lemma double_inj n m : double n = double m -> n = m. +Proof. +intro H. rewrite <- (div2_double n), H. apply div2_double. +Qed. -Theorem Nmult_0_l : forall n:N, N0 * n = N0. +Lemma succ_double_inj n m : succ_double n = succ_double m -> n = m. Proof. -reflexivity. +intro H. rewrite <- (div2_succ_double n), H. apply div2_succ_double. Qed. -Theorem Nmult_1_l : forall n:N, Npos 1 * n = n. +Lemma succ_double_lt n m : n<m -> succ_double n < double m. Proof. -destruct n; reflexivity. + 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 Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. + +(** Specification of minimum and maximum *) + +Theorem min_l n m : n <= m -> min n m = n. Proof. -destruct n as [| n]; destruct m as [| m]; simpl; auto. -rewrite Pmult_Sn_m; reflexivity. +unfold min, le. case compare; trivial. now destruct 1. Qed. -Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n. +Theorem min_r n m : m <= n -> min n m = m. Proof. -destruct n; simpl in |- *; try reflexivity. -rewrite Pmult_1_r; reflexivity. +unfold min, le. rewrite compare_antisym. +case compare_spec; trivial. now destruct 2. Qed. -Theorem Nmult_comm : forall n m:N, n * m = m * n. +Theorem max_l n m : m <= n -> max n m = n. Proof. -intros. -destruct n; destruct m; simpl in |- *; try reflexivity. -rewrite Pmult_comm; reflexivity. +unfold max, le. rewrite compare_antisym. +case compare_spec; auto. now destruct 2. Qed. -Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p. +Theorem max_r n m : n <= m -> max n m = m. Proof. -intros. -destruct n; try reflexivity. -destruct m; try reflexivity. -destruct p; try reflexivity. -simpl in |- *; rewrite Pmult_assoc; reflexivity. +unfold max, le. case compare; trivial. now destruct 1. Qed. -Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p. +(** 0 is the least natural number *) + +Theorem compare_0_r n : (n ?= 0) <> Lt. Proof. -intros. -destruct n; try reflexivity. -destruct m; destruct p; try reflexivity. -simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity. +now destruct n. Qed. -Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m. +(** Specifications of power *) + +Lemma pow_0_r n : n ^ 0 = 1. +Proof. reflexivity. Qed. + +Lemma pow_succ_r n p : 0<=p -> n^(succ p) = n * n^p. +Proof. + intros _. + destruct n, p; simpl; trivial; f_equal. apply Pos.pow_succ_r. +Qed. + +Lemma pow_neg_r n p : p<0 -> n^p = 0. 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. + now destruct p. Qed. -(** Properties of boolean order. *) +(** Specification of square *) -Lemma Neqb_eq : forall n m, Neqb n m = true <-> n=m. +Lemma square_spec n : square n = n * n. Proof. -destruct n as [|n], m as [|m]; simpl; split; auto; try discriminate. -intros; f_equal. apply (Peqb_eq n m); auto. -intros. apply (Peqb_eq n m). congruence. + destruct n; trivial. simpl. f_equal. apply Pos.square_spec. Qed. -(** Properties of comparison *) +(** Specification of Base-2 logarithm *) -Lemma Ncompare_refl : forall n, (n ?= n) = Eq. +Lemma size_log2 n : n<>0 -> size n = succ (log2 n). Proof. -destruct n; simpl; auto. -apply Pcompare_refl. + destruct n as [|[n|n| ]]; trivial. now destruct 1. Qed. -Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m. +Lemma size_gt n : n < 2^(size n). Proof. -destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H; - reflexivity || (try discriminate H). - rewrite (Pcompare_Eq_eq n m H); reflexivity. + destruct n. reflexivity. simpl. apply Pos.size_gt. Qed. -Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m. +Lemma size_le n : 2^(size n) <= succ_double n. Proof. -split; intros; - [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ]. + destruct n. discriminate. simpl. + change (2^Pos.size p <= Pos.succ (p~0))%positive. + apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le. Qed. -Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n). +Lemma log2_spec n : 0 < n -> + 2^(log2 n) <= n < 2^(succ (log2 n)). Proof. -destruct n; destruct m; simpl; auto. -exact (Pcompare_antisym p p0 Eq). + destruct n as [|[p|p|]]; discriminate || intros _; simpl; split. + apply (size_le (Npos p)). + apply Pos.size_gt. + apply Pos.size_le. + apply Pos.size_gt. + discriminate. + reflexivity. Qed. -Lemma Ngt_Nlt : forall n m, n > m -> m < n. +Lemma log2_nonpos n : n<=0 -> log2 n = 0. Proof. -unfold Ngt, Nlt; intros n m GT. -rewrite <- Ncompare_antisym, GT; reflexivity. + destruct n; intros Hn. reflexivity. now destruct Hn. Qed. -Theorem Nlt_irrefl : forall n : N, ~ n < n. +(** Specification of parity functions *) + +Lemma even_spec n : even n = true <-> Even n. Proof. -intro n; unfold Nlt; now rewrite Ncompare_refl. + destruct n. + split. now exists 0. + trivial. + destruct p; simpl; split; try easy. + intros (m,H). now destruct m. + now exists (Npos p). + intros (m,H). now destruct m. Qed. -Theorem Nlt_trans : forall n m q, n < m -> m < q -> n < q. +Lemma odd_spec n : odd n = true <-> Odd n. Proof. -destruct n; - destruct m; try discriminate; - destruct q; try discriminate; auto. -eapply Plt_trans; eauto. + destruct n. + split. discriminate. + intros (m,H). now destruct m. + destruct p; simpl; split; try easy. + now exists (Npos p). + intros (m,H). now destruct m. + now exists 0. Qed. -Theorem Nlt_not_eq : forall n m, n < m -> ~ n = m. +(** 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. - intros n m LT EQ. subst m. elim (Nlt_irrefl n); auto. + induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta. + (* a~1 *) + destruct pos_div_eucl as (q,r). + change (Npos a~1) with (succ_double (Npos a)). + rewrite IHa, succ_double_add, double_mul. + case leb_spec; intros H; trivial. + rewrite succ_double_mul, <- add_assoc. f_equal. + now rewrite (add_comm b), sub_add. + (* a~0 *) + destruct pos_div_eucl as (q,r). + change (Npos a~0) with (double (Npos a)). + rewrite IHa, double_add, double_mul. + case leb_spec; intros H; trivial. + rewrite succ_double_mul, <- add_assoc. f_equal. + now rewrite (add_comm b), sub_add. + (* 1 *) + now destruct b as [|[ | | ]]. Qed. -Theorem Ncompare_n_Sm : - forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m. +Theorem div_eucl_spec a b : + let (q,r) := div_eucl a b in a = b * q + r. Proof. -intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto. -destruct p; simpl; intros; discriminate. -pose proof (Pcompare_p_Sq p q) as (?,_). -assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. -intros H; destruct H; discriminate. -pose proof (Pcompare_p_Sq p q) as (_,?); -assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. + 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. -Lemma Nle_lteq : forall x y, x <= y <-> x < y \/ x=y. +Theorem div_mod' a b : a = b * (a/b) + (a mod b). Proof. -unfold Nle, Nlt; intros. -generalize (Ncompare_eq_correct x y). -destruct (x ?= y); intuition; discriminate. + generalize (div_eucl_spec a b). + unfold div, modulo. now destruct div_eucl. Qed. -Lemma Ncompare_spec : forall x y, CompSpec eq Nlt x y (Ncompare x y). +Definition div_mod a b : b<>0 -> a = b * (a/b) + (a mod b). Proof. -intros. -destruct (Ncompare x y) as [ ]_eqn; constructor; auto. -apply Ncompare_Eq_eq; auto. -apply Ngt_Nlt; auto. + intros _. apply div_mod'. Qed. -(** 0 is the least natural number *) +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<b -> 0 <= a mod b < b. +Proof. + intros _ H. split. apply le_0_l. apply mod_lt. now destruct b. +Qed. -Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. +(** 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. + now rewrite mul_comm. +Qed. + +Lemma gcd_divide_r a b : (gcd a b | b). Proof. -destruct n; discriminate. + rewrite <- ggcd_gcd. generalize (ggcd_correct_divisors a b). + destruct ggcd as (g,(aa,bb)); simpl. intros (_,H). exists bb. + now rewrite mul_comm. Qed. -(** Dividing by 2 *) +(** We now prove directly that gcd is the greatest amongst common divisors *) -Definition Ndiv2 (n:N) := - match n with - | N0 => N0 - | Npos 1 => N0 - | Npos (xO p) => Npos p - | Npos (xI p) => Npos p - end. +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). destruct s; 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 Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. Proof. - destruct n; trivial. + now destruct a. Qed. -Lemma Ndouble_plus_one_div2 : - forall n:N, Ndiv2 (Ndouble_plus_one n) = n. +Lemma testbit_succ_r_div2 a n : 0<=n -> + testbit a (succ n) = testbit (div2 a) n. Proof. - destruct n; trivial. + intros _. destruct a as [|[a|a| ]], n as [|n]; simpl; trivial; + f_equal; apply Pos.pred_N_succ. Qed. -Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m. +Lemma testbit_odd_succ a n : 0<=n -> + testbit (2*a+1) (succ n) = testbit a n. Proof. - intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2. + intros H. rewrite testbit_succ_r_div2 by trivial. f_equal. now destruct a. Qed. -Lemma Ndouble_plus_one_inj : - forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m. +Lemma testbit_even_succ a n : 0<=n -> + testbit (2*a) (succ n) = testbit a n. Proof. - intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. + 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<n -> + 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. + +(** Specification of constants *) + +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. + +(** Proofs 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. + +(** Otherwise N stays associated with abstract_scope : (TODO FIX) *) +Bind Scope N_scope with N. + +(** In generic statements, the predicates [lt] and [le] have been + favored, whereas [gt] and [ge] don't even exist in the abstract + layers. The use of [gt] and [ge] is hence not recommended. We provide + here the bare minimal results to related them with [lt] and [le]. *) + +Lemma gt_lt_iff n m : n > m <-> m < n. +Proof. + unfold lt, gt. now rewrite compare_antisym, CompOpp_iff. +Qed. + +Lemma gt_lt n m : n > m -> m < n. +Proof. + apply gt_lt_iff. +Qed. + +Lemma lt_gt n m : n < m -> m > n. +Proof. + apply gt_lt_iff. +Qed. + +Lemma ge_le_iff n m : n >= m <-> m <= n. +Proof. + unfold le, ge. now rewrite compare_antisym, CompOpp_iff. +Qed. + +Lemma ge_le n m : n >= m -> m <= n. +Proof. + apply ge_le_iff. +Qed. + +Lemma le_ge n m : n <= m -> m >= n. +Proof. + apply ge_le_iff. +Qed. + +(** Auxiliary results about right shift on positive numbers, + used in BinInt *) + +Lemma pos_pred_shiftl_low : forall p n m, m<n -> + testbit (Pos.pred_N (Pos.shiftl p n)) m = true. +Proof. + induction n using peano_ind. + now destruct m. + intros m H. unfold Pos.shiftl. + destruct n as [|n]; simpl in *. + destruct m. now destruct p. elim (Pos.nlt_1_r _ H). + rewrite Pos.iter_succ. simpl. + set (u:=Pos.iter n xO p) in *; clearbody u. + destruct m as [|m]. now destruct u. + rewrite <- (IHn (Pos.pred_N m)). + rewrite <- (testbit_odd_succ _ (Pos.pred_N m)). + rewrite succ_pos_pred. now destruct u. + apply le_0_l. + apply succ_lt_mono. now rewrite succ_pos_pred. +Qed. + +Lemma pos_pred_shiftl_high : forall p n m, n<=m -> + testbit (Pos.pred_N (Pos.shiftl p n)) m = + testbit (shiftl (Pos.pred_N p) n) m. +Proof. + induction n using peano_ind; intros m H. + unfold shiftl. simpl. now destruct (Pos.pred_N p). + rewrite shiftl_succ_r. + destruct n as [|n]. + destruct m as [|m]. now destruct H. now destruct p. + destruct m as [|m]. now destruct H. + rewrite <- (succ_pos_pred m). + rewrite double_spec, testbit_even_succ by apply le_0_l. + rewrite <- IHn. + rewrite testbit_succ_r_div2 by apply le_0_l. + f_equal. simpl. rewrite Pos.iter_succ. + now destruct (Pos.iter n xO p). + apply succ_le_mono. now rewrite succ_pos_pred. +Qed. + +Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p). +Proof. + destruct p as [p|p| ]; trivial. + simpl. apply Pos.pred_N_succ. + destruct p; simpl; trivial. +Qed. + +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 "<?" := N.ltb (at level 70, no associativity) : N_scope. + +Infix "/" := N.div : N_scope. +Infix "mod" := N.modulo (at level 40, no associativity) : N_scope. + +Notation "( p | q )" := (N.divide p q) (at level 0) : N_scope. + +(** Compatibility notations *) + +(*Notation N := N (only parsing).*) (*hidden by module N above *) +Notation N_rect := N_rect (only parsing). +Notation N_rec := N_rec (only parsing). +Notation N_ind := N_ind (only parsing). +Notation N0 := N0 (only parsing). +Notation Npos := Npos (only parsing). + +Notation Ndiscr := N.discr (only parsing). +Notation Ndouble_plus_one := N.succ_double. +Notation Ndouble := N.double (only parsing). +Notation Nsucc := N.succ (only parsing). +Notation Npred := N.pred (only parsing). +Notation Nsucc_pos := N.succ_pos (only parsing). +Notation Ppred_N := Pos.pred_N (only parsing). +Notation Nplus := N.add (only parsing). +Notation Nminus := N.sub (only parsing). +Notation Nmult := N.mul (only parsing). +Notation Neqb := N.eqb (only parsing). +Notation Ncompare := N.compare (only parsing). +Notation Nlt := N.lt (only parsing). +Notation Ngt := N.gt (only parsing). +Notation Nle := N.le (only parsing). +Notation Nge := N.ge (only parsing). +Notation Nmin := N.min (only parsing). +Notation Nmax := N.max (only parsing). +Notation Ndiv2 := N.div2 (only parsing). +Notation Neven := N.even (only parsing). +Notation Nodd := N.odd (only parsing). +Notation Npow := N.pow (only parsing). +Notation Nlog2 := N.log2 (only parsing). + +Notation nat_of_N := N.to_nat (only parsing). +Notation N_of_nat := N.of_nat (only parsing). +Notation N_eq_dec := N.eq_dec (only parsing). +Notation Nrect := N.peano_rect (only parsing). +Notation Nrect_base := N.peano_rect_base (only parsing). +Notation Nrect_step := N.peano_rect_succ (only parsing). +Notation Nind := N.peano_ind (only parsing). +Notation Nrec := N.peano_rec (only parsing). +Notation Nrec_base := N.peano_rec_base (only parsing). +Notation Nrec_succ := N.peano_rec_succ (only parsing). + +Notation Npred_succ := N.pred_succ (only parsing). +Notation Npred_minus := N.pred_sub (only parsing). +Notation Nsucc_pred := N.succ_pred (only parsing). +Notation Ppred_N_spec := N.pos_pred_spec (only parsing). +Notation Nsucc_pos_spec := N.succ_pos_spec (only parsing). +Notation Ppred_Nsucc := N.pos_pred_succ (only parsing). +Notation Nplus_0_l := N.add_0_l (only parsing). +Notation Nplus_0_r := N.add_0_r (only parsing). +Notation Nplus_comm := N.add_comm (only parsing). +Notation Nplus_assoc := N.add_assoc (only parsing). +Notation Nplus_succ := N.add_succ_l (only parsing). +Notation Nsucc_0 := N.succ_0_discr (only parsing). +Notation Nsucc_inj := N.succ_inj (only parsing). +Notation Nminus_N0_Nle := N.sub_0_le (only parsing). +Notation Nminus_0_r := N.sub_0_r (only parsing). +Notation Nminus_succ_r:= N.sub_succ_r (only parsing). +Notation Nmult_0_l := N.mul_0_l (only parsing). +Notation Nmult_1_l := N.mul_1_l (only parsing). +Notation Nmult_1_r := N.mul_1_r (only parsing). +Notation Nmult_comm := N.mul_comm (only parsing). +Notation Nmult_assoc := N.mul_assoc (only parsing). +Notation Nmult_plus_distr_r := N.mul_add_distr_r (only parsing). +Notation Neqb_eq := N.eqb_eq (only parsing). +Notation Nle_0 := N.le_0_l (only parsing). +Notation Ncompare_refl := N.compare_refl (only parsing). +Notation Ncompare_Eq_eq := N.compare_eq (only parsing). +Notation Ncompare_eq_correct := N.compare_eq_iff (only parsing). +Notation Nlt_irrefl := N.lt_irrefl (only parsing). +Notation Nlt_trans := N.lt_trans (only parsing). +Notation Nle_lteq := N.lt_eq_cases (only parsing). +Notation Nlt_succ_r := N.lt_succ_r (only parsing). +Notation Nle_trans := N.le_trans (only parsing). +Notation Nle_succ_l := N.le_succ_l (only parsing). +Notation Ncompare_spec := N.compare_spec (only parsing). +Notation Ncompare_0 := N.compare_0_r (only parsing). +Notation Ndouble_div2 := N.div2_double (only parsing). +Notation Ndouble_plus_one_div2 := N.div2_succ_double (only parsing). +Notation Ndouble_inj := N.double_inj (only parsing). +Notation Ndouble_plus_one_inj := N.succ_double_inj (only parsing). +Notation Npow_0_r := N.pow_0_r (only parsing). +Notation Npow_succ_r := N.pow_succ_r (only parsing). +Notation Nlog2_spec := N.log2_spec (only parsing). +Notation Nlog2_nonpos := N.log2_nonpos (only parsing). +Notation Neven_spec := N.even_spec (only parsing). +Notation Nodd_spec := N.odd_spec (only parsing). +Notation Nlt_not_eq := N.lt_neq (only parsing). +Notation Ngt_Nlt := N.gt_lt (only parsing). + +(** More complex compatibility facts, expressed as lemmas + (to preserve scopes for instance) *) + +Lemma Nplus_reg_l n m p : n + m = n + p -> 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 Ncompare_antisym n m : CompOpp (n ?= m) = (m ?= n). +Proof (eq_sym (N.compare_antisym n m)). + +Definition N_ind_double a P f0 f2 fS2 := N.binary_ind P f0 f2 fS2 a. +Definition N_rec_double a P f0 f2 fS2 := N.binary_rec P f0 f2 fS2 a. + +(** Not kept : Ncompare_n_Sm Nplus_lt_cancel_l *) diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v new file mode 100644 index 00000000..d7660422 --- /dev/null +++ b/theories/NArith/BinNatDef.v @@ -0,0 +1,381 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Export BinNums. +Require Import BinPos. + +Local Open Scope N_scope. + +(**********************************************************************) +(** * Binary natural numbers, definitions of operations *) +(**********************************************************************) + +Module N. + +Definition t := N. + +(** ** Constants *) + +Definition zero := 0. +Definition one := 1. +Definition two := 2. + +(** ** Operation [x -> 2*x+1] *) + +Definition succ_double x := + match x with + | 0 => 1 + | Npos p => Npos p~1 + end. + +(** ** Operation [x -> 2*x] *) + +Definition double n := + match n with + | 0 => 0 + | Npos p => Npos p~0 + end. + +(** ** Successor *) + +Definition succ n := + match n with + | 0 => 1 + | Npos p => Npos (Pos.succ p) + end. + +(** ** Predecessor *) + +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 succ_pos (n : N) : positive := + match n with + | N0 => 1%positive + | Npos p => Pos.succ p + end. + +(** ** Addition *) + +Definition add n m := + match n, m with + | 0, _ => m + | _, 0 => n + | Npos p, Npos q => Npos (p + q) + end. + +Infix "+" := add : N_scope. + +(** Subtraction *) + +Definition sub n m := +match n, m with +| 0, _ => 0 +| n, 0 => n +| Npos n', Npos m' => + match Pos.sub_mask n' m' with + | IsPos p => Npos p + | _ => 0 + end +end. + +Infix "-" := sub : N_scope. + +(** Multiplication *) + +Definition mul n m := + match n, m with + | 0, _ => 0 + | _, 0 => 0 + | Npos p, Npos q => Npos (p * q) + end. + +Infix "*" := mul : N_scope. + +(** Order *) + +Definition compare n m := + match n, m with + | 0, 0 => Eq + | 0, Npos m' => Lt + | Npos n', 0 => Gt + | Npos n', Npos m' => (n' ?= m')%positive + end. + +Infix "?=" := compare (at level 70, no associativity) : 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 "<?" := ltb (at level 70, no associativity) : N_scope. + +(** Min and max *) + +Definition min n n' := match n ?= n' with + | Lt | Eq => n + | Gt => n' + end. + +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 + | 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, _ => 1 + | _, 0 => 0 + | Npos p, Npos q => Npos (q^p) + end. + +Infix "^" := pow : N_scope. + +(** Square *) + +Definition square n := + match n with + | 0 => 0 + | Npos p => Npos (Pos.square p) + end. + +(** Base-2 logarithm *) + +Definition log2 n := + match n with + | 0 => 0 + | 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 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) := nat_iter n double a. +Definition shiftr_nat (a:N)(n:nat) := nat_iter 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 to_nat (a:N) := + match a with + | 0 => O + | Npos p => Pos.to_nat p + end. + +Definition of_nat (n:nat) := + match n with + | O => 0 + | S n' => Npos (Pos.of_succ_nat n') + end. + +(** Iteration of a function *) + +Definition iter (n:N) {A} (f:A->A) (x:A) : A := + match n with + | 0 => x + | Npos p => Pos.iter p f x + end. + +End N.
\ No newline at end of file diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v deleted file mode 100644 index 62bd57c0..00000000 --- a/theories/NArith/BinPos.v +++ /dev/null @@ -1,1172 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: BinPos.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Unset Boxed Definitions. - -Declare ML Module "z_syntax_plugin". - -(**********************************************************************) -(** Binary positive numbers *) - -(** Original development by Pierre Crégut, CNET, Lannion, France *) - -Inductive positive : Set := -| xI : positive -> positive -| xO : positive -> positive -| xH : positive. - -(** Declare binding key for scope positive_scope *) - -Delimit Scope positive_scope with positive. - -(** Automatically open scope positive_scope for type positive, xO and xI *) - -Bind Scope positive_scope with positive. -Arguments Scope xO [positive_scope]. -Arguments Scope xI [positive_scope]. - -(** Postfix notation for positive numbers, allowing to mimic - the position of bits in a big-endian representation. - For instance, we can write 1~1~0 instead of (xO (xI xH)) - for the number 6 (which is 110 in binary notation). -*) - -Notation "p ~ 1" := (xI p) - (at level 7, left associativity, format "p '~' '1'") : positive_scope. -Notation "p ~ 0" := (xO p) - (at level 7, left associativity, format "p '~' '0'") : positive_scope. - -Open Local Scope positive_scope. - -(* In the current file, [xH] cannot yet be written as [1], since the - interpretation of positive numerical constants is not available - yet. We fix this here with an ad-hoc temporary notation. *) - -Notation Local "1" := xH (at level 7). - -(** Successor *) - -Fixpoint Psucc (x:positive) : positive := - match x with - | p~1 => (Psucc p)~0 - | p~0 => p~1 - | 1 => 1~0 - end. - -(** Addition *) - -Set Boxed Definitions. - -Fixpoint Pplus (x y:positive) : positive := - match x, y with - | p~1, q~1 => (Pplus_carry p q)~0 - | p~1, q~0 => (Pplus p q)~1 - | p~1, 1 => (Psucc p)~0 - | p~0, q~1 => (Pplus p q)~1 - | p~0, q~0 => (Pplus p q)~0 - | p~0, 1 => p~1 - | 1, q~1 => (Psucc q)~0 - | 1, q~0 => q~1 - | 1, 1 => 1~0 - end - -with Pplus_carry (x y:positive) : positive := - match x, y with - | p~1, q~1 => (Pplus_carry p q)~1 - | p~1, q~0 => (Pplus_carry p q)~0 - | p~1, 1 => (Psucc p)~1 - | p~0, q~1 => (Pplus_carry p q)~0 - | p~0, q~0 => (Pplus p q)~1 - | p~0, 1 => (Psucc p)~0 - | 1, q~1 => (Psucc q)~1 - | 1, q~0 => (Psucc q)~0 - | 1, 1 => 1~1 - end. - -Unset Boxed Definitions. - -Infix "+" := Pplus : positive_scope. - -(** From binary positive numbers to Peano natural numbers *) - -Fixpoint Pmult_nat (x:positive) (pow2:nat) : nat := - match x with - | p~1 => (pow2 + Pmult_nat p (pow2 + pow2))%nat - | p~0 => Pmult_nat p (pow2 + pow2)%nat - | 1 => pow2 - end. - -Definition nat_of_P (x:positive) := Pmult_nat x (S O). - -(** From Peano natural numbers to binary positive numbers *) - -Fixpoint P_of_succ_nat (n:nat) : positive := - match n with - | O => 1 - | S x => Psucc (P_of_succ_nat x) - end. - -(** Operation x -> 2*x-1 *) - -Fixpoint Pdouble_minus_one (x:positive) : positive := - match x with - | p~1 => p~0~1 - | p~0 => (Pdouble_minus_one p)~1 - | 1 => 1 - end. - -(** Predecessor *) - -Definition Ppred (x:positive) := - match x with - | p~1 => p~0 - | p~0 => Pdouble_minus_one p - | 1 => 1 - end. - -(** An auxiliary type for subtraction *) - -Inductive positive_mask : Set := -| IsNul : positive_mask -| IsPos : positive -> positive_mask -| IsNeg : positive_mask. - -(** Operation x -> 2*x+1 *) - -Definition Pdouble_plus_one_mask (x:positive_mask) := - match x with - | IsNul => IsPos 1 - | IsNeg => IsNeg - | IsPos p => IsPos p~1 - end. - -(** Operation x -> 2*x *) - -Definition Pdouble_mask (x:positive_mask) := - match x with - | IsNul => IsNul - | IsNeg => IsNeg - | IsPos p => IsPos p~0 - end. - -(** Operation x -> 2*x-2 *) - -Definition Pdouble_minus_two (x:positive) := - match x with - | p~1 => IsPos p~0~0 - | p~0 => IsPos (Pdouble_minus_one p)~0 - | 1 => IsNul - end. - -(** Subtraction of binary positive numbers into a positive numbers mask *) - -Fixpoint Pminus_mask (x y:positive) {struct y} : positive_mask := - match x, y with - | p~1, q~1 => Pdouble_mask (Pminus_mask p q) - | p~1, q~0 => Pdouble_plus_one_mask (Pminus_mask p q) - | p~1, 1 => IsPos p~0 - | p~0, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q) - | p~0, q~0 => Pdouble_mask (Pminus_mask p q) - | p~0, 1 => IsPos (Pdouble_minus_one p) - | 1, 1 => IsNul - | 1, _ => IsNeg - end - -with Pminus_mask_carry (x y:positive) {struct y} : positive_mask := - match x, y with - | p~1, q~1 => Pdouble_plus_one_mask (Pminus_mask_carry p q) - | p~1, q~0 => Pdouble_mask (Pminus_mask p q) - | p~1, 1 => IsPos (Pdouble_minus_one p) - | p~0, q~1 => Pdouble_mask (Pminus_mask_carry p q) - | p~0, q~0 => Pdouble_plus_one_mask (Pminus_mask_carry p q) - | p~0, 1 => Pdouble_minus_two p - | 1, _ => IsNeg - end. - -(** Subtraction of binary positive numbers x and y, returns 1 if x<=y *) - -Definition Pminus (x y:positive) := - match Pminus_mask x y with - | IsPos z => z - | _ => 1 - end. - -Infix "-" := Pminus : positive_scope. - -(** Multiplication on binary positive numbers *) - -Fixpoint Pmult (x y:positive) : positive := - match x with - | p~1 => y + (Pmult p y)~0 - | p~0 => (Pmult p y)~0 - | 1 => y - end. - -Infix "*" := Pmult : positive_scope. - -(** Division by 2 rounded below but for 1 *) - -Definition Pdiv2 (z:positive) := - match z with - | 1 => 1 - | p~0 => p - | p~1 => p - end. - -Infix "/" := Pdiv2 : positive_scope. - -(** Comparison on binary positive numbers *) - -Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison := - match x, y with - | p~1, q~1 => Pcompare p q r - | p~1, q~0 => Pcompare p q Gt - | p~1, 1 => Gt - | p~0, q~1 => Pcompare p q Lt - | p~0, q~0 => Pcompare p q r - | p~0, 1 => Gt - | 1, q~1 => Lt - | 1, q~0 => Lt - | 1, 1 => r - end. - -Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope. - -Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt. -Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt. -Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt. -Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt. - -Infix "<=" := Ple : positive_scope. -Infix "<" := Plt : positive_scope. -Infix ">=" := Pge : positive_scope. -Infix ">" := Pgt : positive_scope. - -Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope. -Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope. -Notation "x < y < z" := (x < y /\ y < z) : positive_scope. -Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope. - - -Definition Pmin (p p' : positive) := match Pcompare p p' Eq with - | Lt | Eq => p - | Gt => p' - end. - -Definition Pmax (p p' : positive) := match Pcompare p p' Eq with - | Lt | Eq => p' - | Gt => p - end. - -(********************************************************************) -(** Boolean equality *) - -Fixpoint Peqb (x y : positive) {struct y} : bool := - match x, y with - | 1, 1 => true - | p~1, q~1 => Peqb p q - | p~0, q~0 => Peqb p q - | _, _ => false - end. - -(**********************************************************************) -(** Decidability of equality on binary positive numbers *) - -Lemma positive_eq_dec : forall x y: positive, {x = y} + {x <> y}. -Proof. - decide equality. -Defined. - -(* begin hide *) -Corollary ZL11 : forall p:positive, p = 1 \/ p <> 1. -Proof. - intro; edestruct positive_eq_dec; eauto. -Qed. -(* end hide *) - -(**********************************************************************) -(** Properties of successor on binary positive numbers *) - -(** Specification of [xI] in term of [Psucc] and [xO] *) - -Lemma xI_succ_xO : forall p:positive, p~1 = Psucc p~0. -Proof. - reflexivity. -Qed. - -Lemma Psucc_discr : forall p:positive, p <> Psucc p. -Proof. - destruct p; discriminate. -Qed. - -(** Successor and double *) - -Lemma Psucc_o_double_minus_one_eq_xO : - forall p:positive, Psucc (Pdouble_minus_one p) = p~0. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -Lemma Pdouble_minus_one_o_succ_eq_xI : - forall p:positive, Pdouble_minus_one (Psucc p) = p~1. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -Lemma xO_succ_permute : - forall p:positive, (Psucc p)~0 = Psucc (Psucc p~0). -Proof. - induction p; simpl; auto. -Qed. - -Lemma double_moins_un_xO_discr : - forall p:positive, Pdouble_minus_one p <> p~0. -Proof. - destruct p; discriminate. -Qed. - -(** Successor and predecessor *) - -Lemma Psucc_not_one : forall p:positive, Psucc p <> 1. -Proof. - destruct p; discriminate. -Qed. - -Lemma Ppred_succ : forall p:positive, Ppred (Psucc p) = p. -Proof. - intros [[p|p| ]|[p|p| ]| ]; simpl; auto. - f_equal; apply Pdouble_minus_one_o_succ_eq_xI. -Qed. - -Lemma Psucc_pred : forall p:positive, p = 1 \/ Psucc (Ppred p) = p. -Proof. - induction p; simpl; auto. - right; apply Psucc_o_double_minus_one_eq_xO. -Qed. - -Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)). - -(** Injectivity of successor *) - -Lemma Psucc_inj : forall p q:positive, Psucc p = Psucc q -> p = q. -Proof. - induction p; intros [q|q| ] H; simpl in *; destr_eq H; f_equal; auto. - elim (Psucc_not_one p); auto. - elim (Psucc_not_one q); auto. -Qed. - -(**********************************************************************) -(** Properties of addition on binary positive numbers *) - -(** Specification of [Psucc] in term of [Pplus] *) - -Lemma Pplus_one_succ_r : forall p:positive, Psucc p = p + 1. -Proof. - destruct p; reflexivity. -Qed. - -Lemma Pplus_one_succ_l : forall p:positive, Psucc p = 1 + p. -Proof. - destruct p; reflexivity. -Qed. - -(** Specification of [Pplus_carry] *) - -Theorem Pplus_carry_spec : - forall p q:positive, Pplus_carry p q = Psucc (p + q). -Proof. - induction p; destruct q; simpl; f_equal; auto. -Qed. - -(** Commutativity *) - -Theorem Pplus_comm : forall p q:positive, p + q = q + p. -Proof. - induction p; destruct q; simpl; f_equal; auto. - rewrite 2 Pplus_carry_spec; f_equal; auto. -Qed. - -(** Permutation of [Pplus] and [Psucc] *) - -Theorem Pplus_succ_permute_r : - forall p q:positive, p + Psucc q = Psucc (p + q). -Proof. - induction p; destruct q; simpl; f_equal; - auto using Pplus_one_succ_r; rewrite Pplus_carry_spec; auto. -Qed. - -Theorem Pplus_succ_permute_l : - forall p q:positive, Psucc p + q = Psucc (p + q). -Proof. - intros p q; rewrite Pplus_comm, (Pplus_comm p); - apply Pplus_succ_permute_r. -Qed. - -Theorem Pplus_carry_pred_eq_plus : - forall p q:positive, q <> 1 -> Pplus_carry p (Ppred q) = p + q. -Proof. - intros p q H; rewrite Pplus_carry_spec, <- Pplus_succ_permute_r; f_equal. - destruct (Psucc_pred q); [ elim H; assumption | assumption ]. -Qed. - -(** No neutral for addition on strictly positive numbers *) - -Lemma Pplus_no_neutral : forall p q:positive, q + p <> p. -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; - destr_eq H; apply (IHp q H). -Qed. - -Lemma Pplus_carry_no_neutral : - forall p q:positive, Pplus_carry q p <> Psucc p. -Proof. - intros p q H; elim (Pplus_no_neutral p q). - apply Psucc_inj; rewrite <- Pplus_carry_spec; assumption. -Qed. - -(** Simplification *) - -Lemma Pplus_carry_plus : - forall p q r s:positive, Pplus_carry p r = Pplus_carry q s -> p + r = q + s. -Proof. - intros p q r s H; apply Psucc_inj; do 2 rewrite <- Pplus_carry_spec; - assumption. -Qed. - -Lemma Pplus_reg_r : forall p q r:positive, p + r = q + r -> p = q. -Proof. - intros p q r; revert p q; induction r. - intros [p|p| ] [q|q| ] H; simpl; destr_eq H; - f_equal; auto using Pplus_carry_plus; - contradict H; auto using Pplus_carry_no_neutral. - intros [p|p| ] [q|q| ] H; simpl; destr_eq H; f_equal; auto; - contradict H; auto using Pplus_no_neutral. - intros p q H; apply Psucc_inj; do 2 rewrite Pplus_one_succ_r; assumption. -Qed. - -Lemma Pplus_reg_l : forall p q r:positive, p + q = p + r -> q = r. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=p). - rewrite (Pplus_comm r), (Pplus_comm q); assumption. -Qed. - -Lemma Pplus_carry_reg_r : - forall p q r:positive, Pplus_carry p r = Pplus_carry q r -> p = q. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=r); apply Pplus_carry_plus; - assumption. -Qed. - -Lemma Pplus_carry_reg_l : - forall p q r:positive, Pplus_carry p q = Pplus_carry p r -> q = r. -Proof. - intros p q r H; apply Pplus_reg_r with (r:=p); - rewrite (Pplus_comm r), (Pplus_comm q); apply Pplus_carry_plus; assumption. -Qed. - -(** Addition on positive is associative *) - -Theorem Pplus_assoc : forall p q r:positive, p + (q + r) = p + q + r. -Proof. - induction p. - intros [q|q| ] [r|r| ]; simpl; f_equal; auto; - rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, - ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto. - intros [q|q| ] [r|r| ]; simpl; f_equal; auto; - rewrite ?Pplus_carry_spec, ?Pplus_succ_permute_r, - ?Pplus_succ_permute_l, ?Pplus_one_succ_r; f_equal; auto. - intros p r; rewrite <- 2 Pplus_one_succ_l, Pplus_succ_permute_l; auto. -Qed. - -(** Commutation of addition with the double of a positive number *) - -Lemma Pplus_xO : forall m n : positive, (m + n)~0 = m~0 + n~0. -Proof. - destruct n; destruct m; simpl; auto. -Qed. - -Lemma Pplus_xI_double_minus_one : - forall p q:positive, (p + q)~0 = p~1 + Pdouble_minus_one q. -Proof. - intros; change (p~1) with (p~0 + 1). - rewrite <- Pplus_assoc, <- Pplus_one_succ_l, Psucc_o_double_minus_one_eq_xO. - reflexivity. -Qed. - -Lemma Pplus_xO_double_minus_one : - forall p q:positive, Pdouble_minus_one (p + q) = p~0 + Pdouble_minus_one q. -Proof. - induction p as [p IHp| p IHp| ]; destruct q; simpl; - rewrite ?Pplus_carry_spec, ?Pdouble_minus_one_o_succ_eq_xI, - ?Pplus_xI_double_minus_one; try reflexivity. - rewrite IHp; auto. - rewrite <- Psucc_o_double_minus_one_eq_xO, Pplus_one_succ_l; reflexivity. -Qed. - -(** Misc *) - -Lemma Pplus_diag : forall p:positive, p + p = p~0. -Proof. - induction p as [p IHp| p IHp| ]; simpl; - try rewrite ?Pplus_carry_spec, ?IHp; reflexivity. -Qed. - -(**********************************************************************) -(** Peano induction and recursion on binary positive positive numbers *) -(** (a nice proof from Conor McBride, see "The view from the left") *) - -Inductive PeanoView : positive -> Type := -| PeanoOne : PeanoView 1 -| PeanoSucc : forall p, PeanoView p -> PeanoView (Psucc p). - -Fixpoint peanoView_xO p (q:PeanoView p) : PeanoView (p~0) := - match q in PeanoView x return PeanoView (x~0) with - | PeanoOne => PeanoSucc _ PeanoOne - | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xO _ q)) - end. - -Fixpoint peanoView_xI p (q:PeanoView p) : PeanoView (p~1) := - match q in PeanoView x return PeanoView (x~1) with - | PeanoOne => PeanoSucc _ (PeanoSucc _ PeanoOne) - | PeanoSucc _ q => PeanoSucc _ (PeanoSucc _ (peanoView_xI _ q)) - end. - -Fixpoint peanoView p : PeanoView p := - match p return PeanoView p with - | 1 => PeanoOne - | p~0 => peanoView_xO p (peanoView p) - | p~1 => peanoView_xI p (peanoView p) - end. - -Definition PeanoView_iter (P:positive->Type) - (a:P 1) (f:forall p, P p -> P (Psucc p)) := - (fix iter p (q:PeanoView p) : P p := - match q in PeanoView p return P p with - | PeanoOne => a - | PeanoSucc _ q => f _ (iter _ q) - end). - -Require Import Eqdep_dec EqdepFacts. - -Theorem eq_dep_eq_positive : - forall (P:positive->Type) (p:positive) (x y:P p), - eq_dep positive P p x p y -> x = y. -Proof. - apply eq_dep_eq_dec. - decide equality. -Qed. - -Theorem PeanoViewUnique : forall p (q q':PeanoView p), q = q'. -Proof. - intros. - induction q as [ | p q IHq ]. - apply eq_dep_eq_positive. - cut (1=1). pattern 1 at 1 2 5, q'. destruct q'. trivial. - destruct p0; intros; discriminate. - trivial. - apply eq_dep_eq_positive. - cut (Psucc p=Psucc p). pattern (Psucc p) at 1 2 5, q'. destruct q'. - intro. destruct p; discriminate. - intro. unfold p0 in H. apply Psucc_inj in H. - generalize q'. rewrite H. intro. - rewrite (IHq q'0). - trivial. - trivial. -Qed. - -Definition Prect (P:positive->Type) (a:P 1) (f:forall p, P p -> P (Psucc p)) - (p:positive) := - PeanoView_iter P a f p (peanoView p). - -Theorem Prect_succ : forall (P:positive->Type) (a:P 1) - (f:forall p, P p -> P (Psucc p)) (p:positive), - Prect P a f (Psucc p) = f _ (Prect P a f p). -Proof. - intros. - unfold Prect. - rewrite (PeanoViewUnique _ (peanoView (Psucc p)) (PeanoSucc _ (peanoView p))). - trivial. -Qed. - -Theorem Prect_base : forall (P:positive->Type) (a:P 1) - (f:forall p, P p -> P (Psucc p)), Prect P a f 1 = a. -Proof. - trivial. -Qed. - -Definition Prec (P:positive->Set) := Prect P. - -(** Peano induction *) - -Definition Pind (P:positive->Prop) := Prect P. - -(** Peano case analysis *) - -Theorem Pcase : - forall P:positive -> Prop, - P 1 -> (forall n:positive, P (Psucc n)) -> forall p:positive, P p. -Proof. - intros; apply Pind; auto. -Qed. - -(**********************************************************************) -(** Properties of multiplication on binary positive numbers *) - -(** One is right neutral for multiplication *) - -Lemma Pmult_1_r : forall p:positive, p * 1 = p. -Proof. - induction p; simpl; f_equal; auto. -Qed. - -(** Successor and multiplication *) - -Lemma Pmult_Sn_m : forall n m : positive, (Psucc n) * m = m + n * m. -Proof. - induction n as [n IHn | n IHn | ]; simpl; intro m. - rewrite IHn, Pplus_assoc, Pplus_diag, <-Pplus_xO; reflexivity. - reflexivity. - symmetry; apply Pplus_diag. -Qed. - -(** Right reduction properties for multiplication *) - -Lemma Pmult_xO_permute_r : forall p q:positive, p * q~0 = (p * q)~0. -Proof. - intros p q; induction p; simpl; do 2 (f_equal; auto). -Qed. - -Lemma Pmult_xI_permute_r : forall p q:positive, p * q~1 = p + (p * q)~0. -Proof. - intros p q; induction p as [p IHp|p IHp| ]; simpl; f_equal; auto. - rewrite IHp, 2 Pplus_assoc, (Pplus_comm p); reflexivity. -Qed. - -(** Commutativity of multiplication *) - -Theorem Pmult_comm : forall p q:positive, p * q = q * p. -Proof. - intros p q; induction q as [q IHq|q IHq| ]; simpl; try rewrite <- IHq; - auto using Pmult_xI_permute_r, Pmult_xO_permute_r, Pmult_1_r. -Qed. - -(** Distributivity of multiplication over addition *) - -Theorem Pmult_plus_distr_l : - forall p q r:positive, p * (q + r) = p * q + p * r. -Proof. - intros p q r; induction p as [p IHp|p IHp| ]; simpl. - rewrite IHp. set (m:=(p*q)~0). set (n:=(p*r)~0). - change ((p*q+p*r)~0) with (m+n). - rewrite 2 Pplus_assoc; f_equal. - rewrite <- 2 Pplus_assoc; f_equal. - apply Pplus_comm. - f_equal; auto. - reflexivity. -Qed. - -Theorem Pmult_plus_distr_r : - forall p q r:positive, (p + q) * r = p * r + q * r. -Proof. - intros p q r; do 3 rewrite Pmult_comm with (q:=r); apply Pmult_plus_distr_l. -Qed. - -(** Associativity of multiplication *) - -Theorem Pmult_assoc : forall p q r:positive, p * (q * r) = p * q * r. -Proof. - induction p as [p IHp| p IHp | ]; simpl; intros q r. - rewrite IHp; rewrite Pmult_plus_distr_r; reflexivity. - rewrite IHp; reflexivity. - reflexivity. -Qed. - -(** Parity properties of multiplication *) - -Lemma Pmult_xI_mult_xO_discr : forall p q r:positive, p~1 * r <> q~0 * r. -Proof. - intros p q r; induction r; try discriminate. - rewrite 2 Pmult_xO_permute_r; intro H; destr_eq H; auto. -Qed. - -Lemma Pmult_xO_discr : forall p q:positive, p~0 * q <> q. -Proof. - intros p q; induction q; try discriminate. - rewrite Pmult_xO_permute_r; injection; assumption. -Qed. - -(** Simplification properties of multiplication *) - -Theorem Pmult_reg_r : forall p q r:positive, p * r = q * r -> p = q. -Proof. - induction p as [p IHp| p IHp| ]; intros [q|q| ] r H; - reflexivity || apply (f_equal (A:=positive)) || apply False_ind. - apply IHp with (r~0); simpl in *; - rewrite 2 Pmult_xO_permute_r; apply Pplus_reg_l with (1:=H). - apply Pmult_xI_mult_xO_discr with (1:=H). - simpl in H; rewrite Pplus_comm in H; apply Pplus_no_neutral with (1:=H). - symmetry in H; apply Pmult_xI_mult_xO_discr with (1:=H). - apply IHp with (r~0); simpl; rewrite 2 Pmult_xO_permute_r; assumption. - apply Pmult_xO_discr with (1:= H). - simpl in H; symmetry in H; rewrite Pplus_comm in H; - apply Pplus_no_neutral with (1:=H). - symmetry in H; apply Pmult_xO_discr with (1:=H). -Qed. - -Theorem Pmult_reg_l : forall p q r:positive, r * p = r * q -> p = q. -Proof. - intros p q r H; apply Pmult_reg_r with (r:=r). - rewrite (Pmult_comm p), (Pmult_comm q); assumption. -Qed. - -(** Inversion of multiplication *) - -Lemma Pmult_1_inversion_l : forall p q:positive, p * q = 1 -> p = 1. -Proof. - intros [p|p| ] [q|q| ] H; destr_eq H; auto. -Qed. - -(*********************************************************************) -(** Properties of boolean equality *) - -Theorem Peqb_refl : forall x:positive, Peqb x x = true. -Proof. - induction x; auto. -Qed. - -Theorem Peqb_true_eq : forall x y:positive, Peqb x y = true -> x=y. -Proof. - induction x; destruct y; simpl; intros; try discriminate. - f_equal; auto. - f_equal; auto. - reflexivity. -Qed. - -Theorem Peqb_eq : forall x y : positive, Peqb x y = true <-> x=y. -Proof. - split. apply Peqb_true_eq. - intros; subst; apply Peqb_refl. -Qed. - - -(**********************************************************************) -(** Properties of comparison on binary positive numbers *) - -Theorem Pcompare_refl : forall p:positive, (p ?= p) Eq = Eq. - induction p; auto. -Qed. - -(* A generalization of Pcompare_refl *) - -Theorem Pcompare_refl_id : forall (p : positive) (r : comparison), (p ?= p) r = r. - induction p; auto. -Qed. - -Theorem Pcompare_not_Eq : - forall p q:positive, (p ?= q) Gt <> Eq /\ (p ?= q) Lt <> Eq. -Proof. - induction p as [p IHp| p IHp| ]; intros [q| q| ]; split; simpl; auto; - discriminate || (elim (IHp q); auto). -Qed. - -Theorem Pcompare_Eq_eq : forall p q:positive, (p ?= q) Eq = Eq -> p = q. -Proof. - induction p; intros [q| q| ] H; simpl in *; auto; - try discriminate H; try (f_equal; auto; fail). - destruct (Pcompare_not_Eq p q) as (H',_); elim H'; auto. - destruct (Pcompare_not_Eq p q) as (_,H'); elim H'; auto. -Qed. - -Lemma Pcompare_eq_iff : forall p q:positive, (p ?= q) Eq = Eq <-> p = q. -Proof. - split. - apply Pcompare_Eq_eq. - intros; subst; apply Pcompare_refl. -Qed. - -Lemma Pcompare_Gt_Lt : - forall p q:positive, (p ?= q) Gt = Lt -> (p ?= q) Eq = Lt. -Proof. - induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_eq_Lt : - forall p q : positive, (p ?= q) Eq = Lt <-> (p ?= q) Gt = Lt. -Proof. - intros p q; split; [| apply Pcompare_Gt_Lt]. - revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_Lt_Gt : - forall p q:positive, (p ?= q) Lt = Gt -> (p ?= q) Eq = Gt. -Proof. - induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_eq_Gt : - forall p q : positive, (p ?= q) Eq = Gt <-> (p ?= q) Lt = Gt. -Proof. - intros p q; split; [| apply Pcompare_Lt_Gt]. - revert q; induction p; intros [q|q| ] H; simpl; auto; discriminate. -Qed. - -Lemma Pcompare_Lt_Lt : - forall p q:positive, (p ?= q) Lt = Lt -> (p ?= q) Eq = Lt \/ p = q. -Proof. - induction p as [p IHp| p IHp| ]; intros [q|q| ] H; simpl in *; auto; - destruct (IHp q H); subst; auto. -Qed. - -Lemma Pcompare_Lt_eq_Lt : - forall p q:positive, (p ?= q) Lt = Lt <-> (p ?= q) Eq = Lt \/ p = q. -Proof. - intros p q; split; [apply Pcompare_Lt_Lt |]. - intros [H|H]; [|subst; apply Pcompare_refl_id]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; discriminate. -Qed. - -Lemma Pcompare_Gt_Gt : - forall p q:positive, (p ?= q) Gt = Gt -> (p ?= q) Eq = Gt \/ p = q. -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; - destruct (IHp q H); subst; auto. -Qed. - -Lemma Pcompare_Gt_eq_Gt : - forall p q:positive, (p ?= q) Gt = Gt <-> (p ?= q) Eq = Gt \/ p = q. -Proof. - intros p q; split; [apply Pcompare_Gt_Gt |]. - intros [H|H]; [|subst; apply Pcompare_refl_id]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; discriminate. -Qed. - -Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt. -Proof. - destruct r; auto. -Qed. - -Ltac ElimPcompare c1 c2 := - elim (Dcompare ((c1 ?= c2) Eq)); - [ idtac | let x := fresh "H" in (intro x; case x; clear x) ]. - -Lemma Pcompare_antisym : - forall (p q:positive) (r:comparison), - CompOpp ((p ?= q) r) = (q ?= p) (CompOpp r). -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] r; simpl; auto; - rewrite IHp; auto. -Qed. - -Lemma ZC1 : forall p q:positive, (p ?= q) Eq = Gt -> (q ?= p) Eq = Lt. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC2 : forall p q:positive, (p ?= q) Eq = Lt -> (q ?= p) Eq = Gt. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC3 : forall p q:positive, (p ?= q) Eq = Eq -> (q ?= p) Eq = Eq. -Proof. - intros p q H; change Eq with (CompOpp Eq). - rewrite <- Pcompare_antisym, H; reflexivity. -Qed. - -Lemma ZC4 : forall p q:positive, (p ?= q) Eq = CompOpp ((q ?= p) Eq). -Proof. - intros; change Eq at 1 with (CompOpp Eq). - symmetry; apply Pcompare_antisym. -Qed. - -Lemma Pcompare_spec : forall p q, CompSpec eq Plt p q ((p ?= q) Eq). -Proof. - intros. destruct ((p ?= q) Eq) as [ ]_eqn; constructor. - apply Pcompare_Eq_eq; auto. - auto. - apply ZC1; auto. -Qed. - - -(** Comparison and the successor *) - -Lemma Pcompare_p_Sp : forall p : positive, (p ?= Psucc p) Eq = Lt. -Proof. - induction p; simpl in *; - [ elim (Pcompare_eq_Lt p (Psucc p)); auto | - apply Pcompare_refl_id | reflexivity]. -Qed. - -Theorem Pcompare_p_Sq : forall p q : positive, - (p ?= Psucc q) Eq = Lt <-> (p ?= q) Eq = Lt \/ p = q. -Proof. - intros p q; split. - (* -> *) - revert p q; induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; - try (left; reflexivity); try (right; reflexivity). - destruct (IHp q (Pcompare_Gt_Lt _ _ H)); subst; auto. - destruct (Pcompare_eq_Lt p q); auto. - destruct p; discriminate. - left; destruct (IHp q H); - [ elim (Pcompare_Lt_eq_Lt p q); auto | subst; apply Pcompare_refl_id]. - destruct (Pcompare_Lt_Lt p q H); subst; auto. - destruct p; discriminate. - (* <- *) - intros [H|H]; [|subst; apply Pcompare_p_Sp]. - revert q H; induction p; intros [q|q| ] H; simpl in *; - auto; try discriminate. - destruct (Pcompare_eq_Lt p (Psucc q)); auto. - apply Pcompare_Gt_Lt; auto. - destruct (Pcompare_Lt_Lt p q H); subst; auto using Pcompare_p_Sp. - destruct (Pcompare_Lt_eq_Lt p q); auto. -Qed. - -(** 1 is the least positive number *) - -Lemma Pcompare_1 : forall p, ~ (p ?= 1) Eq = Lt. -Proof. - destruct p; discriminate. -Qed. - -(** Properties of the strict order on positive numbers *) - -Lemma Plt_1 : forall p, ~ p < 1. -Proof. - exact Pcompare_1. -Qed. - -Lemma Plt_lt_succ : forall n m : positive, n < m -> n < Psucc m. -Proof. - unfold Plt; intros n m H; apply <- Pcompare_p_Sq; auto. -Qed. - -Lemma Plt_irrefl : forall p : positive, ~ p < p. -Proof. - unfold Plt; intro p; rewrite Pcompare_refl; discriminate. -Qed. - -Lemma Plt_trans : forall n m p : positive, n < m -> m < p -> n < p. -Proof. - intros n m p; induction p using Pind; intros H H0. - elim (Plt_1 _ H0). - apply Plt_lt_succ. - destruct (Pcompare_p_Sq m p) as (H',_); destruct (H' H0); subst; auto. -Qed. - -Theorem Plt_ind : forall (A : positive -> Prop) (n : positive), - A (Psucc n) -> - (forall m : positive, n < m -> A m -> A (Psucc m)) -> - forall m : positive, n < m -> A m. -Proof. - intros A n AB AS m. induction m using Pind; intros H. - elim (Plt_1 _ H). - destruct (Pcompare_p_Sq n m) as (H',_); destruct (H' H); subst; auto. -Qed. - -Lemma Ple_lteq : forall p q, p <= q <-> p < q \/ p = q. -Proof. - unfold Ple, Plt. intros. - generalize (Pcompare_eq_iff p q). - destruct ((p ?= q) Eq); intuition; discriminate. -Qed. - - -(**********************************************************************) -(** Properties of subtraction on binary positive numbers *) - -Lemma Ppred_minus : forall p, Ppred p = Pminus p 1. -Proof. - destruct p; auto. -Qed. - -Definition Ppred_mask (p : positive_mask) := -match p with -| IsPos 1 => IsNul -| IsPos q => IsPos (Ppred q) -| IsNul => IsNeg -| IsNeg => IsNeg -end. - -Lemma Pminus_mask_succ_r : - forall p q : positive, Pminus_mask p (Psucc q) = Pminus_mask_carry p q. -Proof. - induction p ; destruct q; simpl; f_equal; auto; destruct p; auto. -Qed. - -Theorem Pminus_mask_carry_spec : - forall p q : positive, Pminus_mask_carry p q = Ppred_mask (Pminus_mask p q). -Proof. - induction p as [p IHp|p IHp| ]; destruct q; simpl; - try reflexivity; try rewrite IHp; - destruct (Pminus_mask p q) as [|[r|r| ]|] || destruct p; auto. -Qed. - -Theorem Pminus_succ_r : forall p q : positive, p - (Psucc q) = Ppred (p - q). -Proof. - intros p q; unfold Pminus; - rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec. - destruct (Pminus_mask p q) as [|[r|r| ]|]; auto. -Qed. - -Lemma double_eq_zero_inversion : - forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul. -Proof. - destruct p; simpl; intros; trivial; discriminate. -Qed. - -Lemma double_plus_one_zero_discr : - forall p:positive_mask, Pdouble_plus_one_mask p <> IsNul. -Proof. - destruct p; discriminate. -Qed. - -Lemma double_plus_one_eq_one_inversion : - forall p:positive_mask, Pdouble_plus_one_mask p = IsPos 1 -> p = IsNul. -Proof. - destruct p; simpl; intros; trivial; discriminate. -Qed. - -Lemma double_eq_one_discr : - forall p:positive_mask, Pdouble_mask p <> IsPos 1. -Proof. - destruct p; discriminate. -Qed. - -Theorem Pminus_mask_diag : forall p:positive, Pminus_mask p p = IsNul. -Proof. - induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. -Qed. - -Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg. -Proof. - induction p as [p IHp| p IHp| ]; simpl; try rewrite IHp; auto. -Qed. - -Lemma Pminus_mask_IsNeg : forall p q:positive, - Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg. -Proof. - induction p as [p IHp|p IHp| ]; intros [q|q| ] H; simpl in *; auto; - try discriminate; unfold Pdouble_mask, Pdouble_plus_one_mask in H; - specialize IHp with q. - destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. - destruct (Pminus_mask p q); simpl; auto; try discriminate. - destruct (Pminus_mask_carry p q); simpl; auto; try discriminate. - destruct (Pminus_mask p q); try discriminate; rewrite IHp; auto. -Qed. - -Lemma ZL10 : - forall p q:positive, - Pminus_mask p q = IsPos 1 -> Pminus_mask_carry p q = IsNul. -Proof. - induction p; intros [q|q| ] H; simpl in *; try discriminate. - elim (double_eq_one_discr _ H). - rewrite (double_plus_one_eq_one_inversion _ H); auto. - rewrite (double_plus_one_eq_one_inversion _ H); auto. - elim (double_eq_one_discr _ H). - destruct p; simpl; auto; discriminate. -Qed. - -(** Properties of subtraction valid only for x>y *) - -Lemma Pminus_mask_Gt : - forall p q:positive, - (p ?= q) Eq = Gt -> - exists h : positive, - Pminus_mask p q = IsPos h /\ - q + h = p /\ (h = 1 \/ Pminus_mask_carry p q = IsPos (Ppred h)). -Proof. - induction p as [p IHp| p IHp| ]; intros [q| q| ] H; simpl in *; - try discriminate H. - (* p~1, q~1 *) - destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto. - repeat split; auto; right. - destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. - rewrite ZL10; subst; auto. - rewrite W; simpl; destruct r; auto; elim NE; auto. - (* p~1, q~0 *) - destruct (Pcompare_Gt_Gt _ _ H) as [H'|H']; clear H; rename H' into H. - destruct (IHp q H) as (r & U & V & W); exists (r~1); rewrite ?U, ?V; auto. - exists 1; subst; rewrite Pminus_mask_diag; auto. - (* p~1, 1 *) - exists (p~0); auto. - (* p~0, q~1 *) - destruct (IHp q (Pcompare_Lt_Gt _ _ H)) as (r & U & V & W). - destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. - exists 1; subst; rewrite ZL10, Pplus_one_succ_r; auto. - exists ((Ppred r)~1); rewrite W, Pplus_carry_pred_eq_plus, V; auto. - (* p~0, q~0 *) - destruct (IHp q H) as (r & U & V & W); exists (r~0); rewrite ?U, ?V; auto. - repeat split; auto; right. - destruct (ZL11 r) as [EQ|NE]; [|destruct W as [|W]; [elim NE; auto|]]. - rewrite ZL10; subst; auto. - rewrite W; simpl; destruct r; auto; elim NE; auto. - (* p~0, 1 *) - exists (Pdouble_minus_one p); repeat split; destruct p; simpl; auto. - rewrite Psucc_o_double_minus_one_eq_xO; auto. -Qed. - -Theorem Pplus_minus : - forall p q:positive, (p ?= q) Eq = Gt -> q + (p - q) = p. -Proof. - intros p q H; destruct (Pminus_mask_Gt p q H) as (r & U & V & _). - unfold Pminus; rewrite U; simpl; auto. -Qed. - -(** When x<y, the substraction of x by y returns 1 *) - -Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg. -Proof. - unfold Plt; induction p as [p IHp|p IHp| ]; destruct q; simpl; intros; - try discriminate; try rewrite IHp; auto. - apply Pcompare_Gt_Lt; auto. - destruct (Pcompare_Lt_Lt _ _ H). - rewrite Pminus_mask_IsNeg; simpl; auto. - subst; rewrite Pminus_mask_carry_diag; auto. -Qed. - -Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = 1. -Proof. - intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto. -Qed. - -(** The substraction of x by x returns 1 *) - -Lemma Pminus_Eq : forall p:positive, p-p = 1. -Proof. - intros; unfold Pminus; rewrite Pminus_mask_diag; auto. -Qed. - -(** Number of digits in a number *) - -Fixpoint Psize (p:positive) : nat := - match p with - | 1 => S O - | p~1 => S (Psize p) - | p~0 => S (Psize p) - end. - -Lemma Psize_monotone : forall p q, (p?=q) Eq = Lt -> (Psize p <= Psize q)%nat. -Proof. - assert (le0 : forall n, (0<=n)%nat) by (induction n; auto). - assert (leS : forall n m, (n<=m -> S n <= S m)%nat) by (induction 1; auto). - induction p; destruct q; simpl; auto; intros; try discriminate. - intros; generalize (Pcompare_Gt_Lt _ _ H); auto. - intros; destruct (Pcompare_Lt_Lt _ _ H); auto; subst; auto. -Qed. - - - - - diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 48f78c50..4a5f4ee1 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -1,18 +1,33 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: NArith.v 14641 2011-11-06 11:59:10Z herbelin $ *) - (** Library for binary natural numbers *) +Require Export BinNums. Require Export BinPos. Require Export BinNat. Require Export Nnat. +Require Export Ndiv_def. +Require Export Nsqrt_def. +Require Export Ngcd_def. Require Export Ndigits. - Require Export NArithRing. + +(** [N] contains an [order] tactic for natural numbers *) + +(** Note that [N.order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + +Local Open Scope N_scope. + +Section TestOrder. + Let test : forall x y, x<=y -> y<=x -> x=y. + Proof. + N.order. + Qed. +End TestOrder. diff --git a/theories/NArith/NOrderedType.v b/theories/NArith/NOrderedType.v deleted file mode 100644 index f1ab4b23..00000000 --- a/theories/NArith/NOrderedType.v +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import BinNat Equalities Orders OrdersTac. - -Local Open Scope N_scope. - -(** * DecidableType structure for [N] binary natural numbers *) - -Module N_as_UBE <: UsualBoolEq. - Definition t := N. - Definition eq := @eq N. - Definition eqb := Neqb. - Definition eqb_eq := Neqb_eq. -End N_as_UBE. - -Module N_as_DT <: UsualDecidableTypeFull := Make_UDTF N_as_UBE. - -(** Note that the last module fulfills by subtyping many other - interfaces, such as [DecidableType] or [EqualityType]. *) - - - -(** * OrderedType structure for [N] numbers *) - -Module N_as_OT <: OrderedTypeFull. - Include N_as_DT. - Definition lt := Nlt. - Definition le := Nle. - Definition compare := Ncompare. - - Instance lt_strorder : StrictOrder Nlt. - Proof. split; [ exact Nlt_irrefl | exact Nlt_trans ]. Qed. - - Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Nlt. - Proof. repeat red; intros; subst; auto. Qed. - - Definition le_lteq := Nle_lteq. - Definition compare_spec := Ncompare_spec. - -End N_as_OT. - -(** Note that [N_as_OT] can also be seen as a [UsualOrderedType] - and a [OrderedType] (and also as a [DecidableType]). *) - - - -(** * An [order] tactic for [N] numbers *) - -Module NOrder := OTF_to_OrderTac N_as_OT. -Ltac n_order := NOrder.order. - -(** Note that [n_order] is domain-agnostic: it will not prove - [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) - diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index 0e1c3de0..f2ee29cc 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndec.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Bool. Require Import Sumbool. Require Import Arith. @@ -29,14 +27,14 @@ Proof. intros. now apply (Peqb_eq p p'). Qed. -Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pcompare p p' Eq = Eq. +Lemma Peqb_Pcompare : forall p p', Peqb p p' = true -> Pos.compare p p' = Eq. Proof. - intros. now rewrite Pcompare_eq_iff, <- Peqb_eq. + intros. now rewrite Pos.compare_eq_iff, <- Peqb_eq. Qed. -Lemma Pcompare_Peqb : forall p p', Pcompare p p' Eq = Eq -> Peqb p p' = true. +Lemma Pcompare_Peqb : forall p p', Pos.compare p p' = Eq -> Peqb p p' = true. Proof. - intros; now rewrite Peqb_eq, <- Pcompare_eq_iff. + intros; now rewrite Peqb_eq, <- Pos.compare_eq_iff. Qed. Lemma Neqb_correct : forall n, Neqb n n = true. diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 6b490dfc..b0c33595 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -1,320 +1,253 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndigits.v 14641 2011-11-06 11:59:10Z herbelin $ i*) +Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat + Pnat Nnat Compare_dec Lt Minus. -Require Import Bool. -Require Import Bvector. -Require Import BinPos. -Require Import BinNat. +Local Open Scope N_scope. -(** Operation over bits of a [N] number. *) +(** This file is mostly obsolete, see directly [BinNat] now. *) -(** [xor] *) +(** Compatibility names for some bitwise operations *) -Fixpoint Pxor (p1 p2:positive) : N := - match p1, p2 with - | xH, xH => N0 - | xH, xO p2 => Npos (xI p2) - | xH, xI p2 => Npos (xO p2) - | xO p1, xH => Npos (xI p1) - | xO p1, xO p2 => Ndouble (Pxor p1 p2) - | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2) - | xI p1, xH => Npos (xO p1) - | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2) - | xI p1, xI p2 => Ndouble (Pxor p1 p2) - end. +Notation Pxor := Pos.lxor (only parsing). +Notation Nxor := N.lxor (only parsing). +Notation Pbit := Pos.testbit_nat (only parsing). +Notation Nbit := N.testbit_nat (only parsing). -Definition Nxor (n n':N) := - match n, n' with - | N0, _ => n' - | _, N0 => n - | Npos p, Npos p' => Pxor p p' - end. +Notation Nxor_eq := N.lxor_eq (only parsing). +Notation Nxor_comm := N.lxor_comm (only parsing). +Notation Nxor_assoc := N.lxor_assoc (only parsing). +Notation Nxor_neutral_left := N.lxor_0_l (only parsing). +Notation Nxor_neutral_right := N.lxor_0_r (only parsing). +Notation Nxor_nilpotent := N.lxor_nilpotent (only parsing). -Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n. +(** Equivalence of bit-testing functions, + either with index in [N] or in [nat]. *) + +Lemma Ptestbit_Pbit : + forall p n, Pos.testbit p (N.of_nat n) = Pbit p n. Proof. - trivial. + induction p as [p IH|p IH| ]; intros [|n]; simpl; trivial; + rewrite <- IH; f_equal; rewrite (pred_Sn n) at 2; now rewrite N_of_pred. Qed. -Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n. +Lemma Ntestbit_Nbit : forall a n, N.testbit a (N.of_nat n) = Nbit a n. Proof. - destruct n; trivial. + destruct a. trivial. apply Ptestbit_Pbit. Qed. -Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n. +Lemma Pbit_Ptestbit : + forall p n, Pbit p (N.to_nat n) = Pos.testbit p n. Proof. - destruct n; destruct n'; simpl; auto. - generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl; - auto. - destruct p0; trivial; rewrite Hrecp; trivial. - destruct p0; trivial; rewrite Hrecp; trivial. - destruct p0 as [p| p| ]; simpl; auto. + intros; now rewrite <- Ptestbit_Pbit, N2Nat.id. Qed. -Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0. +Lemma Nbit_Ntestbit : + forall a n, Nbit a (N.to_nat n) = N.testbit a n. Proof. - destruct n; trivial. - simpl. induction p as [p IHp| p IHp| ]; trivial. - simpl. rewrite IHp; reflexivity. - simpl. rewrite IHp; reflexivity. + destruct a. trivial. apply Pbit_Ptestbit. Qed. -(** Checking whether a particular bit is set on not *) - -Fixpoint Pbit (p:positive) : nat -> bool := - match p with - | xH => fun n:nat => match n with - | O => true - | S _ => false - end - | xO p => - fun n:nat => match n with - | O => false - | S n' => Pbit p n' - end - | xI p => fun n:nat => match n with - | O => true - | S n' => Pbit p n' - end - end. +(** Equivalence of shifts, index in [N] or [nat] *) -Definition Nbit (a:N) := - match a with - | N0 => fun _ => false - | Npos p => Pbit p - end. +Lemma Nshiftr_nat_S : forall a n, + N.shiftr_nat a (S n) = N.div2 (N.shiftr_nat a n). +Proof. + reflexivity. +Qed. -(** Auxiliary results about streams of bits *) +Lemma Nshiftl_nat_S : forall a n, + N.shiftl_nat a (S n) = N.double (N.shiftl_nat a n). +Proof. + reflexivity. +Qed. -Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. +Lemma Nshiftr_nat_equiv : + forall a n, N.shiftr_nat a (N.to_nat n) = N.shiftr a n. +Proof. + intros a [|n]; simpl. unfold N.shiftr_nat. + trivial. + symmetry. apply iter_nat_of_P. +Qed. -Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f. +Lemma Nshiftr_equiv_nat : + forall a n, N.shiftr a (N.of_nat n) = N.shiftr_nat a n. Proof. - unfold eqf. intros. rewrite H. reflexivity. + intros. now rewrite <- Nshiftr_nat_equiv, Nat2N.id. Qed. -Lemma eqf_refl : forall f:nat -> bool, eqf f f. +Lemma Nshiftl_nat_equiv : + forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n. Proof. - unfold eqf. trivial. + intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial. + apply nat_iter_invariant; intros; now subst. + rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen. Qed. -Lemma eqf_trans : - forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''. +Lemma Nshiftl_equiv_nat : + forall a n, N.shiftl a (N.of_nat n) = N.shiftl_nat a n. Proof. - unfold eqf. intros. rewrite H. exact (H0 n). + intros. now rewrite <- Nshiftl_nat_equiv, Nat2N.id. Qed. -Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n). +(** Correctness proofs for shifts, nat version *) -Lemma xorf_eq : - forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'. +Lemma Nshiftr_nat_spec : forall a n m, + Nbit (N.shiftr_nat a n) m = Nbit a (m+n). Proof. - unfold eqf, xorf. intros. apply xorb_eq, H. + induction n; intros m. + now rewrite <- plus_n_O. + simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S. + destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial. Qed. -Lemma xorf_assoc : - forall f f' f'', - eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')). +Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> + Nbit (N.shiftl_nat a n) m = Nbit a (m-n). Proof. - unfold eqf, xorf. intros. apply xorb_assoc. + induction n; intros m H. + now rewrite <- minus_n_O. + destruct m. inversion H. apply le_S_n in H. + simpl. rewrite <- IHn, Nshiftl_nat_S; trivial. + destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial. Qed. -Lemma eqf_xorf : - forall f f' f'' f''', - eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f'''). +Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat -> + Nbit (N.shiftl_nat a n) m = false. Proof. - unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity. + induction n; intros m H. inversion H. + rewrite Nshiftl_nat_S. + destruct m. + destruct (N.shiftl_nat a n); trivial. + specialize (IHn m (lt_S_n _ _ H)). + destruct (N.shiftl_nat a n); trivial. Qed. -(** End of auxilliary results *) +(** A left shift for positive numbers (used in BigN) *) + +Lemma Pshiftl_nat_0 : forall p, Pos.shiftl_nat p 0 = p. +Proof. reflexivity. Qed. -(** This part is aimed at proving that if two numbers produce - the same stream of bits, then they are equal. *) +Lemma Pshiftl_nat_S : + forall p n, Pos.shiftl_nat p (S n) = xO (Pos.shiftl_nat p n). +Proof. reflexivity. Qed. -Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a. +Lemma Pshiftl_nat_N : + forall p n, Npos (Pos.shiftl_nat p n) = N.shiftl_nat (Npos p) n. Proof. - destruct a. trivial. - induction p as [p IHp| p IHp| ]; intro H. - absurd (N0 = Npos p). discriminate. - exact (IHp (fun n => H (S n))). - absurd (N0 = Npos p). discriminate. - exact (IHp (fun n => H (S n))). - absurd (false = true). discriminate. - exact (H 0). + unfold Pos.shiftl_nat, N.shiftl_nat. + induction n; simpl; auto. now rewrite <- IHn. Qed. -Lemma Nbit_faithful_2 : - forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a. +Lemma Pshiftl_nat_plus : forall n m p, + Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m. Proof. - destruct a. intros. absurd (true = false). discriminate. - exact (H 0). - destruct p. intro H. absurd (N0 = Npos p). discriminate. - exact (Nbit_faithful_1 (Npos p) (fun n:nat => H (S n))). - intros. absurd (true = false). discriminate. - exact (H 0). - trivial. + induction m; simpl; intros. reflexivity. + rewrite 2 Pshiftl_nat_S. now f_equal. +Qed. + +(** Semantics of bitwise operations with respect to [Nbit] *) + +Lemma Pxor_semantics p p' n : + Nbit (Pos.lxor p p') n = xorb (Pbit p n) (Pbit p' n). +Proof. + rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_lxor_spec. Qed. -Lemma Nbit_faithful_3 : - forall (a:N) (p:positive), - (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> - eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a. +Lemma Nxor_semantics a a' n : + Nbit (N.lxor a a') n = xorb (Nbit a n) (Nbit a' n). Proof. - destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))). - intro. rewrite (Nbit_faithful_1 (Npos (xO p)) H1). reflexivity. - unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity. - destruct p. discriminate (H0 O). - rewrite (H p (fun n => H0 (S n))). reflexivity. - discriminate (H0 0). + rewrite <- !Ntestbit_Nbit. apply N.lxor_spec. Qed. -Lemma Nbit_faithful_4 : - forall (a:N) (p:positive), - (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') -> - eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a. +Lemma Por_semantics p p' n : + Pbit (Pos.lor p p') n = (Pbit p n) || (Pbit p' n). Proof. - destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))). - intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity. - intro. rewrite H0. reflexivity. - destruct p. rewrite (H p (fun n:nat => H0 (S n))). reflexivity. - discriminate (H0 0). - cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))). - intro. discriminate (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))). - intro. rewrite H0. reflexivity. + rewrite <- !Ptestbit_Pbit. apply N.pos_lor_spec. Qed. -Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'. +Lemma Nor_semantics a a' n : + Nbit (N.lor a a') n = (Nbit a n) || (Nbit a' n). Proof. - destruct a. exact Nbit_faithful_1. - induction p. intros a' H. apply Nbit_faithful_4. intros. - assert (Npos p = Npos p') by exact (IHp (Npos p') H0). - inversion H1. reflexivity. - assumption. - intros. apply Nbit_faithful_3. intros. - assert (Npos p = Npos p') by exact (IHp (Npos p') H0). - inversion H1. reflexivity. - assumption. - exact Nbit_faithful_2. + rewrite <- !Ntestbit_Nbit. apply N.lor_spec. Qed. -(** We now describe the semantics of [Nxor] in terms of bit streams. *) +Lemma Pand_semantics p p' n : + Nbit (Pos.land p p') n = (Pbit p n) && (Pbit p' n). +Proof. + rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_land_spec. +Qed. -Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0. +Lemma Nand_semantics a a' n : + Nbit (N.land a a') n = (Nbit a n) && (Nbit a' n). Proof. - trivial. + rewrite <- !Ntestbit_Nbit. apply N.land_spec. Qed. -Lemma Nxor_sem_2 : - forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0). +Lemma Pdiff_semantics p p' n : + Nbit (Pos.ldiff p p') n = (Pbit p n) && negb (Pbit p' n). Proof. - intro. destruct a'. trivial. - destruct p; trivial. + rewrite <- Ntestbit_Nbit, <- !Ptestbit_Pbit. apply N.pos_ldiff_spec. +Qed. + +Lemma Ndiff_semantics a a' n : + Nbit (N.ldiff a a') n = (Nbit a n) && negb (Nbit a' n). +Proof. + rewrite <- !Ntestbit_Nbit. apply N.ldiff_spec. Qed. -Lemma Nxor_sem_3 : - forall (p:positive) (a':N), - Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0. +(** Equality over functional streams of bits *) + +Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n. + +Program Instance eqf_equiv : Equivalence eqf. + +Local Infix "==" := eqf (at level 70, no associativity). + +(** If two numbers produce the same stream of bits, they are equal. *) + +Local Notation Step H := (fun n => H (S n)). + +Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)). Proof. - intros. destruct a'. trivial. - simpl. destruct p0; trivial. - destruct (Pxor p p0); trivial. - destruct (Pxor p p0); trivial. + induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O). + apply (IHp (Step H)). Qed. -Lemma Nxor_sem_4 : - forall (p:positive) (a':N), - Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0). +Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'. Proof. - intros. destruct a'. trivial. - simpl. destruct p0; trivial. - destruct (Pxor p p0); trivial. - destruct (Pxor p p0); trivial. + induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial; + try discriminate (H O). + f_equal. apply (IHp _ (Step H)). + destruct (Pbit_faithful_0 _ (Step H)). + f_equal. apply (IHp _ (Step H)). + symmetry in H. destruct (Pbit_faithful_0 _ (Step H)). Qed. -Lemma Nxor_sem_5 : - forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0. +Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'. Proof. - destruct a; intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial. - destruct p. apply Nxor_sem_4. - change (Nbit (Nxor (Npos (xO p)) a') 0 = xorb false (Nbit a' 0)). - rewrite false_xorb. apply Nxor_sem_3. apply Nxor_sem_2. + intros [|p] [|p'] H; trivial. + symmetry in H. destruct (Pbit_faithful_0 _ H). + destruct (Pbit_faithful_0 _ H). + f_equal. apply Pbit_faithful, H. Qed. -Lemma Nxor_sem_6 : - forall n:nat, - (forall a a':N, Nbit (Nxor a a') n = xorf (Nbit a) (Nbit a') n) -> - forall a a':N, - Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n). +Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'. Proof. - intros. -(* pose proof (fun p1 p2 => H (Npos p1) (Npos p2)) as H'. clear H. rename H' into H.*) - generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H. - unfold xorf in *. - destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity. - destruct a' as [|p0]. - simpl Nbit; rewrite xorb_false. reflexivity. - destruct p. destruct p0; simpl Nbit in *. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite xorb_false. reflexivity. - destruct p0; simpl Nbit in *. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite <- H; simpl; case (Pxor p p0); trivial. - rewrite xorb_false. reflexivity. - simpl Nbit. rewrite false_xorb. destruct p0; trivial. -Qed. - -Lemma Nxor_semantics : - forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')). -Proof. - unfold eqf. intros; generalize a, a'. induction n. - apply Nxor_sem_5. apply Nxor_sem_6; assumption. -Qed. - -(** Consequences: - - only equal numbers lead to a null xor - - xor is associative -*) - -Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'. -Proof. - intros. apply Nbit_faithful, xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')). - apply eqf_sym, Nxor_semantics. - rewrite H. unfold eqf. trivial. -Qed. - -Lemma Nxor_assoc : - forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a''). -Proof. - intros. apply Nbit_faithful. - apply eqf_trans with (xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')). - apply eqf_trans with (xorf (Nbit (Nxor a a')) (Nbit a'')). - apply Nxor_semantics. - apply eqf_xorf. apply Nxor_semantics. - apply eqf_refl. - apply eqf_trans with (xorf (Nbit a) (xorf (Nbit a') (Nbit a''))). - apply xorf_assoc. - apply eqf_trans with (xorf (Nbit a) (Nbit (Nxor a' a''))). - apply eqf_xorf. apply eqf_refl. - apply eqf_sym, Nxor_semantics. - apply eqf_sym, Nxor_semantics. + split. apply Nbit_faithful. intros; now subst. Qed. +Local Close Scope N_scope. + (** Checking whether a number is odd, i.e. if its lower bit is set. *) -Definition Nbit0 (n:N) := - match n with - | N0 => false - | Npos (xO _) => false - | _ => true - end. +Notation Nbit0 := N.odd (only parsing). Definition Nodd (n:N) := Nbit0 n = true. Definition Neven (n:N) := Nbit0 n = false. @@ -363,8 +296,8 @@ Qed. Lemma Nxor_bit0 : forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a'). Proof. - intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' 0). - unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity. + intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O). + rewrite Nbit0_correct, Nbit0_correct. reflexivity. Qed. Lemma Nxor_div2 : @@ -372,7 +305,7 @@ Lemma Nxor_div2 : Proof. intros. apply Nbit_faithful. unfold eqf. intro. rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)). - unfold xorf. rewrite 2! Ndiv2_correct. + rewrite 2! Ndiv2_correct. reflexivity. Qed. @@ -381,7 +314,8 @@ Lemma Nneg_bit0 : Nbit0 (Nxor a a') = true -> Nbit0 a = negb (Nbit0 a'). Proof. intros. - rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, xorb_nilpotent, xorb_false. + rewrite <- true_xorb, <- H, Nxor_bit0, xorb_assoc, + xorb_nilpotent, xorb_false. reflexivity. Qed. @@ -404,7 +338,8 @@ Lemma Nsame_bit0 : Proof. intros. rewrite <- (xorb_false (Nbit0 a)). assert (H0: Nbit0 (Npos (xO p)) = false) by reflexivity. - rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. reflexivity. + rewrite <- H0, <- H, Nxor_bit0, <- xorb_assoc, xorb_nilpotent, false_xorb. + reflexivity. Qed. (** a lexicographic order on bits, starting from the lowest bit *) @@ -511,8 +446,8 @@ Lemma Nless_trans : Nless a a' = true -> Nless a' a'' = true -> Nless a a'' = true. Proof. induction a as [|a IHa|a IHa] using N_ind_double; intros a' a'' H H0. - destruct (Nless N0 a'') as []_eqn:Heqb. trivial. - rewrite (N0_less_2 a'' Heqb), (Nless_z a') in H0. discriminate H0. + case_eq (Nless N0 a'') ; intros Heqn. trivial. + rewrite (N0_less_2 a'' Heqn), (Nless_z a') in H0. discriminate H0. induction a' as [|a' _|a' _] using N_ind_double. rewrite (Nless_z (Ndouble a)) in H. discriminate H. rewrite (Nless_def_1 a a') in H. @@ -539,10 +474,10 @@ Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. induction a using N_rec_double; intro a'. - destruct (Nless N0 a') as []_eqn:Heqb. left. left. auto. + case_eq (Nless N0 a') ; intros Heqb. left. left. auto. right. rewrite (N0_less_2 a' Heqb). reflexivity. induction a' as [|a' _|a' _] using N_rec_double. - destruct (Nless N0 (Ndouble a)) as []_eqn:Heqb. left. right. auto. + case_eq (Nless N0 (Ndouble a)) ; intros Heqb. left. right. auto. right. exact (N0_less_2 _ Heqb). rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. left. assumption. @@ -558,11 +493,7 @@ Qed. (** Number of digits in a number *) -Definition Nsize (n:N) : nat := match n with - | N0 => 0%nat - | Npos p => Psize p - end. - +Notation Nsize := N.size_nat (only parsing). (** conversions between N and bit vectors. *) @@ -581,9 +512,9 @@ Definition N2Bv (n:N) : Bvector (Nsize n) := Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with - | Vnil => N0 - | Vcons false n bv => Ndouble (Bv2N n bv) - | Vcons true n bv => Ndouble_plus_one (Bv2N n bv) + | Vector.nil => N0 + | Vector.cons false n bv => Ndouble (Bv2N n bv) + | Vector.cons true n bv => Ndouble_plus_one (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. @@ -599,13 +530,12 @@ Qed. Lemma Bv2N_Nsize : forall n (bv:Bvector n), Nsize (Bv2N n bv) <= n. Proof. -induction n; intros. -rewrite (V0_eq _ bv); simpl; auto. -rewrite (VSn_eq _ _ bv); simpl. -specialize IHn with (Vtail _ _ bv). -destruct (Vhead _ _ bv); - destruct (Bv2N n (Vtail bool n bv)); - simpl; auto with arith. +induction bv; intros. +auto. +simpl. +destruct h; + destruct (Bv2N n bv); + simpl ; auto with arith. Qed. (** In the previous lemma, we can only replace the inequality by @@ -615,15 +545,10 @@ Lemma Bv2N_Nsize_1 : forall n (bv:Bvector (S n)), Bsign _ bv = true <-> Nsize (Bv2N _ bv) = (S n). Proof. -induction n; intro. -rewrite (VSn_eq _ _ bv); simpl. -rewrite (V0_eq _ (Vtail _ _ bv)); simpl. -destruct (Vhead _ _ bv); simpl; intuition; try discriminate. -rewrite (VSn_eq _ _ bv); simpl. -generalize (IHn (Vtail _ _ bv)); clear IHn. -destruct (Vhead _ _ bv); - destruct (Bv2N (S n) (Vtail bool (S n) bv)); - simpl; intuition; try discriminate. +apply Vector.rectS ; intros ; simpl. +destruct a ; compute ; split ; intros x ; now inversion x. + destruct a, (Bv2N (S n) v) ; + simpl ;intuition ; try discriminate. Qed. (** To state nonetheless a second result about composition of @@ -653,7 +578,7 @@ Qed. [a] plus some zeros. *) Lemma N2Bv_N2Bv_gen_above : forall (a:N)(k:nat), - N2Bv_gen (Nsize a + k) a = Vextend _ _ _ (N2Bv a) (Bvect_false k). + N2Bv_gen (Nsize a + k) a = Vector.append (N2Bv a) (Bvect_false k). Proof. destruct a; simpl. destruct k; simpl; auto. @@ -665,13 +590,13 @@ Qed. Lemma N2Bv_Bv2N : forall n (bv:Bvector n), N2Bv_gen n (Bv2N n bv) = bv. Proof. -induction n; intros. -rewrite (V0_eq _ bv); simpl; auto. -rewrite (VSn_eq _ _ bv); simpl. -generalize (IHn (Vtail _ _ bv)); clear IHn. +induction bv; intros. +auto. +simpl. +generalize IHbv; clear IHbv. unfold Bcons. -destruct (Bv2N _ (Vtail _ _ bv)); - destruct (Vhead _ _ bv); intro H; rewrite <- H; simpl; trivial; +destruct (Bv2N _ bv); + destruct h; intro H; rewrite <- H; simpl; trivial; induction n; simpl; auto. Qed. @@ -680,31 +605,25 @@ Qed. Lemma Nbit0_Blow : forall n, forall (bv:Bvector (S n)), Nbit0 (Bv2N _ bv) = Blow _ bv. Proof. +apply Vector.caseS. intros. unfold Blow. -rewrite (VSn_eq _ _ bv) at 1. simpl. -destruct (Bv2N n (Vtail bool n bv)); simpl; - destruct (Vhead bool n bv); auto. +destruct (Bv2N n t); simpl; + destruct h; auto. Qed. -Definition Bnth (n:nat)(bv:Bvector n)(p:nat) : p<n -> bool. -Proof. - induction bv in p |- *. - intros. - exfalso; inversion H. - intros. - destruct p. - exact a. - apply (IHbv p); auto with arith. -Defined. +Notation Bnth := (@Vector.nth_order bool). Lemma Bnth_Nbit : forall n (bv:Bvector n) p (H:p<n), - Bnth _ bv p H = Nbit (Bv2N _ bv) p. + Bnth bv H = Nbit (Bv2N _ bv) p. Proof. induction bv; intros. inversion H. -destruct p; simpl; destruct (Bv2N n bv); destruct a; simpl in *; auto. +destruct p ; simpl. + destruct (Bv2N n bv); destruct h; simpl in *; auto. + specialize IHbv with p (lt_S_n _ _ H). + simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. Qed. Lemma Nbit_Nsize : forall n p, Nsize n <= p -> Nbit n p = false. @@ -716,26 +635,30 @@ inversion H. inversion H. Qed. -Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth _ (N2Bv n) p H. +Lemma Nbit_Bth: forall n p (H:p < Nsize n), Nbit n p = Bnth (N2Bv n) H. Proof. destruct n as [|n]. inversion H. -induction n; simpl in *; intros; destruct p; auto with arith. -inversion H; inversion H1. +induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. +intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)). Qed. -(** Xor is the same in the two worlds. *) +(** Binary bitwise operations are the same in the two worlds. *) Lemma Nxor_BVxor : forall n (bv bv' : Bvector n), Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv'). Proof. -induction n. -intros. -rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto. -intros. -rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto. -rewrite IHn. -destruct (Vhead bool n bv); destruct (Vhead bool n bv'); - destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto. +apply Vector.rect2 ; intros. +now simpl. +simpl. +destruct a, b, (Bv2N n v1), (Bv2N n v2); simpl in *; rewrite H ; now simpl. Qed. +Lemma Nand_BVand : forall n (bv bv' : Bvector n), + Bv2N _ (BVand _ bv bv') = N.land (Bv2N _ bv) (Bv2N _ bv'). +Proof. +refine (@Vector.rect2 _ _ _ _ _); simpl; intros; auto. +rewrite H. +destruct a, b, (Bv2N n v1), (Bv2N n v2); + simpl; auto. +Qed. diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 586c1114..22adc505 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -1,12 +1,10 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Ndist.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import Arith. Require Import Min. Require Import BinPos. @@ -303,7 +301,7 @@ Proof. cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false). intros. apply H1. reflexivity. intro a''. case a''. intro. reflexivity. - intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). unfold xorf in |- *. + intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) (refl_equal (Nplength (Npos p))) k H0). @@ -335,4 +333,4 @@ Proof. 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 +Qed. diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v new file mode 100644 index 00000000..559f01f1 --- /dev/null +++ b/theories/NArith/Ndiv_def.v @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinNat. +Local Open Scope N_scope. + +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) + +Definition Pdiv_eucl a b := N.pos_div_eucl a (Npos b). + +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). + +Lemma Pdiv_eucl_remainder a b : + snd (Pdiv_eucl a b) < Npos b. +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). + +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 new file mode 100644 index 00000000..13211f46 --- /dev/null +++ b/theories/NArith/Ngcd_def.v @@ -0,0 +1,22 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinPos BinNat. +Local Open Scope N_scope. + +(** 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/Nminmax.v b/theories/NArith/Nminmax.v deleted file mode 100644 index 58184a4f..00000000 --- a/theories/NArith/Nminmax.v +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Orders BinNat Nnat NOrderedType GenericMinMax. - -(** * Maximum and Minimum of two [N] numbers *) - -Local Open Scope N_scope. - -(** The functions [Nmax] and [Nmin] implement indeed - a maximum and a minimum *) - -Lemma Nmax_l : forall x y, y<=x -> Nmax x y = x. -Proof. - unfold Nle, Nmax. intros x y. - generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). - destruct (x ?= y); intuition. -Qed. - -Lemma Nmax_r : forall x y, x<=y -> Nmax x y = y. -Proof. - unfold Nle, Nmax. intros x y. destruct (x ?= y); intuition. -Qed. - -Lemma Nmin_l : forall x y, x<=y -> Nmin x y = x. -Proof. - unfold Nle, Nmin. intros x y. destruct (x ?= y); intuition. -Qed. - -Lemma Nmin_r : forall x y, y<=x -> Nmin x y = y. -Proof. - unfold Nle, Nmin. intros x y. - generalize (Ncompare_eq_correct x y). rewrite <- (Ncompare_antisym x y). - destruct (x ?= y); intuition. -Qed. - -Module NHasMinMax <: HasMinMax N_as_OT. - Definition max := Nmax. - Definition min := Nmin. - Definition max_l := Nmax_l. - Definition max_r := Nmax_r. - Definition min_l := Nmin_l. - Definition min_r := Nmin_r. -End NHasMinMax. - -Module N. - -(** We obtain hence all the generic properties of max and min. *) - -Include UsualMinMaxProperties N_as_OT NHasMinMax. - -(** * Properties specific to the [positive] domain *) - -(** Simplifications *) - -Lemma max_0_l : forall n, Nmax 0 n = n. -Proof. - intros. unfold Nmax. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). - destruct (n ?= 0); intuition. -Qed. - -Lemma max_0_r : forall n, Nmax n 0 = n. -Proof. intros. rewrite N.max_comm. apply max_0_l. Qed. - -Lemma min_0_l : forall n, Nmin 0 n = 0. -Proof. - intros. unfold Nmin. rewrite <- Ncompare_antisym. generalize (Ncompare_0 n). - destruct (n ?= 0); intuition. -Qed. - -Lemma min_0_r : forall n, Nmin n 0 = 0. -Proof. intros. rewrite N.min_comm. apply min_0_l. Qed. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma succ_max_distr : - forall n m, Nsucc (Nmax n m) = Nmax (Nsucc n) (Nsucc m). -Proof. - intros. symmetry. apply max_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. - simpl; auto. -Qed. - -Lemma succ_min_distr : forall n m, Nsucc (Nmin n m) = Nmin (Nsucc n) (Nsucc m). -Proof. - intros. symmetry. apply min_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nsucc. - simpl; auto. -Qed. - -Lemma plus_max_distr_l : forall n m p, Nmax (p + n) (p + m) = p + Nmax n m. -Proof. - intros. apply max_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma plus_max_distr_r : forall n m p, Nmax (n + p) (m + p) = Nmax n m + p. -Proof. - intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). - apply plus_max_distr_l. -Qed. - -Lemma plus_min_distr_l : forall n m p, Nmin (p + n) (p + m) = p + Nmin n m. -Proof. - intros. apply min_monotone. - intros x x'. unfold Nle. - rewrite 2 nat_of_Ncompare, 2 nat_of_Nplus. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma plus_min_distr_r : forall n m p, Nmin (n + p) (m + p) = Nmin n m + p. -Proof. - intros. rewrite (Nplus_comm n p), (Nplus_comm m p), (Nplus_comm _ p). - apply plus_min_distr_l. -Qed. - -End N.
\ No newline at end of file diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index f57fab0f..133d4c23 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -1,370 +1,232 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Nnat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import Arith_base. -Require Import Compare_dec. -Require Import Sumbool. -Require Import Div2. -Require Import Min. -Require Import Max. -Require Import BinPos. -Require Import BinNat. -Require Import BinInt. -Require Import Pnat. -Require Import Zmax. -Require Import Zmin. -Require Import Znat. - -(** 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_Nminus : - forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat. -Proof. - destruct a; destruct a'; simpl; auto with arith. - case_eq (Pcompare p p0 Eq); simpl; intros. - rewrite (Pcompare_Eq_eq _ _ H); auto with arith. - rewrite Pminus_mask_diag. simpl. apply minus_n_n. - rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl. - symmetry; apply not_le_minus_0. auto with arith. assumption. - pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl. - replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1). - apply nat_of_P_minus_morphism; auto. -Qed. - -Lemma N_of_minus : - forall n n', N_of_nat (n-n') = Nminus (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_Nminus. - 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. +Require Import Arith_base Compare_dec Sumbool Div2 Min Max. +Require Import BinPos BinNat Pnat. -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. - reflexivity. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. - destruct nat_of_P; [inversion NZ|auto]. - apply nat_of_P_compare_morphism. -Qed. +(** * Conversions from [N] to [nat] *) -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. +Module N2Nat. -Lemma nat_of_Nmin : - forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). -Proof. - intros; unfold Nmin; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply min_l; rewrite e; auto with arith. -Qed. +(** [N.to_nat] is a bijection between [N] and [nat], + with [Pos.of_nat] as reciprocal. + See [Nat2N.id] below for the dual equation. *) -Lemma N_of_min : - forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n'). +Lemma id a : N.of_nat (N.to_nat a) = a. 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_Nmin. - apply N_of_nat_of_N. + destruct a as [| p]; simpl; trivial. + destruct (Pos2Nat.is_succ p) as (n,H). rewrite H. simpl. f_equal. + apply Pos2Nat.inj. rewrite H. apply SuccNat2Pos.id_succ. Qed. -Lemma nat_of_Nmax : - forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). -Proof. - intros; unfold Nmax; rewrite nat_of_Ncompare. - rewrite nat_compare_equiv; unfold nat_compare_alt. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; - simpl; intros; symmetry; auto with arith. - apply max_r; rewrite e; auto with arith. -Qed. +(** [N.to_nat] is hence injective *) -Lemma N_of_max : - forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n'). +Lemma inj a a' : N.to_nat a = N.to_nat a' -> a = a'. 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_Nmax. - apply N_of_nat_of_N. + intro H. rewrite <- (id a), <- (id a'). now f_equal. Qed. -(** Properties concerning [Z_of_N] *) - -Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n. +Lemma inj_iff a a' : N.to_nat a = N.to_nat a' <-> a = a'. Proof. - destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P. + split. apply inj. intros; now subst. Qed. -Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m. -Proof. - intros; f_equal; assumption. -Qed. +(** Interaction of this translation and usual operations. *) -Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m. +Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a). Proof. - intros [|n] [|m]; simpl; intros; try discriminate; congruence. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xO. Qed. -Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m. +Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a)). Proof. - split; [apply Z_of_N_eq | apply Z_of_N_eq_rev]. + destruct a; simpl N.to_nat; trivial. apply Pos2Nat.inj_xI. Qed. -Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z. +Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a). Proof. - intros [|n] [|m]; simpl; auto. + destruct a; simpl; trivial. apply Pos2Nat.inj_succ. Qed. -Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N. +Lemma inj_add a a' : + N.to_nat (a + a') = N.to_nat a + N.to_nat a'. Proof. - intros [|n] [|m]; simpl; auto. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_add. Qed. -Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z. +Lemma inj_mul a a' : + N.to_nat (a * a') = N.to_nat a * N.to_nat a'. Proof. - split; [apply Z_of_N_le | apply Z_of_N_le_rev]. + destruct a, a'; simpl; trivial. apply Pos2Nat.inj_mul. Qed. -Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z. +Lemma inj_sub a a' : + N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. - intros [|n] [|m]; simpl; auto. + destruct a as [|a], a' as [|a']; simpl; auto with arith. + destruct (Pos.compare_spec a a'). + subst. now rewrite Pos.sub_mask_diag, <- minus_n_n. + rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. + simpl; symmetry; apply not_le_minus_0; auto with arith. + destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). + simpl. apply plus_minus. now rewrite <- Hq, Pos2Nat.inj_add. Qed. -Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N. +Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a). Proof. - intros [|n] [|m]; simpl; auto. + intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub. Qed. -Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z. +Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a). Proof. - split; [apply Z_of_N_lt | apply Z_of_N_lt_rev]. + destruct a as [|[p|p| ]]; trivial. + simpl N.to_nat. now rewrite Pos2Nat.inj_xI, div2_double_plus_one. + simpl N.to_nat. now rewrite Pos2Nat.inj_xO, div2_double. Qed. -Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z. +Lemma inj_compare a a' : + (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a'). Proof. - intros [|n] [|m]; simpl; auto. + destruct a, a'; simpl; trivial. + now destruct (Pos2Nat.is_succ p) as (n,->). + now destruct (Pos2Nat.is_succ p) as (n,->). + apply Pos2Nat.inj_compare. Qed. -Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N. +Lemma inj_max a a' : + N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a'). Proof. - intros [|n] [|m]; simpl; auto. + unfold N.max. rewrite inj_compare; symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z. +Lemma inj_min a a' : + N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a'). Proof. - split; [apply Z_of_N_ge | apply Z_of_N_ge_rev]. + unfold N.min; rewrite inj_compare. symmetry. + case nat_compare_spec; intros H; try rewrite H; auto with arith. Qed. -Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z. +Lemma inj_iter a {A} (f:A->A) (x:A) : + N.iter a f x = nat_iter (N.to_nat a) f x. Proof. - intros [|n] [|m]; simpl; auto. + destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. -Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N. -Proof. - intros [|n] [|m]; simpl; auto. -Qed. +End N2Nat. -Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z. -Proof. - split; [apply Z_of_N_gt | apply Z_of_N_gt_rev]. -Qed. +Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double + N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub + N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min + N2Nat.id + : Nnat. -Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n. -Proof. - destruct n; simpl; auto. -Qed. -Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p. -Proof. - destruct p; simpl; auto. -Qed. +(** * Conversions from [nat] to [N] *) -Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z. -Proof. - destruct z; simpl; auto. -Qed. +Module Nat2N. -Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z. -Proof. - destruct n; intro; discriminate. -Qed. +(** [N.of_nat] is an bijection between [nat] and [N], + with [Pos.to_nat] as reciprocal. + See [N2Nat.id] above for the dual equation. *) -Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z. +Lemma id n : N.to_nat (N.of_nat n) = n. Proof. - destruct n; destruct m; auto. + induction n; simpl; trivial. apply SuccNat2Pos.id_succ. Qed. -Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z. -Proof. - destruct n; destruct m; auto. -Qed. +Hint Rewrite id : Nnat. +Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat. -Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). -Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus. -Qed. +(** [N.of_nat] is hence injective *) -Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). +Lemma inj n n' : N.of_nat n = N.of_nat n' -> n = n'. Proof. - intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S. + intros H. rewrite <- (id n), <- (id n'). now f_equal. Qed. -Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). +Lemma inj_iff n n' : N.of_nat n = N.of_nat n' <-> n = n'. Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min. + split. apply inj. intros; now subst. Qed. -Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). -Proof. - intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max. -Qed. +(** Interaction of this translation and usual operations. *) +Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_pred n : N.of_nat (pred n) = N.pred (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N. +Proof. nat2N. Qed. + +Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N. +Proof. nat2N. Qed. + +Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N. +Proof. nat2N. Qed. + +Lemma inj_div2 n : N.of_nat (div2 n) = N.div2 (N.of_nat n). +Proof. nat2N. Qed. + +Lemma inj_compare n n' : + nat_compare n n' = (N.of_nat n ?= N.of_nat n')%N. +Proof. now rewrite N2Nat.inj_compare, !id. Qed. + +Lemma inj_min n n' : + N.of_nat (min n n') = N.min (N.of_nat n) (N.of_nat n'). +Proof. nat2N. Qed. + +Lemma inj_max n n' : + N.of_nat (max n n') = N.max (N.of_nat n) (N.of_nat n'). +Proof. nat2N. Qed. + +Lemma inj_iter n {A} (f:A->A) (x:A) : + nat_iter n f x = N.iter (N.of_nat n) f x. +Proof. now rewrite N2Nat.inj_iter, !id. Qed. + +End Nat2N. + +Hint Rewrite Nat2N.id : Nnat. + +(** Compatibility notations *) + +Notation nat_of_N_inj := N2Nat.inj (only parsing). +Notation N_of_nat_of_N := N2Nat.id (only parsing). +Notation nat_of_Ndouble := N2Nat.inj_double (only parsing). +Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing). +Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing). +Notation nat_of_Nplus := N2Nat.inj_add (only parsing). +Notation nat_of_Nmult := N2Nat.inj_mul (only parsing). +Notation nat_of_Nminus := N2Nat.inj_sub (only parsing). +Notation nat_of_Npred := N2Nat.inj_pred (only parsing). +Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing). +Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing). +Notation nat_of_Nmax := N2Nat.inj_max (only parsing). +Notation nat_of_Nmin := N2Nat.inj_min (only parsing). + +Notation nat_of_N_of_nat := Nat2N.id (only parsing). +Notation N_of_nat_inj := Nat2N.inj (only parsing). +Notation N_of_double := Nat2N.inj_double (only parsing). +Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing). +Notation N_of_S := Nat2N.inj_succ (only parsing). +Notation N_of_pred := Nat2N.inj_pred (only parsing). +Notation N_of_plus := Nat2N.inj_add (only parsing). +Notation N_of_minus := Nat2N.inj_sub (only parsing). +Notation N_of_mult := Nat2N.inj_mul (only parsing). +Notation N_of_div2 := Nat2N.inj_div2 (only parsing). +Notation N_of_nat_compare := Nat2N.inj_compare (only parsing). +Notation N_of_min := Nat2N.inj_min (only parsing). +Notation N_of_max := Nat2N.inj_max (only parsing). diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v new file mode 100644 index 00000000..edb6b289 --- /dev/null +++ b/theories/NArith/Nsqrt_def.v @@ -0,0 +1,18 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import BinNat. + +(** Obsolete file, see [BinNat] now, + only compatibility notations remain here. *) + +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). diff --git a/theories/NArith/POrderedType.v b/theories/NArith/POrderedType.v deleted file mode 100644 index 0ff03c31..00000000 --- a/theories/NArith/POrderedType.v +++ /dev/null @@ -1,60 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import BinPos Equalities Orders OrdersTac. - -Local Open Scope positive_scope. - -(** * DecidableType structure for [positive] numbers *) - -Module Positive_as_UBE <: UsualBoolEq. - Definition t := positive. - Definition eq := @eq positive. - Definition eqb := Peqb. - Definition eqb_eq := Peqb_eq. -End Positive_as_UBE. - -Module Positive_as_DT <: UsualDecidableTypeFull - := Make_UDTF Positive_as_UBE. - -(** Note that the last module fulfills by subtyping many other - interfaces, such as [DecidableType] or [EqualityType]. *) - - - -(** * OrderedType structure for [positive] numbers *) - -Module Positive_as_OT <: OrderedTypeFull. - Include Positive_as_DT. - Definition lt := Plt. - Definition le := Ple. - Definition compare p q := Pcompare p q Eq. - - Instance lt_strorder : StrictOrder Plt. - Proof. split; [ exact Plt_irrefl | exact Plt_trans ]. Qed. - - Instance lt_compat : Proper (Logic.eq==>Logic.eq==>iff) Plt. - Proof. repeat red; intros; subst; auto. Qed. - - Definition le_lteq := Ple_lteq. - Definition compare_spec := Pcompare_spec. - -End Positive_as_OT. - -(** Note that [Positive_as_OT] can also be seen as a [UsualOrderedType] - and a [OrderedType] (and also as a [DecidableType]). *) - - - -(** * An [order] tactic for positive numbers *) - -Module PositiveOrder := OTF_to_OrderTac Positive_as_OT. -Ltac p_order := PositiveOrder.order. - -(** Note that [p_order] is domain-agnostic: it will not prove - [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v deleted file mode 100644 index 6bac033c..00000000 --- a/theories/NArith/Pminmax.v +++ /dev/null @@ -1,126 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Orders BinPos Pnat POrderedType GenericMinMax. - -(** * Maximum and Minimum of two positive numbers *) - -Local Open Scope positive_scope. - -(** The functions [Pmax] and [Pmin] implement indeed - a maximum and a minimum *) - -Lemma Pmax_l : forall x y, y<=x -> Pmax x y = x. -Proof. - unfold Ple, Pmax. intros x y. - rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). - destruct ((x ?= y) Eq); intuition. -Qed. - -Lemma Pmax_r : forall x y, x<=y -> Pmax x y = y. -Proof. - unfold Ple, Pmax. intros x y. destruct ((x ?= y) Eq); intuition. -Qed. - -Lemma Pmin_l : forall x y, x<=y -> Pmin x y = x. -Proof. - unfold Ple, Pmin. intros x y. destruct ((x ?= y) Eq); intuition. -Qed. - -Lemma Pmin_r : forall x y, y<=x -> Pmin x y = y. -Proof. - unfold Ple, Pmin. intros x y. - rewrite (ZC4 y x). generalize (Pcompare_eq_iff x y). - destruct ((x ?= y) Eq); intuition. -Qed. - -Module PositiveHasMinMax <: HasMinMax Positive_as_OT. - Definition max := Pmax. - Definition min := Pmin. - Definition max_l := Pmax_l. - Definition max_r := Pmax_r. - Definition min_l := Pmin_l. - Definition min_r := Pmin_r. -End PositiveHasMinMax. - - -Module P. -(** We obtain hence all the generic properties of max and min. *) - -Include UsualMinMaxProperties Positive_as_OT PositiveHasMinMax. - -(** * Properties specific to the [positive] domain *) - -(** Simplifications *) - -Lemma max_1_l : forall n, Pmax 1 n = n. -Proof. - intros. unfold Pmax. rewrite ZC4. generalize (Pcompare_1 n). - destruct (n ?= 1); intuition. -Qed. - -Lemma max_1_r : forall n, Pmax n 1 = n. -Proof. intros. rewrite P.max_comm. apply max_1_l. Qed. - -Lemma min_1_l : forall n, Pmin 1 n = 1. -Proof. - intros. unfold Pmin. rewrite ZC4. generalize (Pcompare_1 n). - destruct (n ?= 1); intuition. -Qed. - -Lemma min_1_r : forall n, Pmin n 1 = 1. -Proof. intros. rewrite P.min_comm. apply min_1_l. Qed. - -(** Compatibilities (consequences of monotonicity) *) - -Lemma succ_max_distr : - forall n m, Psucc (Pmax n m) = Pmax (Psucc n) (Psucc m). -Proof. - intros. symmetry. apply max_monotone. - intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. - simpl; auto. -Qed. - -Lemma succ_min_distr : forall n m, Psucc (Pmin n m) = Pmin (Psucc n) (Psucc m). -Proof. - intros. symmetry. apply min_monotone. - intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_succ_morphism. - simpl; auto. -Qed. - -Lemma plus_max_distr_l : forall n m p, Pmax (p + n) (p + m) = p + Pmax n m. -Proof. - intros. apply max_monotone. - intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma plus_max_distr_r : forall n m p, Pmax (n + p) (m + p) = Pmax n m + p. -Proof. - intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). - apply plus_max_distr_l. -Qed. - -Lemma plus_min_distr_l : forall n m p, Pmin (p + n) (p + m) = p + Pmin n m. -Proof. - intros. apply min_monotone. - intros x x'. unfold Ple. - rewrite 2 nat_of_P_compare_morphism, 2 nat_of_P_plus_morphism. - rewrite <- 2 Compare_dec.nat_compare_le. auto with arith. -Qed. - -Lemma plus_min_distr_r : forall n m p, Pmin (n + p) (m + p) = Pmin n m + p. -Proof. - intros. rewrite (Pplus_comm n p), (Pplus_comm m p), (Pplus_comm _ p). - apply plus_min_distr_l. -Qed. - -End P.
\ No newline at end of file diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v deleted file mode 100644 index 29641dbe..00000000 --- a/theories/NArith/Pnat.v +++ /dev/null @@ -1,462 +0,0 @@ -(* -*- coding: utf-8 -*- *) -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(*i $Id: Pnat.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - -Require Import BinPos. - -(**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano - natural numbers *) - -(** Original development by Pierre Crégut, CNET, Lannion, France *) - -Require Import Le. -Require Import Lt. -Require Import Gt. -Require Import Plus. -Require Import Mult. -Require Import Minus. -Require Import Compare_dec. - -Local Open Scope positive_scope. -Local Open Scope nat_scope. - -(** [nat_of_P] is a morphism for addition *) - -Lemma Pmult_nat_succ_morphism : - forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n. -Proof. -intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m; - rewrite IHp; rewrite plus_assoc; trivial. -Qed. - -Lemma nat_of_P_succ_morphism : - forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p). -Proof. - intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *; - unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism. -Qed. - -Theorem Pmult_nat_plus_carry_morphism : - forall (p q:positive) (n:nat), - Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n. -Proof. -intro x; induction x as [p IHp| p IHp| ]; intro y; - [ destruct y as [p0| p0| ] - | destruct y as [p0| p0| ] - | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; - intro m; - [ rewrite IHp; rewrite plus_assoc; trivial with arith - | rewrite IHp; rewrite plus_assoc; trivial with arith - | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith - | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. -Qed. - -Theorem nat_of_P_plus_carry_morphism : - forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)). -Proof. -intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism; - simpl in |- *; trivial with arith. -Qed. - -Theorem Pmult_nat_l_plus_morphism : - forall (p q:positive) (n:nat), - Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n. -Proof. -intro x; induction x as [p IHp| p IHp| ]; intro y; - [ destruct y as [p0| p0| ] - | destruct y as [p0| p0| ] - | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; - [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp; - rewrite plus_assoc_reverse; rewrite plus_assoc_reverse; - rewrite (plus_permute m (Pmult_nat p (m + m))); - trivial with arith - | intros m; rewrite IHp; apply plus_assoc - | intros m; rewrite Pmult_nat_succ_morphism; - rewrite (plus_comm (m + Pmult_nat p (m + m))); - apply plus_assoc_reverse - | intros m; rewrite IHp; apply plus_permute - | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ]. -Qed. - -Theorem nat_of_P_plus_morphism : - forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q. -Proof. -intros x y; exact (Pmult_nat_l_plus_morphism x y 1). -Qed. - -(** [Pmult_nat] is a morphism for addition *) - -Lemma Pmult_nat_r_plus_morphism : - forall (p:positive) (n:nat), - Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. -Proof. -intro y; induction y as [p H| p H| ]; intro m; - [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse; - rewrite (plus_permute m (Pmult_nat p (m + m))); - rewrite plus_assoc_reverse; auto with arith - | simpl in |- *; rewrite H; auto with arith - | simpl in |- *; trivial with arith ]. -Qed. - -Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p. -Proof. -intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism; - trivial. -Qed. - -(** [nat_of_P] is a morphism for multiplication *) - -Theorem nat_of_P_mult_morphism : - forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q. -Proof. -intros x y; induction x as [x' H| x' H| ]; - [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *; - rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *; - simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r; - reflexivity - | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H; - rewrite mult_plus_distr_r; reflexivity - | simpl in |- *; rewrite <- plus_n_O; reflexivity ]. -Qed. - -(** [nat_of_P] maps to the strictly positive subset of [nat] *) - -Lemma ZL4 : forall p:positive, exists h : nat, nat_of_P p = S h. -Proof. -intro y; induction y as [p H| p H| ]; - [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; - simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; - rewrite H1; auto with arith - | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *; - simpl in |- *; change 2 with (1 + 1) in |- *; - rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; - rewrite H2; auto with arith - | exists 0; auto with arith ]. -Qed. - -(** Extra lemmas on [lt] on Peano natural numbers *) - -Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m. -Proof. -intros m n H; apply lt_trans with (m := m + n); - [ apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. -Qed. - -Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. -Proof. -intros m n H; apply le_lt_trans with (m := m + n); - [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H) - | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ]. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 1: [lt] on [positive] is finer than [lt] on [nat] -*) - -Lemma nat_of_P_lt_Lt_compare_morphism : - forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q. -Proof. -intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; - intro H2; - [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6; - apply ZL7; apply H; simpl in H2; assumption - | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8; - apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption - | simpl in |- *; discriminate H2 - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - elim (Pcompare_Lt_Lt p q H2); - [ intros H3; apply lt_S; apply ZL7; apply H; apply H3 - | intros E; rewrite E; apply lt_n_Sn ] - | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; - apply ZL7; apply H; assumption - | simpl in |- *; discriminate H2 - | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6; - elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; - apply lt_O_Sn - | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q); - intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm; - apply lt_n_S; apply lt_O_Sn - | simpl in |- *; discriminate H2 ]. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 1: [gt] on [positive] is finer than [gt] on [nat] -*) - -Lemma nat_of_P_gt_Gt_compare_morphism : - forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q. -Proof. -intros p q GT. unfold gt. -apply nat_of_P_lt_Lt_compare_morphism. -change ((q ?= p) (CompOpp Eq) = CompOpp Gt). -rewrite <- Pcompare_antisym, GT; auto. -Qed. - -(** [nat_of_P] is a morphism for [Pcompare] and [nat_compare] *) - -Lemma nat_of_P_compare_morphism : forall p q, - (p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q). -Proof. - intros p q; symmetry. - destruct ((p ?= q) Eq) as [ | | ]_eqn. - rewrite (Pcompare_Eq_eq p q); auto. - apply <- nat_compare_eq_iff; auto. - apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto. - apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto. -Qed. - -(** [nat_of_P] is hence injective. *) - -Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. -Proof. -intros. -apply Pcompare_Eq_eq. -rewrite nat_of_P_compare_morphism. -apply <- nat_compare_eq_iff; auto. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) - - Part 2: [lt] on [nat] is finer than [lt] on [positive] -*) - -Lemma nat_of_P_lt_Lt_compare_complement_morphism : - forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt. -Proof. - intros. rewrite nat_of_P_compare_morphism. - apply -> nat_compare_lt; auto. -Qed. - -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) - - Part 2: [gt] on [nat] is finer than [gt] on [positive] -*) - -Lemma nat_of_P_gt_Gt_compare_complement_morphism : - forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt. -Proof. - intros. rewrite nat_of_P_compare_morphism. - apply -> nat_compare_gt; auto. -Qed. - - -(** [nat_of_P] is strictly positive *) - -Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n. -induction p; simpl in |- *; auto with arith. -intro m; apply le_trans with (m + m); auto with arith. -Qed. - -Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p. -intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith. -apply le_Pmult_nat. -Qed. - -(** Pmult_nat permutes with multiplication *) - -Lemma Pmult_nat_mult_permute : - forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n. -Proof. - simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n). - rewrite (H (n + n) m). reflexivity. - intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H. - trivial. -Qed. - -Lemma Pmult_nat_2_mult_2_permute : - forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. -Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. -Qed. - -Lemma Pmult_nat_4_mult_2_permute : - forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. -Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. -Qed. - -(** Mapping of xH, xO and xI through [nat_of_P] *) - -Lemma nat_of_P_xH : nat_of_P 1 = 1. -Proof. - reflexivity. -Qed. - -Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. -Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism. - f_equal. -Qed. - -Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p). -Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism. - f_equal. -Qed. - -(**********************************************************************) -(** Properties of the shifted injection from Peano natural numbers to - binary positive numbers *) - -(** Composition of [P_of_succ_nat] and [nat_of_P] is successor on [nat] *) - -Theorem nat_of_P_o_P_of_succ_nat_eq_succ : - forall n:nat, nat_of_P (P_of_succ_nat n) = S n. -Proof. -induction n as [|n H]. -reflexivity. -simpl; rewrite nat_of_P_succ_morphism, H; auto. -Qed. - -(** Miscellaneous lemmas on [P_of_succ_nat] *) - -Lemma ZL3 : - forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n). -Proof. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite plus_comm; simpl; rewrite H; - rewrite xO_succ_permute; auto with arith ]. -Qed. - -Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n). -Proof. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; - auto with arith ]. -Qed. - -(** Composition of [nat_of_P] and [P_of_succ_nat] is successor on [positive] *) - -Theorem P_of_succ_nat_o_nat_of_P_eq_succ : - forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p. -Proof. -intros. -apply nat_of_P_inj. -rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto. -Qed. - -(** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity - on [positive] *) - -Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id : - forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p. -Proof. -intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto. -Qed. - -(**********************************************************************) -(** Extra properties of the injection from binary positive numbers to Peano - natural numbers *) - -(** [nat_of_P] is a morphism for subtraction on positive numbers *) - -Theorem nat_of_P_minus_morphism : - forall p q:positive, - (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. -Proof. -intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r; - [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith - | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ]. -Qed. - - -Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p. -Proof. -intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1; - rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; - apply le_minus. -Qed. - -Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q). -Proof. -intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q); - intros k H; rewrite H; rewrite plus_comm; simpl in |- *; - apply le_n_S; apply le_plus_r. -Qed. - -(** Comparison and subtraction *) - -Lemma Pcompare_minus_r : - forall p q r:positive, - (q ?= p) Eq = Lt -> - (r ?= p) Eq = Gt -> - (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt. -Proof. -intros; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r; - [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p); - rewrite plus_assoc; rewrite le_plus_minus_r; - [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l; - apply nat_of_P_lt_Lt_compare_morphism; - assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -Lemma Pcompare_minus_l : - forall p q r:positive, - (q ?= p) Eq = Lt -> - (p ?= r) Eq = Gt -> - (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt. -Proof. -intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z); - rewrite le_plus_minus_r; - [ rewrite le_plus_minus_r; - [ apply nat_of_P_lt_Lt_compare_morphism; assumption - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; - apply ZC1; assumption ] - | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; - assumption ] - | assumption ] - | assumption ]. -Qed. - -(** Distributivity of multiplication over subtraction *) - -Theorem Pmult_minus_distr_l : - forall p q r:positive, - (q ?= r) Eq = Gt -> - (p * (q - r) = p * q - p * r)%positive. -Proof. -intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism; - rewrite nat_of_P_minus_morphism; - [ rewrite nat_of_P_minus_morphism; - [ do 2 rewrite nat_of_P_mult_morphism; - do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r - | apply nat_of_P_gt_Gt_compare_complement_morphism; - do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; - elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l; - exact (nat_of_P_gt_Gt_compare_morphism y z H) ] - | assumption ]. -Qed. diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex index 83eed970..bf39bc36 100644 --- a/theories/NArith/intro.tex +++ b/theories/NArith/intro.tex @@ -1,4 +1,4 @@ -\section{Binary positive and non negative integers : NArith}\label{NArith} +\section{Binary natural numbers : NArith}\label{NArith} Here are defined various arithmetical notions and their properties, similar to those of {\tt Arith}. diff --git a/theories/NArith/vo.itarget b/theories/NArith/vo.itarget index 32f94f01..e76033f7 100644 --- a/theories/NArith/vo.itarget +++ b/theories/NArith/vo.itarget @@ -1,12 +1,10 @@ +BinNatDef.vo BinNat.vo -BinPos.vo NArith.vo Ndec.vo Ndigits.vo Ndist.vo Nnat.vo -Pnat.vo -POrderedType.vo -Pminmax.vo -NOrderedType.vo -Nminmax.vo +Ndiv_def.vo +Nsqrt_def.vo +Ngcd_def.vo
\ No newline at end of file |