From 1ee05f6d40ee3bb3351f0893d360b85f6ff81ba2 Mon Sep 17 00:00:00 2001 From: emakarov Date: Wed, 7 Nov 2007 21:32:04 +0000 Subject: Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10299 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile.common | 2 +- theories/NArith/BinNat.v | 222 ----------------------------------------------- 2 files changed, 1 insertion(+), 223 deletions(-) delete mode 100644 theories/NArith/BinNat.v diff --git a/Makefile.common b/Makefile.common index eb6639ea70..8e3294ee62 100644 --- a/Makefile.common +++ b/Makefile.common @@ -672,7 +672,7 @@ NATURALABSTRACTVO:=\ NATURALPEANOVO:=$(NATURALDIR)/Peano/NPeano.vo NATURALBINARYVO:=\ - $(NATURALDIR)/Binary/NBinDefs.vo + $(NATURALDIR)/Binary/NBinDefs.vo\ $(NATURALDIR)/Binary/NBinary.vo NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v deleted file mode 100644 index 349892b992..0000000000 --- a/theories/NArith/BinNat.v +++ /dev/null @@ -1,222 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Lt. -Notation Nmin := min. -Notation Nmax := max. - -(* 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]. - -Infix "+" := Nplus : N_scope. -Infix "-" := Nminus : N_scope. -Infix "*" := Nmult : N_scope. -Infix "?=" := Ncompare (at level 70, no associativity) : N_scope. -Infix "<=" := Nle : N_scope. -Infix "<" := Nlt : N_scope. -Infix ">=" := Nge : N_scope. -Infix ">" := Ngt : N_scope. - -(** Peano induction and recursion *) - -Notation Nrect := Nrect. -Notation Nrect_base := Nrect_base. -Notation Nrect_step := Nrect_step. -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. -Proof. -intros P a f; unfold Nrec; apply Nrect_base. -Qed. - -Theorem Nrec_step : forall P a f n, Nrec P a f (Nsucc n) = f n (Nrec P a f n). -Proof. -intros P a f; unfold Nrec; apply Nrect_step. -Qed. - -(** Properties of successor and predecessor *) - -Notation Npred_succ := pred_succ. -Notation Nsucc_0 := neq_succ_0. -Notation Nsucc_inj := succ_inj. - -(** Properties of addition *) - -Notation Nplus_0_l := plus_0_l. -Notation Nplus_0_r := plus_0_r. -Notation Nplus_comm := plus_comm. -Notation Nplus_assoc := plus_assoc. -Notation Nplus_succ := plus_succ_l. -Notation Nplus_reg_l := (fun n m p : N => proj1 (plus_cancel_l m p n)). - -(** Properties of subtraction. *) - -Notation Nminus_N0_Nle := - (fun n m : N => (conj (proj2 (le_minus_0 n m)) (proj1 (le_minus_0 n m)))). -Notation Nminus_0_r := minus_0_r. -Notation Nminus_succ_r := minus_succ_r. - -(** Properties of multiplication *) - -Notation Nmult_0_l := times_0_l. -Notation Nmult_1_l := times_1_l. -Notation Nmult_1_r := times_1_r. -Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m. -Proof. -intros; now rewrite times_succ_l, Nplus_comm. -Qed. -Notation Nmult_comm := times_comm. -Notation Nmult_assoc := times_assoc. -Notation Nmult_plus_distr_r := times_plus_distr_r. -Notation Nmult_reg_r := - (fun (n m p : N) (H : p <> N0) => proj1 (times_cancel_r n m p H)). - -(** Properties of comparison *) - -Notation Ncompare_Eq_eq := (fun n m : N => proj1 (Ncompare_eq_correct n m)). -Notation Ncompare_refl := Ncompare_diag. -Notation Nlt_irrefl := lt_irrefl. - -Lemma Ncompare_antisym : forall n m, CompOpp (n ?= m) = (m ?= n). -Proof. -destruct n; destruct m; simpl; auto. -exact (Pcompare_antisym p p0 Eq). -Qed. - -Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt. -Proof. -destruct n; discriminate. -Qed. - -(** Other properties and operations; given explicitly *) - -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. - -(** convenient induction principles *) - -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. -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. - -(** Division by 2 *) - -Definition Ndiv2 (n:N) := - match n with - | N0 => N0 - | Npos 1 => N0 - | Npos (xO p) => Npos p - | Npos (xI p) => Npos p - end. - -Lemma Ndouble_div2 : forall n:N, Ndiv2 (Ndouble n) = n. -Proof. - destruct n; trivial. -Qed. - -Lemma Ndouble_plus_one_div2 : - forall n:N, Ndiv2 (Ndouble_plus_one n) = n. -Proof. - destruct n; trivial. -Qed. - -Lemma Ndouble_inj : forall n m, Ndouble n = Ndouble m -> n = m. -Proof. - intros. rewrite <- (Ndouble_div2 n). rewrite H. apply Ndouble_div2. -Qed. - -Lemma Ndouble_plus_one_inj : - forall n m, Ndouble_plus_one n = Ndouble_plus_one m -> n = m. -Proof. - intros. rewrite <- (Ndouble_plus_one_div2 n). rewrite H. apply Ndouble_plus_one_div2. -Qed. - -- cgit v1.2.3