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
>
> Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad <
> 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> 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_______________________________________________
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> 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/
>
>
>
--
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/
------------------------------------------------------------------------------
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
