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