X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Procedural%2Fftc%2FPartFunEquality.mma;h=eabeadd4b5fb69b9443ce207cce8dcabf58f6d66;hb=a89360d64f1fcbba917ad743b97a2d973ecf6db2;hp=3b22af3fda5e95e250f234d25882e7aa786b4dac;hpb=32e77480c65cbf23ae7dea38a519c83dfeaf3830;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Procedural/ftc/PartFunEquality.mma b/helm/software/matita/contribs/CoRN-Procedural/ftc/PartFunEquality.mma index 3b22af3fd..eabeadd4b 100644 --- a/helm/software/matita/contribs/CoRN-Procedural/ftc/PartFunEquality.mma +++ b/helm/software/matita/contribs/CoRN-Procedural/ftc/PartFunEquality.mma @@ -38,7 +38,7 @@ given predicate rather than to the predicate itself. The following definition makes this possible. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/subset.con" as definition. (*#* The core of our work will revolve around the following fundamental @@ -50,7 +50,7 @@ it is easier to consider a generic case%.}%. This file is concerned with proving the main properties of this equality relation. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq.con" as definition. (*#* Notice that, because the quantification over the proofs is universal, @@ -93,9 +93,9 @@ alias id "G" = "cic:/CoRN/ftc/PartFunEquality/Equality_Results/G.var". (* begin hide *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/P.con" "Equality_Results__" as definition. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Equality_Results/Q.con" "Equality_Results__" as definition. (* end hide *) @@ -106,11 +106,11 @@ We start with two lemmas which make it much easier to prove and use this definition: *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/eq_imp_Feq.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_imp_eq.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/included_IR.con" as lemma. (* UNEXPORTED End Equality_Results @@ -128,7 +128,7 @@ Section Some_More If two function coincide on a given subset then they coincide in any smaller subset. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/included_Feq.con" as lemma. (* UNEXPORTED End Some_More @@ -160,11 +160,11 @@ alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/F.var". (* begin hide *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/P.con" "Away_from_Zero__Definitions__" as definition. (* end hide *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero.con" as definition. (*#* If [F] is bounded away from zero in [I] then [F] is necessarily apart from zero in [I]; also this means that [I] is included in the domain of [{1/}F]. @@ -176,11 +176,11 @@ alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Definitions/Hf.var (* end show *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_ap_zero.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_recip.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_imp_inc_div.con" as lemma. (* UNEXPORTED End Definitions @@ -199,25 +199,25 @@ alias id "P" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/P.var". alias id "Q" = "cic:/CoRN/ftc/PartFunEquality/Away_from_Zero/Q.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/included_imp_bnd.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd.con" as lemma. (*#* A function is said to be bounded away from zero everywhere if it is bounded away from zero in every compact subinterval of its domain; a similar definition is made for arbitrary sets, which will be necessary for future work. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_everywhere.con" as definition. -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_away_zero_in_P.con" as definition. (*#* An immediate consequence: *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/bnd_in_P_imp_ap_zero.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_bnd'.con" as lemma. (* UNEXPORTED End Away_from_Zero @@ -271,11 +271,11 @@ alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/G alias id "H" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Feq_Equivalence/H.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_reflexive.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_symmetric.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_transitive.con" as lemma. (* UNEXPORTED End Feq_Equivalence @@ -297,23 +297,23 @@ alias id "G" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G.var" alias id "G'" = "cic:/CoRN/ftc/PartFunEquality/More_on_Equality/Operations/G'.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_plus.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_inv.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_minus.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_mult.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_nth.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_recip'.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Feq_div'.con" as lemma. (*#* Notice that in the case of division we only need to require boundedness away from zero for one of the functions (as they are equal); thus the two last lemmas are stated in two different ways, as according to the context one or the other condition may be easier to prove. @@ -321,13 +321,13 @@ Notice that in the case of division we only need to require boundedness away fro The restriction of a function is well defined. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FRestr_wd.con" as lemma. (*#* The image of a set is extensional. *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/fun_image_wd.con" as lemma. (* UNEXPORTED End Operations @@ -357,7 +357,7 @@ alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/F.var". (* begin hide *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Nth_Power/P.con" "Nth_Power__" as definition. (* end hide *) @@ -367,13 +367,13 @@ alias id "H" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H.var". alias id "Hf" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/Hf.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero.con" as lemma. alias id "n" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/n.var". alias id "H'" = "cic:/CoRN/ftc/PartFunEquality/Nth_Power/H'.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult.con" as lemma. (* UNEXPORTED End Nth_Power @@ -397,7 +397,7 @@ alias id "Hab" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/Hab.var". (* begin hide *) -inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__". +inline procedural "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/I.con" "Strong_Nth_Power__" as definition. (* end hide *) @@ -405,9 +405,9 @@ alias id "F" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/F.var". alias id "incF" = "cic:/CoRN/ftc/PartFunEquality/Strong_Nth_Power/incF.var". -inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_zero'.con" as lemma. -inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con". +inline procedural "cic:/CoRN/ftc/PartFunEquality/FNth_mult'.con" as lemma. (* UNEXPORTED End Strong_Nth_Power