Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Chun Tian (binghe)]

The original version of EXTREAL_SUM_IMAGE_INSERT (or the initial part of 
EXTREAL_SUM_IMAGE section) is a mimic of ITSET_INSERT in pred_setTheory without 
any knowledge of extreals:

|- !s. FINITE s ==>
!f x. EXTREAL_SUM_IMAGE f (x INSERT s) =
   f (CHOICE (x INSERT s)) +  EXTREAL_SUM_IMAGE f (REST (x INSERT 
s))

it’s just the original definition, if you replace all appearances of ``(x 
INSERT s)`` with t and see ``FINITE t`` easily holds.

I don’t need to repeat the same basic proof schemas for handling CHOICE and 
REST, once I finished the core proof.

This is mainly an improvement at proof engineering level. All set iteration 
operators should be defined by ITSET, I think it was abandoned because the 
original authors could resolve the issues that I saw and resolved. However, all 
existing definitions (of SUM_IMAGE) are equivalent, for people who doesn’t 
care, my changes are meaningless (except the selective merging of new “add”, 
“sub” but keeping old “inv”).

—Chun

> Il giorno 10 ago 2018, alle ore 00:20, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> 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)  > 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. 

[Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Chun Tian (binghe)]

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

Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)

[Waqar Ahmad via hol-info]

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) 
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) 
> wrote:
>
>> Hi,
>>
>> I just want to see a textbook-correct theory of extended reals. Actually
>> I’m not quite sure how the improved measureTheory