Beside, there’re two other benefits: 1) Hurd’s original elegant long proof of CARATHEODORY is now preserved in old_measureTheory. 2) Coble’s “dining cryptographers” work (example/diningcryptos) can also be fixed (in the future) under old_measureTheory and old_probabilityTheory, because his work also doesn’t use anything from lebesgueTheory and extrealTheory (also these scripts were included).
—Chun > Il giorno 07 gen 2019, alle ore 16:19, Chun Tian (binghe) > <binghe.l...@gmail.com> ha scritto: > > Hi Micheal, > > thanks for your trust. Now I’ve done the following solution for preserving > some backwards compatibilities: > > My goal is to make minimal efforts to make sure that Hurd's Miller-Rabin work > (examples/miller) can still build after my PR. I found that, the code in > “miller” depends only on “measureTheory” and “probabilityTheory” but > “lebesgueTheory”. Thus I thought maybe I can keep a minimal copy of just the > old “measureTheory” and “probabilityTheory” with all extreal and lebesgue > stuff removed. > > This is indeed possible: 90% of the current probabilityTheory (1208 of 1348 > lines) does not use “lebesgueTheory” at all. And the only part in the current > “measureTheory” which depends on extended reals are those related to “Borel” > measurable sets, which is not needed by Miller-Rabin example. > > The result is: I kept the old version of measureTheory and probabilityTheory > with minimal deletions. Now they’re at > “src/probability/old_measureScript.sml” and > “src/probability/old_probabilityScript.sml. And I've successfully fixed the > Miller-Rabin example using these “old” scripts. > > The fact that these two old scripts (formalizing a minimal abstract > probabilityTheory based on real-valued measureTheory) can still support the > Miller-Rabin example, shows that it’s worthy to keep them in latest HOL4, I > think, unless one day someone completely ported Hurd’s code into the > forthcoming new probabilityTheory. > > The working codebase with all above ideas implemented is at my working branch > [1] > > Regards, > > Chun Tian > > [1] https://github.com/binghe/HOL/tree/Probability-6/ > >> Il giorno 07 gen 2019, alle ore 01:24, michael.norr...@data61.csiro.au ha >> scritto: >> >> I am happy to let those most affected by or interested in the PR to discuss >> the best way forward, here, or on the hol-developers mailing list, or >> privately. >> >> My main concern would be to minimise unnecessary backwards >> incompatibilities. As someone who introduces the most incompatibilities from >> release to release, it is clear that I don't view this as an absolute >> requirement, so I'm happy to trust the interested parties to come to an >> appropriate agreement about the right way forward. >> >> Michael >> >> On 5/1/19, 09:02, "Chun Tian (binghe)" <binghe.l...@gmail.com> wrote: >> >> 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/ >>> >> >> >> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net >> https://lists.sourceforge.net/lists/listinfo/hol-info >
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
