Hi, I’ve done some rework on EXTREAL_SUM_IMAGE (or SIGMA) of extrealTheory.
My general idea is: SIGMA of extreal can only be defined when there’s no mixing
of +inf and -inf in the summation. So I start with the old definition based on
ITSET:
[EXTREAL_SUM_IMAGE_def] Definition
⊢ ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0
And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all its
properties (thus all remaining results should be derived from just this single
theorem without using the original definition):
[EXTREAL_SUM_IMAGE_THM] Theorem
⊢ ∀f.
(SIGMA f ∅ = 0) ∧
∀e s.
((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
a weaker (but practical) corollary is the following one (see the differences of
function f):
[EXTREAL_SUM_IMAGE_INSERT] Theorem
⊢ ∀f s.
(∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
∀e s.
FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
once I got EXTREAL_SUM_IMAGE_THM almost all other SIGMA theorems either has
trivial proofs or their existing proofs still work. But the proof of above
theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3 for -inf), I
show the ones for +inf here:
[lemma1]
⊢ ∀f s.
FINITE s ⇒
∀x b.
(∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
(ITSET (λe acc. f e + acc) (x INSERT s) b =
ITSET (λe acc. f e + acc) (s DELETE x)
((λe acc. f e + acc) x b))
[lemma2]
⊢ ∀f s.
(∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf
[lemma3]
⊢ ∀b f x s.
(∀y. y ∈ x INSERT s ⇒ f y ≠ PosInf) ∧ b ≠ PosInf ∧ FINITE s ⇒
(ITSET (λe acc. f e + acc) (x INSERT s) b =
(λe acc. f e + acc) x (ITSET (λe acc. f e + acc) (s DELETE x) b))
These proofs were learnt from similar proofs in pred_setTheory and digged into
the nature of extreal. Noticed that they are all lemmas about ITSET
(pred_setTheory), λ-function (λe acc. f e + acc), and a extreal `b`, and once I
set `b = 0` the whole ITSET just become SIGMA for extreals. Thus these proofs
were done even before EXTREAL_SUM_IMAGE is defined.
Then I re-used most proofs from the new version of extrealTheory, with almost
all new theorems originally in HOL4’s version preserved (sometimes re-proved).
The new “extrealScript.sml” can be found here [1]. Now I have a satisfied
extended real theory and have switched to merge the new measureTheory (with
measure type ``:‘a set -> extreal`` instead of old ``:’a set -> real``) into
HOL4.
[1]
https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml
Feel free to comment, I’ll be appreciated if you could let the original authors
know these changes.
Regards,
Chun
> Il giorno 07 ago 2018, alle ore 18:35, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi,
>
> You're welcome to suggest improvements.. maybe step forward to put the
> extrealTheory on right footings.. I'll be more than happy, if I could be of
> any help to you at any point.
>
> On Tue, Aug 7, 2018 at 11:56 AM Chun Tian (binghe) <binghe.l...@gmail.com
> <mailto:binghe.l...@gmail.com>> wrote:
> Hi,
>
> I just want to see a textbook-correct theory of extended reals. Actually I’m
> not quite sure how the improved measureTheory (of extreal) is connected with
> the improved extrealTheory (with different definitions on +, -, inv). What I
> observed so far is, the new measureTheory does use some new theorems from the
> new extrealTheory, but those theorems should be also proved in the old
> version of extrealTheory.
>
> Of course the consequent formalization must be consistent, as long as we
> don’t use axioms and cheats in the proof scripts. The biggest enemy in
> formalizations is the “wrong” definition, a correctly proved theorem based on
> wrongly defined things would be useless. (but here it’s not that “wrong”
> actually, because in probability measure there’s no mixing of PosInf and
> NegInf at all; on the other side I’m not sure how the changes in
> “extreal_inv” affects the new measureTheory.)
>
>> Skipping the PosInf + a = PosInf requires to prove the termination of
>> "EXTREAL_SUM_IMAGE" function as it has been done.
>
>
> I don’t think so. The termination of both old and new definition comes from
> the finiteness of sets involved. A proper subset of finite set always has
> smaller (by one) cardinality (CARD_PSUBSET), as shown in the following proof
> scripts:
>
> (WF_REL_TAC `measure (CARD o SND)` THEN
> METIS_TAC [CARD_PSUBSET, REST_PSUBSET])
>
> Actually under the new definition of ``extreal_add``, we can’t prove the
> following theorem (EXTREAL_SUM_IMAGE_THM in old version):
>
> ``!f. (EXTREAL_SUM_IMAGE f {} = 0) /\
> (!e s. FINITE s ==>
> (EXTREAL_SUM_IMAGE f (e INSERT s) =
> f e + EXTREAL_SUM_IMAGE f (s DELETE e)))``,
>
> why? because there could be mixing of PosInf and NegInf returned by the
> function f, and the resulting sum is not defined. The proof of above theorem
> used to depend on COMMUTING_ITSET_RECURSES (pred_setTheory):
>
> !f e s b. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==>
> (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b))
>
> but now the antecedent "(!x y z. f x (f y z) = f y (f x z))” is not
> satisfiable any more. (i.e. can’t be directly proved by “add_assoc” and
> “add_comm” of extreals)
>
> —Chun
>
>> Il giorno 07 ago 2018, alle ore 17:27, Waqar Ahmad <12phdwah...@seecs.edu.pk
>> <mailto:12phdwah...@seecs.edu.pk>> ha scritto:
>>
>> Hi,
>>
>> let me make a little more comments to the formalized extended reals.
>>
>> I’m actually reviewing the improved version of extrealTheory as part of [1]
>> (the link "Required Theories”). I don’t know if there’re further updates,
>> but comparing with the existing definitions shipped in HOL4, I think the new
>> version fixed some issue yet introduced more others. For example, the
>> definition of extreal_inv now allows division by zero:
>>
>> val extreal_inv_def = Define
>> `(extreal_inv NegInf = Normal 0) /\
>> (extreal_inv PosInf = Normal 0) /\
>> (extreal_inv (Normal x) = (if x = 0 then PosInf else Normal (inv x)))`;
>>
>> This is not aligned with any textbook, and it doesn’t make sense to let
>> ``(Normal _) / 0 = PosInf``, because I think PosInf and NegInf should have
>> equal positions in the formal theory. It may look like PosInf is more
>> important than NegInf (as measureTheory only uses PosInf) but for the theory
>> of extended real itself, they should be of the same importance.
>>
>> Actually, both version of extrealtheory are developed by the original
>> authors (maybe at the same time) but for some reason the version that is
>> little more flexible is made part of HOL repositories. The source files that
>> you're referring are the latest one. The major difference is that the
>> measure can now be of type extreal, which is essential to reason about
>> Lebesgue integral properties in particular. I'm not sure what made you
>> worry about the less use of NegInf. Is this makes the consequent
>> formalization inconsistent?
>>
>>
>> The other thing is, once it’s not allowed to have “PosInf + NegInf” with a
>> defined value, the arithmetic of extended reals are not commutative and
>> associative without further restrictions (e.g. mixing of PosInf and NegInf
>> must be disabled, as the resulting summation has no definition). The
>> consequence is, summation over finite sets are hard to formalize now,
>> because theorems like COMMUTING_ITSET_RECURSES (pred_setTheory) depends on
>> the commutativity of summation. But syntactically, the following (old)
>> definition should still be true:
>>
>> val EXTREAL_SUM_IMAGE_DEF = new_definition
>> ("EXTREAL_SUM_IMAGE_DEF",
>> ``EXTREAL_SUM_IMAGE f s = ITSET (\e acc. f e + acc) s (0:extreal)``);
>>
>> because re-proving deep lemmas about ITSET is not that easy. The improved
>> version now defines EXTREAL_SUM_IMAGE from grounds:
>>
>> val EXTREAL_SUM_IMAGE_def =
>> let open TotalDefn
>> in
>> tDefine "EXTREAL_SUM_IMAGE"
>> `EXTREAL_SUM_IMAGE (f:'a -> extreal) (s: 'a -> bool) =
>> if FINITE s then
>> if s={} then 0:extreal
>> else f (CHOICE s) + EXTREAL_SUM_IMAGE f (REST s)
>> else ARB`
>> (WF_REL_TAC `measure (CARD o SND)` THEN
>> METIS_TAC [CARD_PSUBSET, REST_PSUBSET])
>> end;
>>
>> but I think it didn’t solve any problem, just making many related theorems
>> harder to be proved.
>>
>> Skipping the PosInf + a = PosInf requires to prove the termination of
>> "EXTREAL_SUM_IMAGE" function as it has been done. Many essential arithmetic
>> properties has been proved for extreal datatype that surely improved the
>> non-trivial reasoning, which you can see in the measure and probability
>> theory formalization. I suppose that the other arithmetic properties on
>> extreal type could be easily infer from the existing properties?
>>
>> Finally, even in Isabelle/HOL, if I read the related scripts
>> (src/HOL/Library/Extended_Real.thy) correctly, the summation of extended
>> reals is also “wrong", i.e. it allows "\<infinity> + -\<infinity> =
>> \<infinity>”.
>>
>> function plus_ereal where
>> "ereal r + ereal p = ereal (r + p)"
>> | "\<infinity> + a = (\<infinity>::ereal)"
>> | "a + \<infinity> = (\<infinity>::ereal)"
>> | "ereal r + -\<infinity> = - \<infinity>"
>> | "-\<infinity> + ereal p = -(\<infinity>::ereal)"
>> | "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
>> proof goal_cases
>> case prems: (1 P x)
>> then obtain a b where "x = (a, b)"
>> by (cases x) auto
>> with prems show P
>> by (cases rule: ereal2_cases[of a b]) auto
>> qed auto
>> termination by standard (rule wf_empty)
>>
>> However, Isabelle/HOL introduced another type (nonnegative extended reals,
>> ennreal) for uses of Probability. With such “half” extended reals all
>> formalization difficulties disappeared but it’s a huge wasting of proving a
>> large piece of arithmetic laws for a new numerical type, and it’s far from
>> standard text books.
>>
>> Comments are welcome.
>>
>> —Chun
>>
>> [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php
>> <http://hvg.ece.concordia.ca/code/hol/DFT/index.php>
>>> Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad
>>> <12phdwah...@seecs.edu.pk <mailto:12phdwah...@seecs.edu.pk>> ha scritto:
>>>
>>> Hi Chun,
>>>
>>> I'm not sure about your potential conflict question but we are now using an
>>> improved definition of "extreal_add_def"
>>>
>>> val extreal_add_def = Define`
>>> (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>>> (extreal_add (Normal _) a = a) /\
>>> (extreal_add b (Normal _) = b) /\
>>> (extreal_add NegInf NegInf = NegInf) /\
>>> (extreal_add PosInf PosInf = PosInf)`;
>>>
>>> This will rule out the possibility of PosInf + a= PosInf... We do have a
>>> plan to update the probability theory to the latest version in the near
>>> future (Speaking on the behalf of original authors).
>>>
>>>
>>>
>>> On Sun, Aug 5, 2018 at 11:14 AM Chun Tian <binghe.l...@gmail.com
>>> <mailto:binghe.l...@gmail.com>> wrote:
>>> Hi,
>>>
>>> the version of “extreal” (extended real numbers) in latest HOL4 has a wrong
>>> definition for sum:
>>>
>>> val _ = Hol_datatype`extreal = NegInf | PosInf | Normal of real`;
>>>
>>> val extreal_add_def = Define`
>>> (extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>>> (extreal_add PosInf a = PosInf) /\
>>> (extreal_add a PosInf = PosInf) /\
>>> (extreal_add NegInf b = NegInf) /\
>>> (extreal_add c NegInf = NegInf)`;
>>>
>>> according to this definition, one could prove the wrong statement ``PosInf
>>> + NegInf = NegInf + PosInf = PosInf``, e.g.
>>>
>>>> PROVE [extreal_add_def] ``extreal_add PosInf NegInf = PosInf``;
>>> Meson search level: ..
>>> val it = ⊢ PosInf + NegInf = PosInf: thm
>>>
>>> P. S. the original authors have fixed this issue in their latest version of
>>> probability theories, which I’m now working on merging them into HOL4.
>>>
>>> What I don’t quite understand here is, shouldn’t one also prove that
>>> ``PosInf + NegInf = NegInf + PosInf = NegInf``, as the last two lines of
>>> extreal_add_def stated, but it turns out that this is not true (PROVE
>>> command doesn’t return):
>>>
>>>> PROVE [extreal_add_def] ``extreal_add NegInf PosInf = NegInf``;
>>> Meson search level: .....................Exception- Interrupt raised
>>>
>>> of course it can’t be proved, because otherwise it means ``PosInf =
>>> NegInf``, contradicting the axioms generated by Hol_datatype, then the
>>> whole logic would be inconsistent.
>>>
>>> But given the fact that above definition can be directly accepted by Define
>>> command, does HOL internally resolve potential conflicts by putting a
>>> priority on each sub-clauses based on their appearance order?
>>>
>>> Regards,
>>>
>>> Chun Tian
>>>
>>> ------------------------------------------------------------------------------
>>> Check out the vibrant tech community on one of the world's most
>>> engaging tech sites, Slashdot.org <http://slashdot.org/>!
>>> http://sdm.link/slashdot
>>> <http://sdm.link/slashdot>_______________________________________________
>>> hol-info mailing list
>>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
>>>
>>>
>>> --
>>> Waqar Ahmad, Ph.D.
>>> Post Doc at Hardware Verification Group (HVG)
>>> Department of Electrical and Computer Engineering
>>> Concordia University, QC, Canada
>>> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>>> <http://save.seecs.nust.edu.pk/waqar-ahmad/>
>>>
>>
>>
>>
>> --
>> Waqar Ahmad, Ph.D.
>> Post Doc at Hardware Verification Group (HVG)
>> Department of Electrical and Computer Engineering
>> Concordia University, QC, Canada
>> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
>> <http://save.seecs.nust.edu.pk/waqar-ahmad/>
>
>
> --
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware Verification Group (HVG)
> Department of Electrical and Computer Engineering
> Concordia University, QC, Canada
> Web: http://save.seecs.nust.edu.pk/waqar-ahmad/
> <http://save.seecs.nust.edu.pk/waqar-ahmad/>
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
