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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
