diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 23:51:06 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-16 23:51:06 +0000 |
commit | 286d7e8201de98dc5cc36b6fbda8f9c1126f37ea (patch) | |
tree | 1ec5317554f488d8abd722e66a7d341d6cf521f1 /theories/NArith/BinNat.v | |
parent | 99ad573113f5afc8bb5409649843567dee40ba40 (diff) |
Definition of N moves back to BinNat (partial backtrack of commits 10298-10300)
This way, no more references to NBinDefs.N when doing "Print N".
Long-term migration to theories/Numbers is still planned, but it needs
more works, for instance to adapt both positive and N and Z at once.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/BinNat.v')
-rw-r--r-- | theories/NArith/BinNat.v | 453 |
1 files changed, 336 insertions, 117 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 9949d612d..b704f3d37 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -5,71 +5,194 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Evgeny Makarov, INRIA, 2007 *) -(************************************************************************) -(*i i*) +(*i $Id$ i*) Require Import BinPos. -Require Import NBinDefs. +Unset Boxed Definitions. + +(**********************************************************************) +(** Binary natural numbers *) + +Inductive N : Set := + | N0 : N + | Npos : positive -> N. -(*Unset Boxed Definitions.*) +(** Declare binding key for scope positive_scope *) Delimit Scope N_scope with N. + +(** Automatically open scope positive_scope for the constructors of N *) + Bind Scope N_scope with N. +Arguments Scope Npos [positive_scope]. + Open Local Scope N_scope. -(** Operations *) - -Notation N := N (only parsing). -Notation N0 := N0 (only parsing). -Notation Npos := Npos (only parsing). -Notation Nsucc := succ (only parsing). -Notation Npred := pred (only parsing). -Notation Nplus := plus (only parsing). -Notation Nminus := minus (only parsing). -Notation Nmult := times (only parsing). -Notation Ncompare := Ncompare (only parsing). -Notation Nlt := lt (only parsing). -Notation Nle := le (only parsing). -Definition Ngt (x y : N) := (Ncompare x y) = Gt. -Definition Nge (x y : N) := (Ncompare x y) <> Lt. -Notation Nmin := min (only parsing). -Notation Nmax := max (only parsing). - -(* If the notations for operations above had been actual definitions, the -arguments scopes would have been N_scope due to the instruction "Bind Scope -N_scope with N". However, the operations were declared in NBinary, where -N_scope has not yet been declared. Therefore, we need to assign the -arguments scopes manually. Note that this has to be done before declaring -infix notations below. Ngt and Nge get their scope from the definition. *) - -Arguments Scope succ [N_scope]. -Arguments Scope pred [N_scope]. -Arguments Scope plus [N_scope N_scope]. -Arguments Scope minus [N_scope N_scope]. -Arguments Scope times [N_scope N_scope]. -Arguments Scope NBinDefs.Ncompare [N_scope N_scope]. -Arguments Scope lt [N_scope N_scope]. -Arguments Scope le [N_scope N_scope]. -Arguments Scope min [N_scope N_scope]. -Arguments Scope max [N_scope N_scope]. +Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }. +Proof. + destruct n; auto. + left; exists p; auto. +Defined. + +(** Operation x -> 2*x+1 *) + +Definition Ndouble_plus_one x := + match x with + | N0 => Npos 1 + | Npos p => Npos (xI p) + end. + +(** Operation x -> 2*x *) + +Definition Ndouble n := + match n with + | N0 => N0 + | Npos p => Npos (xO p) + end. + +(** Successor *) + +Definition Nsucc n := + match n with + | N0 => Npos 1 + | Npos p => Npos (Psucc p) + end. + +(** Predecessor *) + +Definition Npred (n : N) := match n with +| N0 => N0 +| Npos p => match p with + | xH => N0 + | _ => Npos (Ppred p) + end +end. + +(** Addition *) + +Definition Nplus n m := + match n, m with + | N0, _ => m + | _, N0 => n + | Npos p, Npos q => Npos (p + q) + end. Infix "+" := Nplus : N_scope. + +(** Subtraction *) + +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. + Infix "-" := Nminus : N_scope. + +(** Multiplication *) + +Definition Nmult n m := + match n, m with + | N0, _ => N0 + | _, N0 => N0 + | Npos p, Npos q => Npos (p * q) + end. + Infix "*" := Nmult : N_scope. + +(** Order *) + +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. + Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. + +Definition Nlt (x y:N) := (x ?= y) = Lt. +Definition Ngt (x y:N) := (x ?= y) = Gt. +Definition Nle (x y:N) := (x ?= y) <> Gt. +Definition Nge (x y:N) := (x ?= y) <> Lt. + Infix "<=" := Nle : N_scope. Infix "<" := Nlt : N_scope. Infix ">=" := Nge : N_scope. Infix ">" := Ngt : N_scope. -(** Peano induction and recursion *) +(** Min and max *) + +Definition Nmin (n n' : N) := match Ncompare n n' with + | Lt | Eq => n + | Gt => n' + end. + +Definition Nmax (n n' : N) := match Ncompare n n' with + | Lt | Eq => n' + | Gt => n + end. + +(** convenient induction principles *) + +Lemma N_ind_double : + forall (a:N) (P:N -> Prop), + P N0 -> + (forall a, P a -> P (Ndouble a)) -> + (forall a, P a -> P (Ndouble_plus_one a)) -> P a. +Proof. + intros; elim a. trivial. + simple induction p. intros. + apply (H1 (Npos p0)); trivial. + intros; apply (H0 (Npos p0)); trivial. + intros; apply (H1 N0); assumption. +Qed. + +Lemma N_rec_double : + forall (a:N) (P:N -> Set), + P N0 -> + (forall a, P a -> P (Ndouble a)) -> + (forall a, P a -> P (Ndouble_plus_one a)) -> P a. +Proof. + intros; elim a. trivial. + simple induction p. intros. + apply (H1 (Npos p0)); trivial. + intros; apply (H0 (Npos p0)); trivial. + intros; apply (H1 N0); assumption. +Qed. + +(** Peano induction on binary natural numbers *) + +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. + +Theorem Nrect_base : forall P a f, Nrect P a f N0 = a. +Proof. +intros P a f; simpl; reflexivity. +Qed. + +Theorem Nrect_step : forall P a f n, Nrect P a f (Nsucc n) = f n (Nrect P a f n). +Proof. +intros P a f; destruct n as [| p]; simpl; +[rewrite Prect_base | rewrite Prect_succ]; reflexivity. +Qed. -Notation Nrect := Nrect (only parsing). -Notation Nrect_base := Nrect_base (only parsing). -Notation Nrect_step := Nrect_step (only parsing). Definition Nind (P : N -> Prop) := Nrect P. + Definition Nrec (P : N -> Set) := Nrect P. Theorem Nrec_base : forall P a f, Nrec P a f N0 = a. @@ -84,117 +207,214 @@ Qed. (** Properties of successor and predecessor *) -Notation Npred_succ := pred_succ (only parsing). -Notation Nsucc_0 := neq_succ_0 (only parsing). -Notation Nsucc_inj := succ_inj (only parsing). +Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n. +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. +Qed. (** Properties of addition *) -Notation Nplus_0_l := plus_0_l (only parsing). -Notation Nplus_0_r := plus_0_r (only parsing). -Notation Nplus_comm := plus_comm (only parsing). -Notation Nplus_assoc := plus_assoc (only parsing). -Notation Nplus_succ := plus_succ_l (only parsing). -Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)) (only parsing). +Theorem Nplus_0_l : forall n:N, N0 + n = n. +Proof. +reflexivity. +Qed. + +Theorem Nplus_0_r : forall n:N, n + N0 = n. +Proof. +destruct n; reflexivity. +Qed. + +Theorem Nplus_comm : forall n m:N, n + m = m + n. +Proof. +intros. +destruct n; destruct m; simpl in |- *; try reflexivity. +rewrite Pplus_comm; reflexivity. +Qed. + +Theorem Nplus_assoc : forall n m p:N, 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. +Qed. + +Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m). +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. +Qed. + +Theorem Nsucc_0 : forall n : N, Nsucc n <> N0. +Proof. +intro n; elim n; simpl Nsucc; intros; discriminate. +Qed. + +Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = 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. +Qed. + +Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p. +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. +Qed. (** Properties of subtraction. *) -Notation Nminus_N0_Nle := minus_0_le (only parsing). -Notation Nminus_0_r := minus_0_r (only parsing). -Notation Nminus_succ_r := minus_succ_r (only parsing). +Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'. +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. +Qed. + +Theorem Nminus_0_r : forall n : N, n - N0 = n. +Proof. +now destruct n. +Qed. + +Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m). +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 |]. +Qed. (** Properties of multiplication *) -Notation Nmult_0_l := times_0_l (only parsing). -Notation Nmult_1_l := times_1_l (only parsing). -Notation Nmult_1_r := times_1_r (only parsing). -Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. +Theorem Nmult_0_l : forall n:N, N0 * n = N0. Proof. -intros; now rewrite times_succ_l, Nplus_comm. +reflexivity. Qed. -Notation Nmult_comm := times_comm (only parsing). -Notation Nmult_assoc := times_assoc (only parsing). -Notation Nmult_plus_distr_r := times_plus_distr_r (only parsing). -Notation Nmult_reg_r := - (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)) (only parsing). -(** Properties of comparison *) +Theorem Nmult_1_l : forall n:N, Npos 1 * n = n. +Proof. +destruct n; reflexivity. +Qed. -Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)) (only parsing). -Notation Ncompare_refl := Ncompare_diag (only parsing). -Notation Nlt_irrefl := lt_irrefl (only parsing). +Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. +Proof. +destruct n as [| n]; destruct m as [| m]; simpl; auto. +rewrite Pmult_Sn_m; reflexivity. +Qed. -Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n). +Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n. Proof. -destruct n; destruct m; simpl; auto. -exact (Pcompare_antisym p p0 Eq). +destruct n; simpl in |- *; try reflexivity. +rewrite Pmult_1_r; reflexivity. Qed. -Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. +Theorem Nmult_comm : forall n m:N, n * m = m * n. Proof. -destruct n; discriminate. +intros. +destruct n; destruct m; simpl in |- *; try reflexivity. +rewrite Pmult_comm; reflexivity. Qed. -(** Other properties and operations; given explicitly *) +Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p. +Proof. +intros. +destruct n; try reflexivity. +destruct m; try reflexivity. +destruct p; try reflexivity. +simpl in |- *; rewrite Pmult_assoc; reflexivity. +Qed. -Definition Ndiscr : forall n : N, {p : positive | n = Npos p} + {n = N0}. +Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p. Proof. -destruct n; auto. -left; exists p; auto. -Defined. +intros. +destruct n; try reflexivity. +destruct m; destruct p; try reflexivity. +simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity. +Qed. -(** Operation x -> 2 * x + 1 *) +Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m. +Proof. +destruct p; intros Hp H. +contradiction Hp; reflexivity. +destruct n; destruct m; reflexivity || (try discriminate H). +injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity. +Qed. -Definition Ndouble_plus_one x := -match x with -| N0 => Npos 1 -| Npos p => Npos p~1 -end. +(** Properties of comparison *) -(** Operation x -> 2 * x *) +Lemma Ncompare_refl : forall n, (n ?= n) = Eq. +Proof. +destruct n; simpl; auto. +apply Pcompare_refl. +Qed. -Definition Ndouble n := -match n with -| N0 => N0 -| Npos p => Npos p~0 -end. +Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m. +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. +Qed. -(** convenient induction principles *) +Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m. +Proof. +split; intros; + [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ]. +Qed. -Theorem 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. +Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= 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. +destruct n; destruct m; simpl; auto. +exact (Pcompare_antisym p p0 Eq). 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. +Theorem Nlt_irrefl : forall n : N, ~ 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. +intro n; unfold Nlt; now rewrite Ncompare_refl. Qed. -(** Division by 2 *) +Theorem Ncompare_n_Sm : + forall n m : N, Ncompare n (Nsucc m) = Lt <-> Ncompare n m = Lt \/ n = m. +Proof. +intros n m; split; destruct n as [| p]; destruct m as [| q]; simpl; auto. +destruct p; simpl; intros; discriminate. +pose proof (proj1 (Pcompare_p_Sq p q)); +assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. +intros H; destruct H; discriminate. +pose proof (proj2 (Pcompare_p_Sq p q)); +assert (p = q <-> Npos p = Npos q); [split; congruence | tauto]. +Qed. + +(** 0 is the least natural number *) + +Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. +Proof. +destruct n; discriminate. +Qed. + +(** Dividing by 2 *) Definition Ndiv2 (n:N) := match n with | N0 => N0 | Npos 1 => N0 - | Npos p~0 => Npos p - | Npos p~1 => Npos p + | Npos (xO p) => Npos p + | Npos (xI p) => Npos p end. Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. @@ -218,4 +438,3 @@ Lemma Ndouble_plus_one_inj : Proof. intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. Qed. - |