diff options
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 -> |