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.
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.
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
> <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://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/>
>
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
