Hi Michael, thanks for your suggestions. I'll redefine ext_suminf to make sure it's only specified on positive functions (usually a measure of sets). The required changes are minimal, as now all proofs trying to expand `ext_suminf` already have already added extra proofs to show the involved functions are positive. (This fact also indicates that the previous version sometimes do not fully reflect their textbook proofs as a little part can be omitted.)
I'll submit a new PR for this change ASAP.
--Chun
Il 20/09/19 03:03, Norrish, Michael (Data61, Acton) ha scritto:
> Fair enough. It seems clear that this is not a huge problem (using a
> function such as this outside of its intended domain is a bad idea), but on
> the other hand, it also seems clear that needlessly having it return the
> wrong value is a bug.
>
> Having said all that, getting suminf (\x. -1) to return -1 doesn't seem much
> of a win: the sum of an infinite sequence of -1s is hardly -1.
>
> I think it would be better style to use new_specification so as to avoid
> giving a specific value when the argument is not always positive.
>
> Michael
>
>
> On 20/9/19, 09:51, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
>
> In fact, even for arbitrary functions with both positive and negative
> values, if the partial sum ever reached +/-Inf, further adding finite values
> on the other side cannot “pull” the result back to “normal”. For instance,
> suppose at some moment the partial sum is +inf, adding any normal reals will
> not change it, it’s then not allowed to add -Inf on it, because under the
> textbook definition of `+`, PosInf + NegInf is unspecified. Thus, in some
> sense the suminf of possible limiting values has a very different behavior
> with the real version.
>
> Chun
>
> Inviato da iPad
>
> > Il giorno 20 set 2019, alle ore 01:33, Chun Tian (binghe)
> <binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > The extreal version of `suminf` is only “correct” and equivalent with
> the real version when the involved function is positive - the partial sum is
> mono-increasing. Its relatively simple definition serves the current need (in
> measure and probability theories). Fully mimicking the real version requires
> a (full) porting of seqTheory (and limTheory, netsTheory, eventually
> metricTheory) to extreals, which is an almost impossible task in my opinion.
> >
> > Besides, I think it’s also not needed to do so, because if the sum
> limit never reaches +Inf, one can just reduce the work back to the ‘suminf’
> of reals. On the hand, If the partial sum ever reached +Inf, assuming it’s
> monotonic, then the limit value must be also +Inf, it’s reduced to a finite
> sum.
> >
> > Chun
> >
> >> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61,
> Acton) <michael.norr...@data61.csiro.au> ha scritto:
> >>
> >> The definition of suminf over the reals (in seqTheory) is completely
> different; is it clear that the extreal version can't mimic the original?
> >>
> >> Michael
> >>
> >> On 18/9/19, 06:18, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote:
> >>
> >> Hi,
> >>
> >> I occasionally found that HOL's current definition of ext_suminf
> (extrealTheory) has a bug:
> >>
> >> [ext_suminf_def] Definition
> >> ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 𝕌(:num))
> >>
> >> The purpose of `suminf f` is to calculate an infinite sum: f(0) +
> f(1) + .... To make the resulting summation "meaningful", all lemmas about
> ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how
> it's used in all applications. For instance, one lemma says, if f is
> positive, so is `suminf f`:
> >>
> >> [ext_suminf_pos] Theorem
> >> ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
> >>
> >> However, I found that the above lemma can be proved even without
> knowing anything of `f`, see the following proofs:
> >>
> >> Theorem ext_suminf_pos_bug :
> >> !f. 0 <= ext_suminf f
> >> Proof
> >> RW_TAC std_ss [ext_suminf_def]
> >>>> MATCH_MP_TAC le_sup_imp'
> >>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
> >>>> Q.EXISTS_TAC `0` >> BETA_TAC
> >>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
> >> QED
> >>
> >> where [le_sup_imp'] is a version of [le_sup_imp] before applying
> IN_APP:
> >>
> >> [le_sup_imp'] Theorem
> >>
> >> ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
> >>
> >> For the reason, ext_suminf is actually calculating the sup of the
> following values:
> >>
> >> 0
> >> f(0)
> >> f(0) + f(1)
> >> f(0) + f(1) + f(2)
> >> ...
> >>
> >> The first line (0) comes from `count 0 = {}` where `0 IN
> univ(:num)`, then SUM_IMAGE f {} = 0.
> >>
> >> Now consider f = (\n. -1), the above list of values are: 0, -1, -2,
> -3 .... But since the sup of a set containing 0 is at least 0, the `suminf
> f` in this case will be 0 (instead of the correct value -1). This is why `0
> <= suminf f` holds for whatever f.
> >>
> >> I believe Isabelle's suminf (in Extended_Real.thy) has the same
> problem (but I can't find its definition, correct me if I'm wrong here), i.e.
> the following theorem holds even without the "assumes":
> >>
> >> lemma suminf_0_le:
> >> fixes f :: "nat ⇒ ereal"
> >> assumes "⋀n. 0 ≤ f n"
> >> shows "0 ≤ (∑n. f n)"
> >> using suminf_upper[of f 0, OF assms]
> >> by simp
> >>
> >> The solution is quite obvious. I'm going to fix HOL's definition of
> ext_suminf with the following one:
> >>
> >> val ext_suminf_def = Define
> >> `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;
> >>
> >> That is, using `SUC n` intead of `n` to eliminate the fake base case
> (0). I believe this change only causes minor incompatibilities.
> >>
> >> Any comment?
> >>
> >> Regards,
> >>
> >> Chun Tian
> >>
> >>
> >>
> >>
> >> _______________________________________________
> >> hol-info mailing list
> >> hol-info@lists.sourceforge.net
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
