diff options
Diffstat (limited to 'theories')
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, |