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