The original version of EXTREAL_SUM_IMAGE_INSERT (or the initial part of EXTREAL_SUM_IMAGE section) is a mimic of ITSET_INSERT in pred_setTheory without any knowledge of extreals:
|- !s. FINITE s ==>
!f x. EXTREAL_SUM_IMAGE f (x INSERT s) =
f (CHOICE (x INSERT s)) + EXTREAL_SUM_IMAGE f (REST (x INSERT
s))
it’s just the original definition, if you replace all appearances of ``(x
INSERT s)`` with t and see ``FINITE t`` easily holds.
I don’t need to repeat the same basic proof schemas for handling CHOICE and
REST, once I finished the core proof.
This is mainly an improvement at proof engineering level. All set iteration
operators should be defined by ITSET, I think it was abandoned because the
original authors could resolve the issues that I saw and resolved. However, all
existing definitions (of SUM_IMAGE) are equivalent, for people who doesn’t
care, my changes are meaningless (except the selective merging of new “add”,
“sub” but keeping old “inv”).
—Chun
> Il giorno 10 ago 2018, alle ore 00:20, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi,
>
> I appreciate the changes that you are making but I'm still not sure that why
> are you re-proving the existing properties that are present in the latest
> version [1]. For instance, EXTREAL_SUM_IMAGE_INSERT is already existed in [1]
> in different forms:
>
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY (THEOREM)
> ------------------------------------------------------
> |- !f s.
> FINITE s ==>
> !e.
> (!x. x IN e INSERT s ==> f x <> NegInf) \/
> (!x. x IN e INSERT s ==> f x <> PosInf) ==>
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
>
>
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_NEG (THEOREM)
> ----------------------------------------------------------
> |- !f s.
> FINITE s ==>
> !e.
> (!x. x IN e INSERT s ==> f x <> NegInf) ==>
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
>
>
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_POS (THEOREM)
> ----------------------------------------------------------
> |- !f s.
> FINITE s ==>
> !e.
> (!x. x IN e INSERT s ==> f x <> PosInf) ==>
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
>
> You can simply merge the latest extrealTheory (extreal_hvgTheory) with the
> HOL sources and that will be it?
>
>
> [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php
> <http://hvg.ece.concordia.ca/code/hol/DFT/index.php>
>
>
> On Thu, Aug 9, 2018 at 5:26 PM Chun Tian (binghe) <binghe.l...@gmail.com
> <mailto:binghe.l...@gmail.com>> wrote:
> 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
>
> <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
>> <mailto: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/>
>>
>
>
>
> --
> 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
