(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This file was automatically generated: do not edit *********************) include "CoRN.ma". (* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *) (*#* printing IR %\ensuremath{\mathbb R}% *) (*#* printing PartIR %\ensuremath{\mathbb R\!\not\rightarrow\!\mathbb R}% *) (*#* printing ZeroR %\ensuremath{\mathbf0}% #0# *) (*#* printing OneR %\ensuremath{\mathbf1}% #1# *) (*#* printing AbsIR %\ensuremath{|\cdot|_{\mathbb R}}% *) include "reals/CReals.ma". (*#* *Real Number Structures %\begin{convention}% Let [IR] be a structure for real numbers. %\end{convention}% *) (* Require Export R_CReals. Definition IR : CReals := Concrete_R. Opaque IR. *) inline procedural "cic:/CoRN/reals/CauchySeq/IR.con". (* NOTATION Notation PartIR := (PartFunct IR). *) (* NOTATION Notation ProjIR1 := (prj1 IR _ _ _). *) (* NOTATION Notation ProjIR2 := (prj2 IR _ _ _). *) include "tactics/Transparent_algebra.ma". (* begin hide *) (* NOTATION Notation ZeroR := (Zero:IR). *) (* NOTATION Notation OneR := (One:IR). *) (* end hide *) (* UNEXPORTED Section CReals_axioms *) (*#* ** [CReals] axioms *) inline procedural "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con" as lemma. (*#* First properties which follow trivially from the axioms. *) inline procedural "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes'.con" as lemma. (*#* A stronger version, which often comes in useful. *) inline procedural "cic:/CoRN/reals/CauchySeq/str_Archimedes.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/CauchySeqR.con" as definition. (* UNEXPORTED End CReals_axioms *) (* UNEXPORTED Section Cauchy_Defs *) (*#* ** Cauchy sequences *** Alternative definitions This section gives several definitions of Cauchy sequences. There are no lemmas in this section. The current definition of Cauchy ([Cauchy_prop]) is: %\[\forall \epsilon>0. \exists N. \forall m\geq N. |seq_m - seq_N|\leq\varepsilon\]% #for all e>0 there exists N such that for all m≥ N |seqm-seqN|≤ e# Variant 1 of Cauchy ([Cauchy_prop1]) is: %\[\forall k. \exists N. \forall m \geq N. |seq_m - seq_N|\leq1/(k+1)\]% #for all k there exists N such that for all m ≥ N |seqm-seqN| ≤ 1/(k+1)# In all of the following variants the limit occurs in the definition. Therefore it is useful to define an auxiliary predicate [Cauchy_Lim_prop?], in terms of which [Cauchy_prop?] is defined. Variant 2 of Cauchy ([Cauchy_prop2]) is [exists y, (Cauchy_Lim_prop2 seq y)] where [[ Cauchy_Lim_prop2 seq y := forall eps [>] Zero, exists N, forall m >= N, (AbsIR seq m - y) [<=] eps ]] Note that [Cauchy_Lim_prop2] equals [seqLimit]. Variant 3 of Cauchy ([Cauchy_prop3]) reads [exists y, (Cauchy_Lim_prop3 seq y)] where [[ Cauchy_Lim_prop3 seq y := forall k, exists N, forall m >= N, (AbsIR seq m - y) [<=] One[/] (k[+]1) ]] The following variant is more restricted. Variant 4 of Cauchy ([Cauchy_prop4]): [exists y, (Cauchy_Lim_prop4 seq y)] where [[ Cauchy_Lim_prop4 seq y := forall k, (AbsIR seq m - y) [<=] One[/] (k[+]1) ]] So [[ Cauchy_prop4 -> Cauchy_prop3 Iff Cauchy_prop2 Iff Cauchy_prop1 Iff Cauchy_prop ]] Note: we don't know which formulations are useful. The inequalities are stated with [[<=]] rather than with [<] for the following reason: both formulations are equivalent, as is well known; and [[<=]] being a negative statement, this makes proofs sometimes easier and program extraction much more efficient. *) inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con" as definition. (* UNEXPORTED End Cauchy_Defs *) (* UNEXPORTED Section Inequalities *) (*#* *** Inequalities of Limits The next lemma is equal to lemma [Lim_Cauchy]. *) inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con" as lemma. (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ]. *) inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Limits_unique.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_strext.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con" as lemma. (* UNEXPORTED End Inequalities *) (* UNEXPORTED Section Equiv_Cauchy *) (*#* *** Equivalence of formulations of Cauchy *) inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con" as lemma. (*#* Well definedness. *) inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd'.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_unique.con" as lemma. (* UNEXPORTED End Equiv_Cauchy *) (* UNEXPORTED Section Cauchy_props *) (*#* *** Properties of Cauchy sequences Some of these lemmas are now obsolete, because they were reproved for arbitrary ordered fields$\ldots$#...# We begin by defining the constant sequence and proving that it is Cauchy with the expected limit. *) inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_const.con" as definition. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_const.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_plus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_inv.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_minus.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con" as lemma. inline procedural "cic:/CoRN/reals/CauchySeq/Lim_mult.con" as lemma. (* UNEXPORTED End Cauchy_props *)