summaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
Diffstat (limited to 'theories')
-rw-r--r--theories/Lists/ListTactics.v10
-rw-r--r--theories/Logic/ClassicalDescription.v42
-rw-r--r--theories/Logic/ConstructiveEpsilon.v155
-rw-r--r--theories/Logic/EqdepFacts.v47
-rw-r--r--theories/Logic/Eqdep_dec.v21
-rw-r--r--theories/NArith/Nnat.v6
-rw-r--r--theories/QArith/Qring.v22
-rw-r--r--theories/Reals/AltSeries.v8
-rw-r--r--theories/Reals/ArithProp.v4
-rw-r--r--theories/Reals/Cos_plus.v6
-rw-r--r--theories/Reals/Cos_rel.v23
-rw-r--r--theories/Reals/Exp_prop.v22
-rw-r--r--theories/Reals/PartSum.v4
-rw-r--r--theories/Reals/RIneq.v14
-rw-r--r--theories/Reals/Rdefinitions.v4
-rw-r--r--theories/Reals/Rfunctions.v13
-rw-r--r--theories/Reals/Rpow_def.v7
-rw-r--r--theories/Reals/Rsigma.v6
-rw-r--r--theories/Reals/Rsqrt_def.v6
-rw-r--r--theories/Reals/Rtrigo.v16
-rw-r--r--theories/Reals/Rtrigo_alt.v6
-rw-r--r--theories/Reals/Rtrigo_reg.v6
-rw-r--r--theories/Reals/SeqProp.v10
-rw-r--r--theories/Relations/Operators_Properties.v8
-rw-r--r--theories/Relations/Relation_Operators.v14
-rw-r--r--theories/Relations/Relations.v6
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v14
-rw-r--r--theories/Wellfounded/Transitive_Closure.v6
-rw-r--r--theories/Wellfounded/Well_Ordering.v16
-rw-r--r--theories/ZArith/Zpow_def.v27
-rw-r--r--theories/ZArith/Zpower.v17
-rw-r--r--theories/ZArith/Zsqrt.v4
33 files changed, 370 insertions, 202 deletions
diff --git a/theories/Lists/ListTactics.v b/theories/Lists/ListTactics.v
index a3b4e647..e46f1279 100644
--- a/theories/Lists/ListTactics.v
+++ b/theories/Lists/ListTactics.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ListTactics.v 9290 2006-10-26 19:20:42Z herbelin $ i*)
+(*i $Id: ListTactics.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import BinPos.
Require Import List.
@@ -17,6 +17,14 @@ Ltac list_fold_right fcons fnil l :=
| nil => fnil
end.
+Ltac lazy_list_fold_right fcons fnil l :=
+ match l with
+ | (cons ?x ?tl) =>
+ let cont := lazy_list_fold_right fcons fnil in
+ fcons x cont tl
+ | nil => fnil
+ end.
+
Ltac list_fold_left fcons fnil l :=
match l with
| (cons ?x ?tl) => list_fold_left fcons ltac:(fcons x fnil) tl
diff --git a/theories/Logic/ClassicalDescription.v b/theories/Logic/ClassicalDescription.v
index 7053266a..1f1c34bf 100644
--- a/theories/Logic/ClassicalDescription.v
+++ b/theories/Logic/ClassicalDescription.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: ClassicalDescription.v 8892 2006-06-04 17:59:53Z herbelin $ i*)
+(*i $Id: ClassicalDescription.v 9514 2007-01-22 14:58:50Z herbelin $ i*)
(** This file provides classical logic and definite description *)
@@ -57,14 +57,11 @@ Definition iota_spec (A : Type) (i:inhabited A) (P : A->Prop) :
(exists! x:A, P x) -> P (iota i P)
:= proj2_sig (classical_definite_description P i).
-(** Weaker lemmas (compatibility lemmas) *)
-
-Unset Implicit Arguments.
-
-Lemma dependent_description :
- forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
- (forall x:A, exists! y : B x, R x y) ->
- (exists f : (forall x:A, B x), forall x:A, R x (f x)).
+(** Axiom of unique "choice" (functional reification of functional relations) *)
+Theorem dependent_unique_choice :
+ forall (A:Type) (B:A -> Type) (R:forall x:A, B x -> Prop),
+ (forall x:A, exists! y : B x, R x y) ->
+ (exists f : (forall x:A, B x), forall x:A, R x (f x)).
Proof.
intros A B R H.
assert (Hexuni:forall x, exists! y, R x y).
@@ -74,27 +71,18 @@ intro x.
apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))).
Qed.
-Theorem description :
- forall (A B:Type) (R:A -> B -> Prop),
- (forall x : A, exists! y : B, R x y) ->
- (exists f : A->B, forall x:A, R x (f x)).
+Theorem unique_choice :
+ forall (A B:Type) (R:A -> B -> Prop),
+ (forall x:A, exists! y : B, R x y) ->
+ (exists f : A -> B, forall x:A, R x (f x)).
Proof.
intros A B.
-apply (dependent_description A (fun _ => B)).
+apply dependent_unique_choice with (B:=fun _:A => B).
Qed.
-(** Axiom of unique "choice" (functional reification of functional relations) *)
+(** Compatibility lemmas *)
-Set Implicit Arguments.
-
-Require Import Setoid.
+Unset Implicit Arguments.
-Theorem unique_choice :
- forall (A B:Type) (R:A -> B -> Prop),
- (forall x:A, exists! y : B, R x y) ->
- (exists f : A -> B, forall x:A, R x (f x)).
-Proof.
-intros A B R H.
-apply (description A B).
-intro x. apply H.
-Qed.
+Definition dependent_description := dependent_unique_choice.
+Definition description := unique_choice.
diff --git a/theories/Logic/ConstructiveEpsilon.v b/theories/Logic/ConstructiveEpsilon.v
new file mode 100644
index 00000000..61e377ea
--- /dev/null
+++ b/theories/Logic/ConstructiveEpsilon.v
@@ -0,0 +1,155 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id:$ i*)
+
+(** This module proves the constructive description schema, which
+infers the sigma-existence (i.e., [Set]-existence) of a witness to a
+predicate from the regular existence (i.e., [Prop]-existence). One
+requires that the underlying set is countable and that the predicate
+is decidable. *)
+
+(** Coq does not allow case analysis on sort [Set] when the goal is in
+[Prop]. Therefore, one cannot eliminate [exists n, P n] in order to
+show [{n : nat | P n}]. However, one can perform a recursion on an
+inductive predicate in sort [Prop] so that the returning type of the
+recursion is in [Set]. This trick is described in Coq'Art book, Sect.
+14.2.3 and 15.4. In particular, this trick is used in the proof of
+[Acc_iter] in the module Coq.Init.Wf. There, recursion is done on an
+inductive predicate [Acc] and the resulting type is in [Type].
+
+The predicate [Acc] delineates elements that are accessible via a
+given relation [R]. An element is accessible if there are no infinite
+[R]-descending chains starting from it.
+
+To use [Acc_iter], we define a relation R and prove that if [exists n,
+P n] then 0 is accessible with respect to R. Then, by induction on the
+definition of [Acc R 0], we show [{n : nat | P n}]. *)
+
+(** Contributed by Yevgeniy Makarov *)
+
+Require Import Arith.
+
+Section ConstructiveIndefiniteDescription.
+
+Variable P : nat -> Prop.
+
+Hypothesis P_decidable : forall x : nat, {P x} + {~ P x}.
+
+(** To find a witness of [P] constructively, we define an algorithm
+that tries P on all natural numbers starting from 0 and going up. The
+relation [R] describes the connection between the two successive
+numbers we try. Namely, [y] is [R]-less then [x] if we try [y] after
+[x], i.e., [y = S x] and [P x] is false. Then the absence of an
+infinite [R]-descending chain from 0 is equivalent to the termination
+of our searching algorithm. *)
+
+Let R (x y : nat) := (x = S y /\ ~ P y).
+Notation Local "'acc' x" := (Acc R x) (at level 10).
+
+Lemma P_implies_acc : forall x : nat, P x -> acc x.
+Proof.
+intros x H. constructor.
+intros y [_ not_Px]. absurd (P x); assumption.
+Qed.
+
+Lemma P_eventually_implies_acc : forall (x : nat) (n : nat), P (n + x) -> acc x.
+Proof.
+intros x n; generalize x; clear x; induction n as [|n IH]; simpl.
+apply P_implies_acc.
+intros x H. constructor. intros y [fxy _].
+apply IH. rewrite fxy.
+replace (n + S x) with (S (n + x)); auto with arith.
+Defined.
+
+Corollary P_eventually_implies_acc_ex : (exists n : nat, P n) -> acc 0.
+Proof.
+intros H; elim H. intros x Px. apply P_eventually_implies_acc with (n := x).
+replace (x + 0) with x; auto with arith.
+Defined.
+
+(** In the following statement, we use the trick with recursion on
+[Acc]. This is also where decidability of [P] is used. *)
+
+Theorem acc_implies_P_eventually : acc 0 -> {n : nat | P n}.
+Proof.
+intros Acc_0. pattern 0. apply Acc_iter with (R := R); [| assumption].
+clear Acc_0; intros x IH.
+destruct (P_decidable x) as [Px | not_Px].
+exists x; simpl; assumption.
+set (y := S x).
+assert (Ryx : R y x). unfold R; split; auto.
+destruct (IH y Ryx) as [n Hn].
+exists n; assumption.
+Defined.
+
+Theorem constructive_indefinite_description_nat : (exists n : nat, P n) -> {n : nat | P n}.
+Proof.
+intros H; apply acc_implies_P_eventually.
+apply P_eventually_implies_acc_ex; assumption.
+Defined.
+
+End ConstructiveIndefiniteDescription.
+
+Section ConstructiveEpsilon.
+
+(** For the current purpose, we say that a set [A] is countable if
+there are functions [f : A -> nat] and [g : nat -> A] such that [g] is
+a left inverse of [f]. *)
+
+Variable A : Type.
+Variable f : A -> nat.
+Variable g : nat -> A.
+
+Hypothesis gof_eq_id : forall x : A, g (f x) = x.
+
+Variable P : A -> Prop.
+
+Hypothesis P_decidable : forall x : A, {P x} + {~ P x}.
+
+Definition P' (x : nat) : Prop := P (g x).
+
+Lemma P'_decidable : forall n : nat, {P' n} + {~ P' n}.
+Proof.
+intro n; unfold P'; destruct (P_decidable (g n)); auto.
+Defined.
+
+Lemma constructive_indefinite_description : (exists x : A, P x) -> {x : A | P x}.
+Proof.
+intro H. assert (H1 : exists n : nat, P' n).
+destruct H as [x Hx]. exists (f x); unfold P'. rewrite gof_eq_id; assumption.
+apply (constructive_indefinite_description_nat P' P'_decidable) in H1.
+destruct H1 as [n Hn]. exists (g n); unfold P' in Hn; assumption.
+Defined.
+
+Lemma constructive_definite_description : (exists! x : A, P x) -> {x : A | P x}.
+Proof.
+ intros; apply constructive_indefinite_description; firstorder.
+Defined.
+
+Definition epsilon (E : exists x : A, P x) : A
+ := proj1_sig (constructive_indefinite_description E).
+
+Definition epsilon_spec (E : (exists x, P x)) : P (epsilon E)
+ := proj2_sig (constructive_indefinite_description E).
+
+End ConstructiveEpsilon.
+
+Theorem choice :
+ forall (A B : Type) (f : B -> nat) (g : nat -> B),
+ (forall x : B, g (f x) = x) ->
+ forall (R : A -> B -> Prop),
+ (forall (x : A) (y : B), {R x y} + {~ R x y}) ->
+ (forall x : A, exists y : B, R x y) ->
+ (exists f : A -> B, forall x : A, R x (f x)).
+Proof.
+intros A B f g gof_eq_id R R_dec H.
+exists (fun x : A => epsilon B f g gof_eq_id (R x) (R_dec x) (H x)).
+intro x.
+apply (epsilon_spec B f g gof_eq_id (R x) (R_dec x) (H x)).
+Qed.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index a257ef55..94a577ca 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: EqdepFacts.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: EqdepFacts.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(** This file defines dependent equality and shows its equivalence with
equality on dependent pairs (inhabiting sigma-types). It derives
@@ -105,8 +105,8 @@ Implicit Arguments eq_dep1 [U P].
(** Dependent equality is equivalent to equality on dependent pairs *)
Lemma eq_sigS_eq_dep :
- forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
- existS P p x = existS P q y -> eq_dep p x q y.
+ forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
+ existT P p x = existT P q y -> eq_dep p x q y.
Proof.
intros.
dependent rewrite H.
@@ -114,7 +114,7 @@ Proof.
Qed.
Lemma equiv_eqex_eqdep :
- forall (U:Set) (P:U -> Set) (p q:U) (x:P p) (y:P q),
+ forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
existS P p x = existS P q y <-> eq_dep p x q y.
Proof.
split.
@@ -248,28 +248,13 @@ End Equivalences.
Section Corollaries.
Variable U:Type.
- Variable V:Set.
(** UIP implies the injectivity of equality on dependent pairs in Type *)
-
- Definition Inj_dep_pairT :=
- forall (P:U -> Type) (p:U) (x y:P p),
- existT P p x = existT P p y -> x = y.
-
- Lemma eq_dep_eq__inj_pairT2 : Eq_dep_eq U -> Inj_dep_pairT.
- Proof.
- intro eq_dep_eq; red; intros.
- apply eq_dep_eq.
- apply eq_sigT_eq_dep.
- assumption.
- Qed.
-
- (** UIP implies the injectivity of equality on dependent pairs in Set *)
- Definition Inj_dep_pairS :=
- forall (P:V -> Set) (p:V) (x y:P p), existS P p x = existS P p y -> x = y.
+ Definition Inj_dep_pair :=
+ forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.
- Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq V -> Inj_dep_pairS.
+ Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.
Proof.
intro eq_dep_eq; red; intros.
apply eq_dep_eq.
@@ -279,6 +264,11 @@ Section Corollaries.
End Corollaries.
+Notation Inj_dep_pairS := Inj_dep_pair.
+Notation Inj_dep_pairT := Inj_dep_pair.
+Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.
+
+
(************************************************************************)
(** *** C. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq *)
@@ -303,7 +293,7 @@ Lemma eq_rect_eq :
Proof M.eq_rect_eq U.
Lemma eq_rec_eq :
- forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h.
+ forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.
Proof (fun p Q => M.eq_rect_eq U p Q).
(** Injectivity of Dependent Equality *)
@@ -333,18 +323,13 @@ End Axioms.
(** UIP implies the injectivity of equality on dependent pairs in Type *)
-Lemma inj_pairT2 :
+Lemma inj_pair2 :
forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
existT P p x = existT P p y -> x = y.
-Proof (fun U => eq_dep_eq__inj_pairT2 U (eq_dep_eq U)).
-
-(** UIP implies the injectivity of equality on dependent pairs in Set *)
-
-Lemma inj_pair2 :
- forall (U:Set) (P:U -> Set) (p:U) (x y:P p),
- existS P p x = existS P p y -> x = y.
Proof (fun U => eq_dep_eq__inj_pair2 U (eq_dep_eq U)).
+Notation inj_pairT2 := inj_pair2.
+
End EqdepTheory.
Implicit Arguments eq_dep [].
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 740fcfcf..103efd22 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Eqdep_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Eqdep_dec.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(** We prove that there is only one proof of [x=x], i.e [refl_equal x].
This holds if the equality upon the set of [x] is decidable.
@@ -235,7 +235,7 @@ End DecidableEqDep.
Module Type DecidableSet.
- Parameter U:Set.
+ Parameter U:Type.
Axiom eq_dec : forall x y:U, {x = y} + {x <> y}.
End DecidableSet.
@@ -276,14 +276,6 @@ Module DecidableEqDepSet (M:DecidableSet).
forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
Proof N.Streicher_K.
- (** Injectivity of equality on dependent pairs with second component
- in [Type] *)
-
- Lemma inj_pairT2 :
- forall (P:U -> Type) (p:U) (x y:P p),
- existT P p x = existT P p y -> x = y.
- Proof N.inj_pairT2.
-
(** Proof-irrelevance on subsets of decidable sets *)
Lemma inj_pairP2 :
@@ -291,11 +283,16 @@ Module DecidableEqDepSet (M:DecidableSet).
ex_intro P x p = ex_intro P x q -> p = q.
Proof N.inj_pairP2.
- (** Injectivity of equality on dependent pairs in [Set] *)
+ (** Injectivity of equality on dependent pairs in [Type] *)
Lemma inj_pair2 :
- forall (P:U -> Set) (p:U) (x y:P p),
+ forall (P:U -> Type) (p:U) (x y:P p),
existS P p x = existS P p y -> x = y.
Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq.
+ (** Injectivity of equality on dependent pairs with second component
+ in [Type] *)
+
+ Notation inj_pairT2 := inj_pair2.
+
End DecidableEqDepSet.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 6ba6ca3d..94f50bd0 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Nnat.v 8733 2006-04-25 22:52:18Z letouzey $ i*)
+(*i $Id: Nnat.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
-Require Import Arith.
+Require Import Arith_base.
Require Import Compare_dec.
Require Import Sumbool.
Require Import Div2.
@@ -174,4 +174,4 @@ Proof.
pattern n at 1; rewrite <- (nat_of_N_of_nat n).
pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
symmetry; apply nat_of_Ncompare.
-Qed. \ No newline at end of file
+Qed.
diff --git a/theories/QArith/Qring.v b/theories/QArith/Qring.v
index 9d294805..f9aa3e50 100644
--- a/theories/QArith/Qring.v
+++ b/theories/QArith/Qring.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Qring.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Qring.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Export Ring.
Require Export QArith_base.
@@ -37,15 +37,15 @@ Proof.
Qed.
Ltac isQcst t :=
- let t := eval hnf in t in
- match t with
- Qmake ?n ?d =>
- match isZcst n with
- true => isZcst d
- | _ => false
- end
- | _ => false
- end.
+ match t with
+ | inject_Z ?z => isZcst z
+ | Qmake ?n ?d =>
+ match isZcst n with
+ true => isPcst d
+ | _ => false
+ end
+ | _ => false
+ end.
Ltac Qcst t :=
match isQcst t with
@@ -74,7 +74,7 @@ Let ex3 : forall x y z : Q, (x+y)+z == x+(y+z).
Qed.
Let ex4 : (inject_Z 1)+(inject_Z 1)==(inject_Z 2).
- ring.
+ ring.
Qed.
Let ex5 : 1+1 == 2#1.
diff --git a/theories/Reals/AltSeries.v b/theories/Reals/AltSeries.v
index fa44b6ff..581c181f 100644
--- a/theories/Reals/AltSeries.v
+++ b/theories/Reals/AltSeries.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: AltSeries.v 9245 2006-10-17 12:53:34Z notin $ i*)
+ (*i $Id: AltSeries.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -92,9 +92,9 @@ Proof.
replace (Un (S (2 * S N)) + (-1 * Un (S (2 * S N)) + Un (S (S (2 * S N)))))
with (Un (S (S (2 * S N)))); [ idtac | ring ].
apply H.
- ring_nat.
+ ring.
apply HrecN.
- ring_nat.
+ ring.
Qed.
(** A more general inequality *)
@@ -300,7 +300,7 @@ Proof.
do 2 rewrite Rmult_1_r; apply le_INR.
replace (2 * S n + 1)%nat with (S (S (2 * n + 1))).
apply le_trans with (S (2 * n + 1)); apply le_n_Sn.
- ring_nat.
+ ring.
apply not_O_INR; discriminate.
apply not_O_INR; replace (2 * n + 1)%nat with (S (2 * n));
[ discriminate | ring ].
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index 48876be2..7dbbd605 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: ArithProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+ (*i $Id: ArithProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rbasic_fun.
@@ -75,7 +75,7 @@ Proof.
apply H3; assumption.
right.
apply H4; assumption.
- unfold double in |- *; ring.
+ unfold double in |- *;ring.
Qed.
(* 2m <= 2n => m<=n *)
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index 3719d551..10965951 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
- (*i $Id: Cos_plus.v 9245 2006-10-17 12:53:34Z notin $ i*)
+ (*i $Id: Cos_plus.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -486,7 +486,7 @@ Proof.
apply le_trans with (pred N).
assumption.
apply le_pred_n.
- ring_nat.
+ ring.
apply Rle_trans with
(sum_f_R0
(fun k:nat =>
@@ -515,7 +515,7 @@ Proof.
apply le_trans with (2 * S (S (n0 + n)))%nat.
replace (2 * S (S (n0 + n)))%nat with (S (2 * S (n0 + n) + 1)).
apply le_n_Sn.
- ring_nat.
+ ring.
omega.
right.
unfold Rdiv in |- *; rewrite Rmult_comm.
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index ac8ffbeb..d410e14a 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Cos_rel.v 9178 2006-09-26 11:18:22Z barras $ i*)
+(*i $Id: Cos_rel.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -109,9 +109,10 @@ pose
C (2 * S p) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (p - l))) p
end).
ring_simplify.
+unfold Rminus.
replace
(* (- old ring compat *)
- (-1 *
+ (-
sum_f_R0
(fun k:nat =>
sum_f_R0
@@ -140,7 +141,6 @@ replace
(fun l:nat =>
C (2 * S i) (S (2 * l)) * x ^ S (2 * l) * y ^ S (2 * (i - l))) i) with
(sum_f_R0 (fun l:nat => Wn (S (2 * l))) i).
-(*rewrite Rplus_comm.*) (* compatibility old ring... *)
apply sum_decomposition.
apply sum_eq; intros.
unfold Wn in |- *.
@@ -154,8 +154,7 @@ apply Rmult_eq_compat_l.
replace (2 * S i - 2 * i0)%nat with (2 * (S i - i0))%nat.
reflexivity.
omega.
-replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
-(*replace (* compatibility old ring... *)
+replace
(-
sum_f_R0
(fun k:nat =>
@@ -171,13 +170,13 @@ replace (sum_f_R0 sin_nnn (S n)) with (-1 * (-1 * sum_f_R0 sin_nnn (S n))).
(fun p:nat =>
(-1) ^ p / INR (fact (2 * p + 1)) * x ^ (2 * p + 1) *
((-1) ^ (k - p) / INR (fact (2 * (k - p) + 1)) *
- y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].*)
-apply Rmult_eq_compat_l.
+ y ^ (2 * (k - p) + 1))) k) n);[idtac|ring].
rewrite scal_sum.
rewrite decomp_sum.
replace (sin_nnn 0%nat) with 0.
-rewrite Rmult_0_l; rewrite Rplus_0_l.
-replace (pred (S n)) with n; [ idtac | reflexivity ].
+rewrite Rplus_0_l.
+change (pred (S n)) with n.
+ (* replace (pred (S n)) with n; [ idtac | reflexivity ]. *)
apply sum_eq; intros.
rewrite Rmult_comm.
unfold sin_nnn in |- *.
@@ -185,8 +184,8 @@ rewrite scal_sum.
rewrite scal_sum.
apply sum_eq; intros.
unfold Rdiv in |- *.
-repeat rewrite Rmult_assoc.
-rewrite (Rmult_comm (/ INR (fact (2 * S i)))).
+(*repeat rewrite Rmult_assoc.*)
+(* rewrite (Rmult_comm (/ INR (fact (2 * S i)))). *)
repeat rewrite <- Rmult_assoc.
rewrite <- (Rmult_comm (/ INR (fact (2 * S i)))).
repeat rewrite <- Rmult_assoc.
@@ -216,7 +215,7 @@ apply INR_fact_neq_0.
apply INR_fact_neq_0.
reflexivity.
apply lt_O_Sn.
-ring.
+(* ring. *)
apply sum_eq; intros.
rewrite scal_sum.
apply sum_eq; intros.
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 5dafec83..beb4b744 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Exp_prop.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Exp_prop.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -87,7 +87,7 @@ Proof.
reflexivity.
replace (2 * S N)%nat with (S (S (2 * N))).
simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
- ring_nat.
+ ring.
Qed.
Lemma div2_S_double : forall N:nat, div2 (S (2 * N)) = N.
@@ -96,7 +96,7 @@ Proof.
reflexivity.
replace (2 * S N)%nat with (S (S (2 * N))).
simpl in |- *; simpl in HrecN; rewrite HrecN; reflexivity.
- ring_nat.
+ ring.
Qed.
Lemma div2_not_R0 : forall N:nat, (1 < N)%nat -> (0 < div2 N)%nat.
@@ -367,7 +367,7 @@ Proof.
apply le_trans with (pred N).
apply H0.
apply le_pred_n.
- rewrite H4; ring_nat.
+ rewrite H4; ring.
cut (S N = (2 * S N0)%nat).
intro.
replace (C (S N) (S N0) / INR (fact (S N))) with (/ Rsqr (INR (fact (S N0)))).
@@ -388,7 +388,7 @@ Proof.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
- rewrite H4; ring_nat.
+ rewrite H4; ring.
unfold C, Rdiv in |- *.
rewrite (Rmult_comm (INR (fact (S N)))).
rewrite Rmult_assoc; rewrite <- Rinv_r_sym.
@@ -494,7 +494,7 @@ Proof.
simpl in |- *.
pattern 1 at 1 in |- *; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left;
apply Rlt_0_1.
- ring_nat.
+ ring.
unfold Rsqr in |- *; apply prod_neq_R0; apply INR_fact_neq_0.
unfold Rsqr in |- *; apply prod_neq_R0; apply not_O_INR; discriminate.
assert (H0 := even_odd_cor N).
@@ -515,7 +515,7 @@ Proof.
replace (S (S (2 * N0))) with (2 * S N0)%nat.
do 2 rewrite div2_double.
reflexivity.
- ring_nat.
+ ring.
apply S_pred with 0%nat; apply H.
Qed.
@@ -585,8 +585,8 @@ Proof.
apply (fun m n p:nat => mult_le_compat_l p n m).
replace (2 * S N1)%nat with (S (S (2 * N1))).
apply le_n_Sn.
- ring_nat.
- ring_nat.
+ ring.
+ ring.
reflexivity.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
@@ -623,7 +623,7 @@ Proof.
replace (2 * N1)%nat with (S (S (2 * pred N1))).
reflexivity.
pattern N1 at 2 in |- *; replace N1 with (S (pred N1)).
- ring_nat.
+ ring.
symmetry in |- *; apply S_pred with 0%nat; apply H8.
apply INR_lt.
apply Rmult_lt_reg_l with (INR 2).
@@ -641,7 +641,7 @@ Proof.
rewrite div2_double.
replace (2 * S N1)%nat with (S (S (2 * N1))).
apply le_n_Sn.
- ring_nat.
+ ring.
reflexivity.
apply le_trans with (max (2 * S N0) 2).
apply le_max_l.
diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 11c6378e..a8f72302 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: PartSum.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: PartSum.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -278,7 +278,7 @@ Proof.
rewrite (tech5 An (2 * S N)).
rewrite <- HrecN.
ring.
- ring_nat.
+ ring.
Qed.
Lemma sum_Rle :
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 51c66afa..7d98a844 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,13 +6,15 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: RIneq.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
(***************************************************************************)
(** Basic lemmas for the classical reals numbers *)
(***************************************************************************)
Require Export Raxioms.
+Require Import Rpow_def.
+Require Import Zpower.
Require Export ZArithRing.
Require Import Omega.
Require Export RealField.
@@ -1528,6 +1530,16 @@ Proof.
rewrite Rmult_opp_opp; auto with real.
Qed.
+Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
+Proof.
+ intros z [|n];simpl;trivial.
+ rewrite Zpower_pos_nat.
+ rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
+ rewrite mult_IZR.
+ induction n;simpl;trivial.
+ rewrite mult_IZR;ring[IHn].
+Qed.
+
(**********)
Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
Proof.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
index f9ba589e..330c0042 100644
--- a/theories/Reals/Rdefinitions.v
+++ b/theories/Reals/Rdefinitions.v
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rdefinitions.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rdefinitions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
(*********************************************************)
@@ -55,6 +55,8 @@ Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R.
(**********)
Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R.
+(**********)
+
Infix "-" := Rminus : R_scope.
Infix "/" := Rdiv : R_scope.
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index c727623c..3d1c0375 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rfunctions.v 9302 2006-10-27 21:21:17Z barras $ i*)
+(*i $Id: Rfunctions.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
(*i Some properties about pow and sum have been made with John Harrison i*)
(*i Some Lemmas (about pow and powerRZ) have been done by Laurent Thery i*)
@@ -15,10 +15,10 @@
(** Definition of the sum functions *)
(* *)
(********************************************************)
-Require Export LegacyArithRing. (* for ring_nat... *)
Require Export ArithRing.
Require Import Rbase.
+Require Export Rpow_def.
Require Export R_Ifp.
Require Export Rbasic_fun.
Require Export R_sqr.
@@ -65,11 +65,6 @@ Qed.
(** * Power *)
(*******************************)
(*********)
-Boxed Fixpoint pow (r:R) (n:nat) {struct n} : R :=
- match n with
- | O => 1
- | S n => r * pow r n
- end.
Infix "^" := pow : R_scope.
@@ -382,7 +377,7 @@ Proof.
replace (x ^ S (S (2 * n))) with (x * x * x ^ (2 * n)).
rewrite Hrecn; reflexivity.
simpl in |- *; ring.
- ring_nat.
+ ring.
Qed.
Lemma pow_le : forall (a:R) (n:nat), 0 <= a -> 0 <= a ^ n.
@@ -429,7 +424,7 @@ Proof.
rewrite Hrecn2.
simpl in |- *.
ring.
- ring_nat.
+ ring.
Qed.
Lemma pow_incr : forall (x y:R) (n:nat), 0 <= x <= y -> x ^ n <= y ^ n.
diff --git a/theories/Reals/Rpow_def.v b/theories/Reals/Rpow_def.v
new file mode 100644
index 00000000..5bdbb76b
--- /dev/null
+++ b/theories/Reals/Rpow_def.v
@@ -0,0 +1,7 @@
+Require Import Rdefinitions.
+
+Fixpoint pow (r:R) (n:nat) {struct n} : R :=
+ match n with
+ | O => R1
+ | S n => Rmult r (pow r n)
+ end.
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 690c420f..cb31d3b2 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsigma.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsigma.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -53,7 +53,7 @@ Section Sigma.
apply lt_minus_O_lt; assumption.
apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
reflexivity.
- ring_nat.
+ ring.
replace (high - S (S k))%nat with (high - S k - 1)%nat.
apply pred_of_minus.
omega.
@@ -71,7 +71,7 @@ Section Sigma.
apply le_lt_trans with (S k); [ rewrite H2; apply le_n | assumption ].
apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
reflexivity.
- ring_nat.
+ ring.
omega.
inversion H; [ right; reflexivity | left; assumption ].
Qed.
diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index 92284e7d..0a9f7754 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rsqrt_def.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rsqrt_def.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Sumbool.
Require Import Rbase.
@@ -522,7 +522,7 @@ Proof.
intro; assumption.
intro; reflexivity.
split.
- intro; elim diff_false_true; assumption.
+ intro feqt;discriminate feqt.
intro.
elim n0; assumption.
unfold Vn in |- *.
@@ -540,7 +540,7 @@ Proof.
unfold cond_positivity in |- *.
case (Rle_dec 0 z); intro.
split.
- intro; elim diff_true_false; assumption.
+ intro feqt; discriminate feqt.
intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)).
split.
intro; auto with real.
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 6e992aa3..b744c788 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -466,10 +466,10 @@ Proof.
unfold x in |- *; replace 0 with (INR 0);
[ apply le_INR; apply le_O_n | reflexivity ].
prove_sup0.
- ring_nat.
+ ring.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
- ring_nat.
+ ring.
Qed.
Lemma SIN : forall a:R, 0 <= a -> a <= PI -> sin_lb a <= sin a <= sin_ub a.
@@ -1580,10 +1580,14 @@ Lemma cos_eq_0_0 :
Proof.
intros x H; rewrite cos_sin in H; generalize (sin_eq_0_0 (PI / INR 2 + x) H);
intro H2; elim H2; intros x0 H3; exists (x0 - Z_of_nat 1)%Z;
- rewrite <- Z_R_minus; simpl; ring_simplify;
-(* rewrite (Rmult_comm PI);*) (* old ring compat *)
+ rewrite <- Z_R_minus; simpl.
+unfold INR in H3. field_simplify [(sym_eq H3)]. field.
+(**
+ ring_simplify.
+ (* rewrite (Rmult_comm PI);*) (* old ring compat *)
rewrite <- H3; simpl;
- field; repeat split; discrR.
+ field;repeat split; discrR.
+*)
Qed.
Lemma cos_eq_0_1 :
diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v
index a95bc54b..89ee1745 100644
--- a/theories/Reals/Rtrigo_alt.v
+++ b/theories/Reals/Rtrigo_alt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_alt.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_alt.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -121,7 +121,7 @@ Proof.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
simpl in |- *; ring.
- ring_nat.
+ ring.
assert (H3 := cv_speed_pow_fact a); unfold Un in |- *; unfold Un_cv in H3;
unfold R_dist in H3; unfold Un_cv in |- *; unfold R_dist in |- *;
intros; elim (H3 eps H4); intros N H5.
@@ -316,7 +316,7 @@ Proof.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
simpl in |- *; ring.
- ring_nat.
+ ring.
assert (H4 := cv_speed_pow_fact a0); unfold Un in |- *; unfold Un_cv in H4;
unfold R_dist in H4; unfold Un_cv in |- *; unfold R_dist in |- *;
intros; elim (H4 eps H5); intros N H6; exists N; intros.
diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v
index 854c0b4a..b105ca69 100644
--- a/theories/Reals/Rtrigo_reg.v
+++ b/theories/Reals/Rtrigo_reg.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rtrigo_reg.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Rtrigo_reg.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -99,7 +99,7 @@ Proof.
apply pow_nonzero; assumption.
replace (2 * S n)%nat with (S (S (2 * n))).
simpl in |- *; ring.
- ring_nat.
+ ring.
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rabs_no_R0; apply pow_nonzero; assumption.
@@ -280,7 +280,7 @@ Proof.
apply pow_nonzero; assumption.
replace (2 * S n)%nat with (S (S (2 * n))).
simpl in |- *; ring.
- ring_nat.
+ ring.
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rle_ge; apply pow_le; left; apply (cond_pos r).
apply Rabs_no_R0; apply pow_nonzero; assumption.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 133f2b89..96351618 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: SeqProp.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: SeqProp.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import Rbase.
Require Import Rfunctions.
@@ -1265,8 +1265,8 @@ Proof.
apply lt_le_trans with 1%nat; [ apply lt_O_Sn | assumption ].
apply INR_fact_neq_0.
apply not_O_INR; discriminate.
- ring_nat.
- ring_nat.
+ ring.
+ ring.
unfold Vn in |- *; rewrite Rmult_assoc; unfold Rdiv in |- *;
rewrite (Rmult_comm (Un 0%nat)); rewrite (Rmult_comm (Un n)).
repeat apply Rmult_le_compat_l.
@@ -1293,8 +1293,8 @@ Proof.
apply le_INR; omega.
apply INR_fact_neq_0.
apply INR_fact_neq_0.
- ring_nat.
- ring_nat.
+ ring.
+ ring.
intro; unfold Un in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat.
apply pow_lt; assumption.
apply Rinv_0_lt_compat; apply lt_INR_0; apply neq_O_lt; red in |- *; intro;
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 40fd8f36..7e202359 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Operators_Properties.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Operators_Properties.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(****************************************************************************)
(* Bruno Barras *)
@@ -18,7 +18,7 @@ Require Import Relation_Operators.
Section Properties.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
@@ -43,7 +43,7 @@ Section Properties.
Qed.
Lemma clos_refl_trans_ind_left :
- forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
+ forall (A:Type) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
P M ->
(forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
forall a:A, clos_refl_trans A R M a -> P a.
@@ -95,4 +95,4 @@ Section Properties.
End Clos_Refl_Sym_Trans.
-End Properties. \ No newline at end of file
+End Properties.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 089246da..4c5a6519 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Relation_Operators.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Relation_Operators.v 9610 2007-02-07 14:45:18Z herbelin $ i*)
(****************************************************************************)
(* Bruno Barras, Cristina Cornes *)
@@ -78,7 +78,7 @@ End Union.
Section Disjoint_Union.
-Variables A B : Set.
+Variables A B : Type.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
@@ -94,8 +94,8 @@ End Disjoint_Union.
Section Lexicographic_Product.
(* Lexicographic order on dependent pairs *)
- Variable A : Set.
- Variable B : A -> Set.
+ Variable A : Type.
+ Variable B : A -> Type.
Variable leA : A -> A -> Prop.
Variable leB : forall x:A, B x -> B x -> Prop.
@@ -110,8 +110,8 @@ End Lexicographic_Product.
Section Symmetric_Product.
- Variable A : Set.
- Variable B : Set.
+ Variable A : Type.
+ Variable B : Type.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
@@ -125,7 +125,7 @@ End Symmetric_Product.
Section Swap.
- Variable A : Set.
+ Variable A : Type.
Variable R : A -> A -> Prop.
Inductive swapprod : A * A -> A * A -> Prop :=
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 9b2f4057..9da30e9b 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -6,14 +6,14 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Relations.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Relations.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
Require Export Relation_Definitions.
Require Export Relation_Operators.
Require Export Operators_Properties.
Lemma inverse_image_of_equivalence :
- forall (A B:Set) (f:A -> B) (r:relation B),
+ forall (A B:Type) (f:A -> B) (r:relation B),
equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
Proof.
intros; split; elim H; red in |- *; auto.
@@ -21,7 +21,7 @@ Proof.
Qed.
Lemma inverse_image_of_eq :
- forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+ forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
Proof.
split; red in |- *;
[ (* reflexivity *) reflexivity
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 24816a20..efdf0495 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Lexicographic_Exponentiation.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Lexicographic_Exponentiation.v 9610 2007-02-07 14:45:18Z herbelin $ i*)
(** Author: Cristina Cornes
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 8ac0d546..051c8127 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Lexicographic_Product.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Lexicographic_Product.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(** Authors: Bruno Barras, Cristina Cornes *)
@@ -18,8 +18,8 @@ Require Import Transitive_Closure.
L. Paulson JSC (1986) 2, 325-355 *)
Section WfLexicographic_Product.
- Variable A : Set.
- Variable B : A -> Set.
+ Variable A : Type.
+ Variable B : A -> Type.
Variable leA : A -> A -> Prop.
Variable leB : forall x:A, B x -> B x -> Prop.
@@ -74,8 +74,8 @@ End WfLexicographic_Product.
Section Wf_Symmetric_Product.
- Variable A : Set.
- Variable B : Set.
+ Variable A : Type.
+ Variable B : Type.
Variable leA : A -> A -> Prop.
Variable leB : B -> B -> Prop.
@@ -106,7 +106,7 @@ End Wf_Symmetric_Product.
Section Swap.
- Variable A : Set.
+ Variable A : Type.
Variable R : A -> A -> Prop.
Notation SwapProd := (swapprod A R).
@@ -168,4 +168,4 @@ Section Swap.
apply Acc_swapprod; auto with sets.
Qed.
-End Swap. \ No newline at end of file
+End Swap.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 5bf82ffb..bd4e4fec 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Transitive_Closure.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Transitive_Closure.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(** Author: Bruno Barras *)
@@ -14,7 +14,7 @@ Require Import Relation_Definitions.
Require Import Relation_Operators.
Section Wf_Transitive_Closure.
- Variable A : Set.
+ Variable A : Type.
Variable R : relation A.
Notation trans_clos := (clos_trans A R).
@@ -44,4 +44,4 @@ Section Wf_Transitive_Closure.
unfold well_founded in |- *; auto with sets.
Qed.
-End Wf_Transitive_Closure. \ No newline at end of file
+End Wf_Transitive_Closure.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index 69617de2..f691f2b7 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Well_Ordering.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Well_Ordering.v 9597 2007-02-06 19:44:05Z herbelin $ i*)
(** Author: Cristina Cornes.
From: Constructing Recursion Operators in Type Theory
@@ -15,10 +15,10 @@
Require Import Eqdep.
Section WellOrdering.
- Variable A : Set.
- Variable B : A -> Set.
+ Variable A : Type.
+ Variable B : A -> Type.
- Inductive WO : Set :=
+ Inductive WO : Type :=
sup : forall (a:A) (f:B a -> WO), WO.
@@ -52,7 +52,7 @@ Section Characterisation_wf_relations.
(* in course of development *)
- Variable A : Set.
+ Variable A : Type.
Variable leA : A -> A -> Prop.
Definition B (a:A) := {x : A | leA x a}.
@@ -60,12 +60,12 @@ Section Characterisation_wf_relations.
Definition wof : well_founded leA -> A -> WO A B.
Proof.
intros.
- apply (well_founded_induction H (fun a:A => WO A B)); auto.
- intros.
+ apply (well_founded_induction_type H (fun a:A => WO A B)); auto.
+ intros x H1.
apply (sup A B x).
unfold B at 1 in |- *.
destruct 1 as [x0].
apply (H1 x0); auto.
Qed.
-End Characterisation_wf_relations. \ No newline at end of file
+End Characterisation_wf_relations.
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
new file mode 100644
index 00000000..b0f372de
--- /dev/null
+++ b/theories/ZArith/Zpow_def.v
@@ -0,0 +1,27 @@
+Require Import ZArith_base.
+Require Import Ring_theory.
+
+Open Local Scope Z_scope.
+
+(** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
+ integer (type [positive]) and [z] a signed integer (type [Z]) *)
+Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
+
+Definition Zpower (x y:Z) :=
+ match y with
+ | Zpos p => Zpower_pos x p
+ | Z0 => 1
+ | Zneg p => 0
+ end.
+
+Lemma Zpower_theory : power_theory 1 Zmult (eq (A:=Z)) Z_of_N Zpower.
+Proof.
+ constructor. intros.
+ destruct n;simpl;trivial.
+ unfold Zpower_pos.
+ assert (forall k, iter_pos p Z (fun x : Z => r * x) k = pow_pos Zmult r p*k).
+ induction p;simpl;intros;repeat rewrite IHp;trivial;
+ repeat rewrite Zmult_assoc;trivial.
+ rewrite H;rewrite Zmult_1_r;trivial.
+Qed.
+
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 446f663c..c9cee31d 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -6,9 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zpower.v 9245 2006-10-17 12:53:34Z notin $ i*)
+(*i $Id: Zpower.v 9551 2007-01-29 15:13:35Z bgregoir $ i*)
Require Import ZArith_base.
+Require Export Zpow_def.
Require Import Omega.
Require Import Zcomplements.
Open Local Scope Z_scope.
@@ -35,11 +36,6 @@ Section section1.
apply Zmult_assoc ].
Qed.
- (** [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
- integer (type [positive]) and [z] a signed integer (type [Z]) *)
-
- Definition Zpower_pos (z:Z) (n:positive) := iter_pos n Z (fun x:Z => z * x) 1.
-
(** This theorem shows that powers of unary and binary integers
are the same thing, modulo the function convert : [positive -> nat] *)
@@ -66,13 +62,6 @@ Section section1.
apply Zpower_nat_is_exp.
Qed.
- Definition Zpower (x y:Z) :=
- match y with
- | Zpos p => Zpower_pos x p
- | Z0 => 1
- | Zneg p => 0
- end.
-
Infix "^" := Zpower : Z_scope.
Hint Immediate Zpower_nat_is_exp: zarith.
@@ -382,4 +371,4 @@ Section power_div_with_rest.
apply Zdiv_rest_proof with (q := a0) (r := b); assumption.
Qed.
-End power_div_with_rest. \ No newline at end of file
+End power_div_with_rest.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 9893bed3..3f475a63 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Zsqrt.v 9245 2006-10-17 12:53:34Z notin $ *)
+(* $Id: Zsqrt.v 9551 2007-01-29 15:13:35Z bgregoir $ *)
Require Import ZArithRing.
Require Import Omega.
@@ -132,7 +132,7 @@ Definition Zsqrt :
(fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
_)
end); try omega.
-split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
+ split; [ omega | rewrite Heq; ring_simplify (s*s) ((s + 1) * (s + 1)); omega ].
Defined.
(** Define a function of type Z->Z that computes the integer square root,