Re: [Hol-info] Best way to conduct a generalized IMP_TRANS
Hi Haitao,
You can introduce the conjunction among the antecedents as:
val GEN_IMP_TRANS_conj = (REWRITE_RULE [GSYM satTheory.AND_IMP]
GEN_IMP_TRANS);
val GEN_IMP_TRANS_conj =
⊢ ∀P Q R S. (∀x. P x ⇒ Q (R x)) ∧ (∀x. Q x ⇒ S x) ⇒ ∀x. P x ⇒ S (R x):
thm
On Tue, Mar 19, 2019 at 5:30 AM Haitao Zhang wrote:
> I have two assumptions both in implicative forms with universal
> quantification. I would like to obtain an MP in the spirit of the following
> theorem:
>
> val GEN_IMP_TRANS = store_thm("GEN_IMP_TRANS",
> ``!P Q R S. (!x. P x ==> Q (R x)) ==> (!x. Q x ==> S x) ==> (!x. P x
> ==> S (R x))``,
> metis_tac []);
>
> However if I use drule with the theorem the antecedent of the resolution
> is put into a conjunction (the last forall is moved left and the antecedent
> becomes (!x. Q x ==> S x) /\ P x') and can not be used to resolve against
> the second assumption. Any suggestions?
>
> Thanks,
> Haitao
> ___
> 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
Re: [Hol-info] 0 / 0 = 0 ???
Hi Chun, I run some experiments so to check if it is violating any fundamental rule. So far it went good. On Tue, Feb 19, 2019 at 5:31 PM Chun Tian (binghe) wrote: > Some further updates: > > With my last definition of `extreal_div`, I still have: > > |- !x. x / 0 = ARB > > and > > |- 0 / 0 = ARB > > trivially holds (by definition). This is still not satisfied to me. > > Now I tried the following new definition which looks more reasonable: > > val extreal_div_def = Define >`extreal_div x y = if y = Normal 0 then > (@x. (x = PosInf) \/ (x = NegInf)) > else extreal_mul x (extreal_inv y)`; > > literally, it says anything (well, let's ignore zero) divides zero is > equal to either +Inf or -Inf. But actually the choice of +Inf/-Inf is > irrelevant, as the sole purpose is to prevent any theorem like ``|- x / > 0 = y`` being proved, in which y is a literal extreal. For example, if I > try to prove ``!x. x / 0 = ARB``: > > (* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't > be proved, e.g. > val test_div = prove ( >`!x. extreal_div x (Normal 0) = ARB`, > RW_TAC std_ss [extreal_div_def] > >> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))` > >- RW_TAC std_ss [] > >> MATCH_MP_TAC SELECT_ELIM_THM > >> RW_TAC std_ss [] (* 3 gubgoals *) >NegInf = ARB > >PosInf = ARB > >∃x. (x = PosInf) ∨ (x = NegInf)); > *) > > at the end I got 3 subgoals like above. I *believe*, no matter what > value I put instead of ARB, at least one of the subgoals must be false. > Thus the theorem should be unprovable. (am I right?) > > Can I adopt this new definition of `extreal_div` in the future? Any > objection or suggestion? > > --Chun > > Il 15/02/19 23:37, Chun Tian (binghe) ha scritto: > > I'm going to use the following definition for `extreal_div`: > > > > (* old definition of `extreal_div`, which allows `0 / 0 = 0` > > val extreal_div_def = Define > >`extreal_div x y = extreal_mul x (extreal_inv y)`; > > > >new definition of `extreal_div`, excluding the case `0 / 0`: *) > > val extreal_div_def = Define > >`extreal_div x y = if (y = Normal 0) then ARB > > else extreal_mul x (extreal_inv y)`; > > > > previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as > > antecedent, which makes perfectly senses. > > > > P.S. the division of extended reals in HOL4 are not used until the > > statement and proof of Radon-Nikodým theorem, then the conditional > > probability. > > > > --Chun > > > > Il 15/02/19 17:39, Mark Adams ha scritto: > >> I think there is definitely an advantage in keeping ``x/y`` undefined > >> (even granted that it will always be possible to prove ``?y. x/0 = y``), > >> namely that it means that your proofs are much more likely to directly > >> translate to other formalisms of real numbers where '/' is not total. > >> > >> Of course there is also a disadvantage, in that it makes proof harder. > >> But then, arguably, being forced to justify that we are staying within > >> the "normal" domain of the function is probably a good thing (in a > >> similar way as being forced to conform to a type system is a good > >> thing). I understand that, historically, it is this disadvantage of > >> harder proofs that was the reason for making ``0/0=0`` in HOL. It's > >> much easier for automated routines if they don't have to consider side > >> conditions. > >> > >> Mark. > >> > >> On 15/02/2019 08:56, Chun Tian (binghe) wrote: > >>> Thanks to all kindly answers. > >>> > >>> Even I wanted ``0 / 0 = 0`` to be excluded from at least > >>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I > >>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's > >>> going to happen, I do case analysis instead. > >>> > >>> --Chun > >>> > >>> Il 14/02/19 18:12, Konrad Slind ha scritto: > It's a deliberate choice. See the discussion in Section 1.2 of > > > http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692=rep1=pdf > > > > > On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) > mailto:binghe.l...@gmail.com>> wrote: > > Hi, > > in HOL's realTheory, division is defined by multiplication: > > [real_div] Definition > > ⊢ ∀x y. x / y = x * y⁻¹ > > and zero multiplies any other real number equals to zero, which is > definitely true: > > [REAL_MUL_LZERO] Theorem > > ⊢ ∀x. 0 * x = 0 > > However, above two theorems together gives ``0 / 0 = 0``, as shown > below: > > > REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div); > val it = ⊢ 0 / 0 = 0: thm > > How do I understand this result? Is there anything "wrong"? > > (The same problems happens also in extrealTheory,
Re: [Hol-info] HOL's new measure theory (in progress)
Hi Chun,
>
> 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.
>
> Ideally, both these measures (real and extreal-valued) should be part of
one script as in Isabelle's measure theory. However, in our case, a fair
argument would be to put the efforts on the new measure theory since it has
more potential for future development compared to the old one. Since, the
old version can be easily accessible from HOL-releases I think there is no
need to drag it along. Please, go ahead and make this PR.
> 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.
>
> Its a good way forward and I'm available for it. Contact me freely when
you need me.
> 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!
>
> Sure.. that will be good!
> 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 ⇒
Re: [Hol-info] assumption matching in SPLIT_LT
Hi,
Suppose, I have 3 subgoals where first 2 subgoals can be proved by apply
tac1 and the third goal may takes some set of tacts, say tac2, tac3...
Is it possible that I can use SPLIT_LT in a way such that first two
subgoals are discharged by applying tac1 and I only end up proving the
third subgoal?
On Fri, Sep 21, 2018 at 3:00 AM wrote:
> match_mp_tac is indeed causing an error because it is not applicable in
> the other subgoals.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Friday, 21 September 2018 at 08:39
> *To: *"konrad.sl...@gmail.com"
> *Cc: *hol-info
> *Subject: *Re: [Hol-info] assumption matching in SPLIT_LT
>
>
>
> Hi,
>
>
>
> Thanks for the reply. I think the match_mp_tac is causing the error since
> if I only pop the assumption the tactic works on first subgoal.
>
>
>
> rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
>
>
>
>
>
> > val it =
>
>
>
>SG3
>
>
>
> A1 ==> B1
>
>
>
>
>
>SG2
>
>
>
> A1 ==> B1
>
>
>
>
>
>(A1 ==> B1) ==> B1
>
>
>
>
>
> 3 subgoals
>
>: proof
>
>
>
>
>
>
>
>
>
> On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind
> wrote:
>
> Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
> first one is the pop_assum match_mp_tac succeeding. So the proof is failing
> before it gets to the THEN_LT.
>
>
>
> Konrad.
>
>
>
>
>
> On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
> hol-info@lists.sourceforge.net> wrote:
>
> Hi,
>
>
>
> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
> facing error with assumption matching. For instance, I've a proof goal of
> this form:
>
>
>
> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>
>
>
> rw []
>
> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
> ALLGOALS (rw[]))
>
>
>
> I'm getting following matching error...
>
>
>
> Exception raised at Tactic.MATCH_MP_TAC:
>
> No match
>
> Exception-
>
>HOL_ERR
>
> {message = "No match", origin_function = "MATCH_MP_TAC",
>
> origin_structure = "Tactic"} raised
>
>
>
> It works otherwise for handling them individually...
>
> --
>
> 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
>
--
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
Re: [Hol-info] assumption matching in SPLIT_LT
Hi,
Thanks for the reply. I think the match_mp_tac is causing the error since
if I only pop the assumption the tactic works on first subgoal.
rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
> val it =
SG3
A1 ==> B1
SG2
A1 ==> B1
(A1 ==> B1) ==> B1
3 subgoals
: proof
On Thu, Sep 20, 2018 at 6:21 PM Konrad Slind wrote:
> Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
> first one is the pop_assum match_mp_tac succeeding. So the proof is failing
> before it gets to the THEN_LT.
>
> Konrad.
>
>
> On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
> hol-info@lists.sourceforge.net> wrote:
>
>> Hi,
>>
>> I'm trying to use the tactical SPLIT_LT to multiple subgoals. However,
>> I'm facing error with assumption matching. For instance, I've a proof goal
>> of this form:
>>
>> `(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
>>
>> rw []
>> \\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
>> ALLGOALS (rw[]))
>>
>> I'm getting following matching error...
>>
>> Exception raised at Tactic.MATCH_MP_TAC:
>> No match
>> Exception-
>>HOL_ERR
>> {message = "No match", origin_function = "MATCH_MP_TAC",
>> origin_structure = "Tactic"} raised
>>
>> It works otherwise for handling them individually...
>> --
>> 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
[Hol-info] assumption matching in SPLIT_LT
Hi,
I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:
`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))
I'm getting following matching error...
Exception raised at Tactic.MATCH_MP_TAC:
No match
Exception-
HOL_ERR
{message = "No match", origin_function = "MATCH_MP_TAC",
origin_structure = "Tactic"} raised
It works otherwise for handling them individually...
--
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
Re: [Hol-info] Prove BIGUNION (IMAGE f 핌(:num)) by induction on (count n)?
Hi, I'd like to try converting the equality to SUBSET form by using Pred_setTheory.SUBSET_ANTISYM (THEOREM) --- |- !s t. s SUBSET t /\ t SUBSET s ==> (s = t) and then use property like topology_hvgTheory.BIGUNION_MONO_IMAGE (THEOREM) [1] |- (!x. x IN s ==> f x SUBSET g x) ==> BIGUNION (IMAGE f s) SUBSET BIGUNION (IMAGE g s) This way you can figure out the relation between 'f' and 'g'... [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php On Sat, Sep 15, 2018 at 4:27 PM Chun Tian (binghe) wrote: > Hi, > > I have a need to prove that, for two certain functions f, (g :num->’a set) > > BIGUNION (IMAGE f 핌(:num)) = BIGUNION (IMAGE g 핌(:num)) > > Following its informal proof, it seems only possible to prove the > following result (by induction) first: > > !(n :num). BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count > n)) > > but once I got this intermediate result, how I can reach to the original > statement? Is there any other assumption needed for going from finite to > infinite union? > > Thanks, > > Chun Tian > > ___ > 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
[Hol-info] Partial Order for Set Supremum
Hi,
Lately, I proved the equivalence of two supremum functions as:
|- !P.
(!x y. P x /\ P y ==> x <= y) /\ P <> {} ==>
(BIGSUP $<= P P = SOME (sup P)): thm
where BIGSUP is defined in [1] and "sup" can be found in HOL realTheory.
I'm not sure why the premise (!x y. P x /\ P y ==> x <= y) is required
mainly due to the fact that the binary relation $<= implicitly maintains
the partial order in a set. This can be easily proved for any set:
rest_WeakOrder_le;
val it = |- !P. rest_WeakOrder P $<=: thm
Is there any way to discharge the first premise or can be inferred from the
lemma "rest_WeakOrder_le"?
[1] (
https://github.com/HOL-Theorem-Prover/HOL/blob/master/examples/separationLogic/src/latticeScript.sml
)
latticeTheory.BIGSUP_def;
val it = |- !f D M. BIGSUP f D M = OPTION_SELECT (\s. IS_SUPREMUM f D M s):
thm
--
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
Re: [Hol-info] Lazy list: Stream in coinduction
Great!. This worked perfectly and solved some persistent issues...:) On Tue, Aug 28, 2018 at 12:54 AM wrote: > Don’t use abbreviations before starting your proof: it’s muddling your > quantifications. > > Instead, use > >!s. (?s0. s = StreamD s0) /\ P s ==> streams A s > > as your goal and follow with > >ho_match_mp_tac streams_coind >> dsimp[] > > You will then end up with > > > >∀s0. > >P (StreamD s0) ⇒ > >∃a s0'. (StreamD s0 = a:::StreamD s0') ∧ a ∈ A ∧ P (StreamD s0') > > as your goal. > > Michael > > > > *From: *Waqar Ahmad via hol-info > *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Tuesday, 28 August 2018 at 13:53 > *To: *hol-info > *Subject: *[Hol-info] Lazy list: Stream in coinduction > > > > Hi, > > > > I see that the coinduction scheme obtained from coinductively definition > predicate, in some cases, may require lazy list must not be LNIL. For > instance, > > using the LUNFOLD, I've defined the stream function mainly to rule out the > LNIL case as: > > > > |- StreamD xs = LUNFOLD (\n. SOME (THE (LTL n),THE (LHD n))) xs: thm > > > > However, when I use it to for proving some useful properties over streams, > which is defined coinductively as: > > > > |- !A a s. a IN A /\ streams A s ==> streams A (a:::s): thm > > > > and the resulting coinductive scheme produced is: > > > > |- !A streams'. > > (!a0. streams' a0 ==> ?a s. (a0 = a:::s) /\ a IN A /\ streams' > s) ==> > > !a0. streams' a0 ==> streams A a0: thm > > > > Suppose, I've a property of form: > > > > `P (StreamD s) ==> streams A (StreamD s)` > > > > By abbreviating the 'xs = StreamD s', I applied the coinduction scheme and > ends up: > > > > ?a xs'. (xs = a:::xs') /\ a IN A /\ Abbrev (xs' = xs) /\ P xs' > > > > 0. Abbrev (xs = StreamD s) > > 1. P xs > > > > The first conjunction can be easily made true by using `LHD xs` and `LTL > xs`. This also require that the lazy list 'xs' should not be LNIL, which > can also be easily inferred (from premise 0). However, this makes Abbrev > (LTL xs = xs) false.. > > > > Is there any way that I can use the coinduction scheme directly such that > I can have > > > >∃a xs'. (StreamD xs = a:::xs') ∧ a ∈ A ∧ P xs' > > > > 0. P xs > > > > > > > > > > > > > > > > > -- > > 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 > -- 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
[Hol-info] Lazy list: Stream in coinduction
Hi, I see that the coinduction scheme obtained from coinductively definition predicate, in some cases, may require lazy list must not be LNIL. For instance, using the LUNFOLD, I've defined the stream function mainly to rule out the LNIL case as: |- StreamD xs = LUNFOLD (\n. SOME (THE (LTL n),THE (LHD n))) xs: thm However, when I use it to for proving some useful properties over streams, which is defined coinductively as: |- !A a s. a IN A /\ streams A s ==> streams A (a:::s): thm and the resulting coinductive scheme produced is: |- !A streams'. (!a0. streams' a0 ==> ?a s. (a0 = a:::s) /\ a IN A /\ streams' s) ==> !a0. streams' a0 ==> streams A a0: thm Suppose, I've a property of form: `P (StreamD s) ==> streams A (StreamD s)` By abbreviating the 'xs = StreamD s', I applied the coinduction scheme and ends up: ?a xs'. (xs = a:::xs') /\ a IN A /\ Abbrev (xs' = xs) /\ P xs' 0. Abbrev (xs = StreamD s) 1. P xs The first conjunction can be easily made true by using `LHD xs` and `LTL xs`. This also require that the lazy list 'xs' should not be LNIL, which can also be easily inferred (from premise 0). However, this makes Abbrev (LTL xs = xs) false.. Is there any way that I can use the coinduction scheme directly such that I can have ∃a xs'. (StreamD xs = a:::xs') ∧ a ∈ A ∧ P xs' 0. P xs -- 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
Re: [Hol-info] measureTheory (was: Re: New extrealTheory)
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. > —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 > > > > -- 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
Re: [Hol-info] New extrealTheory (was: Re: conflicts auto-resolved by Define?)
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
Re: [Hol-info] Partial Function on lazy list
Hi,
Thanks!. The tip is spot on..:) Now, I'm able to define it as
val recur_llist_fn1_thm =
(recur_llist_fn1 P e [||] = [||]) [image: \wedge]
(recur_llist_fn1 P e (h:::t) =
if P h then h:::recur_llist_fn1 P e t
else e:::recur_llist_fn1 P e t)
On Wed, Aug 8, 2018 at 7:20 PM wrote:
> The function is already ready for use with any P; the final until_thm
> looks like
>
>
>
> val until_thm =
>
>⊢ (until P [||] = [||]) ∧
>
> (until P (h:::t) = if P h then [|h|] else h:::until P t): thm
>
>
>
> meaning that one can write things like
>
>
>
> until (\x. x MOD 3 = 0) ll
>
>
>
> for example. This seems like a suitably polymorphic function.
>
>
>
> To tweak it to put your example element Q into the list instead of the
> actual elements, change the core definition to also refer to Q. You will
> then need to generalise Q as well as P, and to then skolemize twice.
>
>
>
> Incidentally, Q is a bad name for an element; it looks too much like a
> name for a predicate. You should use a name like ‘e’ instead.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Thursday, 9 August 2018 at 06:08
> *To: *"Norrish, Michael (Data61, Acton)"
> *Cc: *hol-info
> *Subject: *Re: [Hol-info] Partial Function on lazy list
>
>
>
> Hi,
>
>
>
> Great!. This really helps alot...:) However, I may be interested in
> defining it for [image: \forall P] so that I don't need to instantiate
> every time with a specific instance of P. I tried this by myself but every
> time I lost in connecting my definition in llist form to its corresponding
> option theory form...:( Also, what change should be made if I change my
> definition a little
>
>
>
> val recur_llist_fn1_def = Define
>
> `recur_llist_fn1 P Q w =
>
> if (w = [||]) then [||]
>
> else if P (THE (LHD w)) then
>
> THE (LHD w) ::: (recur_llist_fn1 P Q (THE (LTL w)))
>
>else Q:::(recur_llist_fn1 P Q (THE (LTL w)))`;
>
>
>
> Any suggestions or thoughts?
>
>
>
>
>
>
>
>
>
> On Mon, Aug 6, 2018 at 8:52 PM wrote:
>
> You need to define a helper function that has as its state not only the
> llist that is being consumed but also a Boolean indicating whether or not
> to stop (because a P-satisfying element has been seen).
>
> - -
> val until0_def =
> new_specification ("until0_def", ["until0"],
> ISPEC ``λbll. if FST bll then NONE
> else if SND bll = [||] then NONE
> else if P (THE (LHD (SND bll))) then
> SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
> else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND
> bll)))``
> llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV
> SKOLEM_THM));
>
> val until0_T =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []
>
> val until0_FCONS =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss())
> []
> |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
> |> SIMP_RULE bool_ss [Once COND_RATOR]
> |> SIMP_RULE (srw_ss()) [until0_T]
>
> val until0_FNIL =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []
>
> val until_def = Define‘until P ll = until0 P (F, ll)’
>
> val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
>[until0_FNIL, until0_FCONS])
> - -
>
> Michael
>
>
>
> From: Waqar Ahmad via hol-info
> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
> Date: Tuesday, 7 August 2018 at 03:26
> To: hol-info
> Subject: [Hol-info] Partial Function on lazy list
>
> Hi all,
>
> Is there any easy way to define the following partial function on lazy list
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w =
> if P (THE (LHD w)) then [|THE (LHD w)|]
> else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> Otherwise, I can also include the LNIL case as
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w = if (w = [||]) then [||] else
> if P (THE (LHD w)) then [|THE (LHD w)|]
> else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> but I'm having issue to write its corresponding axiomatic form for
>
> llist_Axiom_1:
>
> !f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
>
> Particularly for P (THE (LHD w)) what will be SOME (?)
>
> Any suggestion or thoughts?
>
> --
> Waqar Ahmad, Ph.D.
> Post Doc at Hardware
Re: [Hol-info] Partial Function on lazy list
Hi,
Great!. This really helps alot...:) However, I may be interested in
defining it for [image: \forall P] so that I don't need to instantiate
every time with a specific instance of P. I tried this by myself but every
time I lost in connecting my definition in llist form to its corresponding
option theory form...:( Also, what change should be made if I change my
definition a little
val recur_llist_fn1_def = Define
`recur_llist_fn1 P Q w =
if (w = [||]) then [||]
else if P (THE (LHD w)) then
THE (LHD w) ::: (recur_llist_fn1 P Q (THE (LTL w)))
else Q:::(recur_llist_fn1 P Q (THE (LTL w)))`;
Any suggestions or thoughts?
On Mon, Aug 6, 2018 at 8:52 PM wrote:
> You need to define a helper function that has as its state not only the
> llist that is being consumed but also a Boolean indicating whether or not
> to stop (because a P-satisfying element has been seen).
>
> - -
> val until0_def =
> new_specification ("until0_def", ["until0"],
> ISPEC ``λbll. if FST bll then NONE
> else if SND bll = [||] then NONE
> else if P (THE (LHD (SND bll))) then
> SOME ((T, THE (LTL (SND bll))), THE (LHD (SND bll)))
> else SOME ((F, THE (LTL (SND bll))), THE (LHD (SND
> bll)))``
> llist_Axiom_1 |> Q.GEN ‘P’ |> CONV_RULE (HO_REWR_CONV
> SKOLEM_THM));
>
> val until0_T =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(T, ll)’ |> SIMP_RULE (srw_ss()) []
>
> val until0_FCONS =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, h:::t)’ |> SIMP_RULE (srw_ss())
> []
> |> SIMP_RULE bool_ss [COND_RAND, Once COND_RATOR]
> |> SIMP_RULE bool_ss [Once COND_RATOR]
> |> SIMP_RULE (srw_ss()) [until0_T]
>
> val until0_FNIL =
> until0_def |> Q.SPEC `P` |> Q.SPEC ‘(F, [||])’ |> SIMP_RULE (srw_ss()) []
>
> val until_def = Define‘until P ll = until0 P (F, ll)’
>
> val until_thm = LIST_CONJ (map (SIMP_RULE bool_ss [GSYM until_def])
>[until0_FNIL, until0_FCONS])
> - -
>
> Michael
>
>
>
> From: Waqar Ahmad via hol-info
> Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
> Date: Tuesday, 7 August 2018 at 03:26
> To: hol-info
> Subject: [Hol-info] Partial Function on lazy list
>
> Hi all,
>
> Is there any easy way to define the following partial function on lazy list
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w =
> if P (THE (LHD w)) then [|THE (LHD w)|]
> else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> Otherwise, I can also include the LNIL case as
>
> val recur_llist_fn_def = Define
> `recur_llist_fn P w = if (w = [||]) then [||] else
> if P (THE (LHD w)) then [|THE (LHD w)|]
> else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`;
>
> but I'm having issue to write its corresponding axiomatic form for
>
> llist_Axiom_1:
>
> !f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a
>
> Particularly for P (THE (LHD w)) what will be SOME (?)
>
> Any suggestion or thoughts?
>
> --
> 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
>
--
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
Re: [Hol-info] conflicts auto-resolved by Define?
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) /\
> (!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
Re: [Hol-info] conflicts auto-resolved by Define?
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 "\ + -\ =
> \”.
>
> function plus_ereal where
> "ereal r + ereal p = ereal (r + p)"
> | "\ + a = (\::ereal)"
> | "a + \ = (\::ereal)"
> | "ereal r + -\ = - \"
> | "-\ + ereal p = -(\::ereal)"
> | "-\ + -\ = -(\::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
[Hol-info] Partial Function on lazy list
Hi all, Is there any easy way to define the following partial function on lazy list val recur_llist_fn_def = Define `recur_llist_fn P w = if P (THE (LHD w)) then [|THE (LHD w)|] else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`; Otherwise, I can also include the LNIL case as val recur_llist_fn_def = Define `recur_llist_fn P w = if (w = [||]) then [||] else if P (THE (LHD w)) then [|THE (LHD w)|] else (THE (LHD w)):::(recur_llist_fn P (THE (LTL w)))`; but I'm having issue to write its corresponding axiomatic form for llist_Axiom_1: !f. ?g. !x. g x = case f x of NONE => [||] | SOME (a,b) => b:::g a Particularly for P (THE (LHD w)) what will be SOME (?) Any suggestion or thoughts? -- 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
Re: [Hol-info] conflicts auto-resolved by Define?
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 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://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/ -- 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
Re: [Hol-info] MESON
Hi, You can rewrite your goal with thm2 by using e (SIMP_TAC [GSYM thm2]); and then use e (SIMP_TAC [thm1]); On Wed, Jul 18, 2018 at 4:43 PM Dylan Melville wrote: > I have a set of theorems, which state: > > let thm1 = A;; > let thm2 = A <=> B;; > > And I want a theorem that states B. I tried making B my goal, and using > MESON_TAC[thm1,thm2] but MESON timed out. What’s the proper way to prove B? > > -- > 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 > -- 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
Re: [Hol-info] Extension of Co-algebraic Datatype
am type, does this mean you want a constructor
> for stream of type
>
>
>
> (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *"Norrish, Michael (Data61, Acton)"
> *Cc: *hol-info
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α*** -> bool) -> *α* llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM, wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”. Because the types are
> co-algebraic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info
> *Cc: *Waqar Ahmad
> *Subject: *[Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Hi,
>
>
>
> Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
> is developed based on the co-algebraic datatype. I understand that the
> datatype *'a llist *is derived as a subset of the option type * :num ->
> 'a option. * Now, I want to define a new datatype based on datatype 'a
> llist. For instance,
>
>
>
> P of 'a llist
>
>
>
> such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially
> the similar datatype as *'a llist* but having different properties. In
> shallow embedding, I can define it by using filter function of llistTheory
> as:
>
>
>
>
>
> val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
>
>
>
> One way of defining the co-inductive datatype *stream* is to follow the
> same procedure as described in "llistTheory", which is quite cumbersome. Is
> there any alternate way similar to that of package "Hol_datatype"?
>
>
>
> Secondly, Is it possible to define a co-inductive datatype that takes a
> set type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
> similar function, in shallow embedding, I can think of is:
>
>
>
> val streams_def = Define
>
> `streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
>
>
>
> where the function streams is of type (:num -> 'a option) ->bool -> 'a
> llist-> bool
>
>
>
> In some cases, the function *streams* doesn't suffice for modeling the
> correct behavior of streams related properties..
>
>
>
> Any suggestion or thoughts would be highly helpful...
>
>
>
>
>
>
>
>
>
>
>
>
>
> --
>
> 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/
> [image:
> http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
>
>
>
> --
> Check out the vibrant tech community on one of the world's
[Hol-info] Strange tactic behavior HOL-k10 vs HOL-k12
Hi all, I observed a strange behavior of the same tactic in HOL-k10 vs HOL-k12 Consider a proof goal ``?!m. ((m = n) \/ m < n) /\ ((if m < n then f m else a) = x)`` e (CONV_TAC(ONCE_DEPTH_CONV COND_ELIM_CONV)); (* In HOL-k10, the tactic results a desired behavior*) ?!m. ((m = n) \/ m < n) /\ (~(m < n) \/ (f m = x)) /\ (m < n \/ (a = x)) (* In HOL-k12, the tactic results *) ?!m. ((m = n) \/ m < n) /\ (if m < n then $= (f m) else $= a) x Am I missing something? -- 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
Re: [Hol-info] Loops in HOL4
I'm not sure what actually you desired with WHILE function but I can
explain its functioning that might help you to define your function.
For instance, you can define a function that continue traversing over a
list until "P h" is true otherwise return the remaining part of the list.
!P L. dropWhile_new P L = WHILE (\a. P (HD a)) TL L
a trivial example could be
val dropWhile_eq = store_thm("dropWhile_eq",
``ALL_DISTINCT [a;b;c] ==> (dropWhile_new ($=a) [a;b;c] = [b;c])``,
rw[dropWhile_new_def]
\\ once_rewrite_tac[WHILE]
\\ rw[]
\\ once_rewrite_tac[WHILE]
\\ rw[]);
I hope this helps
On Mon, Jun 4, 2018 at 10:08 AM, 尚亚龙 <2016210...@mail.buct.edu.cn> wrote:
> Hi everyone,
>
>
> I'm just beginning to learn HOL4. And I have a question.
>
>
>
> The problem is as follows: I have a list 'a',
>
> I want to use a loop to retrieve the number of 'num' in a each time until
> the list is empty,
>
> and I see WHILE theorems can be used in the HOL library, but I can not
> succeed,
>
> So I would like to ask how to implement the WHILE theorem,
>
> if you can, please attach an example to explain. Thank you!
>
>
>
> Shang
>
>
> --
> 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
>
>
--
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
Re: [Hol-info] Reverse Function on LazyLists
Thanks. As reverse on llist only really works when the argument is finite, the > easiest definition would be > > > > Lrev ll = fromList (REVERSE (toList ll)) > > > > You could lift this to infinite lists by having > > > > ~LFINITE ll ==> (Lrev ll = infinite-list-of something) > > > > Or similar. As it happens, I believe such a definition then satisfies > your desired characterisation. > This is exactly what I'm doing for mimic the Isabelle definitions like primcorec flat where "shd (flat ws) = hd (shd ws)" | "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)" !L. sflat L = LFLATTEN (fromList L) where sflat is lifted from the ordinary list to lazylists. Since, there is not function available for reversing the lazy list so I've to define it from scratch. I prefer axiomatic characterization of reverse in this case > > One f you could instantiate the axiom with to get this effect would be > > > > f ll = if LFINITE ll then if ll = [||] then NONE else SOME (fromList > (FRONT (toList ll)), LAST (toList ll)) > > else SOME (ll, ARB) > > > > Your characterisation should follow from a bisimulation argument. > Thanks. I modified the reverse function definition to incorporate the effect of finite lazy lists as ?reverse. (reverse [||] = [||]) /\ !xs. reverse xs = if LFINITE xs then LAPPEND (reverse (THE (LTL xs))) [|THE (LHD xs)|] else xs from LLIST_BISIMULATION, I need to assign an instance of relation R between the characterizations as ?R. R (g xs) (if LFINITE xs then LAPPEND (g (THE (LTL xs))) [|THE (LHD xs)|] else xs) /\ !ll3 ll4. R ll3 ll4 ==> (ll3 = [||]) /\ (ll4 = [||]) \/ (LHD ll3 = LHD ll4) /\ R (THE (LTL ll3)) (THE (LTL ll4)) 0. !x. LHD (g x) = OPTION_MAP SND ((\ll. if LFINITE ll then if ll = [||] then NONE else SOME (fromList (FRONT (THE (toList ll))), LAST (THE (toList ll))) else SOME (ll,ARB)) x) 1. !x. LTL (g x) = OPTION_MAP (g o FST) ((\ll. if LFINITE ll then if ll = [||] then NONE else SOME (fromList (FRONT (THE (toList ll))), LAST (THE (toList ll))) else SOME (ll,ARB)) x) I've tried several options, one of them is `\ll1 ll2. ?xs. (ll1 = g xs) /\ (ll2 = (if LFINITE xs then LAPPEND (g (THE (LTL xs))) [|THE (LHD xs)|] else xs))` but at some point in proof I cannot reason it further. Any suggestion or comments? > > Michael > > > > *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net> > *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Wednesday, 23 May 2018 at 15:21 > *To: *hol-info <hol-info@lists.sourceforge.net> > *Subject: *[Hol-info] Reverse Function on LazyLists > > > > Hi, > > > > Lately, I've been trying to define the "reverse" function on lazy lists > but I'm facing some issues. I understand that, unlike lists, in order to > define recursive function over lazy lists every time I need to justify the > definition of (co-)recursive functions (reverse in my case) that map into > the llist type using > > > > llist_Axiom; > > val it = > >|- !f. > > ?g. > >(!x. LHD (g x) = OPTION_MAP SND (f x)) /\ > >!x. LTL (g x) = OPTION_MAP (g o FST) (f x): > >thm > > > > So I'm trying to prove the following reverse function definition over > llist type > > > > `?reverse. > > ( reverse ([||]) = LNIL) /\ > > (!x xs. reverse (LCONS x xs) = LAPPEND ( reverse xs) [|x|])` > > > > but could not find the appropriate instance of "f" in llist_Axiom to prove > both the base and the inductive cases... > > > > Any suggestion or comments? > > > > -- > > 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 > > -- Waqar Ahmad, Ph.D. Post Doc at Hardware Verifica
[Hol-info] Reverse Function on LazyLists
Hi, Lately, I've been trying to define the "reverse" function on lazy lists but I'm facing some issues. I understand that, unlike lists, in order to define recursive function over lazy lists every time I need to justify the definition of (co-)recursive functions (reverse in my case) that map into the llist type using llist_Axiom; val it = |- !f. ?g. (!x. LHD (g x) = OPTION_MAP SND (f x)) /\ !x. LTL (g x) = OPTION_MAP (g o FST) (f x): thm So I'm trying to prove the following reverse function definition over llist type `?reverse. ( reverse ([||]) = LNIL) /\ (!x xs. reverse (LCONS x xs) = LAPPEND ( reverse xs) [|x|])` but could not find the appropriate instance of "f" in llist_Axiom to prove both the base and the inductive cases... Any suggestion or comments? -- 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
Re: [Hol-info] Extension of Co-algebraic Datatype
uot;Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α*** -> bool) -> *α* llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM, <michael.norr...@data61.csiro.au> wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”. Because the types are
> co-algebraic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info <hol-info@lists.sourceforge.net>
> *Cc: *Waqar Ahmad <waqar.ah...@seecs.edu.pk>
> *Subject: *[Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Hi,
>
>
>
> Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
> is developed based on the co-algebraic datatype. I understand that the
> datatype *'a llist *is derived as a subset of the option type * :num ->
> 'a option. * Now, I want to define a new datatype based on datatype 'a
> llist. For instance,
>
>
>
> P of 'a llist
>
>
>
> such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially
> the similar datatype as *'a llist* but having different properties. In
> shallow embedding, I can define it by using filter function of llistTheory
> as:
>
>
>
>
>
> val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
>
>
>
> One way of defining the co-inductive datatype *stream* is to follow the
> same procedure as described in "llistTheory", which is quite cumbersome. Is
> there any alternate way similar to that of package "Hol_datatype"?
>
>
>
> Secondly, Is it possible to define a co-inductive datatype that takes a
> set type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
> similar function, in shallow embedding, I can think of is:
>
>
>
> val streams_def = Define
>
> `streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
>
>
>
> where the function streams is of type (:num -> 'a option) ->bool -> 'a
> llist-> bool
>
>
>
> In some cases, the function *streams* doesn't suffice for modeling the
> correct behavior of streams related properties..
>
>
>
> Any suggestion or thoughts would be highly helpful...
>
>
>
>
>
>
>
>
>
>
>
>
>
> --
>
> 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/
> [image:
> http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
>
>
>
> --
> 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
>
>
>
>
>
> --
>
> Waqar Ahmad, Ph.D.
> Post Doc a
Re: [Hol-info] Extension of Co-algebraic Datatype
Thanks!. I understand that the working of LNIL and LCONS constructors
since I'm exploring "llistTheory" for quite some time. To be very clear,
I'm in the process of porting "stream theory" form Isabelle
https://www.isa-afp.org/browser_info/current/HOL/HOL-Library/Stream.html which
is formalized as coinductive "stream":
codatatype (sset: 'a) stream =
SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
for
map: smap
rel: stream_all2
I can see that its datatype is very similar to lazy list (llistTheory)
datatype so rather defining a new type I defined a function that returns
the same 'a llist-typed (lazy) list as given to its input:
∀L. Stream L = LFILTER (λn. T) L:
type_of ``stream``;
``:α llist -> α llist``:
Later in Isabelle "stream theory", a coinductive set "streams" is defined
based on "stream" datatype as:
coinductive_set
streams :: "'a set *⇒ * 'a stream set"
for A :: "'a set"
where
Stream[intro!, simp, no_atp]: "[[a ∈ A; s ∈ streams A]] ⟹ a ## s
∈ streams
A"
end
Using llistTheory functions, I'm able to define a similar function as:
∀A. streams A = IMAGE (λa. Stream a) {llist_abs (λn. SOME x) | x ∈
A}:
type_of ``streams``;
``:('a -> bool) -> 'a llist -> bool``:
However, by using shallow embedding approach, I'm not able to use some
essential properties that are accompanied when a new coinductive datatype
is defined. For instance, if a streams datatype is define, I may have this
property of form:
streams.cases (Isabelle):
a ∈ streams A ⇒ (? a s. a = a ##s ⇒* a *∈* A *⇒* s *∈ streams A
⇒ P) ⇒ P
I'm having the issues of defining these types in HOL4. Is there any way
that I can replicate the same in HOL4?
On Mon, May 7, 2018 at 8:49 PM, <michael.norr...@data61.csiro.au> wrote:
> You can probably define a function of that type, but you can’t define a *
> *constructor** of that type for llist. (Contrast what I’d consider to
> be llist’s standard constructors, LNIL and LCONS. They have types α llist,
> and α -> α llist -> α llist respectively.)
>
>
>
> You said you wanted a stream type, does this mean you want a constructor
> for stream of type
>
>
>
> (α -> bool) -> α stream
>
>
>
> ?
>
>
>
> Such a constructor is not recursive, so I can just write
>
>
>
> Datatype`stream = SetConstructor (α -> bool)`
>
>
>
> The SetConstructor term then has the desired type.
>
>
>
> So I’m afraid I still don’t understand your question.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Monday, 7 May 2018 at 11:38
> *To: *"Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au>
> *Cc: *hol-info <hol-info@lists.sourceforge.net>
> *Subject: *Re: [Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Thanks for the explanation. Let me state it clearly. Can I write down a
> constructor of type
>
>
>
> (*α*** -> bool) -> *α* llist
>
>
>
>
>
>
>
> On Sun, May 6, 2018 at 8:39 PM, <michael.norr...@data61.csiro.au> wrote:
>
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”. Because the types are
> co-algebraic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 Ma
Re: [Hol-info] Extension of Co-algebraic Datatype
Thanks for the explanation. Let me state it clearly. Can I write down a
constructor of type
(α -> bool) -> α llist
On Sun, May 6, 2018 at 8:39 PM, <michael.norr...@data61.csiro.au> wrote:
> I think you may be able to make your needs more precise by explicitly
> considering what your co-algebra would be.
>
>
>
> In particular, write down the type of the “general” destructor
>
>
>
> myType -> F(myType)
>
>
>
> For lazy lists, this is
>
>
>
> α llist -> (α # α llist) option
>
>
>
> For the co-algebraic numbers it’s
>
>
>
> num -> num option
>
>
>
> For arbitrarily (but finite)-branching trees, it’s
>
>
>
> Tree -> Tree list
>
>
>
> (If you change list to llist you get possibly infinitely branching trees.)
>
>
>
> In the lazy lists, this destructor might be called “HDTL”; in the numbers,
> it’s “predecessor”; in the trees it’s “children”. Because the types are
> co-algebraic each might be iterable an infinite number of times. (The
> corresponding destructors in the algebraic types are always well-founded.)
>
>
>
> What are the co-algebras for your desired types? I don’t think I’ve
> understood what you want, but it superficially appears as if you want
> dependent types, where you combine the type with some term-level predicate.
> That sort of thing is impossible to capture within a HOL type.
>
>
>
> Finally, I’m afraid that there is no general tool for defining
> co-algebraic types in HOL4 at the moment.
>
>
>
> Michael
>
>
>
> *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net>
> *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk>
> *Date: *Sunday, 6 May 2018 at 11:58
> *To: *hol-info <hol-info@lists.sourceforge.net>
> *Cc: *Waqar Ahmad <waqar.ah...@seecs.edu.pk>
> *Subject: *[Hol-info] Extension of Co-algebraic Datatype
>
>
>
> Hi,
>
>
>
> Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
> is developed based on the co-algebraic datatype. I understand that the
> datatype *'a llist *is derived as a subset of the option type *:num ->
> 'a option. * Now, I want to define a new datatype based on datatype 'a
> llist. For instance,
>
>
>
> P of 'a llist
>
>
>
> such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially
> the similar datatype as *'a llist* but having different properties. In
> shallow embedding, I can define it by using filter function of llistTheory
> as:
>
>
>
>
>
> val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
>
>
>
> One way of defining the co-inductive datatype *stream* is to follow the
> same procedure as described in "llistTheory", which is quite cumbersome. Is
> there any alternate way similar to that of package "Hol_datatype"?
>
>
>
> Secondly, Is it possible to define a co-inductive datatype that takes a
> set type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
> similar function, in shallow embedding, I can think of is:
>
>
>
> val streams_def = Define
>
> `streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
>
>
>
> where the function streams is of type (:num -> 'a option) ->bool -> 'a
> llist-> bool
>
>
>
> In some cases, the function *streams* doesn't suffice for modeling the
> correct behavior of streams related properties..
>
>
>
> Any suggestion or thoughts would be highly helpful...
>
>
>
>
>
>
>
>
>
>
>
>
>
> --
>
> 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/
> [image:
> http://research.bournemouth.ac.uk/wp-content/uploads/2014/02/NUST_Logo2.png]
>
>
> --
> 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
>
>
--
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
[Hol-info] Extension of Co-algebraic Datatype
Hi,
Lately, I've been exploring the HOL4 lazy list theory "llistTheory", which
is developed based on the co-algebraic datatype. I understand that the
datatype *'a llist *is derived as a subset of the option type *:num -> 'a
option. * Now, I want to define a new datatype based on datatype 'a llist.
For instance,
P of 'a llist
such that *P: 'a llist -> 'a stream*, where *'a stream* is essentially the
similar datatype as *'a llist* but having different properties. In shallow
embedding, I can define it by using filter function of llistTheory as:
val Stream = Define `Stream L = LFILTER (\n:'a. T) L`;
One way of defining the co-inductive datatype *stream* is to follow the
same procedure as described in "llistTheory", which is quite cumbersome. Is
there any alternate way similar to that of package "Hol_datatype"?
Secondly, Is it possible to define a co-inductive datatype that takes a set
type (:'a -> bool) and maps it to a set of type (:'a llist -> bool)? A
similar function, in shallow embedding, I can think of is:
val streams_def = Define
`streams A = IMAGE (\a. Stream a) {llist_abs x | x IN A} `;
where the function streams is of type (:num -> 'a option) ->bool -> 'a
llist-> bool
In some cases, the function *streams* doesn't suffice for modeling the
correct behavior of streams related properties..
Any suggestion or thoughts would be highly helpful...
--
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
Re: [Hol-info] build failed with latest HOL
Thanks..that solves the issue... On Mon, Oct 30, 2017 at 4:20 AM, <michael.norr...@data61.csiro.au> wrote: > That’s a Poly/ML bug. Please use the 5.7 release available at > > > > https://github.com/polyml/polyml/archive/v5.7.tar.gz > > > > Michael > > > > *From: *Waqar Ahmad via hol-info <hol-info@lists.sourceforge.net> > *Reply-To: *Waqar Ahmad <12phdwah...@seecs.edu.pk> > *Date: *Saturday, 28 October 2017 at 18:13 > *To: *hol-info <hol-info@lists.sourceforge.net> > *Subject: *[Hol-info] build failed with latest HOL > > > > Hi all, > > I'm installing the latest HOL (Github version) in Ubuntu. The installation > of the polyml v5.7.1 went successfully. However, the building of HOL failed > with following error message: > > waqar@waqar-VirtualBox:~/Downloads/HOL/HOL$ bin/build > *** Using kernel option -stdknl from earlier build command; > use -expk, -otknl, or -stdknl to override > *** Using -j 2 from earlier build command; use -j to override > Cleaning out /home/waqar/Downloads/HOL/HOL/sigobj > /home/waqar/Downloads/HOL/HOL/sigobj cleaned > *** Build log exists; new logging will concatenate onto this file > Building directory tools/mlyacc/mlyacclib [28 اكتوبر, 11:36:46] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/portableML/poly [28 اكتوبر, 11:36:49] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/portableML [28 اكتوبر, 11:37:03] > FunctionalRecordUpdate.sml > OK > GetOpt.sig > OK > GetOpt.sml > OK > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/portableML/monads [28 اكتوبر, 11:37:32] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/prekernel [28 اكتوبر, 11:37:41] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/0 [28 اكتوبر, 11:38:01] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/postkernel [28 اكتوبر, 11:38:11] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/parse [28 اكتوبر, 11:38:21] > base_lexer.sml > OK > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/opentheory [28 اكتوبر, 11:39:29] > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/bool [28 اكتوبر, 11:39:33] > boolTheory > OK > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/1 [28 اكتوبر, 11:39:49] > DiskFiles.lex.sml > OK > DiskFiles.grm-sig.sml DiskFiles.grm.sml > OK > DiskFiles.grm-sig.sml DiskFiles.grm.sml > OK > ConseqConvTheory > OK > Uploading files to /home/waqar/Downloads/HOL/HOL/sigobj > Building directory src/proofman [28 اكتوبر, 11:41:00] > /home/waqar/Downloads/HOL/HOL/bin/hol.state0 > FAILED! > error in quse /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec.sml : Fail > "Exception- InternalError: codeToPRegRev raised while compiling" > error in load /home/waqar/Downloads/HOL/HOL/src/1/Prim_rec : Fail > "Exception- InternalError: codeToPRegRev raised while compiling" > error in load boolLib : Fail "Exception- InternalError: codeToPRegRev > raised while compiling" > Exception- InternalError: codeToPRegRev raised while compiling > > Build failed in directory /home/waqar/Downloads/HOL/HOL/src/proofman > (exited with code 1) > > I wonder whether this error is due to polyml or HOL.. Can anybody help me > in fixing this issue? > > > -- > > Waqar Ahmed, Ph.D. > System Analysis and Verification (SAVe) Lab > School of Electrical Engineering and Computer Science (SEECS) > National University of Science and Technology (NUST), H-12, Islamabad, > Pakistan > > 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 > > -- Waqar Ahmed, Ph.D. System Analysis and Verification (SAVe) Lab School of Electrical Engineering and Computer Science (SEECS) National University of Science and Technology (NUST), H-12, Islamabad, Pakistan 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
