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
On Thu, Aug 9, 2018 at 5:26 PM Chun Tian (binghe) <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
>
> 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> 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>
> 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/
>
>
>
--
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
