diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/BinNat.v | 233 | ||||
| -rw-r--r-- | theories/NArith/BinNatDef.v | 10 | ||||
| -rw-r--r-- | theories/NArith/NArith.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 12 | ||||
| -rw-r--r-- | theories/NArith/Ndigits.v | 113 | ||||
| -rw-r--r-- | theories/NArith/Ndist.v | 59 | ||||
| -rw-r--r-- | theories/NArith/Ndiv_def.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Ngcd_def.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 63 | ||||
| -rw-r--r-- | theories/NArith/Nsqrt_def.v | 2 |
10 files changed, 221 insertions, 277 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index 1023924e..641ec02f 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,71 +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). +(** Instantiation of generic properties of advanced functions + (pow, sqrt, log2, div, gcd, ...) *) -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 *) - -(** The Bind Scope prevents N to stay associated with abstract_scope. - (TODO FIX) *) - -Include NProp. Bind Scope N_scope with N. -Include 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 @@ -946,7 +887,7 @@ Proof. destruct n as [|n]; simpl in *. destruct m. now destruct p. elim (Pos.nlt_1_r _ H). rewrite Pos.iter_succ. simpl. - set (u:=Pos.iter n xO p) in *; clearbody u. + set (u:=Pos.iter xO p n) in *; clearbody u. destruct m as [|m]. now destruct u. rewrite <- (IHn (Pos.pred_N m)). rewrite <- (testbit_odd_succ _ (Pos.pred_N m)). @@ -970,7 +911,7 @@ Proof. rewrite <- IHn. rewrite testbit_succ_r_div2 by apply le_0_l. f_equal. simpl. rewrite Pos.iter_succ. - now destruct (Pos.iter n xO p). + now destruct (Pos.iter xO p n). apply succ_le_mono. now rewrite succ_pos_pred. Qed. @@ -983,6 +924,8 @@ Qed. End N. +Bind Scope N_scope with N.t N. + (** Exportation of notations *) Infix "+" := N.add : N_scope. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index 9abf4955..9de2e7e1 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -325,8 +325,8 @@ Definition lxor n m := (** Shifts *) -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_nat (a:N) := nat_rect _ a (fun _ => double). +Definition shiftr_nat (a:N) := nat_rect _ a (fun _ => div2). Definition shiftl a n := match a with @@ -337,7 +337,7 @@ Definition shiftl a n := Definition shiftr a n := match n with | 0 => a - | pos p => Pos.iter p div2 a + | pos p => Pos.iter div2 a p end. (** Checking whether a particular bit is set or not *) @@ -375,7 +375,7 @@ Definition of_nat (n:nat) := Definition iter (n:N) {A} (f:A->A) (x:A) : A := match n with | 0 => x - | pos p => Pos.iter p f x + | pos p => Pos.iter f x p end. End N.
\ No newline at end of file diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index ff0be4a3..43614543 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index e38ce5ba..5b1815bd 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -119,11 +119,11 @@ Lemma Nneq_elim a a' : N.odd a = negb (N.odd a') \/ N.eqb (N.div2 a) (N.div2 a') = false. Proof. - intros. cut (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')). - intros. elim H0. intro. right. apply Ndiv2_bit_neq. assumption. - assumption. - intro. left. assumption. - case (N.odd a), (N.odd a'); auto. + intros. + enough (N.odd a = N.odd a' \/ N.odd a = negb (N.odd a')) as []. + - right. apply Ndiv2_bit_neq; assumption. + - left. assumption. + - case (N.odd a), (N.odd a'); auto. Qed. Lemma Ndouble_or_double_plus_un a : diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 764ecc12..55ef451e 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * 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. @@ -86,7 +85,7 @@ Lemma Nshiftl_nat_equiv : forall a n, N.shiftl_nat a (N.to_nat n) = N.shiftl a n. Proof. intros [|a] [|n]; simpl; unfold N.shiftl_nat; trivial. - apply nat_iter_invariant; intros; now subst. + induction (Pos.to_nat n) as [|? H]; simpl; now try rewrite H. rewrite <- Pos2Nat.inj_iter. symmetry. now apply Pos.iter_swap_gen. Qed. @@ -103,7 +102,7 @@ Lemma Nshiftr_nat_spec : forall a n m, Proof. induction n; intros m. now rewrite <- plus_n_O. - simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S. + simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn. destruct (N.shiftr_nat a n) as [|[p|p|]]; simpl; trivial. Qed. @@ -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, Nshiftl_nat_S; 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) *) @@ -148,7 +150,7 @@ Lemma Pshiftl_nat_plus : forall n m p, Pos.shiftl_nat p (m + n) = Pos.shiftl_nat (Pos.shiftl_nat p n) m. Proof. induction m; simpl; intros. reflexivity. - rewrite 2 Pshiftl_nat_S. now f_equal. + now f_equal. Qed. (** Semantics of bitwise operations with respect to [N.testbit_nat] *) @@ -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 *) @@ -512,9 +517,9 @@ Definition N2Bv (n:N) : Bvector (N.size_nat n) := Fixpoint Bv2N (n:nat)(bv:Bvector n) : N := match bv with - | Vector.nil => N0 - | Vector.cons false n bv => N.double (Bv2N n bv) - | Vector.cons true n bv => N.succ_double (Bv2N n bv) + | Vector.nil _ => N0 + | Vector.cons _ false n bv => N.double (Bv2N n bv) + | Vector.cons _ true n bv => N.succ_double (Bv2N n bv) end. Lemma Bv2N_N2Bv : forall n, Bv2N _ (N2Bv n) = n. @@ -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/Ndist.v b/theories/NArith/Ndist.v index 0bff1a96..5467f9cb 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -71,7 +71,7 @@ Proof. auto with bool arith. intros. generalize H0 H1. case n. intros. simpl in H3. discriminate H3. intros. simpl. unfold Nplength in H. - cut (ni (Pplength p0) = ni n0). intro. inversion H4. reflexivity. + enough (ni (Pplength p0) = ni n0) by (inversion H4; reflexivity). apply H. intros. change (N.testbit_nat (Npos (xO p0)) (S k) = false). apply H2. apply lt_n_S. exact H4. exact H3. intro. case n. trivial. @@ -104,10 +104,9 @@ Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d. Proof. simple induction d. simple induction d'; trivial. simple induction d'; trivial. elim n. simple induction n0; trivial. - intros. elim n1; trivial. intros. unfold ni_min in H. cut (min n0 n2 = min n2 n0). - intro. unfold ni_min. simpl. rewrite H1. reflexivity. - cut (ni (min n0 n2) = ni (min n2 n0)). intros. - inversion H1; trivial. + intros. elim n1; trivial. intros. unfold ni_min in H. + enough (min n0 n2 = min n2 n0) by (unfold ni_min; simpl; rewrite H1; reflexivity). + enough (ni (min n0 n2) = ni (min n2 n0)) by (inversion H1; trivial). exact (H n2). Qed. @@ -116,10 +115,10 @@ Lemma ni_min_assoc : Proof. simple induction d; trivial. simple induction d'; trivial. simple induction d''; trivial. - unfold ni_min. intro. cut (min (min n n0) n1 = min n (min n0 n1)). - intro. rewrite H. reflexivity. - generalize n0 n1. elim n; trivial. - simple induction n3; trivial. simple induction n5; trivial. + unfold ni_min. intro. + enough (min (min n n0) n1 = min n (min n0 n1)) by (rewrite H; reflexivity). + induction n in n0, n1 |- *; trivial. + destruct n0; trivial. destruct n1; trivial. intros. simpl. auto. Qed. @@ -174,15 +173,13 @@ Qed. Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'. Proof. - simple induction d. intro. right. exact (ni_min_inf_l d'). - simple induction d'. left. exact (ni_min_inf_r (ni n)). - unfold ni_min. cut (forall n0:nat, min n n0 = n \/ min n n0 = n0). - intros. case (H n0). intro. left. rewrite H0. reflexivity. - intro. right. rewrite H0. reflexivity. - elim n. intro. left. reflexivity. - simple induction n1. right. reflexivity. - intros. case (H n2). intro. left. simpl. rewrite H1. reflexivity. - intro. right. simpl. rewrite H1. reflexivity. + destruct d. right. exact (ni_min_inf_l d'). + destruct d'. left. exact (ni_min_inf_r (ni n)). + unfold ni_min. + enough (min n n0 = n \/ min n n0 = n0) as [-> | ->]. + left. reflexivity. + right. reflexivity. + destruct (Nat.min_dec n n0); [left|right]; assumption. Qed. Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d. @@ -208,11 +205,7 @@ Qed. Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n). Proof. - cut (forall m n:nat, m <= n -> min m n = m). - intros. unfold ni_le, ni_min. rewrite (H m n H0). reflexivity. - simple induction m. trivial. - simple induction n0. intro. inversion H0. - intros. simpl. rewrite (H n1 (le_S_n n n1 H1)). reflexivity. + intros * H. unfold ni_le, ni_min. rewrite (Peano.min_l m n H). reflexivity. Qed. Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n. @@ -298,30 +291,28 @@ Proof. rewrite (ni_min_inf_l (Nplength a')) in H. rewrite (Nplength_infty a' H). simpl. apply ni_le_refl. intros. unfold Nplength at 1. apply Nplength_lb. intros. - cut (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). - intros. apply H1. reflexivity. + enough (forall a'':N, N.lxor (Npos p) a' = a'' -> N.testbit_nat a'' k = false). + { apply H1. reflexivity. } intro a''. case a''. intro. reflexivity. intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). rewrite (Nplength_zeros (Npos p) (Pplength p) (eq_refl (Nplength (Npos p))) k H0). - generalize H. case a'. trivial. - intros. cut (N.testbit_nat (Npos p1) k = false). intros. rewrite H3. reflexivity. + destruct a'. trivial. + enough (N.testbit_nat (Npos p1) k = false) as -> by reflexivity. apply Nplength_zeros with (n := Pplength p1). reflexivity. apply (lt_le_trans k (Pplength p) (Pplength p1)). exact H0. - apply ni_le_le. exact H2. + apply ni_le_le. exact H. Qed. Lemma Nplength_ultra : forall a a':N, ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')). Proof. - intros. case (ni_le_total (Nplength a) (Nplength a')). intro. - cut (ni_min (Nplength a) (Nplength a') = Nplength a). - intro. rewrite H0. apply Nplength_ultra_1. exact H. + intros. destruct (ni_le_total (Nplength a) (Nplength a')). + enough (ni_min (Nplength a) (Nplength a') = Nplength a) as -> by (apply Nplength_ultra_1; exact H). exact H. - intro. cut (ni_min (Nplength a) (Nplength a') = Nplength a'). - intro. rewrite H0. rewrite N.lxor_comm. apply Nplength_ultra_1. exact H. + enough (ni_min (Nplength a) (Nplength a') = Nplength a') as -> by (rewrite N.lxor_comm; apply Nplength_ultra_1; exact H). rewrite ni_min_comm. exact H. Qed. diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index d21361cd..5ae388e3 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index 9faddddb..1750ffeb 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 64c9a48e..0dcaa71d 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -1,13 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import Arith_base 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. + - unfold N.div2, N.to_nat. now rewrite Pos2Nat.inj_xI, Nat.div2_succ_double. + - unfold N.div2, 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_iter (N.to_nat a) f x. + 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_iter n f x = 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/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index d43c752d..da7829a9 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |