Thanks. I think it’s better to let HOL maintainers to decide if we should keep the old version (14,700 lines) in “examples”, e.g. “examples/old-probability”. I personally don’t like this idea, because the old version is always accessible from previous HOL releases. And there’re still many redundant probability-related scripts to be cleaned up from the example folder.
Comparing with the proof scripts I get from HVG’s web site, beside a lot of
additions, I actually didn’t change any definition, and almost didn’t change
any theorem name. I believe it should be quite easy to load HVG’s other proof
scripts on top of my current work.
So far I haven’t touched or merged anything in the following scripts:
- normal_rv_hvgScript.sml
- PIE_EXTREALScript.sml
- lebesgue_measure_hvgScript.sml
- integration_hvgScript.sml
- derivative_hvgScript.sml
my future plan is to merge the first 3 (or 2) scripts and abandon last two, as
the last two must be the so-called “Gauge integral” for constructing Lesbegue
measure. (Now with the new carathéodory theorem and the recent ported
“real_topologyScript.sml” in HOL4, we can easily construct Lesbegue measure)
If their original authors (you and Qasim, e.g.) could help, that will be great!
We should finally work out a usable and feature-rich probability theory for
HOL4, and let it become the standard theory library for other applications of
future HOL4 users.
In particular, If you have new theorems that can be added into my current
version of “measureTheory”, I suggest you sending PRs to me for now. All your
work will finally go into HOL official for sure!
Regards,
Chun Tian
> Il giorno 04 gen 2019, alle ore 22:08, Waqar Ahmad <12phdwah...@seecs.edu.pk>
> ha scritto:
>
> Hi Chun,
>
> Great work!!! I briefly went through the proof script and looks good to me.
> However, there are few things that need be discussed before this PR that are
> as follows:
>
> 1) The current version of the measure theory, which is still part of
> HOL-sources, is formalized by taking a real-valued 'measure': ('a -> bool) ->
> real ... whereas, you're working on the version having extreal-valued
> 'measure': ('a -> bool) -> extreal ... Do you have any plan to keep the
> previous version?
>
> 2) My suggestion is to place the real-valued 'measure' theory somewhere in
> HOL/examples and continue further development on extreal-valued 'measure'
> theory.
>
> 3) I've also further extended the Qasim's measure theory by porting more
> necessary defs/thms from Isabelle. I'd like to make them part of future
> measure theory PRs.. Let me know if you have any suggestions regarding it...
>
>
> Feel free to share your thoughts...
>
>
> On Fri, Jan 4, 2019 at 11:01 AM Chun Tian (binghe) <binghe.l...@gmail.com>
> wrote:
> Hi all,
>
> after 4 months’ hard work (mostly using my spare time), among other things,
> finally I have (re)proved Carathéodory's extension theorem [6] under the new
> [0, +Inf] measure theory (from HVG [5]). This is the most general version
> based on semi-ring, also with uniqueness arguments:
>
> [CARATHEODORY_SEMIRING] Theorem
>
> ⊢ ∀m0.
> semiring (m_space m0,measurable_sets m0) ∧ premeasure m0 ⇒
> ∃m.
> measure_space m ∧
> (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
> ((m_space m,measurable_sets m) =
> sigma (m_space m0) (measurable_sets m0)) ∧
> (sigma_finite m0 ⇒
> ∀m'.
> measure_space m' ∧ (m_space m' = m_space m) ∧
> (measurable_sets m' = measurable_sets m) ∧
> (∀s.
> s ∈ measurable_sets m0 ⇒
> (measure m' s = measure m0 s)) ⇒
> ∀s.
> s ∈ measurable_sets m' ⇒
> (measure m' s = measure m s))
>
> The original CARATHEODORY (back to Joe Hurd [1] and A. R. Coble [2]) now
> becomes an easy corollary (as any algebra is also semiring):
>
> [CARATHEODORY] Theorem
>
> ⊢ ∀m0.
> algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
> countably_additive m0 ⇒
> ∃m.
> (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s)) ∧
> ((m_space m,measurable_sets m) =
> sigma (m_space m0) (measurable_sets m0)) ∧ measure_space m
>
> The new “src/probability/measureScript.sml” [3] (7737 lines), starting from
> line 3783 were all newly written by me. The formal proof of
> CARATHEODORY_SEMIRING strictly follows a newer textbook [4, p.38-43] with all
> gaps filled and small mistakes corrected. This single proof has 1600+ lines
> of code...
>
> Before sending this huge PR to HOL official, I still need to merge a few
> other changes from HVG’s version into “src/probability/lebesgueScript.sml”
> and "“src/probability/probabilityScript.sml”, to make sure the PR doesn’t
> remove any existing theorem in these scripts. I also need to fix
> “examples/miller” under the new [0, +inf] measure theory as it needs
> CARATHEODORY to construct the discrete probability measure.
>
> Comments and suggestions are welcome.
>
> Regards,
>
> Chun Tian
> FBK and University of Trento, Italy
>
> [1] Hurd, J.: Formal verification of probabilistic algorithms. (2001).
> [2] Coble, A.R.: Anonymity, information, and machine-assisted proof, (2010).
> [3]
> https://github.com/binghe/HOL/blob/Probability-6/src/probability/measureScript.sml
> [4] Schilling, R.L.: Measures, Integrals and Martingales. Cambridge
> University Press (2005).
> [5] http://hvg.ece.concordia.ca/code/hol/DFT/index.php
> [6] https://en.wikipedia.org/wiki/Carathéodory%27s_extension_theorem
>
> > Il giorno 11 ago 2018, alle ore 19:29, Waqar Ahmad
> > <12phdwah...@seecs.edu.pk> ha scritto:
> >
> > Hi,
> >
> >
> > I have a question about the new version of measureTheory
> > (measure_hvgScript.sml): why the Carathéodory's extension theorem
> > (CARATHEODORY), with all related definitions and lemmas, are removed?
> >
> > [CARATHEODORY]
> > |- ∀m0.
> > algebra (m_space m0,measurable_sets m0) ∧ positive m0 ∧
> > countably_additive m0 ⇒
> > ∃m.
> > (∀s. s ∈ measurable_sets m0 ⇒ (measure m s = measure m0 s))
> > ∧
> > ((m_space m,measurable_sets m) =
> > sigma (m_space m0) (measurable_sets m0)) ∧ measure_space m
> >
> > This is a fundamental result in measure theory. It is one way of arriving
> > at the concept of Lebesgue measure. Without it, how did you manage to
> > define the Lebesgue measure on all Borel sets? (sorry, I’ve lost in the
> > long lebesgue_measure_hvgScript.sml to find out by myself)
> >
> > P. S. If the goal is to just merge the latest version of measureTheory into
> > HOL4, we cannot loose CARATHEODORY, as it’s needed by other work (e.g..
> > HOL’s "examples/miller/prob/probScript.sml”). I’m trying to fix its old
> > proofs using under the new extrealTheory, it seems that each proof is a bit
> > harder to prove, but essentially there’s no difficulty at al, CARATHEODORY
> > must still hold.
> >
> >
> > I'm not sure why the original authors removed CARATHEODORY properties in
> > measure_hvg.sml (maybe its not needed at that time). However, Lebesgue
> > measure (in lebesgue_measure_hvgScript.sml) is formalized using Gauge
> > integral that has been ported from HOL-Light (Multivariate Calculus
> > formalized by J. Horrison). You can find the details of this project from
> > this link http://hvg.ece.concordia.ca/projects/prob-it/pr7.html
> >
> > Let me know if you need any help regarding it.
> >
> >
> >
> > --
> > 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/
>
> _______________________________________________
> 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/
>
signature.asc
Description: Message signed with OpenPGP using GPGMail
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
