X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FReals%2FRanalysis1.mma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprocedural%2FCoq%2FReals%2FRanalysis1.mma;h=9356ac6c66a386beb5151f526f2cf9e1f6e45966;hb=29714797b01e0ac8c22e4df2827b1785a759f482;hp=0000000000000000000000000000000000000000;hpb=1fb0f39de8b87920d2f15f9e33929d372fa518dd;p=helm.git diff --git a/helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma b/helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma new file mode 100644 index 000000000..9356ac6c6 --- /dev/null +++ b/helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis1.mma @@ -0,0 +1,405 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "Coq.ma". + +(*#**********************************************************************) + +(* v * The Coq Proof Assistant / The Coq Development Team *) + +(* R. +*) + +(*#***************************************************) + +(*#* Basic operations on functions *) + +(*#***************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/plus_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/opp_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/mult_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/mult_real_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/minus_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/div_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/div_real_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/comp.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/inv_fct.con" as definition. + +(* NOTATION +Infix "+" := plus_fct : Rfun_scope. +*) + +(* NOTATION +Notation "- x" := (opp_fct x) : Rfun_scope. +*) + +(* NOTATION +Infix "*" := mult_fct : Rfun_scope. +*) + +(* NOTATION +Infix "-" := minus_fct : Rfun_scope. +*) + +(* NOTATION +Infix "/" := div_fct : Rfun_scope. +*) + +(* NOTATION +Notation Local "f1 'o' f2" := (comp f1 f2) + (at level 20, right associativity) : Rfun_scope. +*) + +(* NOTATION +Notation "/ x" := (inv_fct x) : Rfun_scope. +*) + +(* UNEXPORTED +Delimit Scope Rfun_scope with F. +*) + +inline procedural "cic:/Coq/Reals/Ranalysis1/fct_cte.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/id.con" as definition. + +(*#***************************************************) + +(*#* Variations of functions *) + +(*#***************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/increasing.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/decreasing.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/strict_increasing.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/strict_decreasing.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/constant.con" as definition. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/no_cond.con" as definition. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/constant_D_eq.con" as definition. + +(*#**************************************************) + +(*#* Definition of continuity as a limit *) + +(*#**************************************************) + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity.con" as definition. + +(* UNEXPORTED +Arguments Scope continuity_pt [Rfun_scope R_scope]. +*) + +(* UNEXPORTED +Arguments Scope continuity [Rfun_scope]. +*) + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_inv.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/div_eq_inv.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_div.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_pt_comp.con" as lemma. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_inv.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_div.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/continuity_comp.con" as lemma. + +(*#****************************************************) + +(*#* Derivative's definition using Landau's kernel *) + +(*#****************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_abs.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive.con" as definition. + +(* UNEXPORTED +Arguments Scope derivable_pt_lim [Rfun_scope R_scope]. +*) + +(* UNEXPORTED +Arguments Scope derivable_pt_abs [Rfun_scope R_scope R_scope]. +*) + +(* UNEXPORTED +Arguments Scope derivable_pt [Rfun_scope R_scope]. +*) + +(* UNEXPORTED +Arguments Scope derivable [Rfun_scope]. +*) + +(* UNEXPORTED +Arguments Scope derive_pt [Rfun_scope R_scope _]. +*) + +(* UNEXPORTED +Arguments Scope derive [Rfun_scope _]. +*) + +inline procedural "cic:/Coq/Reals/Ranalysis1/antiderivative.con" as definition. + +(*#***********************************) + +(*#* Class of differential functions *) + +(*#***********************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/Differential.ind". + +inline procedural "cic:/Coq/Reals/Ranalysis1/Differential_D2.ind". + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step1.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step2.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_step3.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/uniqueness_limite.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq.con" as lemma. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_0.con" as lemma. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_eq_1.con" as lemma. + +(*#*******************************************************************) + +(*#* Equivalence of this definition with the one using limit concept *) + +(*#*******************************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_D_in.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_D_in.con" as lemma. + +(*#**********************************) + +(*#* derivability -> continuity *) + +(*#**********************************) + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_derive.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous_pt.con" as theorem. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_continuous.con" as theorem. + +(*#***************************************************************) + +(*#* Main rules *) + +(*#***************************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_id.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_Rsqr.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_comp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_id.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_Rsqr.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_comp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_id.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_Rsqr.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_comp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_plus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_opp.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_minus.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_mult.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_const.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_scal.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_id.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_Rsqr.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_comp.con" as lemma. + +(* Pow *) + +inline procedural "cic:/Coq/Reals/Ranalysis1/pow_fct.con" as definition. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow_pos.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_lim_pow.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pt_pow.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derivable_pow.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/derive_pt_pow.con" as lemma. + +inline procedural "cic:/Coq/Reals/Ranalysis1/pr_nu.con" as lemma. + +(*#***********************************************************) + +(*#* Local extremum's condition *) + +(*#***********************************************************) + +inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_maximum.con" as theorem. + +inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_minimum.con" as theorem. + +inline procedural "cic:/Coq/Reals/Ranalysis1/deriv_constant2.con" as theorem. + +(*#*********) + +inline procedural "cic:/Coq/Reals/Ranalysis1/nonneg_derivative_0.con" as lemma. +