From 286d7e8201de98dc5cc36b6fbda8f9c1126f37ea Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 16 Apr 2008 23:51:06 +0000 Subject: 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 --- parsing/g_zsyntax.ml | 2 +- theories/NArith/BinNat.v | 453 +++++++++++++++++++++-------- theories/Numbers/Natural/Binary/NBinDefs.v | 191 ++---------- 3 files changed, 362 insertions(+), 284 deletions(-) diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml index 6c20107f3a..5d57c49dbb 100644 --- a/parsing/g_zsyntax.ml +++ b/parsing/g_zsyntax.ml @@ -96,7 +96,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope" (* Parsing N via scopes *) (**********************************************************************) -let binnat_module = ["Coq";"Numbers";"Natural";"Binary";"NBinDefs"] +let binnat_module = ["Coq";"NArith";"BinNat"] let n_kn = make_kn (make_dir binnat_module) (id_of_string "N") let glob_n = IndRef (n_kn,0) let path_of_N0 = ((n_kn,0),1) diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 9949d612d0..b704f3d378 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. - diff --git a/theories/Numbers/Natural/Binary/NBinDefs.v b/theories/Numbers/Natural/Binary/NBinDefs.v index 66402f7614..3110da36a6 100644 --- a/theories/Numbers/Natural/Binary/NBinDefs.v +++ b/theories/Numbers/Natural/Binary/NBinDefs.v @@ -11,166 +11,25 @@ (*i i*) Require Import BinPos. +Require Export BinNat. Require Import NMinus. -(** Definitions *) +Open Local Scope N_scope. -Inductive N : Set := -| N0 : N -| Npos : positive -> N. - -Definition succ n := -match n with -| N0 => Npos 1 -| Npos p => Npos (Psucc p) -end. - -Definition pred (n : N) := -match n with -| N0 => N0 -| Npos p => - match p with - | xH => N0 - | _ => Npos (Ppred p) - end -end. - -Definition plus n m := -match n, m with -| N0, _ => m -| _, N0 => n -| Npos p, Npos q => Npos (p + q) -end. - -Definition minus (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 times n m := -match n, m with -| N0, _ => N0 -| _, N0 => N0 -| Npos p, Npos q => Npos (p * q) -end. - -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 lt (x y : N) := (Ncompare x y) = Lt. -Definition le (x y : N) := (Ncompare x y) <> Gt. - -Definition min (n m : N) := -match Ncompare n m with -| Lt | Eq => n -| Gt => m -end. - -Definition max (n m : N) := -match Ncompare n m with -| Lt | Eq => m -| Gt => n -end. - -Delimit Scope NatScope with Nat. -Bind Scope NatScope with N. - -Notation "0" := N0 : NatScope. -Notation "1" := (Npos xH) : NatScope. -Infix "+" := plus : NatScope. -Infix "-" := minus : NatScope. -Infix "*" := times : NatScope. -Infix "?=" := Ncompare (at level 70, no associativity) : NatScope. -Infix "<" := lt : NatScope. -Infix "<=" := le : NatScope. - -Open Local Scope NatScope. - -(** Peano induction on binary natural numbers *) - -Definition Nrect - (P : N -> Type) (a : P N0) - (f : forall n : N, P n -> P (succ n)) (n : N) : P n := -let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in -let P' (p : positive) := P (Npos p) in -match n return (P n) with -| 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. -reflexivity. -Qed. - -Theorem Nrect_step : forall P a f n, Nrect P a f (succ 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. - -(*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.*) - -(** Results about the order *) - -Theorem Ncompare_eq_correct : forall n m : N, (n ?= m) = Eq <-> n = m. -Proof. -destruct n as [| n]; destruct m as [| m]; simpl; -split; intro H; try reflexivity; try discriminate H. -apply Pcompare_Eq_eq in H; now rewrite H. -injection H; intro H1; rewrite H1; apply Pcompare_refl. -Qed. - -Theorem Ncompare_diag : forall n : N, n ?= n = Eq. -Proof. -intro n; now apply <- Ncompare_eq_correct. -Qed. - -Theorem Ncompare_antisymm : - forall (n m : N) (c : comparison), n ?= m = c -> m ?= n = CompOpp c. -Proof. -destruct n; destruct m; destruct c; simpl; intro H; try discriminate H; try reflexivity; -replace Eq with (CompOpp Eq) by reflexivity; rewrite <- Pcompare_antisym; -now rewrite H. -Qed. - -(** Implementation of NAxiomsSig module type *) +(** Implementation of [NAxiomsSig] module type via [BinNat.N] *) Module NBinaryAxiomsMod <: NAxiomsSig. Module Export NZOrdAxiomsMod <: NZOrdAxiomsSig. Module Export NZAxiomsMod <: NZAxiomsSig. Definition NZ := N. -Definition NZeq := (@eq N). +Definition NZeq := @eq N. Definition NZ0 := N0. -Definition NZsucc := succ. -Definition NZpred := pred. -Definition NZplus := plus. -Definition NZminus := minus. -Definition NZtimes := times. +Definition NZsucc := Nsucc. +Definition NZpred := Npred. +Definition NZplus := Nplus. +Definition NZminus := Nminus. +Definition NZtimes := Nmult. Theorem NZeq_equiv : equiv N NZeq. Proof (eq_equiv N). @@ -229,7 +88,7 @@ Theorem NZplus_succ_l : forall n m : NZ, (NZsucc n) + m = NZsucc (n + m). Proof. destruct n; destruct m. simpl in |- *; reflexivity. -unfold NZsucc, NZplus, succ, plus. rewrite <- Pplus_one_succ_l; reflexivity. +unfold NZsucc, NZplus, Nsucc, Nplus. rewrite <- Pplus_one_succ_l; reflexivity. simpl in |- *; reflexivity. simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity. Qed. @@ -260,10 +119,10 @@ Qed. End NZAxiomsMod. -Definition NZlt := lt. -Definition NZle := le. -Definition NZmin := min. -Definition NZmax := max. +Definition NZlt := Nlt. +Definition NZle := Nle. +Definition NZmin := Nmin. +Definition NZmax := Nmax. Add Morphism NZlt with signature NZeq ==> NZeq ==> iff as NZlt_wd. Proof. @@ -287,19 +146,19 @@ Qed. Theorem NZlt_eq_cases : forall n m : N, n <= m <-> n < m \/ n = m. Proof. -intros n m. unfold le, lt. rewrite <- Ncompare_eq_correct. +intros n m. unfold Nle, Nlt. rewrite <- Ncompare_eq_correct. destruct (n ?= m); split; intro H1; (try discriminate); try (now left); try now right. now elim H1. destruct H1; discriminate. Qed. Theorem NZlt_irrefl : forall n : NZ, ~ n < n. Proof. -intro n; unfold lt; now rewrite Ncompare_diag. +intro n; unfold Nlt; now rewrite Ncompare_refl. Qed. Theorem NZlt_succ_r : forall n m : NZ, n < (NZsucc m) <-> n <= m. Proof. -intros n m; unfold lt, le; destruct n as [| p]; destruct m as [| q]; simpl; +intros n m; unfold Nlt, Nle; destruct n as [| p]; destruct m as [| q]; simpl; split; intro H; try reflexivity; try discriminate. destruct p; simpl; intros; discriminate. elimtype False; now apply H. apply -> Pcompare_p_Sq in H. destruct H as [H | H]. @@ -310,29 +169,29 @@ Qed. Theorem NZmin_l : forall n m : N, n <= m -> NZmin n m = n. Proof. -unfold NZmin, min, le; intros n m H. +unfold NZmin, Nmin, Nle; intros n m H. destruct (n ?= m); try reflexivity. now elim H. Qed. Theorem NZmin_r : forall n m : N, m <= n -> NZmin n m = m. Proof. -unfold NZmin, min, le; intros n m H. +unfold NZmin, Nmin, Nle; intros n m H. case_eq (n ?= m); intro H1; try reflexivity. now apply -> Ncompare_eq_correct. -apply Ncompare_antisymm in H1. now elim H. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. Qed. Theorem NZmax_l : forall n m : N, m <= n -> NZmax n m = n. Proof. -unfold NZmax, max, le; intros n m H. +unfold NZmax, Nmax, Nle; intros n m H. case_eq (n ?= m); intro H1; try reflexivity. symmetry; now apply -> Ncompare_eq_correct. -apply Ncompare_antisymm in H1. now elim H. +rewrite <- Ncompare_antisym, H1 in H; elim H; auto. Qed. Theorem NZmax_r : forall n m : N, n <= m -> NZmax n m = m. Proof. -unfold NZmax, max, le; intros n m H. +unfold NZmax, Nmax, Nle; intros n m H. destruct (n ?= m); try reflexivity. now elim H. Qed. @@ -342,7 +201,7 @@ Definition recursion (A : Set) (a : A) (f : N -> A -> A) (n : N) := Nrect (fun _ => A) a f n. Implicit Arguments recursion [A]. -Theorem pred_0 : pred N0 = N0. +Theorem pred_0 : Npred N0 = N0. Proof. reflexivity. Qed. @@ -373,7 +232,7 @@ Qed. Theorem recursion_succ : forall (A : Set) (Aeq : relation A) (a : A) (f : N -> A -> A), Aeq a a -> fun2_wd NZeq Aeq Aeq f -> - forall n : N, Aeq (recursion a f (succ n)) (f n (recursion a f n)). + forall n : N, Aeq (recursion a f (Nsucc n)) (f n (recursion a f n)). Proof. unfold NZeq, recursion, fun2_wd; intros A Aeq a f EAaa f_wd n; pattern n; apply Nrect. rewrite Nrect_step; rewrite Nrect_base; now apply f_wd. -- cgit v1.2.3