summaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r--theories/Numbers/NatInt/NZAdd.v2
-rw-r--r--theories/Numbers/NatInt/NZAddOrder.v2
-rw-r--r--theories/Numbers/NatInt/NZAxioms.v5
-rw-r--r--theories/Numbers/NatInt/NZBase.v7
-rw-r--r--theories/Numbers/NatInt/NZBits.v2
-rw-r--r--theories/Numbers/NatInt/NZDiv.v2
-rw-r--r--theories/Numbers/NatInt/NZDomain.v40
-rw-r--r--theories/Numbers/NatInt/NZGcd.v6
-rw-r--r--theories/Numbers/NatInt/NZLog.v2
-rw-r--r--theories/Numbers/NatInt/NZMul.v2
-rw-r--r--theories/Numbers/NatInt/NZMulOrder.v2
-rw-r--r--theories/Numbers/NatInt/NZOrder.v6
-rw-r--r--theories/Numbers/NatInt/NZParity.v4
-rw-r--r--theories/Numbers/NatInt/NZPow.v4
-rw-r--r--theories/Numbers/NatInt/NZProperties.v2
-rw-r--r--theories/Numbers/NatInt/NZSqrt.v6
16 files changed, 49 insertions, 45 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 2cef31ae..501583ae 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.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/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index c9bc8824..619a6634 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.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/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index e8f7def7..c88341fa 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.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 *)
@@ -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/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 56c999d4..c0afa098 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.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 *)
@@ -12,11 +12,6 @@ Require Import NZAxioms.
Module Type NZBaseProp (Import NZ : NZDomainSig').
-(** An artificial scope meant to be substituted later *)
-
-Delimit Scope abstract_scope with abstract.
-Bind Scope abstract_scope with t.
-
Include BackportEq NZ NZ. (** eq_refl, eq_sym, eq_trans *)
Lemma eq_sym_iff : forall x y, x==y <-> y==x.
diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v
index 31e99340..1c118597 100644
--- a/theories/Numbers/NatInt/NZBits.v
+++ b/theories/Numbers/NatInt/NZBits.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/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 339563c0..4a127216 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.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/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index c9001db2..ffb04f08 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.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 *)
@@ -14,14 +14,12 @@ Require Import NZBase NZOrder NZAddOrder Plus Minus.
translation from Peano numbers [nat] into NZ.
*)
-(** First, some complements about [nat_iter] *)
+Local Notation "f ^ n" := (fun x => nat_rect _ x (fun _ => f) n).
-Local Notation "f ^ n" := (nat_iter n f).
-
-Instance nat_iter_wd n {A} (R:relation A) :
- Proper ((R==>R)==>R==>R) (nat_iter n).
+Instance nat_rect_wd n {A} (R:relation A) :
+ Proper (R==>(R==>R)==>R) (fun x f => nat_rect (fun _ => _) x (fun _ => f) n).
Proof.
-intros f f' Hf. induction n; simpl; red; auto.
+intros x y eq_xy f g eq_fg; induction n; [assumption | now apply eq_fg].
Qed.
Module NZDomainProp (Import NZ:NZDomainSig').
@@ -33,17 +31,24 @@ Include NZBaseProp NZ.
Lemma itersucc_or_itersucc n m : exists k, n == (S^k) m \/ m == (S^k) n.
Proof.
-nzinduct n m.
+revert n.
+apply central_induction with (z:=m).
+ { intros x y eq_xy; apply ex_iff_morphism.
+ intros n; apply or_iff_morphism.
+ + split; intros; etransitivity; try eassumption; now symmetry.
+ + split; intros; (etransitivity; [eassumption|]); [|symmetry];
+ (eapply nat_rect_wd; [eassumption|apply succ_wd]).
+ }
exists 0%nat. now left.
intros n. split; intros [k [L|R]].
exists (Datatypes.S k). left. now apply succ_wd.
destruct k as [|k].
simpl in R. exists 1%nat. left. now apply succ_wd.
-rewrite nat_iter_succ_r in R. exists k. now right.
+rewrite nat_rect_succ_r in R. exists k. now right.
destruct k as [|k]; simpl in L.
exists 1%nat. now right.
apply succ_inj in L. exists k. now left.
-exists (Datatypes.S k). right. now rewrite nat_iter_succ_r.
+exists (Datatypes.S k). right. now rewrite nat_rect_succ_r.
Qed.
(** Generalized version of [pred_succ] when iterating *)
@@ -53,7 +58,7 @@ Proof.
induction k.
simpl; auto with *.
simpl; intros. apply pred_wd in H. rewrite pred_succ in H. apply IHk in H; auto.
-rewrite <- nat_iter_succ_r in H; auto.
+rewrite <- nat_rect_succ_r in H; auto.
Qed.
(** From a given point, all others are iterated successors
@@ -319,7 +324,7 @@ Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
Proof.
intros. rewrite ofnat_add_l.
induction n; simpl. reflexivity.
- rewrite ofnat_succ. now f_equiv.
+ now f_equiv.
Qed.
Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -327,15 +332,15 @@ Proof.
induction n; simpl; intros.
symmetry. apply mul_0_l.
rewrite plus_comm.
- rewrite ofnat_succ, ofnat_add, mul_succ_l.
+ rewrite ofnat_add, mul_succ_l.
now f_equiv.
Qed.
Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
Proof.
induction m; simpl; intros.
- rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now f_equiv.
+ apply sub_0_r.
+ rewrite sub_succ_r. now f_equiv.
Qed.
Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
@@ -346,9 +351,10 @@ Proof.
intros.
destruct n.
inversion H.
- rewrite nat_iter_succ_r.
+ rewrite nat_rect_succ_r.
simpl.
- rewrite ofnat_succ, pred_succ; auto with arith.
+ etransitivity. apply IHm. auto with arith.
+ eapply nat_rect_wd; [symmetry;apply pred_succ|apply pred_wd].
Qed.
End NZOfNatOps.
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 0fd543c0..42bee315 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.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 *)
@@ -107,8 +107,8 @@ Proof.
now rewrite Hr, Hq, mul_assoc.
Qed.
-Instance divide_reflexive : Reflexive divide := divide_refl.
-Instance divide_transitive : Transitive divide := divide_trans.
+Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
+Instance divide_transitive : Transitive divide | 5 := divide_trans.
(** Due to sign, no general antisymmetry result *)
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 72f5e516..9cd1f877 100644
--- a/theories/Numbers/NatInt/NZLog.v
+++ b/theories/Numbers/NatInt/NZLog.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/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index a3419383..89ace4de 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.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/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index ef5250fa..e79e50a9 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.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/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 0f7be085..c1e83529 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.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 *)
@@ -644,6 +644,8 @@ End NZOrderProp.
(** If we have moreover a [compare] function, we can build
an [OrderedType] structure. *)
+(* Temporary workaround for bug #2949: remove this problematic + unused functor
Module NZOrderedType (NZ : NZDecOrdSig')
<: DecidableTypeFull <: OrderedTypeFull
- := NZ <+ NZBaseProp <+ NZOrderProp NZ <+ Compare2EqBool <+ HasEqBool2Dec.
+ := NZ <+ NZBaseProp <+ NZOrderProp <+ Compare2EqBool <+ HasEqBool2Dec.
+*)
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 074fbfdd..6b9a680a 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.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 *)
@@ -95,7 +95,7 @@ Proof.
intros.
generalize (Even_or_Odd n) (Even_Odd_False n).
rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
+ destruct (odd n), (even n) ; simpl; intuition.
Qed.
Lemma negb_even : forall n, negb (even n) = odd n.
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index d2d34190..38452119 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.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 *)
@@ -30,7 +30,7 @@ Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
End NZPowSpec.
(** The above [pow_neg_r] specification is useless (and trivially
- provable) for N. Having it here allows to already derive
+ provable) for N. Having it here already allows deriving
some slightly more general statements. *)
Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
diff --git a/theories/Numbers/NatInt/NZProperties.v b/theories/Numbers/NatInt/NZProperties.v
index f44f23e9..0f3a5caf 100644
--- a/theories/Numbers/NatInt/NZProperties.v
+++ b/theories/Numbers/NatInt/NZProperties.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/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 304a84a8..894c0806 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.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 *)
@@ -66,7 +66,7 @@ Qed.
Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b.
Proof.
intros a b (LEb,LTb).
- assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg).
+ assert (Ha : 0<=a) by (transitivity (b²); trivial using square_nonneg).
assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order).
assert (Ha': 0<=√a) by now apply sqrt_nonneg.
destruct (sqrt_spec a Ha) as (LEa,LTa).
@@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up.
Proof.
assert (Proper (eq==>eq==>Logic.eq) compare).
intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order.
- intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx.
+ intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx.
Qed.
(** The spec of [sqrt_up] indeed determines it *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 21:01:24 +0000