diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-06-26 11:04:34 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-07-09 18:47:26 +0200 |
| commit | 8836eae5d52fbbadf7722548052da3f7ceb5b260 (patch) | |
| tree | ff067362a375c7c5e9539bb230378ca8bc0cf1ee | |
| parent | 6e9a1c4c71f58aba8bb0bb5942c5063a5984a1bc (diff) | |
Arith: full integration of the "Numbers" modular framework
- The earlier proof-of-concept file NPeano (which instantiates
the "Numbers" framework for nat) becomes now the entry point
in the Arith lib, and gets renamed PeanoNat. It still provides
an inner module "Nat" which sums up everything about type nat
(functions, predicates and properties of them).
This inner module Nat is usable as soon as you Require Import Arith,
or just Arith_base, or simply PeanoNat.
- Definitions of operations over type nat are now grouped in a new
file Init/Nat.v. This file is meant to be used without "Import",
hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
starts (but no proofs about them).
- The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
where here Nat is Init/Nat.v).
- This Coq.Init.Nat module (with only pure definitions) is Include'd
in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
sometimes instead of just Nat (for instance when doing "Print plus").
Normally it should be ok to just ignore these "Init" since
Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
it's possible to get rid of these "Init" prefixes.
- Concerning predicates, orders le and lt are still defined in Init/Peano.v,
with their notations "<=" and "<". Properties in PeanoNat.Nat directly
refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
we cannot yet include an Inductive to implement a Parameter), but these
aliased predicates won't probably be very convenient to use.
- Technical remark: I've split the previous property functor NProp in
two parts (NBasicProp and NExtraProp), it helps a lot for building
PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:
Module Nat.
Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
... (** proofs of specifications for basic ops such as + * - *)
Include NBasicProp. (** generic properties of these basic ops *)
... (** proofs of specifications for advanced ops (pow sqrt log2...)
that may rely on proofs for + * - *)
Include NExtraProp. (** all remaining properties *)
End Nat.
- All other files in directory Arith are now taking advantage of PeanoNat :
they are now filled with compatibility notations (when earlier lemmas
have exact counterpart in the Nat module) or lemmas with one-line proofs
based on the Nat module. All hints for database "arith" remain declared
in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
files are still Require'd (or not) by Arith.v, just as before.
- Compatibility should be almost complete. For instance in the stdlib,
the only adaptations were due to .ml code referring to some Coq constant
name such as Coq.Init.Peano.pred, which doesn't live well with the
new compatibility notations.
52 files changed, 2373 insertions, 2605 deletions
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index fb2483db7..c3b2aad58 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -29,6 +29,7 @@ through the <tt>Require Import</tt> command.</p> theories/Init/Datatypes.v theories/Init/Logic.v theories/Init/Logic_Type.v + theories/Init/Nat.v theories/Init/Peano.v theories/Init/Specif.v theories/Init/Tactics.v @@ -108,8 +109,8 @@ through the <tt>Require Import</tt> command.</p> <dt> <b>Arith</b>: Basic Peano arithmetic </dt> - <dd> - theories/Arith/Arith_base.v + <dd> + theories/Arith/PeanoNat.v theories/Arith/Le.v theories/Arith/Lt.v theories/Arith/Plus.v @@ -119,6 +120,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Between.v theories/Arith/Peano_dec.v theories/Arith/Compare_dec.v + (theories/Arith/Arith_base.v) (theories/Arith/Arith.v) theories/Arith/Min.v theories/Arith/Max.v diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 6c4d76340..b8a3b23b8 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -119,6 +119,7 @@ let init_modules = [ init_dir@["Logic"]; init_dir@["Specif"]; init_dir@["Logic_Type"]; + init_dir@["Nat"]; init_dir@["Peano"]; init_dir@["Wf"] ] diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v index e28c845cc..e4671ccd1 100644 --- a/plugins/funind/Recdef.v +++ b/plugins/funind/Recdef.v @@ -5,6 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) + +Require Import PeanoNat. + Require Compare_dec. Require Wf_nat. @@ -19,32 +22,29 @@ Fixpoint iter (n : nat) : (A -> A) -> A -> A := end. End Iter. -Theorem SSplus_lt : forall p p' : nat, p < S (S (p + p')). - intro p; intro p'; change (S p <= S (S (p + p'))); - apply le_S; apply Gt.gt_le_S; change (p < S (p + p')); - apply Lt.le_lt_n_Sm; apply Plus.le_plus_l. +Theorem le_lt_SS x y : x <= y -> x < S (S y). +Proof. + intros. now apply Nat.lt_succ_r, Nat.le_le_succ_r. Qed. - -Theorem Splus_lt : forall p p' : nat, p' < S (p + p'). - intro p; intro p'; change (S p' <= S (p + p')); - apply Gt.gt_le_S; change (p' < S (p + p')); apply Lt.le_lt_n_Sm; - apply Plus.le_plus_r. +Theorem Splus_lt x y : y < S (x + y). +Proof. + apply Nat.lt_succ_r. rewrite Nat.add_comm. apply Nat.le_add_r. Qed. -Theorem le_lt_SS : forall x y, x <= y -> x < S (S y). -intro x; intro y; intro H; change (S x <= S (S y)); - apply le_S; apply Gt.gt_le_S; change (x < S y); - apply Lt.le_lt_n_Sm; exact H. +Theorem SSplus_lt x y : x < S (S (x + y)). +Proof. + apply le_lt_SS, Nat.le_add_r. Qed. Inductive max_type (m n:nat) : Set := cmt : forall v, m <= v -> n <= v -> max_type m n. -Definition max : forall m n:nat, max_type m n. -intros m n; case (Compare_dec.le_gt_dec m n). -intros h; exists n; [exact h | apply le_n]. -intros h; exists m; [apply le_n | apply Lt.lt_le_weak; exact h]. +Definition max m n : max_type m n. +Proof. + destruct (Compare_dec.le_gt_dec m n) as [h|h]. + - exists n; [exact h | apply le_n]. + - exists m; [apply le_n | apply Nat.lt_le_incl; exact h]. Defined. -Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100.
\ No newline at end of file +Definition Acc_intro_generator_function := fun A R => @Acc_intro_generator A R 100. diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 38cbd0c53..1fa16a301 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -43,9 +43,14 @@ open Indfun_common (* Ugly things which should not be here *) -let coq_base_constant s = - Coqlib.gen_constant_in_modules "RecursiveDefinition" - (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;; +let coq_constant m s = + Coqlib.coq_constant "RecursiveDefinition" m s + +let arith_Nat = ["Arith";"PeanoNat";"Nat"] +let arith_Lt = ["Arith";"Lt"] + +let coq_init_constant s = + Coqlib.gen_constant_in_modules "RecursiveDefinition" Coqlib.init_modules s let find_reference sl s = let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in @@ -120,25 +125,25 @@ let v_id = Id.of_string "v" let def_id = Id.of_string "def" let p_id = Id.of_string "p" let rec_res_id = Id.of_string "rec_res";; -let lt = function () -> (coq_base_constant "lt") -let le = function () -> (coq_base_constant "le") -let ex = function () -> (coq_base_constant "ex") -let nat = function () -> (coq_base_constant "nat") +let lt = function () -> (coq_init_constant "lt") +let le = function () -> (coq_init_constant "le") +let ex = function () -> (coq_init_constant "ex") +let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded" let iter = function () -> (constr_of_global (delayed_force iter_ref)) -let eq = function () -> (coq_base_constant "eq") +let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") -let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm") -let le_trans = function () -> (coq_base_constant "le_trans") -let le_lt_trans = function () -> (coq_base_constant "le_lt_trans") -let lt_S_n = function () -> (coq_base_constant "lt_S_n") -let le_n = function () -> (coq_base_constant "le_n") +let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") +let le_trans = function () -> (coq_constant arith_Nat "le_trans") +let le_lt_trans = function () -> (coq_constant arith_Nat "le_lt_trans") +let lt_S_n = function () -> (coq_constant arith_Lt "lt_S_n") +let le_n = function () -> (coq_init_constant "le_n") let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig") -let coq_O = function () -> (coq_base_constant "O") -let coq_S = function () -> (coq_base_constant "S") -let lt_n_O = function () -> (coq_base_constant "lt_n_O") +let coq_O = function () -> (coq_init_constant "O") +let coq_S = function () -> (coq_init_constant "S") +let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") let max_constr = function () -> (constr_of_global (delayed_force max_ref)) let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj" diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 88958d014..83f346242 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -304,10 +304,10 @@ let coq_le = lazy (init_constant "le") let coq_lt = lazy (init_constant "lt") let coq_ge = lazy (init_constant "ge") let coq_gt = lazy (init_constant "gt") -let coq_minus = lazy (init_constant "minus") -let coq_plus = lazy (init_constant "plus") -let coq_mult = lazy (init_constant "mult") -let coq_pred = lazy (init_constant "pred") +let coq_minus = lazy (init_constant "Nat.sub") +let coq_plus = lazy (init_constant "Nat.add") +let coq_mult = lazy (init_constant "Nat.mul") +let coq_pred = lazy (init_constant "Nat.pred") let coq_nat = lazy (init_constant "nat") let coq_S = lazy (init_constant "S") let coq_O = lazy (init_constant "O") diff --git a/test-suite/success/NumberScopes.v b/test-suite/success/NumberScopes.v index ca9457be7..6d7872107 100644 --- a/test-suite/success/NumberScopes.v +++ b/test-suite/success/NumberScopes.v @@ -31,7 +31,7 @@ Definition f_N' (x:N.t) := x. Check (f_N 1). Check (f_N' 1). -Require Import NPeano. +Require Import Arith. Check (Nat.add 1 2). Check (Nat.add_comm 1 2). Check (Nat.min_comm 1 2). diff --git a/theories/Arith/Arith_base.v b/theories/Arith/Arith_base.v index 9f0f05db4..290ce548a 100644 --- a/theories/Arith/Arith_base.v +++ b/theories/Arith/Arith_base.v @@ -6,6 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +Require Export PeanoNat. + Require Export Le. Require Export Lt. Require Export Plus. diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v index 76132aed0..bcf409e66 100644 --- a/theories/Arith/Compare_dec.v +++ b/theories/Arith/Compare_dec.v @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Le. -Require Import Lt. -Require Import Gt. -Require Import Decidable. +Require Import Le Lt Gt Decidable PeanoNat. Local Open Scope nat_scope. @@ -29,31 +26,31 @@ Defined. Definition gt_eq_gt_dec n m : {m > n} + {n = m} + {n > m}. Proof. - intros; apply lt_eq_lt_dec; assumption. + now apply lt_eq_lt_dec. Defined. Definition le_lt_dec n m : {n <= m} + {m < n}. Proof. induction n in m |- *. - auto with arith. - destruct m. - auto with arith. - elim (IHn m); auto with arith. + - left; auto with arith. + - destruct m. + + right; auto with arith. + + elim (IHn m); [left|right]; auto with arith. Defined. Definition le_le_S_dec n m : {n <= m} + {S m <= n}. Proof. - intros; exact (le_lt_dec n m). + exact (le_lt_dec n m). Defined. Definition le_ge_dec n m : {n <= m} + {n >= m}. Proof. - intros; elim (le_lt_dec n m); auto with arith. + elim (le_lt_dec n m); auto with arith. Defined. Definition le_gt_dec n m : {n <= m} + {n > m}. Proof. - intros; exact (le_lt_dec n m). + exact (le_lt_dec n m). Defined. Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}. @@ -62,162 +59,121 @@ Proof. intros; absurd (m < n); auto with arith. Defined. -Theorem le_dec : forall n m, {n <= m} + {~ n <= m}. +Theorem le_dec n m : {n <= m} + {~ n <= m}. Proof. - intros n m. destruct (le_gt_dec n m). - auto with arith. - right. apply gt_not_le. assumption. + destruct (le_gt_dec n m). + - now left. + - right. now apply gt_not_le. Defined. -Theorem lt_dec : forall n m, {n < m} + {~ n < m}. +Theorem lt_dec n m : {n < m} + {~ n < m}. Proof. - intros; apply le_dec. + apply le_dec. Defined. -Theorem gt_dec : forall n m, {n > m} + {~ n > m}. +Theorem gt_dec n m : {n > m} + {~ n > m}. Proof. - intros; apply lt_dec. + apply lt_dec. Defined. -Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}. +Theorem ge_dec n m : {n >= m} + {~ n >= m}. Proof. - intros; apply le_dec. + apply le_dec. Defined. (** Proofs of decidability *) -Theorem dec_le : forall n m, decidable (n <= m). +Theorem dec_le n m : decidable (n <= m). Proof. - intros n m; destruct (le_dec n m); unfold decidable; auto. + apply Nat.le_decidable. Qed. -Theorem dec_lt : forall n m, decidable (n < m). +Theorem dec_lt n m : decidable (n < m). Proof. - intros; apply dec_le. + apply Nat.lt_decidable. Qed. -Theorem dec_gt : forall n m, decidable (n > m). +Theorem dec_gt n m : decidable (n > m). Proof. - intros; apply dec_lt. + apply Nat.lt_decidable. Qed. -Theorem dec_ge : forall n m, decidable (n >= m). +Theorem dec_ge n m : decidable (n >= m). Proof. - intros; apply dec_le. + apply Nat.le_decidable. Qed. -Theorem not_eq : forall n m, n <> m -> n < m \/ m < n. +Theorem not_eq n m : n <> m -> n < m \/ m < n. Proof. - intros x y H; elim (lt_eq_lt_dec x y); - [ intros H1; elim H1; - [ auto with arith | intros H2; absurd (x = y); assumption ] - | auto with arith ]. + apply Nat.lt_gt_cases. Qed. - -Theorem not_le : forall n m, ~ n <= m -> n > m. +Theorem not_le n m : ~ n <= m -> n > m. Proof. - intros x y H; elim (le_gt_dec x y); - [ intros H1; absurd (x <= y); assumption | trivial with arith ]. + apply Nat.nle_gt. Qed. -Theorem not_gt : forall n m, ~ n > m -> n <= m. +Theorem not_gt n m : ~ n > m -> n <= m. Proof. - intros x y H; elim (le_gt_dec x y); - [ trivial with arith | intros H1; absurd (x > y); assumption ]. + apply Nat.nlt_ge. Qed. -Theorem not_ge : forall n m, ~ n >= m -> n < m. +Theorem not_ge n m : ~ n >= m -> n < m. Proof. - intros x y H; exact (not_le y x H). + apply Nat.nle_gt. Qed. -Theorem not_lt : forall n m, ~ n < m -> n >= m. +Theorem not_lt n m : ~ n < m -> n >= m. Proof. - intros x y H; exact (not_gt y x H). + apply Nat.nlt_ge. Qed. -(** A ternary comparison function in the spirit of [Z.compare]. *) +(** A ternary comparison function in the spirit of [Z.compare]. + See now [Nat.compare] and its properties. + In scope [nat_scope], the notation for [Nat.compare] is "?=" *) -Fixpoint nat_compare n m := - match n, m with - | O, O => Eq - | O, S _ => Lt - | S _, O => Gt - | S n', S m' => nat_compare n' m' - end. +Notation nat_compare := Nat.compare (compat "8.4"). -Lemma nat_compare_S : forall n m, nat_compare (S n) (S m) = nat_compare n m. -Proof. - reflexivity. -Qed. +Notation nat_compare_spec := Nat.compare_spec (compat "8.4"). +Notation nat_compare_eq_iff := Nat.compare_eq_iff (compat "8.4"). +Notation nat_compare_S := Nat.compare_succ (compat "8.4"). -Lemma nat_compare_eq_iff : forall n m, nat_compare n m = Eq <-> n = m. +Lemma nat_compare_lt n m : n<m <-> (n ?= m) = Lt. Proof. - induction n; destruct m; simpl; split; auto; try discriminate; - destruct (IHn m); auto. + symmetry. apply Nat.compare_lt_iff. Qed. -Lemma nat_compare_eq : forall n m, nat_compare n m = Eq -> n = m. +Lemma nat_compare_gt n m : n>m <-> (n ?= m) = Gt. Proof. - intros; apply -> nat_compare_eq_iff; auto. + symmetry. apply Nat.compare_gt_iff. Qed. -Lemma nat_compare_lt : forall n m, n<m <-> nat_compare n m = Lt. +Lemma nat_compare_le n m : n<=m <-> (n ?= m) <> Gt. Proof. - induction n; destruct m; simpl; split; auto with arith; - try solve [inversion 1]. - destruct (IHn m); auto with arith. - destruct (IHn m); auto with arith. + symmetry. apply Nat.compare_le_iff. Qed. -Lemma nat_compare_gt : forall n m, n>m <-> nat_compare n m = Gt. +Lemma nat_compare_ge n m : n>=m <-> (n ?= m) <> Lt. Proof. - induction n; destruct m; simpl; split; auto with arith; - try solve [inversion 1]. - destruct (IHn m); auto with arith. - destruct (IHn m); auto with arith. + symmetry. apply Nat.compare_ge_iff. Qed. -Lemma nat_compare_le : forall n m, n<=m <-> nat_compare n m <> Gt. -Proof. - split. - intros LE; contradict LE. - apply lt_not_le. apply <- nat_compare_gt; auto. - intros NGT. apply not_lt. contradict NGT. - apply -> nat_compare_gt; auto. -Qed. - -Lemma nat_compare_ge : forall n m, n>=m <-> nat_compare n m <> Lt. -Proof. - split. - intros GE; contradict GE. - apply lt_not_le. apply <- nat_compare_lt; auto. - intros NLT. apply not_lt. contradict NLT. - apply -> nat_compare_lt; auto. -Qed. +(** Some projections of the above equivalences. *) -Lemma nat_compare_spec : - forall x y, CompareSpec (x=y) (x<y) (y<x) (nat_compare x y). +Lemma nat_compare_eq n m : (n ?= m) = Eq -> n = m. Proof. - intros. - destruct (nat_compare x y) eqn:?; constructor. - apply nat_compare_eq; auto. - apply <- nat_compare_lt; auto. - apply <- nat_compare_gt; auto. + apply Nat.compare_eq_iff. Qed. -(** Some projections of the above equivalences. *) - -Lemma nat_compare_Lt_lt : forall n m, nat_compare n m = Lt -> n<m. +Lemma nat_compare_Lt_lt n m : (n ?= m) = Lt -> n<m. Proof. - intros; apply <- nat_compare_lt; auto. + apply Nat.compare_lt_iff. Qed. -Lemma nat_compare_Gt_gt : forall n m, nat_compare n m = Gt -> n>m. +Lemma nat_compare_Gt_gt n m : (n ?= m) = Gt -> n>m. Proof. - intros; apply <- nat_compare_gt; auto. + apply Nat.compare_gt_iff. Qed. (** A previous definition of [nat_compare] in terms of [lt_eq_lt_dec]. @@ -230,70 +186,48 @@ Definition nat_compare_alt (n m:nat) := | inright _ => Gt end. -Lemma nat_compare_equiv: forall n m, - nat_compare n m = nat_compare_alt n m. +Lemma nat_compare_equiv n m : (n ?= m) = nat_compare_alt n m. Proof. - intros; unfold nat_compare_alt; destruct lt_eq_lt_dec as [[LT|EQ]|GT]. - apply -> nat_compare_lt; auto. - apply <- nat_compare_eq_iff; auto. - apply -> nat_compare_gt; auto. + unfold nat_compare_alt; destruct lt_eq_lt_dec as [[|]|]. + - now apply Nat.compare_lt_iff. + - now apply Nat.compare_eq_iff. + - now apply Nat.compare_gt_iff. Qed. +(** A boolean version of [le] over [nat]. + See now [Nat.leb] and its properties. + In scope [nat_scope], the notation for [Nat.leb] is "<=?" *) -(** A boolean version of [le] over [nat]. *) - -Fixpoint leb (m:nat) : nat -> bool := - match m with - | O => fun _:nat => true - | S m' => - fun n:nat => match n with - | O => false - | S n' => leb m' n' - end - end. +Notation leb := Nat.leb (compat "8.4"). -Lemma leb_correct : forall m n, m <= n -> leb m n = true. -Proof. - induction m as [| m IHm]. trivial. - destruct n. intro H. elim (le_Sn_O _ H). - intros. simpl. apply IHm. apply le_S_n. assumption. -Qed. +Notation leb_iff := Nat.leb_le (compat "8.4"). -Lemma leb_complete : forall m n, leb m n = true -> m <= n. +Lemma leb_iff_conv m n : (n <=? m) = false <-> m < n. Proof. - induction m. trivial with arith. - destruct n. intro H. discriminate H. - auto with arith. + rewrite Nat.leb_nle. apply Nat.nle_gt. Qed. -Lemma leb_iff : forall m n, leb m n = true <-> m <= n. +Lemma leb_correct m n : m <= n -> (m <=? n) = true. Proof. - split; auto using leb_correct, leb_complete. + apply Nat.leb_le. Qed. -Lemma leb_correct_conv : forall m n, m < n -> leb n m = false. +Lemma leb_complete m n : (m <=? n) = true -> m <= n. Proof. - intros. - generalize (leb_complete n m). - destruct (leb n m); auto. - intros; elim (lt_not_le m n); auto. + apply Nat.leb_le. Qed. -Lemma leb_complete_conv : forall m n, leb n m = false -> m < n. +Lemma leb_correct_conv m n : m < n -> (n <=? m) = false. Proof. - intros m n EQ. apply not_le. - intro LE. apply leb_correct in LE. rewrite LE in EQ; discriminate. + apply leb_iff_conv. Qed. -Lemma leb_iff_conv : forall m n, leb n m = false <-> m < n. +Lemma leb_complete_conv m n : (n <=? m) = false -> m < n. Proof. - split; auto using leb_complete_conv, leb_correct_conv. + apply leb_iff_conv. Qed. -Lemma leb_compare : forall n m, leb n m = true <-> nat_compare n m <> Gt. +Lemma leb_compare n m : (n <=? m) = true <-> (n ?= m) <> Gt. Proof. - split; intros. - apply -> nat_compare_le. auto using leb_complete. - apply leb_correct. apply <- nat_compare_le; auto. + rewrite Nat.compare_le_iff. apply Nat.leb_le. Qed. - diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 56115c7f0..8cef48b69 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Lt. -Require Import Plus. -Require Import Compare_dec. -Require Import Even. +(** Nota : this file is OBSOLETE, and left only for compatibility. + Please consider using [Nat.div2] directly, and results about it + (see file PeanoNat). *) + +Require Import PeanoNat Even. Local Open Scope nat_scope. @@ -17,12 +18,7 @@ Implicit Type n : nat. (** Here we define [n/2] and prove some of its properties *) -Fixpoint div2 n : nat := - match n with - | O => 0 - | S O => 0 - | S (S n') => S (div2 n') - end. +Notation div2 := Nat.div2 (compat "8.4"). (** Since [div2] is recursively defined on [0], [1] and [(S (S n))], it is useful to prove the corresponding induction principle *) @@ -31,53 +27,48 @@ Lemma ind_0_1_SS : forall P:nat -> Prop, P 0 -> P 1 -> (forall n, P n -> P (S (S n))) -> forall n, P n. Proof. - intros P H0 H1 Hn. - cut (forall n, P n /\ P (S n)). - intros H'n n. elim (H'n n). auto with arith. - - induction n. auto with arith. - intros. elim IHn; auto with arith. + intros P H0 H1 H2. + fix 1. + destruct n as [|[|n]]. + - exact H0. + - exact H1. + - apply H2, ind_0_1_SS. Qed. (** [0 <n => n/2 < n] *) -Lemma lt_div2 : forall n, 0 < n -> div2 n < n. -Proof. - intro n. pattern n. apply ind_0_1_SS. - (* n = 0 *) - inversion 1. - (* n=1 *) - simpl; trivial. - (* n=S S n' *) - intro n'; case (zerop n'). - intro n'_eq_0. rewrite n'_eq_0. auto with arith. - auto with arith. -Qed. +Lemma lt_div2 n : 0 < n -> div2 n < n. +Proof. apply Nat.lt_div2. Qed. Hint Resolve lt_div2: arith. (** Properties related to the parity *) -Lemma even_div2 : forall n, even n -> div2 n = div2 (S n) -with odd_div2 : forall n, odd n -> S (div2 n) = div2 (S n). +Lemma even_div2 n : even n -> div2 n = div2 (S n). Proof. - destruct n; intro H. - (* 0 *) trivial. - (* S n *) inversion_clear H. apply odd_div2 in H0 as <-. trivial. - destruct n; intro. - (* 0 *) inversion H. - (* S n *) inversion_clear H. apply even_div2 in H0 as <-. trivial. + rewrite Even.even_equiv. intros (p,->). + rewrite Nat.div2_succ_double. apply Nat.div2_double. Qed. -Lemma div2_even n : div2 n = div2 (S n) -> even n -with div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Lemma odd_div2 n : odd n -> S (div2 n) = div2 (S n). Proof. -{ destruct n; intro H. - - constructor. - - constructor. apply div2_odd. rewrite H. trivial. } -{ destruct n; intro H. - - discriminate. - - constructor. apply div2_even. injection H as <-. trivial. } + rewrite Even.odd_equiv. intros (p,->). + rewrite Nat.add_1_r, Nat.div2_succ_double. + simpl. f_equal. symmetry. apply Nat.div2_double. +Qed. + +Lemma div2_even n : div2 n = div2 (S n) -> even n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply odd_div2 in Od. rewrite <- Od. intro Od'. + elim (n_Sn _ Od'). +Qed. + +Lemma div2_odd n : S (div2 n) = div2 (S n) -> odd n. +Proof. + destruct (even_or_odd n) as [Ev|Od]; trivial. + apply even_div2 in Ev. rewrite <- Ev. intro Ev'. + symmetry in Ev'. elim (n_Sn _ Ev'). Qed. Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. @@ -93,58 +84,52 @@ Qed. (** Properties related to the double ([2n]) *) -Definition double n := n + n. +Notation double := Nat.double (compat "8.4"). -Hint Unfold double: arith. +Hint Unfold double Nat.double: arith. -Lemma double_S : forall n, double (S n) = S (S (double n)). +Lemma double_S n : double (S n) = S (S (double n)). Proof. - intro. unfold double. simpl. auto with arith. + apply Nat.add_succ_r. Qed. -Lemma double_plus : forall n (m:nat), double (n + m) = double n + double m. +Lemma double_plus n m : double (n + m) = double n + double m. Proof. - intros m n. unfold double. - do 2 rewrite plus_assoc_reverse. rewrite (plus_permute n). - reflexivity. + apply Nat.add_shuffle1. Qed. Hint Resolve double_S: arith. -Lemma even_odd_double : - forall n, - (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). +Lemma even_odd_double n : + (even n <-> n = double (div2 n)) /\ (odd n <-> n = S (double (div2 n))). Proof. - intro n. pattern n. apply ind_0_1_SS. - (* n = 0 *) - split; split; auto with arith. - intro H. inversion H. - (* n = 1 *) - split; split; auto with arith. - intro H. inversion H. inversion H1. - (* n = (S (S n')) *) - intros. destruct H as ((IH1,IH2),(IH3,IH4)). - split; split. - intro H. inversion H. inversion H1. - simpl. rewrite (double_S (div2 n0)). auto with arith. - simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. - intro H. inversion H. inversion H1. - simpl. rewrite (double_S (div2 n0)). auto with arith. - simpl. rewrite (double_S (div2 n0)). intro H. injection H. auto with arith. + revert n. fix 1. destruct n as [|[|n]]. + - (* n = 0 *) + split; split; auto with arith. inversion 1. + - (* n = 1 *) + split; split; auto with arith. inversion_clear 1. inversion H0. + - (* n = (S (S n')) *) + destruct (even_odd_double n) as ((Ev,Ev'),(Od,Od')). + split; split; simpl; rewrite ?double_S. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. + + inversion_clear 1. inversion_clear H0. auto. + + injection 1. auto with arith. Qed. + (** Specializations *) -Lemma even_double : forall n, even n -> n = double (div2 n). -Proof fun n => proj1 (proj1 (even_odd_double n)). +Lemma even_double n : even n -> n = double (div2 n). +Proof proj1 (proj1 (even_odd_double n)). -Lemma double_even : forall n, n = double (div2 n) -> even n. -Proof fun n => proj2 (proj1 (even_odd_double n)). +Lemma double_even n : n = double (div2 n) -> even n. +Proof proj2 (proj1 (even_odd_double n)). -Lemma odd_double : forall n, odd n -> n = S (double (div2 n)). -Proof fun n => proj1 (proj2 (even_odd_double n)). +Lemma odd_double n : odd n -> n = S (double (div2 n)). +Proof proj1 (proj2 (even_odd_double n)). -Lemma double_odd : forall n, n = S (double (div2 n)) -> odd n. -Proof fun n => proj2 (proj2 (even_odd_double n)). +Lemma double_odd n : n = S (double (div2 n)) -> odd n. +Proof proj2 (proj2 (even_odd_double n)). Hint Resolve even_double double_even odd_double double_odd: arith. @@ -166,22 +151,8 @@ Defined. (** Doubling before dividing by two brings back to the initial number. *) -Lemma div2_double : forall n:nat, div2 (2*n) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double n : div2 (2*n) = n. +Proof. apply Nat.div2_double. Qed. -Lemma div2_double_plus_one : forall n:nat, div2 (S (2*n)) = n. -Proof. - induction n. - simpl; auto. - simpl. - replace (n+S(n+0)) with (S (2*n)). - f_equal; auto. - simpl; auto with arith. -Qed. +Lemma div2_double_plus_one n : div2 (S (2*n)) = n. +Proof. apply Nat.div2_succ_double. Qed. diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index ce8eb4785..699ac281e 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -6,11 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Equality on natural numbers *) - +Require Import PeanoNat. Local Open Scope nat_scope. -Implicit Types m n x y : nat. +(** Equality on natural numbers *) (** * Propositional equality *) @@ -22,28 +21,33 @@ Fixpoint eq_nat n m : Prop := | S n1, S m1 => eq_nat n1 m1 end. -Theorem eq_nat_refl : forall n, eq_nat n n. +Theorem eq_nat_refl n : eq_nat n n. +Proof. induction n; simpl; auto. Qed. Hint Resolve eq_nat_refl: arith v62. (** [eq] restricted to [nat] and [eq_nat] are equivalent *) -Lemma eq_eq_nat : forall n m, n = m -> eq_nat n m. - induction 1; trivial with arith. +Theorem eq_nat_is_eq n m : eq_nat n m <-> n = m. +Proof. + split. + - revert m; induction n; destruct m; simpl; contradiction || auto. + - intros <-; apply eq_nat_refl. Qed. -Hint Immediate eq_eq_nat: arith v62. -Lemma eq_nat_eq : forall n m, eq_nat n m -> n = m. - induction n; induction m; simpl; contradiction || auto with arith. +Lemma eq_eq_nat n m : n = m -> eq_nat n m. +Proof. + apply eq_nat_is_eq. Qed. -Hint Immediate eq_nat_eq: arith v62. -Theorem eq_nat_is_eq : forall n m, eq_nat n m <-> n = m. +Lemma eq_nat_eq n m : eq_nat n m -> n = m. Proof. - split; auto with arith. + apply eq_nat_is_eq. Qed. +Hint Immediate eq_eq_nat eq_nat_eq: arith v62. + Theorem eq_nat_elim : forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m. Proof. @@ -52,63 +56,47 @@ Qed. Theorem eq_nat_decide : forall n m, {eq_nat n m} + {~ eq_nat n m}. Proof. - induction n. - destruct m as [| n]. - auto with arith. - intros; right; red; trivial with arith. - destruct m as [| n0]. - right; red; auto with arith. - intros. - simpl. - apply IHn. + induction n; destruct m; simpl. + - left; trivial. + - right; intro; trivial. + - right; intro; trivial. + - apply IHn. Defined. -(** * Boolean equality on [nat] *) +(** * Boolean equality on [nat]. -Fixpoint beq_nat n m : bool := - match n, m with - | O, O => true - | O, S _ => false - | S _, O => false - | S n1, S m1 => beq_nat n1 m1 - end. + We reuse the one already defined in module [Nat]. + In scope [nat_scope], the notation "=?" can be used. *) -Lemma beq_nat_refl : forall n, true = beq_nat n n. -Proof. - intro x; induction x; simpl; auto. -Qed. +Notation beq_nat := Nat.eqb (compat "8.4"). -Definition beq_nat_eq : forall x y, true = beq_nat x y -> x = y. -Proof. - double induction x y; simpl. - reflexivity. - intros n H1 H2. discriminate H2. - intros n H1 H2. discriminate H2. - intros n H1 z H2 H3. case (H2 _ H3). reflexivity. -Defined. +Notation beq_nat_true_iff := Nat.eqb_eq (compat "8.4"). +Notation beq_nat_false_iff := Nat.eqb_neq (compat "8.4"). -Lemma beq_nat_true : forall x y, beq_nat x y = true -> x=y. +Lemma beq_nat_refl n : true = (n =? n). Proof. - induction x; destruct y; simpl; auto; intros; discriminate. + symmetry. apply Nat.eqb_refl. Qed. -Lemma beq_nat_false : forall x y, beq_nat x y = false -> x<>y. +Lemma beq_nat_true n m : (n =? m) = true -> n=m. Proof. - induction x; destruct y; simpl; auto; intros; discriminate. + apply Nat.eqb_eq. Qed. -Lemma beq_nat_true_iff : forall x y, beq_nat x y = true <-> x=y. +Lemma beq_nat_false n m : (n =? m) = false -> n<>m. Proof. - split. apply beq_nat_true. - intros; subst; symmetry; apply beq_nat_refl. + apply Nat.eqb_neq. Qed. -Lemma beq_nat_false_iff : forall x y, beq_nat x y = false <-> x<>y. +(** TODO: is it really useful here to have a Defined ? + Otherwise we could use Nat.eqb_eq *) + +Definition beq_nat_eq : forall n m, true = (n =? m) -> n = m. Proof. - intros x y. - split. apply beq_nat_false. - generalize (beq_nat_true_iff x y). - destruct beq_nat; auto. - intros IFF NEQ. elim NEQ. apply IFF; auto. -Qed. + induction n; destruct m; simpl. + - reflexivity. + - discriminate. + - discriminate. + - intros H. case (IHn _ H). reflexivity. +Defined. diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 4f679fe2b..050b45ed9 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -6,16 +6,22 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(** Nota : this file is OBSOLETE, and left only for compatibility. + Please consider instead predicates [Nat.Even] and [Nat.Odd] + and Boolean functions [Nat.even] and [Nat.odd]. *) + (** Here we define the predicates [even] and [odd] by mutual induction and we prove the decidability and the exclusion of those predicates. The main results about parity are proved in the module Div2. *) +Require Import PeanoNat. + Local Open Scope nat_scope. Implicit Types m n : nat. -(** * Definition of [even] and [odd], and basic facts *) +(** * Inductive definition of [even] and [odd] *) Inductive even : nat -> Prop := | even_O : even 0 @@ -26,225 +32,150 @@ with odd : nat -> Prop := Hint Constructors even: arith. Hint Constructors odd: arith. -Lemma even_or_odd : forall n, even n \/ odd n. +(** * Equivalence with predicates [Nat.Even] and [Nat.odd] *) + +Lemma even_equiv : forall n, even n <-> Nat.Even n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [now exists 0 | constructor]. + - split. + + inversion_clear 1. inversion_clear H0. + + now rewrite <- Nat.even_spec. + - rewrite Nat.Even_succ_succ, <- even_equiv. + split. + + inversion_clear 1. now inversion_clear H0. + + now do 2 constructor. +Qed. + +Lemma odd_equiv : forall n, odd n <-> Nat.Odd n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split. + + inversion_clear 1. + + now rewrite <- Nat.odd_spec. + - split; [ now exists 0 | do 2 constructor ]. + - rewrite Nat.Odd_succ_succ, <- odd_equiv. + split. + + inversion_clear 1. now inversion_clear H0. + + now do 2 constructor. +Qed. + +(** Basic facts *) + +Lemma even_or_odd n : even n \/ odd n. Proof. induction n. - auto with arith. - elim IHn; auto with arith. + - auto with arith. + - elim IHn; auto with arith. Qed. -Lemma even_odd_dec : forall n, {even n} + {odd n}. +Lemma even_odd_dec n : {even n} + {odd n}. Proof. induction n. - auto with arith. - elim IHn; auto with arith. + - auto with arith. + - elim IHn; auto with arith. Defined. -Lemma not_even_and_odd : forall n, even n -> odd n -> False. +Lemma not_even_and_odd n : even n -> odd n -> False. Proof. induction n. - intros even_0 odd_0. inversion odd_0. - intros even_Sn odd_Sn. inversion even_Sn. inversion odd_Sn. auto with arith. + - intros Ev Od. inversion Od. + - intros Ev Od. inversion Ev. inversion Od. auto with arith. Qed. (** * Facts about [even] & [odd] wrt. [plus] *) -Lemma even_plus_split : forall n m, - (even (n + m) -> even n /\ even m \/ odd n /\ odd m) -with odd_plus_split : forall n m, +Ltac parity2bool := + rewrite ?even_equiv, ?odd_equiv, <- ?Nat.even_spec, <- ?Nat.odd_spec. + +Ltac parity_binop_spec := + rewrite ?Nat.even_add, ?Nat.odd_add, ?Nat.even_mul, ?Nat.odd_mul. + +Ltac parity_binop := + parity2bool; parity_binop_spec; unfold Nat.odd; + do 2 destruct Nat.even; simpl; tauto. + + +Lemma even_plus_split n m : + even (n + m) -> even n /\ even m \/ odd n /\ odd m. +Proof. parity_binop. Qed. + +Lemma odd_plus_split n m : odd (n + m) -> odd n /\ even m \/ even n /\ odd m. -Proof. -intros. clear even_plus_split. destruct n; simpl in *. - auto with arith. - inversion_clear H; - apply odd_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. -intros. clear odd_plus_split. destruct n; simpl in *. - auto with arith. - inversion_clear H; - apply even_plus_split in H0 as [(H0,?)|(H0,?)]; auto with arith. -Qed. +Proof. parity_binop. Qed. -Lemma even_even_plus : forall n m, even n -> even m -> even (n + m) -with odd_plus_l : forall n m, odd n -> even m -> odd (n + m). -Proof. -intros n m [|] ?. trivial. apply even_S, odd_plus_l; trivial. -intros n m [] ?. apply odd_S, even_even_plus; trivial. -Qed. +Lemma even_even_plus n m : even n -> even m -> even (n + m). +Proof. parity_binop. Qed. -Lemma odd_plus_r : forall n m, even n -> odd m -> odd (n + m) -with odd_even_plus : forall n m, odd n -> odd m -> even (n + m). -Proof. -intros n m [|] ?. trivial. apply odd_S, odd_even_plus; trivial. -intros n m [] ?. apply even_S, odd_plus_r; trivial. -Qed. +Lemma odd_plus_l n m : odd n -> even m -> odd (n + m). +Proof. parity_binop. Qed. + +Lemma odd_plus_r n m : even n -> odd m -> odd (n + m). +Proof. parity_binop. Qed. -Lemma even_plus_aux : forall n m, +Lemma odd_even_plus n m : odd n -> odd m -> even (n + m). +Proof. parity_binop. Qed. + +Lemma even_plus_aux n m : (odd (n + m) <-> odd n /\ even m \/ even n /\ odd m) /\ (even (n + m) <-> even n /\ even m \/ odd n /\ odd m). -Proof. -split; split; auto using odd_plus_split, even_plus_split. -intros [[]|[]]; auto using odd_plus_r, odd_plus_l. -intros [[]|[]]; auto using even_even_plus, odd_even_plus. -Qed. +Proof. parity_binop. Qed. -Lemma even_plus_even_inv_r : forall n m, even (n + m) -> even n -> even m. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma even_plus_even_inv_r n m : even (n + m) -> even n -> even m. +Proof. parity_binop. Qed. -Lemma even_plus_even_inv_l : forall n m, even (n + m) -> even m -> even n. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma even_plus_even_inv_l n m : even (n + m) -> even m -> even n. +Proof. parity_binop. Qed. -Lemma even_plus_odd_inv_r : forall n m, even (n + m) -> odd n -> odd m. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma even_plus_odd_inv_r n m : even (n + m) -> odd n -> odd m. +Proof. parity_binop. Qed. -Lemma even_plus_odd_inv_l : forall n m, even (n + m) -> odd m -> odd n. -Proof. - intros n m H; destruct (even_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. -Hint Resolve even_even_plus odd_even_plus: arith. +Lemma even_plus_odd_inv_l n m : even (n + m) -> odd m -> odd n. +Proof. parity_binop. Qed. -Lemma odd_plus_even_inv_l : forall n m, odd (n + m) -> odd m -> even n. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma odd_plus_even_inv_l n m : odd (n + m) -> odd m -> even n. +Proof. parity_binop. Qed. -Lemma odd_plus_even_inv_r : forall n m, odd (n + m) -> odd n -> even m. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. +Lemma odd_plus_even_inv_r n m : odd (n + m) -> odd n -> even m. +Proof. parity_binop. Qed. -Lemma odd_plus_odd_inv_l : forall n m, odd (n + m) -> even m -> odd n. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd m); auto. -Qed. +Lemma odd_plus_odd_inv_l n m : odd (n + m) -> even m -> odd n. +Proof. parity_binop. Qed. -Lemma odd_plus_odd_inv_r : forall n m, odd (n + m) -> even n -> odd m. -Proof. - intros n m H; destruct (odd_plus_split n m) as [[]|[]]; auto. - intro; destruct (not_even_and_odd n); auto. -Qed. -Hint Resolve odd_plus_l odd_plus_r: arith. +Lemma odd_plus_odd_inv_r n m : odd (n + m) -> even n -> odd m. +Proof. parity_binop. Qed. (** * Facts about [even] and [odd] wrt. [mult] *) -Lemma even_mult_aux : - forall n m, - (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). -Proof. - intros n; elim n; simpl; auto with arith. - intros m; split; split; auto with arith. - intros H'; inversion H'. - intros H'; elim H'; auto. - intros n0 H' m; split; split; auto with arith. - intros H'0. - elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'3; intros H'1 H'2; - case H'1; auto. - intros H'5; elim H'5; intros H'6 H'7; auto with arith. - split; auto with arith. - case (H' m). - intros H'8 H'9; case H'9. - intros H'10; case H'10; auto with arith. - intros H'11 H'12; case (not_even_and_odd m); auto with arith. - intros H'5; elim H'5; intros H'6 H'7; case (not_even_and_odd (n0 * m)); auto. - case (H' m). - intros H'8 H'9; case H'9; auto. - intros H'0; elim H'0; intros H'1 H'2; clear H'0. - elim (even_plus_aux m (n0 * m)); auto. - intros H'0 H'3. - elim H'0. - intros H'4 H'5; apply H'5; auto. - left; split; auto with arith. - case (H' m). - intros H'6 H'7; elim H'7. - intros H'8 H'9; apply H'9. - left. - inversion H'1; auto. - intros H'0. - elim (even_plus_aux m (n0 * m)); intros H'3 H'4; case H'4. - intros H'1 H'2. - elim H'1; auto. - intros H; case H; auto. - intros H'5; elim H'5; intros H'6 H'7; auto with arith. - left. - case (H' m). - intros H'8; elim H'8. - intros H'9; elim H'9; auto with arith. - intros H'0; elim H'0; intros H'1. - case (even_or_odd m); intros H'2. - apply even_even_plus; auto. - case (H' m). - intros H H0; case H0; auto. - apply odd_even_plus; auto. - inversion H'1; case (H' m); auto. - intros H1; case H1; auto. - apply even_even_plus; auto. - case (H' m). - intros H H0; case H0; auto. -Qed. +Lemma even_mult_aux n m : + (odd (n * m) <-> odd n /\ odd m) /\ (even (n * m) <-> even n \/ even m). +Proof. parity_binop. Qed. -Lemma even_mult_l : forall n m, even n -> even (n * m). -Proof. - intros n m; case (even_mult_aux n m); auto. - intros H H0; case H0; auto. -Qed. +Lemma even_mult_l n m : even n -> even (n * m). +Proof. parity_binop. Qed. -Lemma even_mult_r : forall n m, even m -> even (n * m). -Proof. - intros n m; case (even_mult_aux n m); auto. - intros H H0; case H0; auto. -Qed. -Hint Resolve even_mult_l even_mult_r: arith. +Lemma even_mult_r n m : even m -> even (n * m). +Proof. parity_binop. Qed. -Lemma even_mult_inv_r : forall n m, even (n * m) -> odd n -> even m. -Proof. - intros n m H' H'0. - case (even_mult_aux n m). - intros H'1 H'2; elim H'2. - intros H'3; elim H'3; auto. - intros H; case (not_even_and_odd n); auto. -Qed. +Lemma even_mult_inv_r n m : even (n * m) -> odd n -> even m. +Proof. parity_binop. Qed. -Lemma even_mult_inv_l : forall n m, even (n * m) -> odd m -> even n. -Proof. - intros n m H' H'0. - case (even_mult_aux n m). - intros H'1 H'2; elim H'2. - intros H'3; elim H'3; auto. - intros H; case (not_even_and_odd m); auto. -Qed. +Lemma even_mult_inv_l n m : even (n * m) -> odd m -> even n. +Proof. parity_binop. Qed. -Lemma odd_mult : forall n m, odd n -> odd m -> odd (n * m). -Proof. - intros n m; case (even_mult_aux n m); intros H; case H; auto. -Qed. -Hint Resolve even_mult_l even_mult_r odd_mult: arith. +Lemma odd_mult n m : odd n -> odd m -> odd (n * m). +Proof. parity_binop. Qed. -Lemma odd_mult_inv_l : forall n m, odd (n * m) -> odd n. -Proof. - intros n m H'. - case (even_mult_aux n m). - intros H'1 H'2; elim H'1. - intros H'3; elim H'3; auto. -Qed. +Lemma odd_mult_inv_l n m : odd (n * m) -> odd n. +Proof. parity_binop. Qed. -Lemma odd_mult_inv_r : forall n m, odd (n * m) -> odd m. -Proof. - intros n m H'. - case (even_mult_aux n m). - intros H'1 H'2; elim H'1. - intros H'3; elim H'3; auto. -Qed. +Lemma odd_mult_inv_r n m : odd (n * m) -> odd m. +Proof. parity_binop. Qed. + +Hint Resolve + even_even_plus odd_even_plus odd_plus_l odd_plus_r + even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith. diff --git a/theories/Arith/Factorial.v b/theories/Arith/Factorial.v index 37aa1b2c5..d560b4af9 100644 --- a/theories/Arith/Factorial.v +++ b/theories/Arith/Factorial.v @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Plus. -Require Import Mult. -Require Import Lt. +Require Import PeanoNat Plus Mult Lt. Local Open Scope nat_scope. (** Factorial *) @@ -21,28 +19,19 @@ Fixpoint fact (n:nat) : nat := Arguments fact n%nat. -Lemma lt_O_fact : forall n:nat, 0 < fact n. +Lemma lt_O_fact n : 0 < fact n. Proof. - simple induction n; unfold lt; simpl; auto with arith. + induction n; simpl; auto with arith. Qed. -Lemma fact_neq_0 : forall n:nat, fact n <> 0. +Lemma fact_neq_0 n : fact n <> 0. Proof. - intro. - apply not_eq_sym. - apply lt_O_neq. - apply lt_O_fact. + apply Nat.neq_0_lt_0, lt_O_fact. Qed. -Lemma fact_le : forall n m:nat, n <= m -> fact n <= fact m. +Lemma fact_le n m : n <= m -> fact n <= fact m. Proof. induction 1. - apply le_n. - assert (1 * fact n <= S m * fact m). - apply mult_le_compat. - apply lt_le_S; apply lt_O_Sn. - assumption. - simpl (1 * fact n) in H0. - rewrite <- plus_n_O in H0. - assumption. + - apply le_n. + - simpl. transitivity (fact m). trivial. apply Nat.le_add_r. Qed. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 31b155071..d142f3105 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -6,149 +6,140 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: +(** Theorems about [gt] in [nat]. + + This file is DEPRECATED now, see module [PeanoNat.Nat] instead, + which favor [lt] over [gt]. + + [gt] is defined in [Init/Peano.v] as: << Definition gt (n m:nat) := m < n. >> *) -Require Import Le. -Require Import Lt. -Require Import Plus. +Require Import PeanoNat Le Lt Plus. Local Open Scope nat_scope. -Implicit Types m n p : nat. - (** * Order and successor *) -Theorem gt_Sn_O : forall n, S n > 0. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_O: arith v62. +Theorem gt_Sn_O n : S n > 0. +Proof Nat.lt_0_succ _. -Theorem gt_Sn_n : forall n, S n > n. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_n: arith v62. +Theorem gt_Sn_n n : S n > n. +Proof Nat.lt_succ_diag_r _. -Theorem gt_n_S : forall n m, n > m -> S n > S m. +Theorem gt_n_S n m : n > m -> S n > S m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Resolve gt_n_S: arith v62. -Lemma gt_S_n : forall n m, S m > S n -> m > n. +Lemma gt_S_n n m : S m > S n -> m > n. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Immediate gt_S_n: arith v62. -Theorem gt_S : forall n m, S n > m -> n > m \/ m = n. +Theorem gt_S n m : S n > m -> n > m \/ m = n. Proof. - intros n m H; unfold gt; apply le_lt_or_eq; auto with arith. + intro. now apply Nat.lt_eq_cases, Nat.succ_le_mono. Qed. -Lemma gt_pred : forall n m, m > S n -> pred m > n. +Lemma gt_pred n m : m > S n -> pred m > n. Proof. - auto with arith. + apply Nat.lt_succ_lt_pred. Qed. -Hint Immediate gt_pred: arith v62. (** * Irreflexivity *) -Lemma gt_irrefl : forall n, ~ n > n. -Proof lt_irrefl. -Hint Resolve gt_irrefl: arith v62. +Lemma gt_irrefl n : ~ n > n. +Proof Nat.lt_irrefl _. (** * Asymmetry *) -Lemma gt_asym : forall n m, n > m -> ~ m > n. -Proof fun n m => lt_asym m n. - -Hint Resolve gt_asym: arith v62. +Lemma gt_asym n m : n > m -> ~ m > n. +Proof Nat.lt_asymm _ _. (** * Relating strict and large orders *) -Lemma le_not_gt : forall n m, n <= m -> ~ n > m. -Proof le_not_lt. -Hint Resolve le_not_gt: arith v62. - -Lemma gt_not_le : forall n m, n > m -> ~ n <= m. +Lemma le_not_gt n m : n <= m -> ~ n > m. Proof. -auto with arith. + apply Nat.le_ngt. Qed. -Hint Resolve gt_not_le: arith v62. +Lemma gt_not_le n m : n > m -> ~ n <= m. +Proof. + apply Nat.lt_nge. +Qed. -Theorem le_S_gt : forall n m, S n <= m -> m > n. +Theorem le_S_gt n m : S n <= m -> m > n. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Immediate le_S_gt: arith v62. -Lemma gt_S_le : forall n m, S m > n -> n <= m. +Lemma gt_S_le n m : S m > n -> n <= m. Proof. - intros n p; exact (lt_n_Sm_le n p). + apply Nat.succ_le_mono. Qed. -Hint Immediate gt_S_le: arith v62. -Lemma gt_le_S : forall n m, m > n -> S n <= m. +Lemma gt_le_S n m : m > n -> S n <= m. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Resolve gt_le_S: arith v62. -Lemma le_gt_S : forall n m, n <= m -> S m > n. +Lemma le_gt_S n m : n <= m -> S m > n. Proof. - auto with arith. + apply Nat.succ_le_mono. Qed. -Hint Resolve le_gt_S: arith v62. (** * Transitivity *) -Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. +Theorem le_gt_trans n m p : m <= n -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. now apply Nat.lt_le_trans with m. Qed. -Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p. +Theorem gt_le_trans n m p : n > m -> p <= m -> n > p. Proof. - red; intros; apply le_lt_trans with m; auto with arith. + intros. now apply Nat.le_lt_trans with m. Qed. -Lemma gt_trans : forall n m p, n > m -> m > p -> n > p. +Lemma gt_trans n m p : n > m -> m > p -> n > p. Proof. - red; intros n m p H1 H2. - apply lt_trans with m; auto with arith. + intros. now apply Nat.lt_trans with m. Qed. -Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p. +Theorem gt_trans_S n m p : S n > m -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. apply Nat.lt_le_trans with m; trivial. now apply Nat.succ_le_mono. Qed. -Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. - (** * Comparison to 0 *) -Theorem gt_0_eq : forall n, n > 0 \/ 0 = n. +Theorem gt_0_eq n : n > 0 \/ 0 = n. Proof. - intro n; apply gt_S; auto with arith. + destruct n; [now right | left; apply Nat.lt_0_succ]. Qed. (** * Simplification and compatibility *) -Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. +Lemma plus_gt_reg_l n m p : p + n > p + m -> n > m. Proof. - red; intros n m p H; apply plus_lt_reg_l with p; auto with arith. + apply Nat.add_lt_mono_l. Qed. -Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m. +Lemma plus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. - auto with arith. + apply Nat.add_lt_mono_l. Qed. + +(** * Hints *) + +Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62. +Hint Immediate gt_S_n gt_pred : arith v62. +Hint Resolve gt_irrefl gt_asym : arith v62. +Hint Resolve le_not_gt gt_not_le : arith v62. +Hint Immediate le_S_gt gt_S_le : arith v62. +Hint Resolve gt_le_S le_gt_S : arith v62. +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. Hint Resolve plus_gt_compat_l: arith v62. (* begin hide *) diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index c3386787d..53bb5cde2 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,7 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Order on natural numbers. [le] is defined in [Init/Peano.v] as: +(** Order on natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [le] is defined in [Init/Peano.v] as: << Inductive le (n:nat) : nat -> Prop := | le_n : n <= n @@ -14,110 +18,58 @@ Inductive le (n:nat) : nat -> Prop := where "n <= m" := (le n m) : nat_scope. >> - *) +*) -Local Open Scope nat_scope. +Require Import PeanoNat. -Implicit Types m n p : nat. +Local Open Scope nat_scope. -(** * [le] is a pre-order *) +(** * [le] is an order on [nat] *) -(** Reflexivity *) -Theorem le_refl : forall n, n <= n. -Proof. - exact le_n. -Qed. +Notation le_refl := Nat.le_refl (compat "8.4"). +Notation le_trans := Nat.le_trans (compat "8.4"). +Notation le_antisym := Nat.le_antisymm (compat "8.4"). -(** Transitivity *) -Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. -Proof. - induction 2; auto. -Qed. Hint Resolve le_trans: arith v62. +Hint Immediate le_antisym: arith v62. -(** * Properties of [le] w.r.t. successor, predecessor and 0 *) - -(** Comparison to 0 *) - -Theorem le_0_n : forall n, 0 <= n. -Proof. - induction n; auto. -Qed. - -Theorem le_Sn_0 : forall n, ~ S n <= 0. -Proof. - red; intros n H. - change (IsSucc 0); elim H; simpl; auto with arith. -Qed. +(** * Properties of [le] w.r.t 0 *) -Hint Resolve le_0_n le_Sn_0: arith v62. +Notation le_0_n := Nat.le_0_l (compat "8.4"). (* 0 <= n *) +Notation le_Sn_0 := Nat.nle_succ_0 (compat "8.4"). (* ~ S n <= 0 *) -Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n. +Lemma le_n_0_eq n : n <= 0 -> 0 = n. Proof. - induction n. auto with arith. idtac. auto with arith. - intro; contradiction le_Sn_0 with n. + intros. symmetry. now apply Nat.le_0_r. Qed. -Hint Immediate le_n_0_eq: arith v62. +(** * Properties of [le] w.r.t successor *) -(** [le] and successor *) +(** See also [Nat.succ_le_mono]. *) Theorem le_n_S : forall n m, n <= m -> S n <= S m. -Proof. - induction 1; auto. -Qed. +Proof Peano.le_n_S. -Theorem le_n_Sn : forall n, n <= S n. -Proof. - auto. -Qed. +Theorem le_S_n : forall n m, S n <= S m -> n <= m. +Proof Peano.le_S_n. -Hint Resolve le_n_S le_n_Sn : arith v62. +Notation le_n_Sn := Nat.le_succ_diag_r (compat "8.4"). (* n <= S n *) +Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. -Proof. - intros n m H; apply le_trans with (S n); auto with arith. -Qed. -Hint Immediate le_Sn_le: arith v62. +Proof Nat.lt_le_incl. -Theorem le_S_n : forall n m, S n <= S m -> n <= m. -Proof. - exact Peano.le_S_n. -Qed. -Hint Immediate le_S_n: arith v62. +Hint Resolve le_0_n le_Sn_0: arith v62. +Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62. +Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62. -Theorem le_Sn_n : forall n, ~ S n <= n. -Proof. - induction n; auto with arith. -Qed. -Hint Resolve le_Sn_n: arith v62. +(** * Properties of [le] w.r.t predecessor *) -(** [le] and predecessor *) +Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *) +Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *) -Theorem le_pred_n : forall n, pred n <= n. -Proof. - induction n; auto with arith. -Qed. Hint Resolve le_pred_n: arith v62. -Theorem le_pred : forall n m, n <= m -> pred n <= pred m. -Proof. - exact Peano.le_pred. -Qed. - -(** * [le] is a order on [nat] *) -(** Antisymmetry *) - -Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m. -Proof. - intros n m H; destruct H as [|m' H]; auto with arith. - intros H1. - absurd (S m' <= m'); auto with arith. - apply le_trans with n; auto with arith. -Qed. -Hint Immediate le_antisym: arith v62. - - (** * A different elimination principle for the order on natural numbers *) Lemma le_elim_rel : @@ -126,10 +78,10 @@ Lemma le_elim_rel : (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. Proof. - induction n; auto with arith. - intros m Le. - elim Le; auto with arith. -Qed. + intros P H0 HS. + induction n; trivial. + intros m Le. elim Le; auto with arith. + Qed. (* begin hide *) Notation le_O_n := le_0_n (only parsing). diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 8559b782b..5a793ffdd 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,185 +6,149 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: +(** Strict order on natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [lt] is defined in library [Init/Peano.v] as: << Definition lt (n m:nat) := S n <= m. Infix "<" := lt : nat_scope. >> *) -Require Import Le. -Local Open Scope nat_scope. +Require Import PeanoNat. -Implicit Types m n p : nat. +Local Open Scope nat_scope. (** * Irreflexivity *) -Theorem lt_irrefl : forall n, ~ n < n. -Proof le_Sn_n. +Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *) + Hint Resolve lt_irrefl: arith v62. (** * Relationship between [le] and [lt] *) -Theorem lt_le_S : forall n m, n < m -> S n <= m. +Theorem lt_le_S n m : n < m -> S n <= m. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Immediate lt_le_S: arith v62. -Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m. +Theorem lt_n_Sm_le n m : n < S m -> n <= m. Proof. - auto with arith. + apply Nat.lt_succ_r. Qed. -Hint Immediate lt_n_Sm_le: arith v62. -Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m. +Theorem le_lt_n_Sm n m : n <= m -> n < S m. Proof. - auto with arith. + apply Nat.lt_succ_r. Qed. + +Hint Immediate lt_le_S: arith v62. +Hint Immediate lt_n_Sm_le: arith v62. Hint Immediate le_lt_n_Sm: arith v62. -Theorem le_not_lt : forall n m, n <= m -> ~ m < n. +Theorem le_not_lt n m : n <= m -> ~ m < n. Proof. - induction 1; auto with arith. + apply Nat.le_ngt. Qed. -Theorem lt_not_le : forall n m, n < m -> ~ m <= n. +Theorem lt_not_le n m : n < m -> ~ m <= n. Proof. - red; intros n m Lt Le; exact (le_not_lt m n Le Lt). + apply Nat.lt_nge. Qed. + Hint Immediate le_not_lt lt_not_le: arith v62. (** * Asymmetry *) -Theorem lt_asym : forall n m, n < m -> ~ m < n. -Proof. - induction 1; auto with arith. -Qed. +Notation lt_asym := Nat.lt_asymm (compat "8.4"). (* n<m -> ~m<n *) -(** * Order and successor *) +(** * Order and 0 *) -Theorem lt_n_Sn : forall n, n < S n. -Proof. - auto with arith. -Qed. -Hint Resolve lt_n_Sn: arith v62. +Notation lt_0_Sn := Nat.lt_0_succ (compat "8.4"). (* 0 < S n *) +Notation lt_n_0 := Nat.nlt_0_r (compat "8.4"). (* ~ n < 0 *) -Theorem lt_S : forall n m, n < m -> n < S m. +Theorem neq_0_lt n : 0 <> n -> 0 < n. Proof. - auto with arith. + intros. now apply Nat.neq_0_lt_0, Nat.neq_sym. Qed. -Hint Resolve lt_S: arith v62. -Theorem lt_n_S : forall n m, n < m -> S n < S m. +Theorem lt_0_neq n : 0 < n -> 0 <> n. Proof. - auto with arith. + intros. now apply Nat.neq_sym, Nat.neq_0_lt_0. Qed. -Hint Resolve lt_n_S: arith v62. -Theorem lt_S_n : forall n m, S n < S m -> n < m. +Hint Resolve lt_0_Sn lt_n_0 : arith v62. +Hint Immediate neq_0_lt lt_0_neq: arith v62. + +(** * Order and successor *) + +Notation lt_n_Sn := Nat.lt_succ_diag_r (compat "8.4"). (* n < S n *) +Notation lt_S := Nat.lt_lt_succ_r (compat "8.4"). (* n < m -> n < S m *) + +Theorem lt_n_S n m : n < m -> S n < S m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Immediate lt_S_n: arith v62. -Theorem lt_0_Sn : forall n, 0 < S n. +Theorem lt_S_n n m : S n < S m -> n < m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Resolve lt_0_Sn: arith v62. -Theorem lt_n_0 : forall n, ~ n < 0. -Proof le_Sn_0. -Hint Resolve lt_n_0: arith v62. +Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62. +Hint Immediate lt_S_n : arith v62. (** * Predecessor *) -Lemma S_pred : forall n m, m < n -> n = S (pred n). +Lemma S_pred n m : m < n -> n = S (pred n). Proof. -induction 1; auto with arith. + intros. symmetry. now apply Nat.lt_succ_pred with m. Qed. -Lemma lt_pred : forall n m, S n < m -> n < pred m. +Lemma lt_pred n m : S n < m -> n < pred m. Proof. -induction 1; simpl; auto with arith. + apply Nat.lt_succ_lt_pred. Qed. -Hint Immediate lt_pred: arith v62. -Lemma lt_pred_n_n : forall n, 0 < n -> pred n < n. -destruct 1; simpl; auto with arith. +Lemma lt_pred_n_n n : 0 < n -> pred n < n. +Proof. + intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0. Qed. + +Hint Immediate lt_pred: arith v62. Hint Resolve lt_pred_n_n: arith v62. (** * Transitivity properties *) -Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. -Proof. - induction 2; auto with arith. -Qed. - -Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. -Proof. - induction 2; auto with arith. -Qed. - -Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. -Proof. - induction 2; auto with arith. -Qed. +Notation lt_trans := Nat.lt_trans (compat "8.4"). +Notation lt_le_trans := Nat.lt_le_trans (compat "8.4"). +Notation le_lt_trans := Nat.le_lt_trans (compat "8.4"). Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. (** * Large = strict or equal *) -Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. -Proof. - induction 1; auto with arith. -Qed. +Notation le_lt_or_eq_iff := Nat.lt_eq_cases (compat "8.4"). -Theorem le_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m. +Theorem le_lt_or_eq n m : n <= m -> n < m \/ n = m. Proof. - split. - intros; apply le_lt_or_eq; auto. - destruct 1; subst; auto with arith. + apply Nat.lt_eq_cases. Qed. -Theorem lt_le_weak : forall n m, n < m -> n <= m. -Proof. - auto with arith. -Qed. +Notation lt_le_weak := Nat.lt_le_incl (compat "8.4"). + Hint Immediate lt_le_weak: arith v62. (** * Dichotomy *) -Theorem le_or_lt : forall n m, n <= m \/ m < n. -Proof. - intros n m; pattern n, m; apply nat_double_ind; auto with arith. - induction 1; auto with arith. -Qed. - -Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n. -Proof. - intros m n diff. - elim (le_or_lt n m); [ intro H'0 | auto with arith ]. - elim (le_lt_or_eq n m); auto with arith. - intro H'; elim diff; auto with arith. -Qed. - -(** * Comparison to 0 *) +Notation le_or_lt := Nat.le_gt_cases (compat "8.4"). (* n <= m \/ m < n *) -Theorem neq_0_lt : forall n, 0 <> n -> 0 < n. +Theorem nat_total_order n m : n <> m -> n < m \/ m < n. Proof. - induction n; auto with arith. - intros; absurd (0 = 0); trivial with arith. + apply Nat.lt_gt_cases. Qed. -Hint Immediate neq_0_lt: arith v62. - -Theorem lt_0_neq : forall n, 0 < n -> 0 <> n. -Proof. - induction 1; auto with arith. -Qed. -Hint Immediate lt_0_neq: arith v62. (* begin hide *) Notation lt_O_Sn := lt_0_Sn (only parsing). @@ -192,3 +156,7 @@ Notation neq_O_lt := neq_0_lt (only parsing). Notation lt_O_neq := lt_0_neq (only parsing). Notation lt_n_O := lt_n_0 (only parsing). (* end hide *) + +(** For compatibility, we "Require" the same files as before *) + +Require Import Le. diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 5623564a2..d38ed7e4e 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) +(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *) -Require Import NPeano. +Require Import PeanoNat. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation max := Peano.max (only parsing). +Notation max := Nat.max (only parsing). Definition max_0_l := Nat.max_0_l. Definition max_0_r := Nat.max_0_r. diff --git a/theories/Arith/Min.v b/theories/Arith/Min.v index a2a7930df..115901792 100644 --- a/theories/Arith/Min.v +++ b/theories/Arith/Min.v @@ -6,14 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** THIS FILE IS DEPRECATED. Use [NPeano.Nat] instead. *) +(** THIS FILE IS DEPRECATED. Use [PeanoNat.Nat] instead. *) -Require Import NPeano. +Require Import PeanoNat. Local Open Scope nat_scope. Implicit Types m n p : nat. -Notation min := Peano.min (only parsing). +Notation min := Nat.min (only parsing). Definition min_0_l := Nat.min_0_l. Definition min_0_r := Nat.min_0_r. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index 480243311..cb6cc646f 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -6,151 +6,114 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** [minus] (difference between two natural numbers) is defined in [Init/Peano.v] as: +(** Properties of subtraction between natural numbers. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [minus] is now an alias for [Nat.sub], which is defined in [Init/Nat.v] as: << -Fixpoint minus (n m:nat) : nat := +Fixpoint sub (n m:nat) : nat := match n, m with - | O, _ => n - | S k, O => S k | S k, S l => k - l + | _, _ => n end -where "n - m" := (minus n m) : nat_scope. +where "n - m" := (sub n m) : nat_scope. >> *) -Require Import Lt. -Require Import Le. +Require Import PeanoNat Lt Le. Local Open Scope nat_scope. -Implicit Types m n p : nat. - (** * 0 is right neutral *) -Lemma minus_n_O : forall n, n = n - 0. +Lemma minus_n_O n : n = n - 0. Proof. - induction n; simpl; auto with arith. + symmetry. apply Nat.sub_0_r. Qed. -Hint Resolve minus_n_O: arith v62. (** * Permutation with successor *) -Lemma minus_Sn_m : forall n m, m <= n -> S (n - m) = S n - m. +Lemma minus_Sn_m n m : m <= n -> S (n - m) = S n - m. Proof. - intros n m Le; pattern m, n; apply le_elim_rel; simpl; - auto with arith. + intros. symmetry. now apply Nat.sub_succ_l. Qed. -Hint Resolve minus_Sn_m: arith v62. -Theorem pred_of_minus : forall n, pred n = n - 1. +Theorem pred_of_minus n : pred n = n - 1. Proof. - intro x; induction x; simpl; auto with arith. + symmetry. apply Nat.sub_1_r. Qed. (** * Diagonal *) -Lemma minus_diag : forall n, n - n = 0. -Proof. - induction n; simpl; auto with arith. -Qed. +Notation minus_diag := Nat.sub_diag (compat "8.4"). (* n - n = 0 *) -Lemma minus_diag_reverse : forall n, 0 = n - n. +Lemma minus_diag_reverse n : 0 = n - n. Proof. - auto using minus_diag. + symmetry. apply Nat.sub_diag. Qed. -Hint Resolve minus_diag_reverse: arith v62. Notation minus_n_n := minus_diag_reverse. (** * Simplification *) -Lemma minus_plus_simpl_l_reverse : forall n m p, n - m = p + n - (p + m). +Lemma minus_plus_simpl_l_reverse n m p : n - m = p + n - (p + m). Proof. - induction p; simpl; auto with arith. + now rewrite Nat.sub_add_distr, Nat.add_comm, Nat.add_sub. Qed. -Hint Resolve minus_plus_simpl_l_reverse: arith v62. (** * Relation with plus *) -Lemma plus_minus : forall n m p, n = m + p -> p = n - m. +Lemma plus_minus n m p : n = m + p -> p = n - m. Proof. - intros n m p; pattern m, n; apply nat_double_ind; simpl; - intros. - replace (n0 - 0) with n0; auto with arith. - absurd (0 = S (n0 + p)); auto with arith. - auto with arith. + symmetry. now apply Nat.add_sub_eq_l. Qed. -Hint Immediate plus_minus: arith v62. -Lemma minus_plus : forall n m, n + m - n = m. - symmetry ; auto with arith. +Lemma minus_plus n m : n + m - n = m. +Proof. + rewrite Nat.add_comm. apply Nat.add_sub. Qed. -Hint Resolve minus_plus: arith v62. -Lemma le_plus_minus : forall n m, n <= m -> m = n + (m - n). +Lemma le_plus_minus_r n m : n <= m -> n + (m - n) = m. Proof. - intros n m Le; pattern n, m; apply le_elim_rel; simpl; - auto with arith. + rewrite Nat.add_comm. apply Nat.sub_add. Qed. -Hint Resolve le_plus_minus: arith v62. -Lemma le_plus_minus_r : forall n m, n <= m -> n + (m - n) = m. +Lemma le_plus_minus n m : n <= m -> m = n + (m - n). Proof. - symmetry ; auto with arith. + intros. symmetry. rewrite Nat.add_comm. now apply Nat.sub_add. Qed. -Hint Resolve le_plus_minus_r: arith v62. (** * Relation with order *) -Theorem minus_le_compat_r : forall n m p : nat, n <= m -> n - p <= m - p. -Proof. - intros n m p; generalize n m; clear n m; induction p as [|p HI]. - intros n m; rewrite <- (minus_n_O n); rewrite <- (minus_n_O m); trivial. - - intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); auto with arith. - intros q r H _. simpl. auto using HI. -Qed. - -Theorem minus_le_compat_l : forall n m p : nat, n <= m -> p - m <= p - n. -Proof. - intros n m p; generalize n m; clear n m; induction p as [|p HI]. - trivial. +Notation minus_le_compat_r := + Nat.sub_le_mono_r (compat "8.4"). (* n <= m -> n - p <= m - p. *) - intros n m Hnm; apply le_elim_rel with (n:=n) (m:=m); trivial. - intros q; destruct q; auto with arith. - simpl. - apply le_trans with (m := p - 0); [apply HI | rewrite <- minus_n_O]; - auto with arith. +Notation minus_le_compat_l := + Nat.sub_le_mono_l (compat "8.4"). (* n <= m -> p - m <= p - n. *) - intros q r Hqr _. simpl. auto using HI. -Qed. +Notation le_minus := Nat.le_sub_l (compat "8.4"). (* n - m <= n *) +Notation lt_minus := Nat.sub_lt (compat "8.4"). (* m <= n -> 0 < m -> n-m < n *) -Corollary le_minus : forall n m, n - m <= n. +Lemma lt_O_minus_lt n m : 0 < n - m -> m < n. Proof. - intros n m; rewrite minus_n_O; auto using minus_le_compat_l with arith. + apply Nat.lt_add_lt_sub_r. Qed. -Lemma lt_minus : forall n m, m <= n -> 0 < m -> n - m < n. +Theorem not_le_minus_0 n m : ~ m <= n -> n - m = 0. Proof. - intros n m Le; pattern m, n; apply le_elim_rel; simpl; - auto using le_minus with arith. - intros; absurd (0 < 0); auto with arith. + intros. now apply Nat.sub_0_le, Nat.lt_le_incl, Nat.lt_nge. Qed. -Hint Resolve lt_minus: arith v62. -Lemma lt_O_minus_lt : forall n m, 0 < n - m -> m < n. -Proof. - intros n m; pattern n, m; apply nat_double_ind; simpl; - auto with arith. - intros; absurd (0 < 0); trivial with arith. -Qed. -Hint Immediate lt_O_minus_lt: arith v62. +(** * Hints *) -Theorem not_le_minus_0 : forall n m, ~ m <= n -> n - m = 0. -Proof. - intros y x; pattern y, x; apply nat_double_ind; - [ simpl; trivial with arith - | intros n H; absurd (0 <= S n); [ assumption | apply le_O_n ] - | simpl; intros n m H1 H2; apply H1; unfold not; intros H3; - apply H2; apply le_n_S; assumption ]. -Qed. +Hint Resolve minus_n_O: arith v62. +Hint Resolve minus_Sn_m: arith v62. +Hint Resolve minus_diag_reverse: arith v62. +Hint Resolve minus_plus_simpl_l_reverse: arith v62. +Hint Immediate plus_minus: arith v62. +Hint Resolve minus_plus: arith v62. +Hint Resolve le_plus_minus: arith v62. +Hint Resolve le_plus_minus_r: arith v62. +Hint Resolve lt_minus: arith v62. +Hint Immediate lt_O_minus_lt: arith v62. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index cbb9b376b..d53a1646a 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -6,215 +6,139 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Export Plus. -Require Export Minus. -Require Export Lt. -Require Export Le. +(** * Properties of multiplication. -Local Open Scope nat_scope. + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [Nat.mul] is defined in [Init/Nat.v]. +*) -Implicit Types m n p : nat. +Require Import PeanoNat. +(** For Compatibility: *) +Require Export Plus Minus Le Lt. -(** Theorems about multiplication in [nat]. [mult] is defined in module [Init/Peano.v]. *) +Local Open Scope nat_scope. (** * [nat] is a semi-ring *) (** ** Zero property *) -Lemma mult_0_r : forall n, n * 0 = 0. -Proof. - intro; symmetry ; apply mult_n_O. -Qed. - -Lemma mult_0_l : forall n, 0 * n = 0. -Proof. - reflexivity. -Qed. +Notation mult_0_l := Nat.mul_0_l (compat "8.4"). (* 0 * n = 0 *) +Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *) (** ** 1 is neutral *) -Lemma mult_1_l : forall n, 1 * n = n. -Proof. - simpl; auto with arith. -Qed. -Hint Resolve mult_1_l: arith v62. +Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *) +Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *) -Lemma mult_1_r : forall n, n * 1 = n. -Proof. - induction n; [ trivial | - simpl; rewrite IHn; reflexivity]. -Qed. -Hint Resolve mult_1_r: arith v62. +Hint Resolve mult_1_l mult_1_r: arith v62. (** ** Commutativity *) -Lemma mult_comm : forall n m, n * m = m * n. -Proof. -intros; induction n; simpl; auto with arith. -rewrite <- mult_n_Sm. -rewrite IHn; apply plus_comm. -Qed. +Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *) + Hint Resolve mult_comm: arith v62. (** ** Distributivity *) -Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. -Proof. - intros; induction n; simpl; auto with arith. - rewrite <- plus_assoc, IHn; auto with arith. -Qed. -Hint Resolve mult_plus_distr_r: arith v62. +Notation mult_plus_distr_r := + Nat.mul_add_distr_r (compat "8.4"). (* (n+m)*p = n*p + m*p *) -Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. -Proof. - induction n. trivial. - intros. simpl. rewrite IHn. symmetry. apply plus_permute_2_in_4. -Qed. +Notation mult_plus_distr_l := + Nat.mul_add_distr_l (compat "8.4"). (* n*(m+p) = n*m + n*p *) -Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. -Proof. - intros; induction n, m using nat_double_ind; simpl; auto with arith. - rewrite <- minus_plus_simpl_l_reverse; auto with arith. -Qed. -Hint Resolve mult_minus_distr_r: arith v62. +Notation mult_minus_distr_r := + Nat.mul_sub_distr_r (compat "8.4"). (* (n-m)*p = n*p - m*p *) -Lemma mult_minus_distr_l : forall n m p, n * (m - p) = n * m - n * p. -Proof. - intros n m p. - rewrite mult_comm, mult_minus_distr_r, (mult_comm m n), (mult_comm p n); reflexivity. -Qed. +Notation mult_minus_distr_l := + Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *) + +Hint Resolve mult_plus_distr_r: arith v62. +Hint Resolve mult_minus_distr_r: arith v62. Hint Resolve mult_minus_distr_l: arith v62. (** ** Associativity *) -Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). -Proof. - intros; induction n; simpl; auto with arith. - rewrite mult_plus_distr_r. - induction IHn; auto with arith. -Qed. -Hint Resolve mult_assoc_reverse: arith v62. +Notation mult_assoc := Nat.mul_assoc (compat "8.4"). (* n*(m*p)=n*m*p *) -Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. +Lemma mult_assoc_reverse n m p : n * m * p = n * (m * p). Proof. - auto with arith. + symmetry. apply Nat.mul_assoc. Qed. + +Hint Resolve mult_assoc_reverse: arith v62. Hint Resolve mult_assoc: arith v62. (** ** Inversion lemmas *) -Lemma mult_is_O : forall n m, n * m = 0 -> n = 0 \/ m = 0. +Lemma mult_is_O n m : n * m = 0 -> n = 0 \/ m = 0. Proof. - destruct n as [| n]; simpl; intros m H. - left; trivial. - right; apply plus_is_O in H; destruct H; trivial. + apply Nat.eq_mul_0. Qed. -Lemma mult_is_one : forall n m, n * m = 1 -> n = 1 /\ m = 1. +Lemma mult_is_one n m : n * m = 1 -> n = 1 /\ m = 1. Proof. - destruct n as [|n]; simpl; intros m H. - edestruct O_S; eauto. - destruct plus_is_one with (1:=H) as [[-> Hnm] | [-> Hnm]]. - simpl in H; rewrite mult_0_r in H; elim (O_S _ H). - rewrite mult_1_r in Hnm; auto. + apply Nat.eq_mul_1. Qed. (** ** Multiplication and successor *) -Lemma mult_succ_l : forall n m:nat, S n * m = n * m + m. -Proof. - intros; simpl. rewrite plus_comm. reflexivity. -Qed. - -Lemma mult_succ_r : forall n m:nat, n * S m = n * m + n. -Proof. - induction n as [| p H]; intro m; simpl. - reflexivity. - rewrite H, <- plus_n_Sm; apply f_equal; rewrite plus_assoc; reflexivity. -Qed. +Notation mult_succ_l := Nat.mul_succ_l (compat "8.4"). (* S n * m = n * m + m *) +Notation mult_succ_r := Nat.mul_succ_r (compat "8.4"). (* n * S m = n * m + n *) (** * Compatibility with orders *) -Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. +Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. - induction m; simpl; auto with arith. + destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. Hint Resolve mult_O_le: arith v62. -Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. +Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. - induction p as [| p IHp]; intros; simpl. - apply le_n. - auto using plus_le_compat. + apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *) Qed. Hint Resolve mult_le_compat_l: arith. - -Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. +Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p. Proof. - intros m n p H; rewrite mult_comm, (mult_comm n); auto with arith. + apply Nat.mul_le_mono_nonneg_r, Nat.le_0_l. Qed. -Lemma mult_le_compat : - forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. +Lemma mult_le_compat n m p q : n <= m -> p <= q -> n * p <= m * q. Proof. - intros m n p q Hmn Hpq; induction Hmn. - induction Hpq. - (* m*p<=m*p *) - apply le_n. - (* m*p<=m*m0 -> m*p<=m*(S m0) *) - rewrite <- mult_n_Sm; apply le_trans with (m * m0). - assumption. - apply le_plus_l. - (* m*p<=m0*q -> m*p<=(S m0)*q *) - simpl; apply le_trans with (m0 * q). - assumption. - apply le_plus_r. + intros. apply Nat.mul_le_mono_nonneg; trivial; apply Nat.le_0_l. Qed. -Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. +Lemma mult_S_lt_compat_l n m p : m < p -> S n * m < S n * p. Proof. - induction n; intros; simpl in *. - rewrite <- 2 plus_n_O; assumption. - auto using plus_lt_compat. + apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ. Qed. Hint Resolve mult_S_lt_compat_l: arith. -Lemma mult_lt_compat_l : forall n m p, n < m -> 0 < p -> p * n < p * m. +Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m. Proof. - intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). - now apply mult_S_lt_compat_l. + intros. now apply Nat.mul_lt_mono_pos_l. Qed. -Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. +Lemma mult_lt_compat_r n m p : n < m -> 0 < p -> n * p < m * p. Proof. - intros m n p H Hp. destruct p. elim (lt_irrefl _ Hp). - rewrite (mult_comm m), (mult_comm n). now apply mult_S_lt_compat_l. + intros. now apply Nat.mul_lt_mono_pos_r. Qed. -Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. +Lemma mult_S_le_reg_l n m p : S n * m <= S n * p -> m <= p. Proof. - intros m n p H; destruct (le_or_lt n p). trivial. - assert (H1:S m * n < S m * n). - apply le_lt_trans with (m := S m * p). assumption. - apply mult_S_lt_compat_l. assumption. - elim (lt_irrefl _ H1). + apply Nat.mul_le_mono_pos_l, Nat.lt_0_succ. Qed. (** * n|->2*n and n|->2n+1 have disjoint image *) -Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. +Theorem odd_even_lem p q : 2 * p + 1 <> 2 * q. Proof. - induction p; destruct q. - discriminate. - simpl; rewrite plus_comm. discriminate. - discriminate. - intro H0; destruct (IHp q). - replace (2 * q) with (2 * S q - 2). - rewrite <- H0; simpl. - repeat rewrite (fun x y => plus_comm x (S y)); simpl; auto. - simpl; rewrite (fun y => plus_comm q (S y)); destruct q; simpl; auto. + intro. apply (Nat.Even_Odd_False (2*q)). + - now exists q. + - now exists p. Qed. @@ -232,10 +156,9 @@ Fixpoint mult_acc (s:nat) m n : nat := Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. - induction n as [| p IHp]; simpl; auto. - intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. - rewrite <- plus_assoc_reverse; apply f_equal2; auto. - rewrite plus_comm; auto. + induction n as [| n IHn]; simpl; auto. + intros. rewrite Nat.add_assoc, IHn. f_equal. + rewrite Nat.add_comm. apply plus_tail_plus. Qed. Definition tail_mult n m := mult_acc 0 m n. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v new file mode 100644 index 000000000..3657d9544 --- /dev/null +++ b/theories/Arith/PeanoNat.v @@ -0,0 +1,755 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +(* Evgeny Makarov, INRIA, 2007 *) +(************************************************************************) + +Require Import NAxioms NProperties OrdersFacts. + +(** Implementation of [NAxiomsSig] by [nat] *) + +Module Nat + <: NAxiomsSig + <: UsualDecidableTypeFull + <: OrderedTypeFull + <: TotalOrder. + +(** Operations over [nat] are defined in a separate module *) + +Include Coq.Init.Nat. + +(** When including property functors, inline t eq zero one two lt le succ *) + +Set Inline Level 50. + +(** All operations are well-defined (trivial here since eq is Leibniz) *) + +Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence. +Local Obligation Tactic := simpl_relation. +Program Instance succ_wd : Proper (eq==>eq) S. +Program Instance pred_wd : Proper (eq==>eq) pred. +Program Instance add_wd : Proper (eq==>eq==>eq) plus. +Program Instance sub_wd : Proper (eq==>eq==>eq) minus. +Program Instance mul_wd : Proper (eq==>eq==>eq) mult. +Program Instance pow_wd : Proper (eq==>eq==>eq) pow. +Program Instance div_wd : Proper (eq==>eq==>eq) div. +Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. +Program Instance lt_wd : Proper (eq==>eq==>iff) lt. +Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit. + +(** Bi-directional induction. *) + +Theorem bi_induction : + forall A : nat -> Prop, Proper (eq==>iff) A -> + A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. +Proof. +intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. +Qed. + +(** Recursion fonction *) + +Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A := + nat_rect (fun _ => A). + +Instance recursion_wd {A} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. +Proof. +intros a a' Ha f f' Hf n n' Hn. subst n'. +induction n; simpl; auto. apply Hf; auto. +Qed. + +Theorem recursion_0 : + forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a. +Proof. +reflexivity. +Qed. + +Theorem recursion_succ : + forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), + Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> + forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). +Proof. +unfold Proper, respectful in *; induction n; simpl; auto. +Qed. + +(** ** Remaining constants not defined in Coq.Init.Nat *) + +(** NB: Aliasing [le] is mandatory, since only a Definition can implement + an interface Parameter... *) + +Definition eq := @Logic.eq nat. +Definition le := Peano.le. +Definition lt := Peano.lt. + +(** ** Basic specifications : pred add sub mul *) + +Lemma pred_succ n : pred (S n) = n. +Proof. +reflexivity. +Qed. + +Lemma pred_0 : pred 0 = 0. +Proof. +reflexivity. +Qed. + +Lemma one_succ : 1 = S 0. +Proof. +reflexivity. +Qed. + +Lemma two_succ : 2 = S 1. +Proof. +reflexivity. +Qed. + +Lemma add_0_l n : 0 + n = n. +Proof. +reflexivity. +Qed. + +Lemma add_succ_l n m : (S n) + m = S (n + m). +Proof. +reflexivity. +Qed. + +Lemma sub_0_r n : n - 0 = n. +Proof. +now destruct n. +Qed. + +Lemma sub_succ_r n m : n - (S m) = pred (n - m). +Proof. +revert m. induction n; destruct m; simpl; auto. apply sub_0_r. +Qed. + +Lemma mul_0_l n : 0 * n = 0. +Proof. +reflexivity. +Qed. + +Lemma mul_succ_l n m : S n * m = n * m + m. +Proof. +assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x. +assert (comm : forall x y, x+y = y+x). +{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. } +now rewrite comm. +Qed. + +Lemma lt_succ_r n m : n < S m <-> n <= m. +Proof. +split. apply Peano.le_S_n. induction 1; auto. +Qed. + +(** ** Boolean comparisons *) + +Lemma eqb_eq n m : eqb n m = true <-> n = m. +Proof. + revert m. + induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + - now intros ->. + - now injection 1. +Qed. + +Lemma leb_le n m : (n <=? m) = true <-> n <= m. +Proof. + revert m. + induction n; destruct m; simpl. + - now split. + - split; trivial. intros; apply Peano.le_0_n. + - now split. + - rewrite IHn; split. + + apply Peano.le_n_S. + + apply Peano.le_S_n. +Qed. + +Lemma ltb_lt n m : (n <? m) = true <-> n < m. +Proof. + apply leb_le. +Qed. + +(** ** Decidability of equality over [nat]. *) + +Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}. +Proof. + induction n; destruct m. + - now left. + - now right. + - now right. + - destruct (IHn m); [left|right]; auto. +Defined. + +(** ** Ternary comparison *) + +(** With [nat], it would be easier to prove first [compare_spec], + then the properties below. But then we wouldn't be able to + benefit from functor [BoolOrderFacts] *) + +Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy. +Qed. + +Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy. + - intros _. apply Peano.le_n_S, Peano.le_0_n. + - apply Peano.le_n_S. + - apply Peano.le_S_n. +Qed. + +Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m. +Proof. + revert m; induction n; destruct m; simpl; rewrite ?IHn. + - now split. + - split; intros. apply Peano.le_0_n. easy. + - split. now destruct 1. inversion 1. + - split; intros. now apply Peano.le_n_S. now apply Peano.le_S_n. +Qed. + +Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m). +Proof. + revert m; induction n; destruct m; simpl; trivial. +Qed. + +Lemma compare_succ n m : (S n ?= S m) = (n ?= m). +Proof. + reflexivity. +Qed. + + +(* BUG: Ajout d'un cas * après preuve finie (deuxième niveau +++*** ) : + * ---> Anomaly: Uncaught exception Proofview.IndexOutOfRange(_). Please report. *) + +(** ** Minimum, maximum *) + +Lemma max_l : forall n m, m <= n -> max n m = n. +Proof. + exact Peano.max_l. +Qed. + +Lemma max_r : forall n m, n <= m -> max n m = m. +Proof. + exact Peano.max_r. +Qed. + +Lemma min_l : forall n m, n <= m -> min n m = n. +Proof. + exact Peano.min_l. +Qed. + +Lemma min_r : forall n m, m <= n -> min n m = m. +Proof. + exact Peano.min_r. +Qed. + +(** Some more advanced properties of comparison and orders, + including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *) + +Include BoolOrderFacts. + +(** We can now derive all properties of basic functions and orders, + and use these properties for proving the specs of more advanced + functions. *) + +Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + +(** ** Power *) + +Lemma pow_neg_r a b : b<0 -> a^b = 0. inversion 1. Qed. + +Lemma pow_0_r a : a^0 = 1. +Proof. reflexivity. Qed. + +Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b. +Proof. reflexivity. Qed. + +(** ** Square *) + +Lemma square_spec n : square n = n * n. +Proof. reflexivity. Qed. + +(** ** Parity *) + +Definition Even n := exists m, n = 2*m. +Definition Odd n := exists m, n = 2*m+1. + +Module Private_Parity. + +Lemma Even_1 : ~ Even 1. +Proof. + intros ([|], H); try discriminate. + simpl in H. now rewrite <- plus_n_Sm in H. +Qed. + +Lemma Even_2 n : Even n <-> Even (S (S n)). +Proof. + split; intros (m,H). + - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. + - destruct m; try discriminate. + exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H. +Qed. + +Lemma Odd_0 : ~ Odd 0. +Proof. + now intros ([|], H). +Qed. + +Lemma Odd_2 n : Odd n <-> Odd (S (S n)). +Proof. + split; intros (m,H). + - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). + - destruct m; try discriminate. + exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H. + simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O. +Qed. + +End Private_Parity. +Import Private_Parity. + +Lemma even_spec : forall n, even n = true <-> Even n. +Proof. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [ now exists 0 | trivial ]. + - split; [ discriminate | intro H; elim (Even_1 H) ]. + - rewrite even_spec. apply Even_2. +Qed. + +Lemma odd_spec : forall n, odd n = true <-> Odd n. +Proof. + unfold odd. + fix 1. + destruct n as [|[|n]]; simpl. + - split; [ discriminate | intro H; elim (Odd_0 H) ]. + - split; [ now exists 0 | trivial ]. + - rewrite odd_spec. apply Odd_2. +Qed. + +(** ** Division *) + +Lemma divmod_spec : forall x y q u, u <= y -> + let (q',u') := divmod x y q u in + x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. +Proof. + induction x. + - simpl; intuition. + - intros y q u H. destruct u; simpl divmod. + + generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ, sub_0_r, sub_diag, add_0_r. + now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r. + + assert (H' : u <= y). + { apply le_trans with (S u); trivial. do 2 constructor. } + generalize (IHx y q u H'). destruct divmod as (q',u'). + intros (EQ,LE); split; trivial. + rewrite <- EQ. + rewrite !add_succ_l, <- add_succ_r. f_equal. now rewrite <- sub_succ_l. +Qed. + +Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y. +Proof. + intros Hy. + destruct y; [ now elim Hy | clear Hy ]. + unfold div, modulo. + generalize (divmod_spec x y 0 y (le_n y)). + destruct divmod as (q,u). + intros (U,V). + simpl in *. + now rewrite mul_0_r, sub_diag, !add_0_r in U. +Qed. + +Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y. +Proof. + intros Hx Hy. split. apply le_0_l. + destruct y; [ now elim Hy | clear Hy ]. + unfold modulo. + apply lt_succ_r, le_sub_l. +Qed. + +(** ** Square root *) + +Lemma sqrt_iter_spec : forall k p q r, + q = p+p -> r<=q -> + let s := sqrt_iter k p q r in + s*s <= k + p*p + (q - r) < (S s)*(S s). +Proof. + induction k. + - (* k = 0 *) + simpl; intros p q r Hq Hr. + split. + + apply le_add_r. + + apply lt_succ_r. + rewrite mul_succ_r. + rewrite add_assoc, (add_comm p), <- add_assoc. + apply add_le_mono_l. + rewrite <- Hq. apply le_sub_l. + - (* k = S k' *) + destruct r. + + (* r = 0 *) + intros Hq _. + replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). + * apply IHk. + simpl. now rewrite add_succ_r, Hq. apply le_n. + * rewrite sub_diag, sub_0_r, add_0_r. simpl. + rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal. + rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal. + + (* r = S r' *) + intros Hq Hr. + replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)). + * apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor. + * simpl. rewrite <- add_succ_r. f_equal. rewrite <- sub_succ_l; trivial. +Qed. + +Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n). +Proof. + set (s:=sqrt n). + replace n with (n + 0*0 + (0-0)). + apply sqrt_iter_spec; auto. + simpl. now rewrite !add_0_r. +Qed. + +Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a. + +Lemma sqrt_neg a : a<0 -> sqrt a = 0. +Proof. inversion 1. Qed. + +(** ** Logarithm *) + +Lemma log2_iter_spec : forall k p q r, + 2^(S p) = q + S r -> r < 2^p -> + let s := log2_iter k p q r in + 2^s <= k + q < 2^(S s). +Proof. + induction k. + - (* k = 0 *) + intros p q r EQ LT. simpl log2_iter. cbv zeta. + split. + + rewrite add_0_l. + rewrite (add_le_mono_l _ _ (2^p)). + simpl pow in EQ. rewrite add_0_r in EQ. rewrite EQ. + rewrite add_comm. apply add_le_mono_r. apply LT. + + rewrite EQ, add_comm. apply add_lt_mono_l. + apply lt_succ_r, le_0_l. + - (* k = S k' *) + intros p q r EQ LT. destruct r. + + (* r = 0 *) + rewrite add_succ_r, add_0_r in EQ. + rewrite add_succ_l, <- add_succ_r. apply IHk. + * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r. + * rewrite EQ. constructor. + + (* r = S r' *) + rewrite add_succ_l, <- add_succ_r. apply IHk. + * now rewrite add_succ_l, <- add_succ_r. + * apply le_lt_trans with (S r); trivial. do 2 constructor. +Qed. + +Lemma log2_spec n : 0<n -> + 2^(log2 n) <= n < 2^(S (log2 n)). +Proof. + intros. + set (s:=log2 n). + replace n with (pred n + 1). + apply log2_iter_spec; auto. + rewrite add_1_r. + apply succ_pred. now apply neq_sym, lt_neq. +Qed. + +Lemma log2_nonpos n : n<=0 -> log2 n = 0. +Proof. + inversion 1; now subst. +Qed. + +(** ** Gcd *) + +Definition divide x y := exists z, y=z*x. +Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. + +Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). +Proof. + fix 1. + intros [|a] b; simpl. + split. + now exists 0. + exists 1. simpl. now rewrite <- plus_n_O. + fold (b mod (S a)). + destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). + set (a':=S a) in *. + split; auto. + rewrite (div_mod b a') at 2 by discriminate. + destruct H as (u,Hu), H' as (v,Hv). + rewrite mul_comm. + exists ((b/a')*v + u). + rewrite mul_add_distr_r. + now rewrite <- mul_assoc, <- Hv, <- Hu. +Qed. + +Lemma gcd_divide_l : forall a b, (gcd a b | a). +Proof. + intros. apply gcd_divide. +Qed. + +Lemma gcd_divide_r : forall a b, (gcd a b | b). +Proof. + intros. apply gcd_divide. +Qed. + +Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b). +Proof. + fix 1. + intros [|a] b; simpl; auto. + fold (b mod (S a)). + intros c H H'. apply gcd_greatest; auto. + set (a':=S a) in *. + rewrite (div_mod b a') in H' by discriminate. + destruct H as (u,Hu), H' as (v,Hv). + exists (v - (b/a')*u). + rewrite mul_comm in Hv. + rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu. + now rewrite add_comm, add_sub. +Qed. + +Lemma gcd_nonneg a b : 0<=gcd a b. +Proof. apply le_0_l. Qed. + + +(** ** Bitwise operations *) + +Lemma div2_double n : div2 (2*n) = n. +Proof. + induction n; trivial. + simpl mul. rewrite add_succ_r. simpl. now f_equal. +Qed. + +Lemma div2_succ_double n : div2 (S (2*n)) = n. +Proof. + induction n; trivial. + simpl. f_equal. now rewrite add_succ_r. +Qed. + +Lemma le_div2 n : div2 (S n) <= n. +Proof. + revert n. + fix 1. + destruct n; simpl; trivial. apply lt_succ_r. + destruct n; [simpl|]; trivial. now constructor. +Qed. + +Lemma lt_div2 n : 0 < n -> div2 n < n. +Proof. + destruct n. + - inversion 1. + - intros _. apply lt_succ_r, le_div2. +Qed. + +Lemma div2_decr a n : a <= S n -> div2 a <= n. +Proof. + destruct a; intros H. + - simpl. apply le_0_l. + - apply succ_le_mono in H. + apply le_trans with a; [ apply le_div2 | trivial ]. +Qed. + +Lemma double_twice : forall n, double n = 2*n. +Proof. + simpl; intros. now rewrite add_0_r. +Qed. + +Lemma testbit_0_l : forall n, testbit 0 n = false. +Proof. + now induction n. +Qed. + +Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. +Proof. + unfold testbit. rewrite odd_spec. now exists a. +Qed. + +Lemma testbit_even_0 a : testbit (2*a) 0 = false. +Proof. + unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial. + now exists a. +Qed. + +Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n. +Proof. + unfold testbit; fold testbit. + rewrite add_1_r. f_equal. + apply div2_succ_double. +Qed. + +Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n. +Proof. + unfold testbit; fold testbit. f_equal. apply div2_double. +Qed. + +Lemma shiftr_specif : forall a n m, + testbit (shiftr a n) m = testbit a (m+n). +Proof. + induction n; intros m. trivial. + now rewrite add_0_r. + now rewrite add_succ_r, <- add_succ_l, <- IHn. +Qed. + +Lemma shiftl_specif_high : forall a n m, n<=m -> + testbit (shiftl a n) m = testbit a (m-n). +Proof. + induction n; intros m H. trivial. + now rewrite sub_0_r. + destruct m. inversion H. + simpl. apply succ_le_mono in H. + change (shiftl a (S n)) with (double (shiftl a n)). + rewrite double_twice, div2_double. now apply IHn. +Qed. + +Lemma shiftl_spec_low : forall a n m, m<n -> + testbit (shiftl a n) m = false. +Proof. + induction n; intros m H. inversion H. + change (shiftl a (S n)) with (double (shiftl a n)). + destruct m; simpl. + unfold odd. apply negb_false_iff. + apply even_spec. exists (shiftl a n). apply double_twice. + rewrite double_twice, div2_double. apply IHn. + now apply succ_le_mono. +Qed. + +Lemma div2_bitwise : forall op n a b, + div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b). +Proof. + intros. unfold bitwise; fold bitwise. + destruct (op (odd a) (odd b)). + now rewrite div2_succ_double. + now rewrite add_0_l, div2_double. +Qed. + +Lemma odd_bitwise : forall op n a b, + odd (bitwise op (S n) a b) = op (odd a) (odd b). +Proof. + intros. unfold bitwise; fold bitwise. + destruct (op (odd a) (odd b)). + apply odd_spec. rewrite add_comm. eexists; eauto. + unfold odd. apply negb_false_iff. apply even_spec. + rewrite add_0_l; eexists; eauto. +Qed. + +Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) -> + forall n m a b, a<=n -> + testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). +Proof. + intros op Hop. + induction n; intros m a b Ha. + simpl. inversion Ha; subst. now rewrite testbit_0_l. + destruct m. + apply odd_bitwise. + unfold testbit; fold testbit. rewrite div2_bitwise. + apply IHn. now apply div2_decr. +Qed. + +Lemma testbit_bitwise_2 : forall op, op false false = false -> + forall n m a b, a<=n -> b<=n -> + testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). +Proof. + intros op Hop. + induction n; intros m a b Ha Hb. + simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l. + destruct m. + apply odd_bitwise. + unfold testbit; fold testbit. rewrite div2_bitwise. + apply IHn; now apply div2_decr. +Qed. + +Lemma land_spec a b n : + testbit (land a b) n = testbit a n && testbit b n. +Proof. + unfold land. apply testbit_bitwise_1; trivial. +Qed. + +Lemma ldiff_spec a b n : + testbit (ldiff a b) n = testbit a n && negb (testbit b n). +Proof. + unfold ldiff. apply testbit_bitwise_1; trivial. +Qed. + +Lemma lor_spec a b n : + testbit (lor a b) n = testbit a n || testbit b n. +Proof. + unfold lor. apply testbit_bitwise_2. + - trivial. + - destruct (compare_spec a b). + + rewrite max_l; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. + - destruct (compare_spec a b). + + rewrite max_r; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. +Qed. + +Lemma lxor_spec a b n : + testbit (lxor a b) n = xorb (testbit a n) (testbit b n). +Proof. + unfold lxor. apply testbit_bitwise_2. + - trivial. + - destruct (compare_spec a b). + + rewrite max_l; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. + - destruct (compare_spec a b). + + rewrite max_r; subst; trivial. + + apply lt_le_incl in H. now rewrite max_r. + + apply lt_le_incl in H. now rewrite max_l. +Qed. + +Lemma div2_spec a : div2 a = shiftr a 1. +Proof. + reflexivity. +Qed. + +(** Aliases with extra dummy hypothesis, to fulfil the interface *) + +Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n. +Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n. +Lemma testbit_neg_r a n (H:n<0) : testbit a n = false. +Proof. inversion H. Qed. + +Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m. +Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m. + +(** Properties of advanced functions (pow, sqrt, log2, ...) *) + +Include NExtraProp. + +End Nat. + +(** Re-export notations that should be available even when + the [Nat] module is not imported. *) + +Bind Scope nat_scope with Nat.t nat. + +Infix "^" := Nat.pow : nat_scope. +Infix "=?" := Nat.eqb (at level 70) : nat_scope. +Infix "<=?" := Nat.leb (at level 70) : nat_scope. +Infix "<?" := Nat.ltb (at level 70) : nat_scope. +Infix "?=" := Nat.compare (at level 70) : nat_scope. +Infix "/" := Nat.div : nat_scope. +Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. + +Hint Unfold Nat.le : core. +Hint Unfold Nat.lt : core. + +(** [Nat] contains an [order] tactic for natural numbers *) + +(** Note that [Nat.order] is domain-agnostic: it will not prove + [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) + +Section TestOrder. + Let test : forall x y, x<=y -> y<=x -> x=y. + Proof. + Nat.order. + Qed. +End TestOrder. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9b8ebfe55..72edc6eef 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -6,47 +6,61 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Decidable. +Require Import Decidable PeanoNat. Require Eqdep_dec. -Require Import Le Lt. Local Open Scope nat_scope. Implicit Types m n x y : nat. -Theorem O_or_S : forall n, {m : nat | S m = n} + {0 = n}. +Theorem O_or_S n : {m : nat | S m = n} + {0 = n}. Proof. induction n. - auto. - left; exists n; auto. + - now right. + - left; exists n; auto. Defined. -Theorem eq_nat_dec : forall n m, {n = m} + {n <> m}. -Proof. - induction n; destruct m; auto. - elim (IHn m); auto. -Defined. +Notation eq_nat_dec := Nat.eq_dec (compat "8.4"). Hint Resolve O_or_S eq_nat_dec: arith. -Theorem dec_eq_nat : forall n m, decidable (n = m). - intros x y; unfold decidable; elim (eq_nat_dec x y); auto with arith. +Theorem dec_eq_nat n m : decidable (n = m). +Proof. + elim (Nat.eq_dec n m); [left|right]; trivial. Defined. -Definition UIP_nat:= Eqdep_dec.UIP_dec eq_nat_dec. +Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec. + +Import EqNotations. Lemma le_unique: forall m n (h1 h2: m <= n), h1 = h2. Proof. fix 3. -refine (fun m _ h1 => match h1 as h' in _ <= k return forall hh: m <= k, h' = hh - with le_n _ => _ |le_S _ i H => _ end). -refine (fun hh => match hh as h' in _ <= k return forall eq: m = k, - le_n m = match eq in _ = p return m <= p -> m <= m with |eq_refl => fun bli => bli end h' with - |le_n _ => fun eq => _ |le_S _ j H' => fun eq => _ end eq_refl). -rewrite (UIP_nat _ _ eq eq_refl). reflexivity. -subst m. destruct (Lt.lt_irrefl j H'). -refine (fun hh => match hh as h' in _ <= k return match k as k' return m <= k' -> Prop - with |0 => fun _ => True |S i' => fun h'' => forall H':m <= i', le_S m i' H' = h'' end h' - with |le_n _ => _ |le_S _ j H2 => fun H' => _ end H). -destruct m. exact I. intros; destruct (Lt.lt_irrefl m H'). -f_equal. apply le_unique. +destruct h1 as [ | i h1 ]; intros h2. +- set (Return k (le:m<=k) := + forall (eq:m=k), + le_n m = (rew eq in fun (le':m<=m) => le') le). + refine + (match h2 as h2' return (Return _ h2') with + | le_n _ => fun eq => _ + | le_S _ j h2 => fun eq => _ + end eq_refl). + + rewrite (UIP_nat _ _ eq eq_refl). simpl. reflexivity. + + exfalso. revert h2. rewrite eq. apply Nat.lt_irrefl. +- set (Return k (le:m<=k) := + match k as k' return (m <= k' -> Prop) with + | 0 => fun _ => True + | S i' => fun (le':m<=S i') => forall (H':m<=i'), le_S _ _ H' = le' + end le). + refine + (match h2 as h2' return (Return _ h2') with + | le_n _ => _ + | le_S _ j h2 => fun h1' => _ + end h1). + + unfold Return; clear. destruct m; simpl. + * exact I. + * intros h1'. destruct (Nat.lt_irrefl _ h1'). + + f_equal. apply le_unique. Qed. + +(** For compatibility *) +Require Import Le Lt. diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 5428ada32..3b823da6f 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -6,176 +6,139 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Properties of addition. [add] is defined in [Init/Peano.v] as: +(** Properties of addition. + + This file is mostly OBSOLETE now, see module [PeanoNat.Nat] instead. + + [Nat.add] is defined in [Init/Nat.v] as: << -Fixpoint plus (n m:nat) : nat := +Fixpoint add (n m:nat) : nat := match n with | O => m | S p => S (p + m) end -where "n + m" := (plus n m) : nat_scope. +where "n + m" := (add n m) : nat_scope. >> - *) +*) -Require Import Le. -Require Import Lt. +Require Import PeanoNat. Local Open Scope nat_scope. -Implicit Types m n p q : nat. - -(** * Zero is neutral -Deprecated : Already in Init/Peano.v *) -Notation plus_0_l := plus_O_n (only parsing). -Definition plus_0_r n := eq_sym (plus_n_O n). - -(** * Commutativity *) - -Lemma plus_comm : forall n m, n + m = m + n. -Proof. - intros n m; elim n; simpl; auto with arith. - intros y H; elim (plus_n_Sm m y); auto with arith. -Qed. -Hint Immediate plus_comm: arith v62. - -(** * Associativity *) +(** * Neutrality of 0, commutativity, associativity *) -Definition plus_Snm_nSm : forall n m, S n + m = n + S m:= - plus_n_Sm. +Notation plus_0_l := Nat.add_0_l (compat "8.4"). +Notation plus_0_r := Nat.add_0_r (compat "8.4"). +Notation plus_comm := Nat.add_comm (compat "8.4"). +Notation plus_assoc := Nat.add_assoc (compat "8.4"). -Lemma plus_assoc : forall n m p, n + (m + p) = n + m + p. -Proof. - intros n m p; elim n; simpl; auto with arith. -Qed. -Hint Resolve plus_assoc: arith v62. +Notation plus_permute := Nat.add_shuffle3 (compat "8.4"). -Lemma plus_permute : forall n m p, n + (m + p) = m + (n + p). -Proof. - intros; rewrite (plus_assoc m n p); rewrite (plus_comm m n); auto with arith. -Qed. +Definition plus_Snm_nSm : forall n m, S n + m = n + S m := + Peano.plus_n_Sm. -Lemma plus_assoc_reverse : forall n m p, n + m + p = n + (m + p). +Lemma plus_assoc_reverse n m p : n + m + p = n + (m + p). Proof. - auto with arith. + symmetry. apply Nat.add_assoc. Qed. -Hint Resolve plus_assoc_reverse: arith v62. (** * Simplification *) -Lemma plus_reg_l : forall n m p, p + n = p + m -> n = m. +Lemma plus_reg_l n m p : p + n = p + m -> n = m. Proof. - intros m p n; induction n; simpl; auto with arith. + apply Nat.add_cancel_l. Qed. -Lemma plus_le_reg_l : forall n m p, p + n <= p + m -> n <= m. +Lemma plus_le_reg_l n m p : p + n <= p + m -> n <= m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_le_mono_l. Qed. -Lemma plus_lt_reg_l : forall n m p, p + n < p + m -> n < m. +Lemma plus_lt_reg_l n m p : p + n < p + m -> n < m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_lt_mono_l. Qed. (** * Compatibility with order *) -Lemma plus_le_compat_l : forall n m p, n <= m -> p + n <= p + m. +Lemma plus_le_compat_l n m p : n <= m -> p + n <= p + m. Proof. - induction p; simpl; auto with arith. + apply Nat.add_le_mono_l. Qed. -Hint Resolve plus_le_compat_l: arith v62. -Lemma plus_le_compat_r : forall n m p, n <= m -> n + p <= m + p. +Lemma plus_le_compat_r n m p : n <= m -> n + p <= m + p. Proof. - induction 1; simpl; auto with arith. + apply Nat.add_le_mono_r. Qed. -Hint Resolve plus_le_compat_r: arith v62. -Lemma le_plus_l : forall n m, n <= n + m. +Lemma plus_lt_compat_l n m p : n < m -> p + n < p + m. Proof. - induction n; simpl; auto with arith. + apply Nat.add_lt_mono_l. Qed. -Hint Resolve le_plus_l: arith v62. -Lemma le_plus_r : forall n m, m <= n + m. +Lemma plus_lt_compat_r n m p : n < m -> n + p < m + p. Proof. - intros n m; elim n; simpl; auto with arith. + apply Nat.add_lt_mono_r. Qed. -Hint Resolve le_plus_r: arith v62. -Theorem le_plus_trans : forall n m p, n <= m -> n <= m + p. +Lemma plus_le_compat n m p q : n <= m -> p <= q -> n + p <= m + q. Proof. - intros; apply le_trans with (m := m); auto with arith. + apply Nat.add_le_mono. Qed. -Hint Resolve le_plus_trans: arith v62. -Theorem lt_plus_trans : forall n m p, n < m -> n < m + p. +Lemma plus_le_lt_compat n m p q : n <= m -> p < q -> n + p < m + q. Proof. - intros; apply lt_le_trans with (m := m); auto with arith. + apply Nat.add_le_lt_mono. Qed. -Hint Immediate lt_plus_trans: arith v62. -Lemma plus_lt_compat_l : forall n m p, n < m -> p + n < p + m. +Lemma plus_lt_le_compat n m p q : n < m -> p <= q -> n + p < m + q. Proof. - induction p; simpl; auto with arith. + apply Nat.add_lt_le_mono. Qed. -Hint Resolve plus_lt_compat_l: arith v62. -Lemma plus_lt_compat_r : forall n m p, n < m -> n + p < m + p. +Lemma plus_lt_compat n m p q : n < m -> p < q -> n + p < m + q. Proof. - intros n m p H; rewrite (plus_comm n p); rewrite (plus_comm m p). - elim p; auto with arith. + apply Nat.add_lt_mono. Qed. -Hint Resolve plus_lt_compat_r: arith v62. -Lemma plus_le_compat : forall n m p q, n <= m -> p <= q -> n + p <= m + q. +Lemma le_plus_l n m : n <= n + m. Proof. - intros n m p q H H0. - elim H; simpl; auto with arith. + apply Nat.le_add_r. Qed. -Lemma plus_le_lt_compat : forall n m p q, n <= m -> p < q -> n + p < m + q. +Lemma le_plus_r n m : m <= n + m. Proof. - unfold lt. intros. change (S n + p <= m + q). rewrite plus_Snm_nSm. - apply plus_le_compat; assumption. + rewrite Nat.add_comm. apply Nat.le_add_r. Qed. -Lemma plus_lt_le_compat : forall n m p q, n < m -> p <= q -> n + p < m + q. +Theorem le_plus_trans n m p : n <= m -> n <= m + p. Proof. - unfold lt. intros. change (S n + p <= m + q). apply plus_le_compat; assumption. + intros. now rewrite <- Nat.le_add_r. Qed. -Lemma plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q. +Theorem lt_plus_trans n m p : n < m -> n < m + p. Proof. - intros. apply plus_lt_le_compat. assumption. - apply lt_le_weak. assumption. + intros. apply Nat.lt_le_trans with m. trivial. apply Nat.le_add_r. Qed. (** * Inversion lemmas *) -Lemma plus_is_O : forall n m, n + m = 0 -> n = 0 /\ m = 0. +Lemma plus_is_O n m : n + m = 0 -> n = 0 /\ m = 0. Proof. - intro m; destruct m as [| n]; auto. - intros. discriminate H. + destruct n; now split. Qed. -Definition plus_is_one : - forall m n, m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. +Definition plus_is_one m n : + m + n = 1 -> {m = 0 /\ n = 1} + {m = 1 /\ n = 0}. Proof. - intro m; destruct m as [| n]; auto. - destruct n; auto. - intros. - simpl in H. discriminate H. + destruct m as [| m]; auto. + destruct m; auto. + discriminate. Defined. (** * Derived properties *) -Lemma plus_permute_2_in_4 : forall n m p q, n + m + (p + q) = n + p + (m + q). -Proof. - intros m n p q. - rewrite <- (plus_assoc m n (p + q)). rewrite (plus_assoc n p q). - rewrite (plus_comm n p). rewrite <- (plus_assoc p n q). apply plus_assoc. -Qed. +Notation plus_permute_2_in_4 := Nat.add_shuffle1 (compat "8.4"). (** * Tail-recursive plus *) @@ -190,31 +153,37 @@ Fixpoint tail_plus n m : nat := end. Lemma plus_tail_plus : forall n m, n + m = tail_plus n m. +Proof. induction n as [| n IHn]; simpl; auto. intro m; rewrite <- IHn; simpl; auto. Qed. (** * Discrimination *) -Lemma succ_plus_discr : forall n m, n <> S (plus m n). +Lemma succ_plus_discr n m : n <> S (m+n). Proof. - intros n m; induction n as [|n IHn]. - discriminate. - intro H; apply IHn; apply eq_add_S; rewrite H; rewrite <- plus_n_Sm; - reflexivity. + apply Nat.succ_add_discr. Qed. -Lemma n_SSn : forall n, n <> S (S n). -Proof. - intro n; exact (succ_plus_discr n 1). -Qed. +Lemma n_SSn n : n <> S (S n). +Proof (succ_plus_discr n 1). -Lemma n_SSSn : forall n, n <> S (S (S n)). -Proof. - intro n; exact (succ_plus_discr n 2). -Qed. +Lemma n_SSSn n : n <> S (S (S n)). +Proof (succ_plus_discr n 2). -Lemma n_SSSSn : forall n, n <> S (S (S (S n))). -Proof. - intro n; exact (succ_plus_discr n 3). -Qed. +Lemma n_SSSSn n : n <> S (S (S (S n))). +Proof (succ_plus_discr n 3). + + +(** * Compatibility Hints *) + +Hint Immediate plus_comm : arith v62. +Hint Resolve plus_assoc plus_assoc_reverse : arith v62. +Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62. +Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62. +Hint Immediate lt_plus_trans : arith v62. +Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62. + +(** For compatibility, we "Require" the same files as before *) + +Require Import Le Lt. diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index 05be5e1a3..2cb7c3c09 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -8,7 +8,7 @@ (** Well-founded relations and natural numbers *) -Require Import Lt. +Require Import PeanoNat Lt. Local Open Scope nat_scope. @@ -24,16 +24,12 @@ Definition gtof (a b:A) := f b > f a. Theorem well_founded_ltof : well_founded ltof. Proof. - red. - cut (forall n (a:A), f a < n -> Acc ltof a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply Acc_intro. - unfold ltof; intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + assert (H : forall n (a:A), f a < n -> Acc ltof a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. unfold ltof at 1. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem well_founded_gtof : well_founded gtof. @@ -67,15 +63,13 @@ Theorem induction_ltof1 : forall P:A -> Set, (forall x:A, (forall y:A, ltof y x -> P y) -> P x) -> forall a:A, P a. Proof. - intros P F; cut (forall n (a:A), f a < n -> P a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply F. - unfold ltof; intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + intros P F. + assert (H : forall n (a:A), f a < n -> P a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply F. unfold ltof. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. Theorem induction_gtof1 : @@ -108,16 +102,12 @@ Hypothesis H_compat : forall x y:A, R x y -> f x < f y. Theorem well_founded_lt_compat : well_founded R. Proof. - red. - cut (forall n (a:A), f a < n -> Acc R a). - intros H a; apply (H (S (f a))); auto with arith. - induction n. - intros; absurd (f a < 0); auto with arith. - intros a ltSma. - apply Acc_intro. - intros b ltfafb. - apply IHn. - apply lt_le_trans with (f a); auto with arith. + assert (H : forall n (a:A), f a < n -> Acc R a). + { induction n. + - intros; absurd (f a < 0); auto with arith. + - intros a Ha. apply Acc_intro. intros b Hb. + apply IHn. apply Nat.lt_le_trans with (f a); auto with arith. } + intros a. apply (H (S (f a))). auto with arith. Defined. End Well_founded_Nat. @@ -208,6 +198,7 @@ End LT_WF_REL. Lemma well_founded_inv_rel_inv_lt_rel : forall (A:Set) (F:A -> nat -> Prop), well_founded (inv_lt_rel A F). +Proof. intros; apply (well_founded_inv_lt_rel_compat A (inv_lt_rel A F) F); trivial. Qed. @@ -230,30 +221,18 @@ Proof. intros P Pdec (n0,HPn0). assert (forall n, (exists n', n'<n /\ P n' /\ forall n'', P n'' -> n'<=n'') - \/(forall n', P n' -> n<=n')). - induction n. - right. - intros n' Hn'. - apply le_O_n. - destruct IHn. - left; destruct H as (n', (Hlt', HPn')). - exists n'; split. - apply lt_S; assumption. - assumption. - destruct (Pdec n). - left; exists n; split. - apply lt_n_Sn. - split; assumption. - right. - intros n' Hltn'. - destruct (le_lt_eq_dec n n') as [Hltn|Heqn]. - apply H; assumption. - assumption. - destruct H0. - rewrite Heqn; assumption. - destruct (H n0) as [(n,(Hltn,(Hmin,Huniqn)))|]; [exists n | exists n0]; - repeat split; - assumption || intros n' (HPn',Hminn'); apply le_antisym; auto. + \/ (forall n', P n' -> n<=n')). + { induction n. + - right. intros. apply Nat.le_0_l. + - destruct IHn as [(n' & IH1 & IH2)|IH]. + + left. exists n'; auto with arith. + + destruct (Pdec n) as [HP|HP]. + * left. exists n; auto with arith. + * right. intros n' Hn'. + apply Nat.le_neq; split; auto. intros <-. auto. } + destruct (H n0) as [(n & H1 & H2 & H3)|H0]; [exists n | exists n0]; + repeat split; trivial; + intros n' (HPn',Hn'); apply Nat.le_antisymm; auto. Qed. Unset Implicit Arguments. diff --git a/theories/Arith/vo.itarget b/theories/Arith/vo.itarget index 0b6564e15..0b3d31e98 100644 --- a/theories/Arith/vo.itarget +++ b/theories/Arith/vo.itarget @@ -1,3 +1,4 @@ +PeanoNat.vo Arith_base.vo Arith.vo Between.vo diff --git a/theories/Classes/DecidableClass.v b/theories/Classes/DecidableClass.v index 3b4ba786a..b80903dc1 100644 --- a/theories/Classes/DecidableClass.v +++ b/theories/Classes/DecidableClass.v @@ -64,33 +64,29 @@ Tactic Notation "decide" constr(P) := Require Import Bool Arith ZArith. Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := { - Decidable_witness := eqb x y + Decidable_witness := Bool.eqb x y }. Next Obligation. -split. - now apply eqb_prop. - now destruct 1; apply eqb_reflx. + apply eqb_true_iff. Qed. Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := { - Decidable_witness := beq_nat x y + Decidable_witness := Nat.eqb x y }. Next Obligation. -split. - now intros H; symmetry in H; apply beq_nat_eq in H; auto. - now destruct 1; symmetry; apply beq_nat_refl. + apply Nat.eqb_eq. Qed. Program Instance Decidable_le_nat : forall (x y : nat), Decidable (x <= y) := { - Decidable_witness := leb x y + Decidable_witness := Nat.leb x y }. Next Obligation. -apply leb_iff. + apply Nat.leb_le. Qed. Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := { - Decidable_witness := Zeq_bool x y + Decidable_witness := Z.eqb x y }. Next Obligation. -split; apply Zeq_is_eq_bool. + apply Z.eqb_eq. Qed. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v new file mode 100644 index 000000000..5764b349b --- /dev/null +++ b/theories/Init/Nat.v @@ -0,0 +1,297 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +Require Import Notations Logic Datatypes. + +Local Open Scope nat_scope. + +(**********************************************************************) +(** * Peano natural numbers, definitions of operations *) +(**********************************************************************) + +(** This file is meant to be used as a whole module, + without importing it, leading to qualified definitions + (e.g. Nat.pred) *) + +Definition t := nat. + +(** ** Constants *) + +Definition zero := 0. +Definition one := 1. +Definition two := 2. + +(** ** Basic operations *) + +Definition succ := S. + +Definition pred n := + match n with + | 0 => n + | S u => u + end. + +Fixpoint add n m := + match n with + | 0 => m + | S p => S (p + m) + end + +where "n + m" := (add n m) : nat_scope. + +Definition double n := n + n. + +Fixpoint mul n m := + match n with + | 0 => 0 + | S p => m + p * m + end + +where "n * m" := (mul n m) : nat_scope. + +(** Truncated subtraction: [n-m] is [0] if [n<=m] *) + +Fixpoint sub n m := + match n, m with + | S k, S l => k - l + | _, _ => n + end + +where "n - m" := (sub n m) : nat_scope. + +(** ** Comparisons *) + +Fixpoint eqb n m : bool := + match n, m with + | 0, 0 => true + | 0, S _ => false + | S _, 0 => false + | S n', S m' => eqb n' m' + end. + +Fixpoint leb n m : bool := + match n, m with + | 0, _ => true + | _, 0 => false + | S n', S m' => leb n' m' + end. + +Definition ltb n m := leb (S n) m. + +Infix "=?" := eqb (at level 70) : nat_scope. +Infix "<=?" := leb (at level 70) : nat_scope. +Infix "<?" := ltb (at level 70) : nat_scope. + +Fixpoint compare n m : comparison := + match n, m with + | 0, 0 => Eq + | 0, S _ => Lt + | S _, 0 => Gt + | S n', S m' => compare n' m' + end. + +Infix "?=" := compare (at level 70) : nat_scope. + +(** ** Minimum, maximum *) + +Fixpoint max n m := + match n, m with + | 0, _ => m + | S n', 0 => n + | S n', S m' => S (max n' m') + end. + +Fixpoint min n m := + match n, m with + | 0, _ => 0 + | S n', 0 => 0 + | S n', S m' => S (min n' m') + end. + +(** ** Parity tests *) + +Fixpoint even n : bool := + match n with + | 0 => true + | 1 => false + | S (S n') => even n' + end. + +Definition odd n := negb (even n). + +(** ** Power *) + +Fixpoint pow n m := + match m with + | 0 => 1 + | S m => n * (n^m) + end + +where "n ^ m" := (pow n m) : nat_scope. + +(** ** Euclidean division *) + +(** This division is linear and tail-recursive. + In [divmod], [y] is the predecessor of the actual divisor, + and [u] is [y] minus the real remainder +*) + +Fixpoint divmod x y q u := + match x with + | 0 => (q,u) + | S x' => match u with + | 0 => divmod x' y (S q) y + | S u' => divmod x' y q u' + end + end. + +Definition div x y := + match y with + | 0 => y + | S y' => fst (divmod x y' 0 y') + end. + +Definition modulo x y := + match y with + | 0 => y + | S y' => y' - snd (divmod x y' 0 y') + end. + +Infix "/" := div : nat_scope. +Infix "mod" := modulo (at level 40, no associativity) : nat_scope. + + +(** ** Greatest common divisor *) + +(** We use Euclid algorithm, which is normally not structural, + but Coq is now clever enough to accept this (behind modulo + there is a subtraction, which now preserves being a subterm) +*) + +Fixpoint gcd a b := + match a with + | O => b + | S a' => gcd (b mod (S a')) (S a') + end. + +(** ** Square *) + +Definition square n := n * n. + +(** ** Square root *) + +(** The following square root function is linear (and tail-recursive). + With Peano representation, we can't do better. For faster algorithm, + see Psqrt/Zsqrt/Nsqrt... + + We search the square root of n = k + p^2 + (q - r) + with q = 2p and 0<=r<=q. We start with p=q=r=0, hence + looking for the square root of n = k. Then we progressively + decrease k and r. When k = S k' and r=0, it means we can use (S p) + as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. + When k reaches 0, we have found the biggest p^2 square contained + in n, hence the square root of n is p. +*) + +Fixpoint sqrt_iter k p q r := + match k with + | O => p + | S k' => match r with + | O => sqrt_iter k' (S p) (S (S q)) (S (S q)) + | S r' => sqrt_iter k' p q r' + end + end. + +Definition sqrt n := sqrt_iter n 0 0 0. + +(** ** Log2 *) + +(** This base-2 logarithm is linear and tail-recursive. + + In [log2_iter], we maintain the logarithm [p] of the counter [q], + while [r] is the distance between [q] and the next power of 2, + more precisely [q + S r = 2^(S p)] and [r<2^p]. At each + recursive call, [q] goes up while [r] goes down. When [r] + is 0, we know that [q] has almost reached a power of 2, + and we increase [p] at the next call, while resetting [r] + to [q]. + + Graphically (numbers are [q], stars are [r]) : + +<< + 10 + 9 + 8 + 7 * + 6 * + 5 ... + 4 + 3 * + 2 * + 1 * * +0 * * * +>> + + We stop when [k], the global downward counter reaches 0. + At that moment, [q] is the number we're considering (since + [k+q] is invariant), and [p] its logarithm. +*) + +Fixpoint log2_iter k p q r := + match k with + | O => p + | S k' => match r with + | O => log2_iter k' (S p) (S q) q + | S r' => log2_iter k' p (S q) r' + end + end. + +Definition log2 n := log2_iter (pred n) 0 1 0. + +(** Iterator on natural numbers *) + +Definition iter (n:nat) {A} (f:A->A) (x:A) : A := + nat_rect (fun _ => A) x (fun _ => f) n. + +(** Bitwise operations *) + +(** We provide here some bitwise operations for unary numbers. + Some might be really naive, they are just there for fullfiling + the same interface as other for natural representations. As + soon as binary representations such as NArith are available, + it is clearly better to convert to/from them and use their ops. +*) + +Fixpoint div2 n := + match n with + | 0 => 0 + | S 0 => 0 + | S (S n') => S (div2 n') + end. + +Fixpoint testbit a n : bool := + match n with + | 0 => odd a + | S n => testbit (div2 a) n + end. + +Definition shiftl a n := iter n double a. +Definition shiftr a n := iter n div2 a. + +Fixpoint bitwise (op:bool->bool->bool) n a b := + match n with + | 0 => 0 + | S n' => + (if op (odd a) (odd b) then 1 else 0) + + 2*(bitwise op n' (div2 a) (div2 b)) + end. + +Definition land a b := bitwise andb a a b. +Definition lor a b := bitwise orb (max a b) a b. +Definition ldiff a b := bitwise (fun b b' => andb b (negb b')) a a b. +Definition lxor a b := bitwise xorb (max a b) a b. diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 6b0db724d..0de06c95d 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -26,6 +26,7 @@ Require Import Notations. Require Import Datatypes. Require Import Logic. +Require Coq.Init.Nat. Open Scope nat_scope. @@ -37,10 +38,8 @@ Hint Resolve f_equal_nat: core. (** The predecessor function *) -Definition pred (n:nat) : nat := match n with - | O => n - | S u => u - end. +Notation pred := Nat.pred (compat "8.4"). + Definition f_equal_pred := f_equal pred. Hint Resolve f_equal_pred: v62. @@ -82,13 +81,8 @@ Hint Resolve n_Sn: core. (** Addition *) -Fixpoint plus (n m:nat) : nat := - match n with - | O => m - | S p => S (p + m) - end - -where "n + m" := (plus n m) : nat_scope. +Notation plus := Nat.add (compat "8.4"). +Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. Hint Resolve f_equal2_plus: v62. @@ -103,7 +97,7 @@ Hint Resolve plus_n_O: core. Lemma plus_O_n : forall n:nat, 0 + n = n. Proof. - auto. + reflexivity. Qed. Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. @@ -114,7 +108,7 @@ Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). Proof. - auto. + reflexivity. Qed. (** Standard associated names *) @@ -124,13 +118,9 @@ Notation plus_succ_r_reverse := plus_n_Sm (compat "8.2"). (** Multiplication *) -Fixpoint mult (n m:nat) : nat := - match n with - | O => 0 - | S p => m + p * m - end +Notation mult := Nat.mul (compat "8.4"). +Infix "*" := Nat.mul : nat_scope. -where "n * m" := (mult n m) : nat_scope. Definition f_equal2_mult := f_equal2 mult. Hint Resolve f_equal2_mult: core. @@ -155,14 +145,8 @@ Notation mult_succ_r_reverse := mult_n_Sm (compat "8.2"). (** Truncated subtraction: [m-n] is [0] if [n>=m] *) -Fixpoint minus (n m:nat) : nat := - match n, m with - | O, _ => n - | S k, O => n - | S k, S l => k - l - end - -where "n - m" := (minus n m) : nat_scope. +Notation minus := Nat.sub (compat "8.4"). +Infix "-" := Nat.sub : nat_scope. (** Definition of the usual orders, the basic properties of [le] and [lt] can be found in files Le and Lt *) @@ -206,6 +190,16 @@ Proof. intros n m. exact (le_pred (S n) (S m)). Qed. +Theorem le_0_n : forall n, 0 <= n. +Proof. + induction n; constructor; trivial. +Qed. + +Theorem le_n_S : forall n m, n <= m -> S n <= S m. +Proof. + induction 1; constructor; trivial. +Qed. + (** Case analysis *) Theorem nat_case : @@ -228,44 +222,38 @@ Qed. (** Maximum and minimum : definitions and specifications *) -Fixpoint max n m : nat := - match n, m with - | O, _ => m - | S n', O => n - | S n', S m' => S (max n' m') - end. +Notation max := Nat.max (compat "8.4"). +Notation min := Nat.min (compat "8.4"). -Fixpoint min n m : nat := - match n, m with - | O, _ => 0 - | S n', O => 0 - | S n', S m' => S (min n' m') - end. - -Theorem max_l : forall n m : nat, m <= n -> max n m = n. +Lemma max_l n m : m <= n -> Nat.max n m = n. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem max_r : forall n m : nat, n <= m -> max n m = m. +Lemma max_r n m : n <= m -> Nat.max n m = m. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem min_l : forall n m : nat, n <= m -> min n m = n. +Lemma min_l n m : n <= m -> Nat.min n m = n. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. -Theorem min_r : forall n m : nat, m <= n -> min n m = m. +Lemma min_r n m : m <= n -> Nat.min n m = m. Proof. -induction n; destruct m; simpl; auto. inversion 1. -intros. apply f_equal. apply IHn. apply le_S_n. trivial. + revert m; induction n; destruct m; simpl; trivial. + - inversion 1. + - intros. apply f_equal, IHn, le_S_n; trivial. Qed. + Lemma nat_rect_succ_r {A} (f: A -> A) (x:A) n : nat_rect (fun _ => A) x (fun _ => f) (S n) = nat_rect (fun _ => A) (f x) (fun _ => f) n. Proof. diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index 3fa62e0a4..01383365e 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -11,6 +11,7 @@ Require Export Logic. Require Export Logic_Type. Require Export Datatypes. Require Export Specif. +Require Coq.Init.Nat. Require Export Peano. Require Export Coq.Init.Wf. Require Export Coq.Init.Tactics. diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget index f53d55e71..cc62e66cc 100644 --- a/theories/Init/vo.itarget +++ b/theories/Init/vo.itarget @@ -7,3 +7,4 @@ Prelude.vo Specif.vo Tactics.vo Wf.vo +Nat.vo
\ No newline at end of file diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 320ced06c..901574235 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -27,7 +27,7 @@ - min_elt max_elt choose *) -Require Import Orders OrdersFacts MSetInterface NPeano. +Require Import Orders OrdersFacts MSetInterface PeanoNat. Local Open Scope list_scope. Local Open Scope lazy_bool_scope. @@ -1129,14 +1129,14 @@ Proof. Qed. Lemma maxdepth_log_cardinal s : s <> Leaf -> - log2 (cardinal s) < maxdepth s. + Nat.log2 (cardinal s) < maxdepth s. Proof. intros H. apply Nat.log2_lt_pow2. destruct s; simpl; intuition. apply maxdepth_cardinal. Qed. -Lemma mindepth_log_cardinal s : mindepth s <= log2 (S (cardinal s)). +Lemma mindepth_log_cardinal s : mindepth s <= Nat.log2 (S (cardinal s)). Proof. apply Nat.log2_le_pow2. auto with arith. apply mindepth_cardinal. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index b79afc616..af67aa1ec 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -31,7 +31,7 @@ Additional suggested reading: *) Require MSetGenTree. -Require Import Bool List BinPos Pnat Setoid SetoidList NPeano. +Require Import Bool List BinPos Pnat Setoid SetoidList PeanoNat. Local Open Scope list_scope. (* For nicer extraction, we create induction principles @@ -1566,7 +1566,7 @@ Proof. Qed. Lemma maxdepth_upperbound s : Rbt s -> - maxdepth s <= 2 * log2 (S (cardinal s)). + maxdepth s <= 2 * Nat.log2 (S (cardinal s)). Proof. intros (n,H). eapply Nat.le_trans; [eapply rb_maxdepth; eauto|]. @@ -1581,7 +1581,7 @@ Proof. Qed. Lemma maxdepth_lowerbound s : s<>Leaf -> - log2 (cardinal s) < maxdepth s. + Nat.log2 (cardinal s) < maxdepth s. Proof. apply maxdepth_log_cardinal. Qed. diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 256dce782..a8b086e77 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -8,7 +8,7 @@ Require Export BinNums. Require Import BinPos RelationClasses Morphisms Setoid - Equalities OrdersFacts GenericMinMax Bool NAxioms NProperties. + Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties. Require BinNatDef. (**********************************************************************) @@ -66,6 +66,20 @@ Notation "( p | q )" := (divide p q) (at level 0) : N_scope. Definition Even n := exists m, n = 2*m. Definition Odd n := exists m, n = 2*m+1. +(** 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 := _. + (** Decidability of equality. *) Definition eq_dec : forall n m : N, { n = m } + { n <> m }. @@ -138,6 +152,50 @@ Proof. apply peano_rect_succ. Qed. +(** Generic induction / recursion *) + +Theorem bi_induction : + forall A : N -> Prop, Proper (Logic.eq==>iff) A -> + A 0 -> (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. + +(** 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. + (** Properties of mixed successor and predecessor. *) Lemma pos_pred_spec p : Pos.pred_N p = pred (pos p). @@ -262,69 +320,30 @@ Qed. 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 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. -destruct n; try reflexivity. -destruct m; try reflexivity. -destruct p; try 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. +(** Specification of minimum and maximum *) -Theorem mul_comm n m : n * m = m * n. +Theorem min_l n m : n <= m -> min n m = n. Proof. -destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm. +unfold min, le. case compare; trivial. now destruct 1. Qed. -Lemma le_0_l n : 0<=n. +Theorem min_r n m : m <= n -> min n m = m. Proof. -now destruct n. +unfold min, le. rewrite compare_antisym. +case compare_spec; trivial. now destruct 2. Qed. -Lemma leb_spec n m : BoolSpec (n<=m) (m<n) (n <=? m). +Theorem max_l n m : m <= n -> max n m = n. Proof. - unfold le, lt, leb. rewrite (compare_antisym n m). - case compare; now constructor. +unfold max, le. rewrite compare_antisym. +case compare_spec; auto. now destruct 2. Qed. -Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m. +Theorem max_r n m : n <= m -> max n m = 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). +unfold max, le. case compare; trivial. now destruct 1. Qed. -End Private_BootStrap. - (** Specification of lt and le. *) Lemma lt_succ_r n m : n < succ m <-> n<=m. @@ -334,6 +353,13 @@ split. now destruct p. now destruct 1. apply Pos.lt_succ_r. Qed. +(** We can now derive all properties of basic functions and orders, + and use these properties for proving the specs of more advanced + functions. *) + +Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + + (** Properties of [double] and [succ_double] *) Lemma double_spec n : double n = 2 * n. @@ -395,30 +421,6 @@ Proof. Qed. -(** Specification of minimum and maximum *) - -Theorem min_l n m : n <= m -> min n m = n. -Proof. -unfold min, le. case compare; trivial. now destruct 1. -Qed. - -Theorem min_r n m : m <= n -> min n m = m. -Proof. -unfold min, le. rewrite compare_antisym. -case compare_spec; trivial. now destruct 2. -Qed. - -Theorem max_l n m : m <= n -> max n m = n. -Proof. -unfold max, le. rewrite compare_antisym. -case compare_spec; auto. now destruct 2. -Qed. - -Theorem max_r n m : n <= m -> max n m = m. -Proof. -unfold max, le. case compare; trivial. now destruct 1. -Qed. - (** 0 is the least natural number *) Theorem compare_0_r n : (n ?= 0) <> Lt. @@ -560,13 +562,13 @@ Proof. (* 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. + apply add_lt_mono_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. + apply add_lt_mono_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 *) @@ -754,7 +756,7 @@ Proof. 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. + apply add_lt_mono_l with 1. rewrite 2 (add_succ_l 0). simpl. now rewrite succ_pos_pred. Qed. @@ -833,69 +835,10 @@ Proof. 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 0 -> (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 *) +(** Instantiation of generic properties of advanced functions + (pow, sqrt, log2, div, gcd, ...) *) -Include NProp - <+ UsualMinMaxLogicalProperties - <+ UsualMinMaxDecProperties. +Include NExtraProp. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 6aeeccaf5..befcf7929 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -325,8 +325,8 @@ Definition lxor n m := (** Shifts *) -Definition shiftl_nat (a:N) := nat_rect _ a (fun _ => double). -Definition shiftr_nat (a:N) := nat_rect _ a (fun _ => div2). +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 diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 662c50abf..b36ea3204 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat - Pnat Nnat Compare_dec Lt Minus. +Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat. Local Open Scope N_scope. @@ -111,10 +110,12 @@ Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat -> N.testbit_nat (N.shiftl_nat a n) m = N.testbit_nat a (m-n). Proof. induction n; intros m H. - now rewrite <- minus_n_O. - destruct m. inversion H. apply le_S_n in H. - simpl. rewrite <- IHn; trivial. - destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial. + - now rewrite Nat.sub_0_r. + - destruct m. + + inversion H. + + apply le_S_n in H. + simpl. rewrite <- IHn; trivial. + destruct (N.shiftl_nat a n) as [|[p|p|]]; simpl; trivial. Qed. Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat -> @@ -123,9 +124,10 @@ Proof. 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. + - destruct (N.shiftl_nat a n); trivial. + - apply Lt.lt_S_n in H. + specialize (IHn m H). + destruct (N.shiftl_nat a n); trivial. Qed. (** A left shift for positive numbers (used in BigN) *) @@ -446,49 +448,52 @@ 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.binary_ind; intros a' a'' H 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.binary_ind. - rewrite (Nless_z (N.double a)) in H. discriminate H. - rewrite (Nless_def_1 a a') in H. - induction a'' using N.binary_ind. - rewrite (Nless_z (N.double a')) in H0. discriminate H0. - rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). - exact (IHa _ _ H H0). - apply Nless_def_3. - induction a'' as [|a'' _|a'' _] using N.binary_ind. - rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. - rewrite (Nless_def_4 a' a'') in H0. discriminate H0. - apply Nless_def_3. - induction a' as [|a' _|a' _] using N.binary_ind. - rewrite (Nless_z (N.succ_double a)) in H. discriminate H. - rewrite (Nless_def_4 a a') in H. discriminate H. + - 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.binary_ind. + + rewrite (Nless_z (N.double a)) in H. discriminate H. + + rewrite (Nless_def_1 a a') in H. induction a'' using N.binary_ind. - rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. - rewrite (Nless_def_4 a' a'') in H0. discriminate H0. - rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. - rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). + * rewrite (Nless_z (N.double a')) in H0. discriminate H0. + * rewrite (Nless_def_1 a' a'') in H0. rewrite (Nless_def_1 a a''). + exact (IHa _ _ H H0). + * apply Nless_def_3. + + induction a'' as [|a'' _|a'' _] using N.binary_ind. + * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. + * rewrite (Nless_def_4 a' a'') in H0. discriminate H0. + * apply Nless_def_3. + - induction a' as [|a' _|a' _] using N.binary_ind. + + rewrite (Nless_z (N.succ_double a)) in H. discriminate H. + + rewrite (Nless_def_4 a a') in H. discriminate H. + + induction a'' using N.binary_ind. + * rewrite (Nless_z (N.succ_double a')) in H0. discriminate H0. + * rewrite (Nless_def_4 a' a'') in H0. discriminate H0. + * rewrite (Nless_def_2 a' a'') in H0. rewrite (Nless_def_2 a a') in H. + rewrite (Nless_def_2 a a''). exact (IHa _ _ H H0). Qed. Lemma Nless_total : forall a a', {Nless a a' = true} + {Nless a' a = true} + {a = a'}. Proof. induction a using N.binary_rec; intro a'. - 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.binary_rec. - case_eq (Nless N0 (N.double a)) ; intros Heqb. left. right. auto. - right. exact (N0_less_2 _ Heqb). - rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. - left. assumption. - right. reflexivity. - left. left. apply Nless_def_3. - induction a' as [|a' _|a' _] using N.binary_rec. - left. right. destruct a; reflexivity. - left. right. apply Nless_def_3. - rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->]. - left. assumption. - right. reflexivity. + - 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.binary_rec. + + case_eq (Nless N0 (N.double a)) ; intros Heqb. + * left. right. auto. + * right. exact (N0_less_2 _ Heqb). + + rewrite 2!Nless_def_1. destruct (IHa a') as [ | ->]. + * left. assumption. + * right. reflexivity. + + left. left. apply Nless_def_3. + - induction a' as [|a' _|a' _] using N.binary_rec. + + left. right. destruct a; reflexivity. + + left. right. apply Nless_def_3. + + rewrite 2!Nless_def_2. destruct (IHa a') as [ | ->]. + * left. assumption. + * right. reflexivity. Qed. (** Number of digits in a number *) @@ -622,7 +627,7 @@ induction bv; intros. inversion H. destruct p ; simpl. destruct (Bv2N n bv); destruct h; simpl in *; auto. - specialize IHbv with p (lt_S_n _ _ H). + specialize IHbv with p (Lt.lt_S_n _ _ H). simpl in * ; destruct (Bv2N n bv); destruct h; simpl in *; auto. Qed. @@ -641,7 +646,7 @@ Proof. destruct n as [|n]. inversion H. induction n ; destruct p ; unfold Vector.nth_order in *; simpl in * ; auto. -intros H ; destruct (lt_n_O _ (lt_S_n _ _ H)). +intros H ; destruct (Lt.lt_n_O _ (Lt.lt_S_n _ _ H)). Qed. (** Binary bitwise operations are the same in the two worlds. *) diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index cddc5f4cf..94242394b 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -6,8 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Minus Compare_dec Sumbool Div2 Min Max. -Require Import BinPos BinNat Pnat. +Require Import BinPos BinNat PeanoNat Pnat. (** * Conversions from [N] to [nat] *) @@ -68,52 +67,58 @@ Qed. Lemma inj_sub a a' : N.to_nat (a - a') = N.to_nat a - N.to_nat a'. Proof. - destruct a as [|a], a' as [|a']; simpl; auto with arith. + destruct a as [|a], a' as [|a']; simpl; rewrite ?Nat.sub_0_r; trivial. 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. + - subst. now rewrite Pos.sub_mask_diag, Nat.sub_diag. + - rewrite Pos.sub_mask_neg; trivial. apply Pos2Nat.inj_lt in H. + simpl; symmetry; apply Nat.sub_0_le. now apply Nat.lt_le_incl. + - destruct (Pos.sub_mask_pos' _ _ H) as (q & -> & Hq). + simpl; symmetry; apply Nat.add_sub_eq_l. now rewrite <- Hq, Pos2Nat.inj_add. Qed. -Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a). +Lemma inj_pred a : N.to_nat (N.pred a) = Nat.pred (N.to_nat a). Proof. - intros. rewrite pred_of_minus, N.pred_sub. apply inj_sub. + rewrite <- Nat.sub_1_r, N.pred_sub. apply inj_sub. Qed. -Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a). +Lemma inj_div2 a : N.to_nat (N.div2 a) = Nat.div2 (N.to_nat a). Proof. 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. + - simpl N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. + - simpl N.to_nat. now rewrite Pos2Nat.inj_xO, Nat.div2_double. Qed. Lemma inj_compare a a' : - (a ?= a')%N = nat_compare (N.to_nat a) (N.to_nat a'). + (a ?= a')%N = (N.to_nat a ?= N.to_nat a'). Proof. 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. + - now destruct (Pos2Nat.is_succ p) as (n,->). + - now destruct (Pos2Nat.is_succ p) as (n,->). + - apply Pos2Nat.inj_compare. Qed. Lemma inj_max a a' : - N.to_nat (N.max a a') = max (N.to_nat a) (N.to_nat a'). + N.to_nat (N.max a a') = Nat.max (N.to_nat a) (N.to_nat a'). Proof. unfold N.max. rewrite inj_compare; symmetry. - case nat_compare_spec; intros H; try rewrite H; auto with arith. + case Nat.compare_spec; intros. + - now apply Nat.max_r, Nat.eq_le_incl. + - now apply Nat.max_r, Nat.lt_le_incl. + - now apply Nat.max_l, Nat.lt_le_incl. Qed. Lemma inj_min a a' : - N.to_nat (N.min a a') = min (N.to_nat a) (N.to_nat a'). + N.to_nat (N.min a a') = Nat.min (N.to_nat a) (N.to_nat a'). Proof. unfold N.min; rewrite inj_compare. symmetry. - case nat_compare_spec; intros H; try rewrite H; auto with arith. + case Nat.compare_spec; intros. + - now apply Nat.min_l, Nat.eq_le_incl. + - now apply Nat.min_l, Nat.lt_le_incl. + - now apply Nat.min_r, Nat.lt_le_incl. Qed. Lemma inj_iter a {A} (f:A->A) (x:A) : - N.iter a f x = nat_rect (fun _ => A) x (fun _ => f) (N.to_nat a). + N.iter a f x = Nat.iter (N.to_nat a) f x. Proof. destruct a as [|a]. trivial. apply Pos2Nat.inj_iter. Qed. @@ -166,7 +171,7 @@ 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). +Lemma inj_pred n : N.of_nat (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. @@ -178,23 +183,23 @@ 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). +Lemma inj_div2 n : N.of_nat (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. + (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'). + N.of_nat (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'). + N.of_nat (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_rect (fun _ => A) x (fun _ => f) n = N.iter (N.of_nat n) f x. + Nat.iter n f x = N.iter (N.of_nat n) f x. Proof. now rewrite N2Nat.inj_iter, !id. Qed. End Nat2N. diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 8973df358..446fd7eb8 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -9,11 +9,22 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor ZGcd ZLcm NZLog NZSqrt ZBits. -(** This functor summarizes all known facts about Z. *) +(** The two following functors summarize all known facts about N. -Module Type ZProp (Z:ZAxiomsSig) := - ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z - <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z - <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z - <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z - <+ ZBitsProp Z. + - [ZBasicProp] provides properties of basic functions: + + - * min max <= < + + - [ZExtraProp] provides properties of advanced functions: + pow, sqrt, log2, div, gcd, and bitwise functions. + + If necessary, the earlier all-in-one functor [ZProp] + could be re-obtained via [ZBasicProp <+ ZExtraProp] *) + +Module Type ZBasicProp (Z:ZAxiomsMiniSig) := ZMaxMinProp Z. + +Module Type ZExtraProp (Z:ZAxiomsSig)(P:ZBasicProp Z) := + ZSgnAbsProp Z P <+ ZParityProp Z P <+ ZPowProp Z P + <+ NZSqrtProp Z Z P <+ NZSqrtUpProp Z Z P + <+ NZLog2Prop Z Z Z P <+ NZLog2UpProp Z Z Z P + <+ ZDivProp Z P <+ ZQuotProp Z P <+ ZGcdProp Z P <+ ZLcmProp Z P + <+ ZBitsProp Z P. diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v index eca97ace9..c1c78d911 100644 --- a/theories/Numbers/Integer/BigZ/BigZ.v +++ b/theories/Numbers/Integer/BigZ/BigZ.v @@ -29,7 +29,7 @@ Delimit Scope bigZ_scope with bigZ. Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder := ZMake.Make BigN <+ ZTypeIsZAxioms - <+ ZProp [no inline] + <+ ZBasicProp [no inline] <+ ZExtraProp [no inline] <+ HasEqBool2Dec [no inline] <+ MinMaxLogicalProperties [no inline] <+ MinMaxDecProperties [no inline]. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index b5e1fa5b0..11eb6e4d0 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -332,9 +332,9 @@ and get their properties *) (* The following lines increase the compilation time at least twice *) (* -Require Import NPeano. +Require PeanoNat. -Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod. +Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod PeanoNat.Nat. Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod. Eval compute in (3, 5) * (4, 6). diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 3a432eaa0..5b41dba43 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -19,7 +19,8 @@ Require Export Equalities Orders NumPrelude GenericMinMax. Module Type ZeroSuccPred (Import T:Typ). Parameter Inline(20) zero : t. - Parameters Inline succ pred : t -> t. + Parameter Inline(50) succ : t -> t. + Parameter Inline pred : t -> t. End ZeroSuccPred. Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T). diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v index 907394101..df3e7c7e4 100644 --- a/theories/Numbers/Natural/Abstract/NProperties.v +++ b/theories/Numbers/Natural/Abstract/NProperties.v @@ -9,9 +9,20 @@ Require Export NAxioms. Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits. -(** This functor summarizes all known facts about N. *) +(** The two following functors summarize all known facts about N. -Module Type NProp (N:NAxiomsSig) := - NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N - <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N - <+ NBitsProp N. + - [NBasicProp] provides properties of basic functions: + + - * min max <= < + + - [NExtraProp] provides properties of advanced functions: + pow, sqrt, log2, div, gcd, and bitwise functions. + + If necessary, the earlier all-in-one functor [NProp] + could be re-obtained via [NBasicProp <+ NExtraProp] *) + +Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N. + +Module Type NExtraProp (N:NAxiomsSig)(P:NBasicProp N) := + NParityProp N P <+ NPowProp N P <+ NSqrtProp N P + <+ NLog2Prop N P <+ NDivProp N P <+ NGcdProp N P <+ NLcmProp N P + <+ NBitsProp N P. diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 380963cff..02ed9fe53 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -31,7 +31,7 @@ Delimit Scope bigN_scope with bigN. Module BigN <: NType <: OrderedTypeFull <: TotalOrder := NMake.Make Int31Cyclic <+ NTypeIsNAxioms - <+ NProp [no inline] + <+ NBasicProp [no inline] <+ NExtraProp [no inline] <+ HasEqBool2Dec [no inline] <+ MinMaxLogicalProperties [no inline] <+ MinMaxDecProperties [no inline]. diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v index 5e36916b9..1620cfed8 100644 --- a/theories/Numbers/Natural/Peano/NPeano.v +++ b/theories/Numbers/Natural/Peano/NPeano.v @@ -8,808 +8,8 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Import - Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat - NAxioms NProperties. +Require Import PeanoNat NAxioms. -(** Functions not already defined *) +(** * [PeanoNat.Nat] already implements [NAxiomSig] *) -Fixpoint leb n m := - match n, m with - | O, _ => true - | _, O => false - | S n', S m' => leb n' m' - end. - -Definition ltb n m := leb (S n) m. - -Infix "<=?" := leb (at level 70) : nat_scope. -Infix "<?" := ltb (at level 70) : nat_scope. - -Lemma leb_le n m : (n <=? m) = true <-> n <= m. -Proof. - revert m. - induction n. split; auto with arith. - destruct m; simpl. now split. - rewrite IHn. split; auto with arith. -Qed. - -Lemma ltb_lt n m : (n <? m) = true <-> n < m. -Proof. - unfold ltb, lt. apply leb_le. -Qed. - -Fixpoint pow n m := - match m with - | O => 1 - | S m => n * (pow n m) - end. - -Infix "^" := pow : nat_scope. - -Lemma pow_0_r : forall a, a^0 = 1. -Proof. reflexivity. Qed. - -Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b. -Proof. reflexivity. Qed. - -Definition square n := n * n. - -Lemma square_spec n : square n = n * n. -Proof. reflexivity. Qed. - -Definition Even n := exists m, n = 2*m. -Definition Odd n := exists m, n = 2*m+1. - -Fixpoint even n := - match n with - | O => true - | 1 => false - | S (S n') => even n' - end. - -Definition odd n := negb (even n). - -Lemma even_spec : forall n, even n = true <-> Even n. -Proof. - fix 1. - destruct n as [|[|n]]; simpl; try rewrite even_spec; split. - now exists 0. - trivial. - discriminate. - intros (m,H). destruct m. discriminate. - simpl in H. rewrite <- plus_n_Sm in H. discriminate. - intros (m,H). exists (S m). rewrite H. simpl. now rewrite plus_n_Sm. - intros (m,H). destruct m. discriminate. exists m. - simpl in H. rewrite <- plus_n_Sm in H. inversion H. reflexivity. -Qed. - -Lemma odd_spec : forall n, odd n = true <-> Odd n. -Proof. - unfold odd. - fix 1. - destruct n as [|[|n]]; simpl; try rewrite odd_spec; split. - discriminate. - intros (m,H). rewrite <- plus_n_Sm in H; discriminate. - now exists 0. - trivial. - intros (m,H). exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m). - intros (m,H). destruct m. discriminate. exists m. - simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl. - now rewrite <- !plus_n_Sm, <- !plus_n_O. -Qed. - -Lemma Even_equiv : forall n, Even n <-> Even.even n. -Proof. - split. intros (p,->). apply Even.even_mult_l. do 3 constructor. - intros H. destruct (even_2n n H) as (p,->). - exists p. unfold double. simpl. now rewrite <- plus_n_O. -Qed. - -Lemma Odd_equiv : forall n, Odd n <-> Even.odd n. -Proof. - split. intros (p,->). rewrite <- plus_n_Sm, <- plus_n_O. - apply Even.odd_S. apply Even.even_mult_l. do 3 constructor. - intros H. destruct (odd_S2n n H) as (p,->). - exists p. unfold double. simpl. now rewrite <- plus_n_Sm, <- !plus_n_O. -Qed. - -(* A linear, tail-recursive, division for nat. - - In [divmod], [y] is the predecessor of the actual divisor, - and [u] is [y] minus the real remainder -*) - -Fixpoint divmod x y q u := - match x with - | 0 => (q,u) - | S x' => match u with - | 0 => divmod x' y (S q) y - | S u' => divmod x' y q u' - end - end. - -Definition div x y := - match y with - | 0 => y - | S y' => fst (divmod x y' 0 y') - end. - -Definition modulo x y := - match y with - | 0 => y - | S y' => y' - snd (divmod x y' 0 y') - end. - -Infix "/" := div : nat_scope. -Infix "mod" := modulo (at level 40, no associativity) : nat_scope. - -Lemma divmod_spec : forall x y q u, u <= y -> - let (q',u') := divmod x y q u in - x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y. -Proof. - induction x. simpl. intuition. - intros y q u H. destruct u; simpl divmod. - generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u'). - intros (EQ,LE); split; trivial. - rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O. - now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm. - generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u'). - intros (EQ,LE); split; trivial. - rewrite <- EQ. - rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m. -Qed. - -Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y. -Proof. - intros x y Hy. - destruct y; [ now elim Hy | clear Hy ]. - unfold div, modulo. - generalize (divmod_spec x y 0 y (le_n y)). - destruct divmod as (q,u). - intros (U,V). - simpl in *. - now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U. -Qed. - -Lemma mod_bound_pos : forall x y, 0<=x -> 0<y -> 0 <= x mod y < y. -Proof. - intros x y Hx Hy. split. auto with arith. - destruct y; [ now elim Hy | clear Hy ]. - unfold modulo. - apply le_n_S, le_minus. -Qed. - -(** Square root *) - -(** The following square root function is linear (and tail-recursive). - With Peano representation, we can't do better. For faster algorithm, - see Psqrt/Zsqrt/Nsqrt... - - We search the square root of n = k + p^2 + (q - r) - with q = 2p and 0<=r<=q. We start with p=q=r=0, hence - looking for the square root of n = k. Then we progressively - decrease k and r. When k = S k' and r=0, it means we can use (S p) - as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2. - When k reaches 0, we have found the biggest p^2 square contained - in n, hence the square root of n is p. -*) - -Fixpoint sqrt_iter k p q r := - match k with - | O => p - | S k' => match r with - | O => sqrt_iter k' (S p) (S (S q)) (S (S q)) - | S r' => sqrt_iter k' p q r' - end - end. - -Definition sqrt n := sqrt_iter n 0 0 0. - -Lemma sqrt_iter_spec : forall k p q r, - q = p+p -> r<=q -> - let s := sqrt_iter k p q r in - s*s <= k + p*p + (q - r) < (S s)*(S s). -Proof. - induction k. - (* k = 0 *) - simpl; intros p q r Hq Hr. - split. - apply le_plus_l. - apply le_lt_n_Sm. - rewrite <- mult_n_Sm. - rewrite plus_assoc, (plus_comm p), <- plus_assoc. - apply plus_le_compat; trivial. - rewrite <- Hq. apply le_minus. - (* k = S k' *) - destruct r. - (* r = 0 *) - intros Hq _. - replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))). - apply IHk. - simpl. rewrite <- plus_n_Sm. congruence. - auto with arith. - rewrite minus_diag, <- minus_n_O, <- plus_n_O. simpl. - rewrite <- plus_n_Sm; f_equal. rewrite <- plus_assoc; f_equal. - rewrite <- mult_n_Sm, (plus_comm p), <- plus_assoc. congruence. - (* r = S r' *) - intros Hq Hr. - replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)). - apply IHk; auto with arith. - simpl. rewrite plus_n_Sm. f_equal. rewrite minus_Sn_m; auto. -Qed. - -Lemma sqrt_spec : forall n, - (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n). -Proof. - intros. - set (s:=sqrt n). - replace n with (n + 0*0 + (0-0)). - apply sqrt_iter_spec; auto. - simpl. now rewrite <- 2 plus_n_O. -Qed. - -(** A linear tail-recursive base-2 logarithm - - In [log2_iter], we maintain the logarithm [p] of the counter [q], - while [r] is the distance between [q] and the next power of 2, - more precisely [q + S r = 2^(S p)] and [r<2^p]. At each - recursive call, [q] goes up while [r] goes down. When [r] - is 0, we know that [q] has almost reached a power of 2, - and we increase [p] at the next call, while resetting [r] - to [q]. - - Graphically (numbers are [q], stars are [r]) : - -<< - 10 - 9 - 8 - 7 * - 6 * - 5 ... - 4 - 3 * - 2 * - 1 * * -0 * * * ->> - - We stop when [k], the global downward counter reaches 0. - At that moment, [q] is the number we're considering (since - [k+q] is invariant), and [p] its logarithm. -*) - -Fixpoint log2_iter k p q r := - match k with - | O => p - | S k' => match r with - | O => log2_iter k' (S p) (S q) q - | S r' => log2_iter k' p (S q) r' - end - end. - -Definition log2 n := log2_iter (pred n) 0 1 0. - -Lemma log2_iter_spec : forall k p q r, - 2^(S p) = q + S r -> r < 2^p -> - let s := log2_iter k p q r in - 2^s <= k + q < 2^(S s). -Proof. - induction k. - (* k = 0 *) - intros p q r EQ LT. simpl log2_iter. cbv zeta. - split. - rewrite plus_O_n. - apply plus_le_reg_l with (2^p). - simpl pow in EQ. rewrite <- plus_n_O in EQ. rewrite EQ. - rewrite plus_comm. apply plus_le_compat_r. now apply lt_le_S. - rewrite EQ, plus_comm. apply plus_lt_compat_l. apply lt_0_Sn. - (* k = S k' *) - intros p q r EQ LT. destruct r. - (* r = 0 *) - rewrite <- plus_n_Sm, <- plus_n_O in EQ. - rewrite plus_Sn_m, plus_n_Sm. apply IHk. - rewrite <- EQ. remember (S p) as p'; simpl. now rewrite <- plus_n_O. - unfold lt. now rewrite EQ. - (* r = S r' *) - rewrite plus_Sn_m, plus_n_Sm. apply IHk. - now rewrite plus_Sn_m, plus_n_Sm. - unfold lt. - now apply lt_le_weak. -Qed. - -Lemma log2_spec : forall n, 0<n -> - 2^(log2 n) <= n < 2^(S (log2 n)). -Proof. - intros. - set (s:=log2 n). - replace n with (pred n + 1). - apply log2_iter_spec; auto. - rewrite <- plus_n_Sm, <- plus_n_O. - symmetry. now apply S_pred with 0. -Qed. - -Lemma log2_nonpos : forall n, n<=0 -> log2 n = 0. -Proof. - inversion 1; now subst. -Qed. - -(** * Gcd *) - -(** We use Euclid algorithm, which is normally not structural, - but Coq is now clever enough to accept this (behind modulo - there is a subtraction, which now preserves being a subterm) -*) - -Fixpoint gcd a b := - match a with - | O => b - | S a' => gcd (b mod (S a')) (S a') - end. - -Definition divide x y := exists z, y=z*x. -Notation "( x | y )" := (divide x y) (at level 0) : nat_scope. - -Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b). -Proof. - fix 1. - intros [|a] b; simpl. - split. - now exists 0. - exists 1. simpl. now rewrite <- plus_n_O. - fold (b mod (S a)). - destruct (gcd_divide (b mod (S a)) (S a)) as (H,H'). - set (a':=S a) in *. - split; auto. - rewrite (div_mod b a') at 2 by discriminate. - destruct H as (u,Hu), H' as (v,Hv). - rewrite mult_comm. - exists ((b/a')*v + u). - rewrite mult_plus_distr_r. - now rewrite <- mult_assoc, <- Hv, <- Hu. -Qed. - -Lemma gcd_divide_l : forall a b, (gcd a b | a). -Proof. - intros. apply gcd_divide. -Qed. - -Lemma gcd_divide_r : forall a b, (gcd a b | b). -Proof. - intros. apply gcd_divide. -Qed. - -Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b). -Proof. - fix 1. - intros [|a] b; simpl; auto. - fold (b mod (S a)). - intros c H H'. apply gcd_greatest; auto. - set (a':=S a) in *. - rewrite (div_mod b a') in H' by discriminate. - destruct H as (u,Hu), H' as (v,Hv). - exists (v - (b/a')*u). - rewrite mult_comm in Hv. - now rewrite mult_minus_distr_r, <- Hv, <-mult_assoc, <-Hu, minus_plus. -Qed. - -(** * Bitwise operations *) - -(** We provide here some bitwise operations for unary numbers. - Some might be really naive, they are just there for fullfiling - the same interface as other for natural representations. As - soon as binary representations such as NArith are available, - it is clearly better to convert to/from them and use their ops. -*) - -Fixpoint testbit a n := - match n with - | O => odd a - | S n => testbit (div2 a) n - end. - -Definition shiftl a n := iter_nat n _ double a. -Definition shiftr a n := iter_nat n _ div2 a. - -Fixpoint bitwise (op:bool->bool->bool) n a b := - match n with - | O => O - | S n' => - (if op (odd a) (odd b) then 1 else 0) + - 2*(bitwise op n' (div2 a) (div2 b)) - end. - -Definition land a b := bitwise andb a a b. -Definition lor a b := bitwise orb (max a b) a b. -Definition ldiff a b := bitwise (fun b b' => b && negb b') a a b. -Definition lxor a b := bitwise xorb (max a b) a b. - -Lemma double_twice : forall n, double n = 2*n. -Proof. - simpl; intros. now rewrite <- plus_n_O. -Qed. - -Lemma testbit_0_l : forall n, testbit 0 n = false. -Proof. - now induction n. -Qed. - -Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true. -Proof. - unfold testbit. rewrite odd_spec. now exists a. -Qed. - -Lemma testbit_even_0 a : testbit (2*a) 0 = false. -Proof. - unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial. - now exists a. -Qed. - -Lemma testbit_odd_succ a n : testbit (2*a+1) (S n) = testbit a n. -Proof. - unfold testbit; fold testbit. - rewrite <- plus_n_Sm, <- plus_n_O. f_equal. - apply div2_double_plus_one. -Qed. - -Lemma testbit_even_succ a n : testbit (2*a) (S n) = testbit a n. -Proof. - unfold testbit; fold testbit. f_equal. apply div2_double. -Qed. - -Lemma shiftr_spec : forall a n m, - testbit (shiftr a n) m = testbit a (m+n). -Proof. - induction n; intros m. trivial. - now rewrite <- plus_n_O. - now rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn. -Qed. - -Lemma shiftl_spec_high : forall a n m, n<=m -> - testbit (shiftl a n) m = testbit a (m-n). -Proof. - induction n; intros m H. trivial. - now rewrite <- minus_n_O. - destruct m. inversion H. - simpl. apply le_S_n in H. - change (shiftl a (S n)) with (double (shiftl a n)). - rewrite double_twice, div2_double. now apply IHn. -Qed. - -Lemma shiftl_spec_low : forall a n m, m<n -> - testbit (shiftl a n) m = false. -Proof. - induction n; intros m H. inversion H. - change (shiftl a (S n)) with (double (shiftl a n)). - destruct m; simpl. - unfold odd. apply negb_false_iff. - apply even_spec. exists (shiftl a n). apply double_twice. - rewrite double_twice, div2_double. apply IHn. - now apply lt_S_n. -Qed. - -Lemma div2_bitwise : forall op n a b, - div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b). -Proof. - intros. unfold bitwise; fold bitwise. - destruct (op (odd a) (odd b)). - now rewrite div2_double_plus_one. - now rewrite plus_O_n, div2_double. -Qed. - -Lemma odd_bitwise : forall op n a b, - odd (bitwise op (S n) a b) = op (odd a) (odd b). -Proof. - intros. unfold bitwise; fold bitwise. - destruct (op (odd a) (odd b)). - apply odd_spec. rewrite plus_comm. eexists; eauto. - unfold odd. apply negb_false_iff. apply even_spec. - rewrite plus_O_n; eexists; eauto. -Qed. - -Lemma div2_decr : forall a n, a <= S n -> div2 a <= n. -Proof. - destruct a; intros. apply le_0_n. - apply le_trans with a. - apply lt_n_Sm_le, lt_div2, lt_0_Sn. now apply le_S_n. -Qed. - -Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) -> - forall n m a b, a<=n -> - testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). -Proof. - intros op Hop. - induction n; intros m a b Ha. - simpl. inversion Ha; subst. now rewrite testbit_0_l. - destruct m. - apply odd_bitwise. - unfold testbit; fold testbit. rewrite div2_bitwise. - apply IHn; now apply div2_decr. -Qed. - -Lemma testbit_bitwise_2 : forall op, op false false = false -> - forall n m a b, a<=n -> b<=n -> - testbit (bitwise op n a b) m = op (testbit a m) (testbit b m). -Proof. - intros op Hop. - induction n; intros m a b Ha Hb. - simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l. - destruct m. - apply odd_bitwise. - unfold testbit; fold testbit. rewrite div2_bitwise. - apply IHn; now apply div2_decr. -Qed. - -Lemma land_spec : forall a b n, - testbit (land a b) n = testbit a n && testbit b n. -Proof. - intros. unfold land. apply testbit_bitwise_1; trivial. -Qed. - -Lemma ldiff_spec : forall a b n, - testbit (ldiff a b) n = testbit a n && negb (testbit b n). -Proof. - intros. unfold ldiff. apply testbit_bitwise_1; trivial. -Qed. - -Lemma lor_spec : forall a b n, - testbit (lor a b) n = testbit a n || testbit b n. -Proof. - intros. unfold lor. apply testbit_bitwise_2. trivial. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. -Qed. - -Lemma lxor_spec : forall a b n, - testbit (lxor a b) n = xorb (testbit a n) (testbit b n). -Proof. - intros. unfold lxor. apply testbit_bitwise_2. trivial. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. - destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l. -Qed. - -(** * Implementation of [NAxiomsSig] by [nat] *) - -Module Nat - <: NAxiomsSig <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder. - -(** Bi-directional induction. *) - -Theorem bi_induction : - forall A : nat -> Prop, Proper (eq==>iff) A -> - A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n. -Proof. -intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS. -Qed. - -(** Basic operations. *) - -Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence. -Local Obligation Tactic := simpl_relation. -Program Instance succ_wd : Proper (eq==>eq) S. -Program Instance pred_wd : Proper (eq==>eq) pred. -Program Instance add_wd : Proper (eq==>eq==>eq) plus. -Program Instance sub_wd : Proper (eq==>eq==>eq) minus. -Program Instance mul_wd : Proper (eq==>eq==>eq) mult. - -Theorem pred_succ : forall n : nat, pred (S n) = n. -Proof. -reflexivity. -Qed. - -Theorem one_succ : 1 = S 0. -Proof. -reflexivity. -Qed. - -Theorem two_succ : 2 = S 1. -Proof. -reflexivity. -Qed. - -Theorem add_0_l : forall n : nat, 0 + n = n. -Proof. -reflexivity. -Qed. - -Theorem add_succ_l : forall n m : nat, (S n) + m = S (n + m). -Proof. -reflexivity. -Qed. - -Theorem sub_0_r : forall n : nat, n - 0 = n. -Proof. -intro n; now destruct n. -Qed. - -Theorem sub_succ_r : forall n m : nat, n - (S m) = pred (n - m). -Proof. -induction n; destruct m; simpl; auto. apply sub_0_r. -Qed. - -Theorem mul_0_l : forall n : nat, 0 * n = 0. -Proof. -reflexivity. -Qed. - -Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m. -Proof. -assert (add_S_r : forall n m, n+S m = S(n+m)) by (induction n; auto). -assert (add_comm : forall n m, n+m = m+n). - induction n; simpl; auto. intros; rewrite add_S_r; auto. -intros n m; now rewrite add_comm. -Qed. - -(** Order on natural numbers *) - -Program Instance lt_wd : Proper (eq==>eq==>iff) lt. - -Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m. -Proof. -unfold lt; split. apply le_S_n. induction 1; auto. -Qed. - - -Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m. -Proof. -split. -inversion 1; auto. rewrite lt_succ_r; auto. -destruct 1; [|subst; auto]. rewrite <- lt_succ_r; auto. -Qed. - -Theorem lt_irrefl : forall n : nat, ~ (n < n). -Proof. -induction n. intro H; inversion H. rewrite lt_succ_r; auto. -Qed. - -(** Facts specific to natural numbers, not integers. *) - -Theorem pred_0 : pred 0 = 0. -Proof. -reflexivity. -Qed. - -(** Recursion fonction *) - -Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A := - nat_rect (fun _ => A). - -Instance recursion_wd {A} (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. -Proof. -intros a a' Ha f f' Hf n n' Hn. subst n'. -induction n; simpl; auto. apply Hf; auto. -Qed. - -Theorem recursion_0 : - forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a. -Proof. -reflexivity. -Qed. - -Theorem recursion_succ : - forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A), - Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> - forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)). -Proof. -unfold Proper, respectful in *; induction n; simpl; auto. -Qed. - -(** The instantiation of operations. - Placing them at the very end avoids having indirections in above lemmas. *) - -Definition t := nat. -Definition eq := @eq nat. -Definition eqb := beq_nat. -Definition compare := nat_compare. -Definition zero := 0. -Definition one := 1. -Definition two := 2. -Definition succ := S. -Definition pred := pred. -Definition add := plus. -Definition sub := minus. -Definition mul := mult. -Definition lt := lt. -Definition le := le. -Definition ltb := ltb. -Definition leb := leb. - -Definition min := min. -Definition max := max. -Definition max_l := max_l. -Definition max_r := max_r. -Definition min_l := min_l. -Definition min_r := min_r. - -Definition eqb_eq := beq_nat_true_iff. -Definition compare_spec := nat_compare_spec. -Definition eq_dec := eq_nat_dec. -Definition leb_le := leb_le. -Definition ltb_lt := ltb_lt. - -Definition Even := Even. -Definition Odd := Odd. -Definition even := even. -Definition odd := odd. -Definition even_spec := even_spec. -Definition odd_spec := odd_spec. - -Program Instance pow_wd : Proper (eq==>eq==>eq) pow. -Definition pow_0_r := pow_0_r. -Definition pow_succ_r := pow_succ_r. -Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed. -Definition pow := pow. - -Definition square := square. -Definition square_spec := square_spec. - -Definition log2_spec := log2_spec. -Definition log2_nonpos := log2_nonpos. -Definition log2 := log2. - -Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a. -Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed. -Definition sqrt := sqrt. - -Definition div := div. -Definition modulo := modulo. -Program Instance div_wd : Proper (eq==>eq==>eq) div. -Program Instance mod_wd : Proper (eq==>eq==>eq) modulo. -Definition div_mod := div_mod. -Definition mod_bound_pos := mod_bound_pos. - -Definition divide := divide. -Definition gcd := gcd. -Definition gcd_divide_l := gcd_divide_l. -Definition gcd_divide_r := gcd_divide_r. -Definition gcd_greatest := gcd_greatest. -Lemma gcd_nonneg : forall a b, 0<=gcd a b. -Proof. intros. apply le_O_n. Qed. - -Definition testbit := testbit. -Definition shiftl := shiftl. -Definition shiftr := shiftr. -Definition lxor := lxor. -Definition land := land. -Definition lor := lor. -Definition ldiff := ldiff. -Definition div2 := div2. - -Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. -Definition testbit_odd_0 := testbit_odd_0. -Definition testbit_even_0 := testbit_even_0. -Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ a n. -Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ a n. -Lemma testbit_neg_r a n (H:n<0) : testbit a n = false. -Proof. inversion H. Qed. -Definition shiftl_spec_low := shiftl_spec_low. -Definition shiftl_spec_high a n m (_:0<=m) := shiftl_spec_high a n m. -Definition shiftr_spec a n m (_:0<=m) := shiftr_spec a n m. -Definition lxor_spec := lxor_spec. -Definition land_spec := land_spec. -Definition lor_spec := lor_spec. -Definition ldiff_spec := ldiff_spec. -Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _. - -(** Generic Properties *) - -Include NProp - <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. - -End Nat. - -Bind Scope nat_scope with Nat.t nat. - -(** [Nat] contains an [order] tactic for natural numbers *) - -(** Note that [Nat.order] is domain-agnostic: it will not prove - [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *) - -Section TestOrder. - Let test : forall x y, x<=y -> y<=x -> x=y. - Proof. - Nat.order. - Qed. -End TestOrder. +Module Nat <: NAxiomsSig := Nat. diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index fe1ec9398..4f8d9ee27 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -482,8 +482,8 @@ Fixpoint lxor (p q:positive) : N := (** Shifts. NB: right shift of 1 stays at 1. *) -Definition shiftl_nat (p:positive) := nat_rect _ p (fun _ => xO). -Definition shiftr_nat (p:positive) := nat_rect _ p (fun _ => div2). +Definition shiftl_nat (p:positive)(n:nat) := Nat.iter n xO p. +Definition shiftr_nat (p:positive)(n:nat) := Nat.iter n div2 p. Definition shiftl (p:positive)(n:N) := match n with diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index 9ce399beb..4336d47af 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec. +Require Import BinPos PeanoNat. (** Properties of the injection from binary positive numbers to Peano natural numbers *) @@ -25,7 +25,7 @@ Module Pos2Nat. Lemma inj_succ p : to_nat (succ p) = S (to_nat p). Proof. unfold to_nat. rewrite iter_op_succ. trivial. - apply plus_assoc. + apply Nat.add_assoc. Qed. Theorem inj_add p q : to_nat (p + q) = to_nat p + to_nat q. @@ -99,38 +99,38 @@ Qed. (** [Pos.to_nat] is a morphism for comparison *) -Lemma inj_compare p q : (p ?= q) = nat_compare (to_nat p) (to_nat q). +Lemma inj_compare p q : (p ?= q)%positive = (to_nat p ?= to_nat q). Proof. revert q. induction p as [ |p IH] using peano_ind; intros q. - destruct (succ_pred_or q) as [Hq|Hq]; [now subst|]. - rewrite <- Hq, lt_1_succ, inj_succ, inj_1, nat_compare_S. - symmetry. apply nat_compare_lt, is_pos. - destruct (succ_pred_or q) as [Hq|Hq]; [subst|]. - rewrite compare_antisym, lt_1_succ, inj_succ. simpl. - symmetry. apply nat_compare_gt, is_pos. - now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH. + - destruct (succ_pred_or q) as [Hq|Hq]; [now subst|]. + rewrite <- Hq, lt_1_succ, inj_succ, inj_1, Nat.compare_succ. + symmetry. apply Nat.compare_lt_iff, is_pos. + - destruct (succ_pred_or q) as [Hq|Hq]; [subst|]. + rewrite compare_antisym, lt_1_succ, inj_succ. simpl. + symmetry. apply Nat.compare_gt_iff, is_pos. + now rewrite <- Hq, 2 inj_succ, compare_succ_succ, IH. Qed. (** [Pos.to_nat] is a morphism for [lt], [le], etc *) Lemma inj_lt p q : (p < q)%positive <-> to_nat p < to_nat q. Proof. - unfold lt. now rewrite inj_compare, nat_compare_lt. + unfold lt. now rewrite inj_compare, Nat.compare_lt_iff. Qed. Lemma inj_le p q : (p <= q)%positive <-> to_nat p <= to_nat q. Proof. - unfold le. now rewrite inj_compare, nat_compare_le. + unfold le. now rewrite inj_compare, Nat.compare_le_iff. Qed. Lemma inj_gt p q : (p > q)%positive <-> to_nat p > to_nat q. Proof. - unfold gt. now rewrite inj_compare, nat_compare_gt. + unfold gt. now rewrite inj_compare, Nat.compare_gt_iff. Qed. Lemma inj_ge p q : (p >= q)%positive <-> to_nat p >= to_nat q. Proof. - unfold ge. now rewrite inj_compare, nat_compare_ge. + unfold ge. now rewrite inj_compare, Nat.compare_ge_iff. Qed. (** [Pos.to_nat] is a morphism for subtraction *) @@ -138,64 +138,65 @@ Qed. Theorem inj_sub p q : (q < p)%positive -> to_nat (p - q) = to_nat p - to_nat q. Proof. - intro H; apply plus_reg_l with (to_nat q); rewrite le_plus_minus_r. - now rewrite <- inj_add, add_comm, sub_add. - now apply lt_le_weak, inj_lt. + intro H. apply Nat.add_cancel_r with (to_nat q). + rewrite Nat.sub_add. + now rewrite <- inj_add, sub_add. + now apply Nat.lt_le_incl, inj_lt. Qed. Theorem inj_sub_max p q : - to_nat (p - q) = Peano.max 1 (to_nat p - to_nat q). + to_nat (p - q) = Nat.max 1 (to_nat p - to_nat q). Proof. destruct (ltb_spec q p). - rewrite <- inj_sub by trivial. - now destruct (is_succ (p - q)) as (m,->). - rewrite sub_le by trivial. - replace (to_nat p - to_nat q) with 0; trivial. - apply le_n_0_eq. - rewrite <- (minus_diag (to_nat p)). - now apply minus_le_compat_l, inj_le. + - (* q < p *) + rewrite <- inj_sub by trivial. + now destruct (is_succ (p - q)) as (m,->). + - (* p <= q *) + rewrite sub_le by trivial. + apply inj_le, Nat.sub_0_le in H. now rewrite H. Qed. Theorem inj_pred p : (1 < p)%positive -> - to_nat (pred p) = Peano.pred (to_nat p). + to_nat (pred p) = Nat.pred (to_nat p). Proof. - intros H. now rewrite <- Pos.sub_1_r, inj_sub, pred_of_minus. + intros. now rewrite <- Pos.sub_1_r, inj_sub, Nat.sub_1_r. Qed. Theorem inj_pred_max p : - to_nat (pred p) = Peano.max 1 (Peano.pred (to_nat p)). + to_nat (pred p) = Nat.max 1 (Peano.pred (to_nat p)). Proof. - rewrite <- Pos.sub_1_r, pred_of_minus. apply inj_sub_max. + rewrite <- Pos.sub_1_r, <- Nat.sub_1_r. apply inj_sub_max. Qed. (** [Pos.to_nat] and other operations *) Lemma inj_min p q : - to_nat (min p q) = Peano.min (to_nat p) (to_nat q). + to_nat (min p q) = Nat.min (to_nat p) (to_nat q). Proof. unfold min. rewrite inj_compare. - case nat_compare_spec; intros H; symmetry. - apply Peano.min_l. now rewrite H. - now apply Peano.min_l, lt_le_weak. - now apply Peano.min_r, lt_le_weak. + case Nat.compare_spec; intros H; symmetry. + - apply Nat.min_l. now rewrite H. + - now apply Nat.min_l, Nat.lt_le_incl. + - now apply Nat.min_r, Nat.lt_le_incl. Qed. Lemma inj_max p q : - to_nat (max p q) = Peano.max (to_nat p) (to_nat q). + to_nat (max p q) = Nat.max (to_nat p) (to_nat q). Proof. unfold max. rewrite inj_compare. - case nat_compare_spec; intros H; symmetry. - apply Peano.max_r. now rewrite H. - now apply Peano.max_r, lt_le_weak. - now apply Peano.max_l, lt_le_weak. + case Nat.compare_spec; intros H; symmetry. + - apply Nat.max_r. now rewrite H. + - now apply Nat.max_r, Nat.lt_le_incl. + - now apply Nat.max_l, Nat.lt_le_incl. Qed. Theorem inj_iter : forall p {A} (f:A->A) (x:A), - Pos.iter f x p = nat_rect (fun _ => A) x (fun _ => f) (to_nat p). + Pos.iter f x p = Nat.iter (to_nat p) f x. Proof. - induction p using peano_ind. trivial. - intros. rewrite inj_succ, iter_succ. simpl. now f_equal. + induction p using peano_ind. + - trivial. + - intros. rewrite inj_succ, iter_succ. simpl. now f_equal. Qed. End Pos2Nat. @@ -257,11 +258,11 @@ Lemma inj_mul (n m : nat) : n<>0 -> m<>0 -> Proof. intros Hn Hm. apply Pos2Nat.inj. rewrite Pos2Nat.inj_mul, !id; trivial. -intros H. apply mult_is_O in H. destruct H. now elim Hn. now elim Hm. +intros H. apply Nat.mul_eq_0 in H. destruct H. now elim Hn. now elim Hm. Qed. Lemma inj_compare (n m : nat) : n<>0 -> m<>0 -> - nat_compare n m = (Pos.of_nat n ?= Pos.of_nat m). + (n ?= m) = (Pos.of_nat n ?= Pos.of_nat m)%positive. Proof. intros Hn Hm. rewrite Pos2Nat.inj_compare, !id; trivial. Qed. @@ -282,8 +283,9 @@ Proof. destruct n as [|n]. simpl. symmetry. apply Pos.min_l, Pos.le_1_l. destruct m as [|m]. simpl. symmetry. apply Pos.min_r, Pos.le_1_l. unfold Pos.min. rewrite <- inj_compare by easy. - case nat_compare_spec; intros H; f_equal; apply min_l || apply min_r. - rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak. + case Nat.compare_spec; intros H; f_equal; + apply Nat.min_l || apply Nat.min_r. + rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl. Qed. Lemma inj_max (n m : nat) : @@ -292,8 +294,9 @@ Proof. destruct n as [|n]. simpl. symmetry. apply Pos.max_r, Pos.le_1_l. destruct m as [|m]. simpl. symmetry. apply Pos.max_l, Pos.le_1_l. unfold Pos.max. rewrite <- inj_compare by easy. - case nat_compare_spec; intros H; f_equal; apply max_l || apply max_r. - rewrite H; auto. now apply lt_le_weak. now apply lt_le_weak. + case Nat.compare_spec; intros H; f_equal; + apply Nat.max_l || apply Nat.max_r. + rewrite H; auto. now apply Nat.lt_le_incl. now apply Nat.lt_le_incl. Qed. End Nat2Pos. @@ -365,7 +368,7 @@ apply Pos2Nat.inj. now rewrite Pos2Nat.inj_succ, !id_succ. Qed. Lemma inj_compare n m : - nat_compare n m = (Pos.of_succ_nat n ?= Pos.of_succ_nat m). + (n ?= m) = (Pos.of_succ_nat n ?= Pos.of_succ_nat m)%positive. Proof. rewrite Pos2Nat.inj_compare, !id_succ; trivial. Qed. @@ -438,11 +441,11 @@ Lemma Pmult_nat_mult : forall p n, Pmult_nat p n = Pos.to_nat p * n. Proof. induction p; intros n; unfold Pos.to_nat; simpl. - f_equal. rewrite 2 IHp. rewrite <- mult_assoc. - f_equal. simpl. now rewrite <- plus_n_O. - rewrite 2 IHp. rewrite <- mult_assoc. - f_equal. simpl. now rewrite <- plus_n_O. - simpl. now rewrite <- plus_n_O. + f_equal. rewrite 2 IHp. rewrite <- Nat.mul_assoc. + f_equal. simpl. now rewrite Nat.add_0_r. + rewrite 2 IHp. rewrite <- Nat.mul_assoc. + f_equal. simpl. now rewrite Nat.add_0_r. + simpl. now rewrite Nat.add_0_r. Qed. Lemma Pmult_nat_succ_morphism : @@ -454,7 +457,7 @@ Qed. Theorem Pmult_nat_l_plus_morphism : forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n. Proof. - intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply mult_plus_distr_r. + intros. rewrite !Pmult_nat_mult, Pos2Nat.inj_add. apply Nat.mul_add_distr_r. Qed. Theorem Pmult_nat_plus_carry_morphism : @@ -466,19 +469,19 @@ Qed. Lemma Pmult_nat_r_plus_morphism : forall p n, Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. Proof. - intros. rewrite !Pmult_nat_mult. apply mult_plus_distr_l. + intros. rewrite !Pmult_nat_mult. apply Nat.mul_add_distr_l. Qed. Lemma ZL6 : forall p, Pmult_nat p 2 = Pos.to_nat p + Pos.to_nat p. Proof. - intros. rewrite Pmult_nat_mult, mult_comm. simpl. now rewrite <- plus_n_O. + intros. rewrite Pmult_nat_mult, Nat.mul_comm. simpl. now rewrite Nat.add_0_r. Qed. Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n. Proof. intros. rewrite Pmult_nat_mult. - apply le_trans with (1*n). now rewrite mult_1_l. - apply mult_le_compat_r. apply Pos2Nat.is_pos. + apply Nat.le_trans with (1*n). now rewrite Nat.mul_1_l. + apply Nat.mul_le_mono_r. apply Pos2Nat.is_pos. Qed. End ObsoletePmultNat. diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index a89b888ec..7d7dcc6d0 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -10,7 +10,7 @@ (** Contributed by Laurent Théry (INRIA); Adapted to Coq V8 by the Coq Development Team *) -Require Import Bool BinPos BinNat Nnat. +Require Import Bool BinPos BinNat PeanoNat Nnat. Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -115,7 +115,7 @@ Proof. unfold N.lt. change 256%N with (N.of_nat 256). rewrite <- Nat2N.inj_compare. - rewrite <- Compare_dec.nat_compare_lt. auto. + now apply Nat.compare_lt_iff. Qed. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index 1d0254397..e179bd8b4 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -15,11 +15,11 @@ Unset Strict Implicit. (** First, signatures with only the order relations *) Module Type HasLt (Import T:Typ). - Parameter Inline lt : t -> t -> Prop. + Parameter Inline(40) lt : t -> t -> Prop. End HasLt. Module Type HasLe (Import T:Typ). - Parameter Inline le : t -> t -> Prop. + Parameter Inline(40) le : t -> t -> Prop. End HasLe. Module Type EqLt := Typ <+ HasEq <+ HasLt. diff --git a/theories/Structures/OrdersEx.v b/theories/Structures/OrdersEx.v index e071d053c..acc7c7673 100644 --- a/theories/Structures/OrdersEx.v +++ b/theories/Structures/OrdersEx.v @@ -11,16 +11,16 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -Require Import Orders NPeano POrderedType NArith - ZArith RelationPairs EqualitiesFacts. +Require Import Orders PeanoNat POrderedType BinNat BinInt + RelationPairs EqualitiesFacts. (** * Examples of Ordered Type structures. *) (** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) -Module Nat_as_OT := NPeano.Nat. -Module Positive_as_OT := POrderedType.Positive_as_OT. +Module Nat_as_OT := PeanoNat.Nat. +Module Positive_as_OT := BinPos.Pos. Module N_as_OT := BinNat.N. Module Z_as_OT := BinInt.Z. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 452e3d148..673eed6bb 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -8,7 +8,7 @@ (************************************************************************) Require Export BinNums BinPos Pnat. -Require Import BinNat Bool Plus Mult Equalities GenericMinMax +Require Import BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties. Require BinIntDef. @@ -73,6 +73,23 @@ Proof. decide equality; apply Pos.eq_dec. Defined. +(** * 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 opp_wd : Proper (eq==>eq) opp := _. +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 quot_wd : Proper (eq==>eq==>eq) quot := _. +Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. +Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. +Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. + (** * Properties of [pos_sub] *) (** [pos_sub] can be written in term of positive comparison @@ -138,15 +155,23 @@ Qed. Module Import Private_BootStrap. -(** * Properties of addition *) - -(** ** Zero is neutral for addition *) +(** ** Operations and constants *) Lemma add_0_r n : n + 0 = n. Proof. now destruct n. Qed. +Lemma mul_0_r n : n * 0 = 0. +Proof. + now destruct n. +Qed. + +Lemma mul_1_l n : 1 * n = n. +Proof. + now destruct n. +Qed. + (** ** Addition is commutative *) Lemma add_comm n m : n + m = m + n. @@ -196,28 +221,25 @@ Proof. symmetry. now apply Pos.add_sub_assoc. Qed. -Lemma add_assoc n m p : n + (m + p) = n + m + p. +Local Arguments add !x !y. + +Lemma add_assoc_pos p n m : pos p + (n + m) = pos p + n + m. Proof. - assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z). - { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial. - - simpl. now rewrite Pos.add_assoc. - - simpl (_ + neg _). symmetry. apply pos_sub_add. - - simpl (neg _ + _); simpl (_ + neg _). - now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm. - - apply opp_inj. rewrite !opp_add_distr. simpl opp. - simpl (neg _ + _); simpl (_ + neg _). - rewrite add_comm, Pos.add_comm. apply pos_sub_add. } - destruct n. - - trivial. - - apply AUX. - - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX. + destruct n as [|n|n], m as [|m|m]; simpl; trivial. + - now rewrite Pos.add_assoc. + - symmetry. apply pos_sub_add. + - symmetry. apply add_0_r. + - now rewrite <- pos_sub_add, add_comm, <- pos_sub_add, Pos.add_comm. + - apply opp_inj. rewrite !opp_add_distr, !pos_sub_opp. + rewrite add_comm, Pos.add_comm. apply pos_sub_add. Qed. -(** ** Subtraction and successor *) - -Lemma sub_succ_l n m : succ n - m = succ (n - m). +Lemma add_assoc n m p : n + (m + p) = n + m + p. Proof. - unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1). + destruct n. + - trivial. + - apply add_assoc_pos. + - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos. Qed. (** ** Opposite is inverse for addition *) @@ -227,132 +249,34 @@ Proof. destruct n; simpl; trivial; now rewrite pos_sub_diag. Qed. -Lemma add_opp_diag_l n : - n + n = 0. -Proof. - rewrite add_comm. apply add_opp_diag_r. -Qed. - -(** ** Commutativity of multiplication *) - -Lemma mul_comm n m : n * m = m * n. -Proof. - destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm. -Qed. - -(** ** Associativity of multiplication *) - -Lemma mul_assoc n m p : n * (m * p) = n * m * p. -Proof. - destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc. -Qed. - -(** Multiplication and constants *) - -Lemma mul_1_l n : 1 * n = n. -Proof. - now destruct n. -Qed. - -Lemma mul_1_r n : n * 1 = n. -Proof. - destruct n; simpl; now rewrite ?Pos.mul_1_r. -Qed. - (** ** Multiplication and Opposite *) -Lemma mul_opp_l n m : - n * m = - (n * m). -Proof. - now destruct n, m. -Qed. - Lemma mul_opp_r n m : n * - m = - (n * m). Proof. now destruct n, m. Qed. -Lemma mul_opp_opp n m : - n * - m = n * m. -Proof. - now destruct n, m. -Qed. - -Lemma mul_opp_comm n m : - n * m = n * - m. -Proof. - now destruct n, m. -Qed. - (** ** Distributivity of multiplication over addition *) Lemma mul_add_distr_pos (p:positive) n m : - pos p * (n + m) = pos p * n + pos p * m. -Proof. - destruct n as [|n|n], m as [|m|m]; simpl; trivial; - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec; - intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l. -Qed. - -Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p. + (n + m) * pos p = n * pos p + m * pos p. Proof. - destruct n as [|n|n]. trivial. - apply mul_add_distr_pos. - change (neg n) with (- pos n). - rewrite !mul_opp_l, <- opp_add_distr. f_equal. - apply mul_add_distr_pos. + destruct n as [|n|n], m as [|m|m]; simpl; trivial. + - now rewrite Pos.mul_add_distr_r. + - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; + simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. + - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec; + simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r. + - now rewrite Pos.mul_add_distr_r. Qed. Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p. Proof. - rewrite !(mul_comm _ p). apply mul_add_distr_l. -Qed. - -(** ** Basic properties of divisibility *) - -Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. -Proof. - split. - intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. - intros (r,H). exists (pos r); simpl; now f_equal. -Qed. - -Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. -Qed. - -Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). -Proof. - split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. -Qed. - -(** ** Conversions between [Z.testbit] and [N.testbit] *) - -Lemma testbit_of_N a n : - testbit (of_N a) (of_N n) = N.testbit a n. -Proof. - destruct a as [|a], n; simpl; trivial. now destruct a. -Qed. - -Lemma testbit_of_N' a n : 0<=n -> - testbit (of_N a) n = N.testbit a (to_N n). -Proof. - intro Hn. rewrite <- testbit_of_N. f_equal. - destruct n; trivial; now destruct Hn. -Qed. - -Lemma testbit_Zpos a n : 0<=n -> - testbit (pos a) n = N.testbit (N.pos a) (to_N n). -Proof. - intro Hn. now rewrite <- testbit_of_N'. -Qed. - -Lemma testbit_Zneg a n : 0<=n -> - testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). -Proof. - intro Hn. - rewrite <- testbit_of_N' by trivial. - destruct n as [ |n|n]; - [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. - unfold testbit. - now destruct a as [|[ | | ]| ]. + destruct p as [|p|p]. + - now rewrite !mul_0_r. + - apply mul_add_distr_pos. + - apply opp_inj. rewrite opp_add_distr, <- !mul_opp_r. + apply mul_add_distr_pos. Qed. End Private_BootStrap. @@ -397,6 +321,8 @@ Qed. (** ** Specification of successor and predecessor *) +Local Arguments pos_sub : simpl nomatch. + Lemma succ_pred n : succ (pred n) = n. Proof. unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. @@ -511,6 +437,45 @@ Proof. rewrite (compare_antisym n m). case compare_spec; intuition. Qed. +(** ** Induction principles based on successor / predecessor *) + +Lemma peano_ind (P : Z -> Prop) : + P 0 -> + (forall x, P x -> P (succ x)) -> + (forall x, P x -> P (pred x)) -> + forall z, P z. +Proof. + intros H0 Hs Hp z; destruct z. + assumption. + induction p using Pos.peano_ind. + now apply (Hs 0). + rewrite <- Pos.add_1_r. + now apply (Hs (pos p)). + induction p using Pos.peano_ind. + now apply (Hp 0). + rewrite <- Pos.add_1_r. + now apply (Hp (neg p)). +Qed. + +Lemma bi_induction (P : Z -> Prop) : + Proper (eq ==> iff) P -> + P 0 -> + (forall x, P x <-> P (succ x)) -> + forall z, P z. +Proof. + intros _ H0 Hs. induction z using peano_ind. + assumption. + now apply -> Hs. + apply Hs. now rewrite succ_pred. +Qed. + +(** We can now derive all properties of basic functions and orders, + and use these properties for proving the specs of more advanced + functions. *) + +Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties. + + (** ** Specification of absolute value *) Lemma abs_eq n : 0 <= n -> abs n = n. @@ -693,7 +658,7 @@ Lemma div_eucl_eq a b : b<>0 -> Proof. destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial; (now destruct 1) || intros _; - generalize (pos_div_eucl_eq a (pos b) (eq_refl _)); + generalize (pos_div_eucl_eq a (pos b) Logic.eq_refl); destruct pos_div_eucl as (q,r); rewrite mul_comm. - (* pos pos *) trivial. @@ -756,7 +721,7 @@ Proof. destruct a as [|a|a]; unfold modulo, div_eucl. now split. now apply pos_div_eucl_bound. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. @@ -773,7 +738,7 @@ Proof. destruct b as [|b|b]; try easy; intros _. destruct a as [|a|a]; unfold modulo, div_eucl. now split. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). destruct r as [|r|r]; (now destruct Hr) || clear Hr. now split. @@ -783,7 +748,7 @@ Proof. change (neg b - neg r <= 0). unfold le, lt in *. rewrite <- compare_sub. simpl in *. now rewrite <- Pos.compare_antisym, Hr'. - generalize (pos_div_eucl_bound a (pos b) (eq_refl _)). + generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl). destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr'). split; destruct r; try easy. red; simpl; now rewrite <- Pos.compare_antisym. @@ -839,6 +804,25 @@ Proof. intros _. apply rem_opp_l'. Qed. Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b. Proof. intros _. apply rem_opp_r'. Qed. +(** ** Extra properties about [divide] *) + +Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive. +Proof. + split. + intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. + intros (r,H). exists (pos r); simpl; now f_equal. +Qed. + +Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. +Qed. + +Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n). +Proof. + split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r. +Qed. + (** ** Correctness proofs for gcd *) Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b. @@ -898,6 +882,38 @@ Proof. destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed. +(** ** Extra properties about [testbit] *) + +Lemma testbit_of_N a n : + testbit (of_N a) (of_N n) = N.testbit a n. +Proof. + destruct a as [|a], n; simpl; trivial. now destruct a. +Qed. + +Lemma testbit_of_N' a n : 0<=n -> + testbit (of_N a) n = N.testbit a (to_N n). +Proof. + intro Hn. rewrite <- testbit_of_N. f_equal. + destruct n; trivial; now destruct Hn. +Qed. + +Lemma testbit_Zpos a n : 0<=n -> + testbit (pos a) n = N.testbit (N.pos a) (to_N n). +Proof. + intro Hn. now rewrite <- testbit_of_N'. +Qed. + +Lemma testbit_Zneg a n : 0<=n -> + testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)). +Proof. + intro Hn. + rewrite <- testbit_of_N' by trivial. + destruct n as [ |n|n]; + [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn]. + unfold testbit. + now destruct a as [|[ | | ]| ]. +Qed. + (** ** Proofs of specifications for bitwise operations *) Lemma div2_spec a : div2 a = shiftr a 1. @@ -1103,59 +1119,10 @@ Proof. now rewrite N.lxor_spec, xorb_negb_negb. Qed. -(** ** Induction principles based on successor / predecessor *) -Lemma peano_ind (P : Z -> Prop) : - P 0 -> - (forall x, P x -> P (succ x)) -> - (forall x, P x -> P (pred x)) -> - forall z, P z. -Proof. - intros H0 Hs Hp z; destruct z. - assumption. - induction p using Pos.peano_ind. - now apply (Hs 0). - rewrite <- Pos.add_1_r. - now apply (Hs (pos p)). - induction p using Pos.peano_ind. - now apply (Hp 0). - rewrite <- Pos.add_1_r. - now apply (Hp (neg p)). -Qed. - -Lemma bi_induction (P : Z -> Prop) : - Proper (eq ==> iff) P -> - P 0 -> - (forall x, P x <-> P (succ x)) -> - forall z, P z. -Proof. - intros _ H0 Hs. induction z using peano_ind. - assumption. - now apply -> Hs. - apply Hs. now rewrite succ_pred. -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 opp_wd : Proper (eq==>eq) opp := _. -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 quot_wd : Proper (eq==>eq==>eq) quot := _. -Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _. -Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _. -Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _. +(** Generic properties of advanced functions. *) -Include ZProp - <+ UsualMinMaxLogicalProperties - <+ UsualMinMaxDecProperties. +Include ZExtraProp. (** In generic statements, the predicates [lt] and [le] have been favored, whereas [gt] and [ge] don't even exist in the abstract @@ -1394,11 +1361,11 @@ Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q). Proof. reflexivity. Qed. Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive. -Proof. apply Z.Private_BootStrap.divide_Zpos. Qed. +Proof. apply Z.divide_Zpos. Qed. Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n). -Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed. +Proof. apply Z.testbit_Zpos. Qed. (** Some results concerning Z.neg *) @@ -1436,14 +1403,14 @@ Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p. Proof. reflexivity. Qed. Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p). -Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed. +Proof. apply Z.divide_Zpos_Zneg_r. Qed. Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n). -Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed. +Proof. apply Z.divide_Zpos_Zneg_l. Qed. Lemma testbit_neg a n : 0<=n -> Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)). -Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed. +Proof. apply Z.testbit_Zneg. Qed. End Pos2Z. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 27fb21bc7..32993b2c0 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -683,7 +683,7 @@ Arguments Zdiv_eucl_extended : default implicits. (** * Division and modulo in Z agree with same in nat: *) -Require Import NPeano. +Require Import PeanoNat. Lemma div_Zdiv (n m: nat): m <> O -> Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m. diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index 27b7e6a0c..28003bc02 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -271,7 +271,7 @@ Qed. Lemma inj_testbit a n : Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n. -Proof. apply Z.Private_BootStrap.testbit_of_N. Qed. +Proof. apply Z.testbit_of_N. Qed. End N2Z. @@ -426,7 +426,7 @@ Qed. Lemma inj_testbit a n : 0<=n -> Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n). -Proof. apply Z.Private_BootStrap.testbit_of_N'. Qed. +Proof. apply Z.testbit_of_N'. Qed. End Z2N. @@ -637,7 +637,7 @@ Qed. (** [Z.of_nat] and usual operations *) -Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m. +Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat. Proof. now rewrite <-!nat_N_Z, N2Z.inj_compare, <- Nat2N.inj_compare. Qed. @@ -690,23 +690,23 @@ Proof. now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub. Qed. -Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)). +Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max. Qed. -Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n). +Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n). Proof. rewrite nat_compare_lt, Nat2N.inj_compare. intros. now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred. Qed. -Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m). +Lemma inj_min n m : Z.of_nat (Nat.min n m) = Z.min (Z.of_nat n) (Z.of_nat m). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min. Qed. -Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m). +Lemma inj_max n m : Z.of_nat (Nat.max n m) = Z.max (Z.of_nat n) (Z.of_nat m). Proof. now rewrite <- !nat_N_Z, Nat2N.inj_max, N2Z.inj_max. Qed. @@ -777,13 +777,13 @@ Proof. intros. now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub. Qed. -Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n). +Lemma inj_pred n : Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n). Proof. now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred. Qed. Lemma inj_compare n m : 0<=n -> 0<=m -> - nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m). + (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m). Proof. intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id. Qed. @@ -798,12 +798,12 @@ Proof. intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare. Qed. -Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m). +Lemma inj_min n m : Z.to_nat (Z.min n m) = Nat.min (Z.to_nat n) (Z.to_nat m). Proof. now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min. Qed. -Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m). +Lemma inj_max n m : Z.to_nat (Z.max n m) = Nat.max (Z.to_nat n) (Z.to_nat m). Proof. now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max. Qed. @@ -876,13 +876,13 @@ Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub. Qed. -Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n). +Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred. Qed. Lemma inj_compare n m : 0<=n -> 0<=m -> - nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m). + (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m). Proof. intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare. Qed. @@ -898,13 +898,13 @@ Proof. Qed. Lemma inj_min n m : 0<=n -> 0<=m -> - Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m). + Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min. Qed. Lemma inj_max n m : 0<=n -> 0<=m -> - Z.abs_nat (Z.max n m) = max (Z.abs_nat n) (Z.abs_nat m). + Z.abs_nat (Z.max n m) = Nat.max (Z.abs_nat n) (Z.abs_nat m). Proof. intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_max, N2Nat.inj_max. Qed. diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index 1da3c7992..485935502 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -25,7 +25,7 @@ Local Open Scope Z_scope. (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary integer (type [nat]) and [z] a signed integer (type [Z]) *) -Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z). +Definition Zpower_nat (z:Z)(n:nat) := Nat.iter n (Z.mul z) 1. Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1. Proof. reflexivity. Qed. @@ -255,7 +255,7 @@ Section power_div_with_rest. Proof. rewrite Pos2Nat.inj_iter, two_power_pos_nat. induction (Pos.to_nat p); simpl; trivial. - destruct (nat_rect _ _ _ n) as ((q,r),d). + destruct (Nat.iter _ _ _) as ((q,r),d). unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal. Qed. diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 2f778be36..5a262fb1c 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -135,6 +135,7 @@ let init_ocaml_path () = [ "grammar" ]; [ "ide" ] ] let get_compat_version = function + | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 | ("8.1" | "8.0") as s -> |