Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem

[Chun Tian (binghe)]

Hi Manuel,

many thanks for your hints. I can't fully understand Isabelle proofs, but I
think I got the idea. In HOL4 we have the following theorem for real-valued
borel measurable functions:

   [in_borel_measurable_add]  Theorem
  ⊢ ∀a f g h.
sigma_algebra a ∧ f ∈ borel_measurable a ∧
g ∈ borel_measurable a ∧ (∀x. x ∈ space a ⇒ h x = f x + g x) ⇒
h ∈ borel_measurable a

and a transition theorem from borel to Borel - the extreal-valued Borel
measurable set:

   [IN_MEASURABLE_BOREL_IMP_BOREL]  Theorem
  ⊢ ∀f m.
f ∈ borel_measurable (m_space m,measurable_sets m) ⇒
Normal ∘ f ∈ Borel_measurable (m_space m,measurable_sets m)

Thus, in theory, by considering a finite number of exceptional values
(infinities) it's possible to prove the previously mentioned lemma without
extra antecedents, no matter what's the actual value of the unspecified
terms.   What I said before was based on the current proofs of
IN_MEASURABLE_BOREL_SUB in HOL4, which (indirectly) involves all 4 cases of
arithmetics of infinities.

I would say, this is still not inline with "real" mathematics, but the
situation is slightly better than (rudely) assuming any fixed value for
`PosInf + NegInf` a priori.

--Chun


On Mon, Jul 27, 2020 at 9:46 PM Manuel Eberl  wrote:

> The way that measurability of subtraction on ereals is proven in
> Isabelle strongly suggests to me that it does not depend on any
> particular choice of what ∞ - ∞ and -∞ - (-∞) are. I quickly checked it
> by defining my own ereals and leaving it undefined, and all those proofs
> still work fine.
>
> In case you are interested in /how/ this is proven in Isabelle: You take
> the following lemma:
>
> lemma borel_measurable_ereal2:
>   fixes f g :: "'a ⇒ ereal"
>   assumes f: "f ∈ borel_measurable M"
>   assumes g: "g ∈ borel_measurable M"
>   assumes H: "(λx. H (ereal (real_of_ereal (f x))) (ereal (real_of_ereal
> (g x ∈ borel_measurable M"
> "(λx. H (-∞) (ereal (real_of_ereal (g x ∈ borel_measurable M"
> "(λx. H (∞) (ereal (real_of_ereal (g x ∈ borel_measurable M"
> "(λx. H (ereal (real_of_ereal (f x))) (-∞)) ∈ borel_measurable M"
> "(λx. H (ereal (real_of_ereal (f x))) (∞)) ∈ borel_measurable M"
>   shows "(λx. H (f x) (g x)) ∈ borel_measurable M"
> proof -
>   let ?G = "λy x. if g x = ∞ then H y ∞ else if g x = - ∞ then H y (-∞)
> else H y (ereal (real_of_ereal (g x)))"
>   let ?F = "λx. if f x = ∞ then ?G ∞ x else if f x = - ∞ then ?G (-∞) x
> else ?G (ereal (real_of_ereal (f x))) x"
>   { fix x have "H (f x) (g x) = ?F x" by (cases "f x" "g x" rule:
> ereal2_cases) auto }
>   note * = this
>   from assms show ?thesis unfolding * by simp
> qed
>
> Then you note that the conversions between "real" and "ereal" (which are
> called "ereal :: real ⇒ ereal" and "real_of_ereal :: ereal ⇒ real" in
> Isabelle) are unconditionally Borel-measurable.
>
> For the first one, that should be obvious. For the second one, note that
> "real_of_ereal" is clearly a continuous map from "UNIV - {±∞} :: ereal"
> to "UNIV :: real" and then still Borel-measurable on the entire Borel
> space of ereal because there are only countable many (namely 2)
> exceptional points.
>
>
> I don't see why this kind of argument should not work in HOL4. This does
> not even assume that "∞ - ∞ = -∞ - (-∞)" or anything of the sort. It
> only assumes that "∞ - ∞" is some arbitrary but globally fixed value –
> surely that is the case in HOL4's logic.
>
> Manuel
>
>

-- 
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem

[Chun Tian (binghe)]

Not that easy, or just impossible. However, if f and g are positive and
negative parts of the same function (h), then the theorem indeed holds
without any extra antecedents:

   [IN_MEASURABLE_BOREL_PLUS_MINUS]  Theorem
  ⊢ ∀a f.
f ∈ Borel_measurable a ⇔
f⁺ ∈ Borel_measurable a ∧ f⁻ ∈ Borel_measurable a

My previous idea actually doesn't work. The problem is that, not only ∞ +
-∞, but also the other three cases (-∞ + ∞, ∞ - ∞, -∞ - -∞) will also
involve when you actually try to prove that proposition, and these four
cases have in total 3^4 possible value combinations, none leads to any
inconsistency.

--Chun

On Mon, Jul 27, 2020 at 5:51 PM Manuel Eberl  wrote:

> In any case, all I said in my last email was that you should be able to
> easily prove
>
> ⊢ ∀a f g h. sigma_algebra a ∧ f ∈ Borel_measurable a ∧ g ∈
> Borel_measurable a ⇒ (λx. f x − g x) ∈ Borel_measurable a
>
> no matter what ∞ + -∞ is defined as (including undefined, which is just
> some globally fixed value in HOL). But perhaps that is the same
> realisation that you also had in your last email.
>
> Manuel
>


-- 
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] [isabelle] Various "models" of extended reals and impacts in Fubini's theorem

[Chun Tian (binghe)]

Hi,

If f and g are both measurable functions, then {x | f x = g x /\ x IN
m_space m} (abbrev: {f = g}) must be a measurable set. However, if you have
just f a measurable function, and {f = g} a measurable set, then it is NOT
true that g is a measurable set, UNLESS m is a complete measure space.

But actually I just got a new idea to resolve my problem:

Although the value of `PosInf + NegInf`, etc. are not specified (in latest
HOL4), but if I let `x = PosInf + NegInf` in a proof, and then do a case
analysis on `x`, there must be only three possibilities: x = PosInf, x =
NegInf, x = Normal r, where r is an arbitrary normal real number.   But I
do have proven the involved theorems under all these 3 cases (with very
different proofs, sometimes), thus in theory I also have a proof when
`PosInf + NegInf` is unspecified!

What I have just benefited from logic is that the same logical term cannot
equal to different values in the same proof.

Regards,

Chun Tian


On Mon, Jul 27, 2020 at 4:28 PM Manuel Eberl  wrote:

> On 27/07/2020 10:04, Chun Tian (binghe) wrote:
> > are conclusions of Fubini's theorem.
>
> Oops, okay, sorry!
>
> > Furthermore, the definition of integrability, besides the finiteness of
> > nn_integral (pos_fn_integral in HOL4) of the positive and negative parts,
> > also includes the measurability of the involved functions.
>
> Perhaps the problem is simply that your measurability theorem for
> subtraction on extreals is too weak. I would be very surprised if it
> were not possible to prove that subtraction of extreals is measurable
> with no preconditions.
>
> After all, there are only finitely many problematic points and you can
> treat those separately. Testing for equality is measurable, constant
> functions are measurable, "if-then-else" is measurable – so a function
> that is measurable with finitely many exceptions should also be measurable.
>
> At the end of the day, pretty much everything you can write down without
> doing something crazy (like choice operators) is Borel-measurable.
>
> Manuel
>
>

-- 
Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Various "models" of extended reals and impacts in Fubini's theorem

[Chun Tian (binghe)]

Dear HOL4 and Isabelle community,

the sole purpose of this email is to have your attention on a recent pull
request on HOL4:

https://github.com/HOL-Theorem-Prover/HOL/pull/845

where I was trying to formalize Fubini's theorem (in Lebesgue Integrals)
but was blocked somehow by HOL4's new arithmetic definitions of extended
reals (extreal), i.e. the addition/subtraction of infinities.

In short words, I feel that the statements of this classical result
(Fubini's theorem) by *Guido Fubini* (1879-1943) are not sufficient,
because its proof seems inevitably relied on the forbidden part of extreal
arithmetics.   As a result, Fubini's theorem in its original statements has
been or (can be) formalized in Isabelle/HOL, Lean and Mizar, but not in
latest HOL4 where `PosInf + NegInf` is unspecified.

Thanks in advance for your opinions and comments!

Regards,

Chun Tian
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Simplify/normalize propositional logic terms?

[Chun Tian (binghe)]

Well, it's not that "perfect", having seen the double "p" in ``x /\ p /\ p
/\ ~q`` returned by normalForms.DNF_CONV. Maybe this indicates some
possible improvements in normalForms.CONTRACT_CONV.  Let me try ...

--Chun

On Tue, Oct 1, 2019 at 11:01 AM Chun Tian (binghe) 
wrote:

> Thanks to both of you.
>
> That SIMP_CONV indeed works: (it also explains why just using bool_ss
> doesn't work)
>
> > SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] ``(q \/ p /\ x) /\ p /\ ~q``;
> val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ ~q: thm
>
> But now I realized that, what I'm looking for is actually a conversion to
> DNF forms with possible simplifications. The normalForms.DNF_CONV (in
> src/metis, by Joe Hurd) did this work perfectly: (by using the
> CONTRACT_CONV in the same lib)
>
> > normalForms.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
> val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ p /\ ~q: thm
>
> while refuteLib.DNF_CONV doesn't do any simplification:
>
> > refuteLib.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
> val it = |- (q \/ p /\ x) /\ p /\ ~q <=> q /\ p /\ ~q \/ p /\ x /\ p /\
> ~q: thm
>
> P. S. "src/metis/normalForms.sml" is currently broken due to the "tight
> equality" changes. To reproduce my above demos, you need to (temporarily)
> put a
>
> val _ = ParseExtras.temp_loose_equality()
>
> at the beginning of that file. I'm preparing a PR to fix this issue.
>
> Regards,
>
> Chun Tian
>
> Il 01/10/19 10:42, Thomas Sewell ha scritto:
> > Try this:
> >
> > SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] `` (q \/ p /\ x) /\ p /\ ~q
> ``;
> >
> > That CONJ_ss just adds a congruence rule that uses each side of a
> conjunction to simplify the other.
> >
> > I found it by investigating bossLib.csimp, which you might also want to
> know about.
> >
> > Once upon a time in Isabelle I had a problem with such congruences,
> since they might locally add rewrites which might be looping or
> inefficient. Is there a similar risk in HOL4?
> >
> > Cheers,
> > Thomas.
> >
> >
> > On 2019-09-30 23:49, Konrad Slind wrote:
> >> A couple of places to look in HOLindex: refuteLib and normalForms
> structure.
> >>
> >>
> >> On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) <
> binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>> wrote:
> >>
> >> Hi,
> >>
> >> it can be proven (by DECIDE_TAC) that,
> >>
> >> |- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x
> >>
> >> but is there any conversion function available in HOL4 such that
> from LHS of above equation I can directly get the RHS - something like a
> canonical form?
> >>
> >> --Chun
> >>
> >>
> >>
> >> ___
> >> hol-info mailing list
> >> hol-info@lists.sourceforge.net  hol-info@lists.sourceforge.net>
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
> >>
> >>
> >>
> >> ___
> >> hol-info mailing list
> >> hol-info@lists.sourceforge.net
> >> https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
> >
> > ___
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
>
>

-- 

Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Simplify/normalize propositional logic terms?

[Chun Tian (binghe)]

Thanks to both of you.

That SIMP_CONV indeed works: (it also explains why just using bool_ss doesn't 
work)

> SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] ``(q \/ p /\ x) /\ p /\ ~q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ ~q: thm

But now I realized that, what I'm looking for is actually a conversion to DNF 
forms with possible simplifications. The normalForms.DNF_CONV (in src/metis, by 
Joe Hurd) did this work perfectly: (by using the CONTRACT_CONV in the same lib)

> normalForms.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> x /\ p /\ p /\ ~q: thm

while refuteLib.DNF_CONV doesn't do any simplification:

> refuteLib.DNF_CONV ``(q ∨ p ∧ x) ∧ p ∧ ¬q``;
val it = |- (q \/ p /\ x) /\ p /\ ~q <=> q /\ p /\ ~q \/ p /\ x /\ p /\ ~q: thm

P. S. "src/metis/normalForms.sml" is currently broken due to the "tight 
equality" changes. To reproduce my above demos, you need to (temporarily) put a

val _ = ParseExtras.temp_loose_equality()

at the beginning of that file. I'm preparing a PR to fix this issue.

Regards,

Chun Tian

Il 01/10/19 10:42, Thomas Sewell ha scritto:
> Try this:
> 
> SIMP_CONV (bool_ss ++ boolSimps.CONJ_ss) [] `` (q \/ p /\ x) /\ p /\ ~q  ``;
> 
> That CONJ_ss just adds a congruence rule that uses each side of a conjunction 
> to simplify the other.
> 
> I found it by investigating bossLib.csimp, which you might also want to know 
> about.
> 
> Once upon a time in Isabelle I had a problem with such congruences, since 
> they might locally add rewrites which might be looping or inefficient. Is 
> there a similar risk in HOL4?
> 
> Cheers,
>     Thomas.
> 
> 
> On 2019-09-30 23:49, Konrad Slind wrote:
>> A couple of places to look in HOLindex: refuteLib and normalForms structure.
>>
>>
>> On Mon, Sep 30, 2019 at 1:31 PM Chun Tian (binghe) > <mailto:binghe.l...@gmail.com>> wrote:
>>
>> Hi,
>>
>> it can be proven (by DECIDE_TAC) that,
>>
>> |- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x
>>
>> but is there any conversion function available in HOL4 such that from 
>> LHS of above equation I can directly get the RHS - something like a 
>> canonical form?
>>
>> --Chun
>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Simplify/normalize propositional logic terms?

[Chun Tian (binghe)]

Hi,

it can be proven (by DECIDE_TAC) that,

|- (q \/ p /\ x) /\ p /\ ~q <=> p /\ ~q /\ x

but is there any conversion function available in HOL4 such that from LHS of 
above equation I can directly get the RHS - something like a canonical form?

--Chun





signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A possible bug in ext_suminf (extrealTheory)?

[Chun Tian (binghe)]

Hi Michael,

thanks for your suggestions. I'll redefine ext_suminf to make sure it's only 
specified on positive functions (usually a measure of sets). The required 
changes are minimal, as now all proofs trying to expand `ext_suminf` already 
have already added extra proofs to show the involved functions are positive. 
(This fact also indicates that the previous version sometimes do not fully 
reflect their textbook proofs as a little part can be omitted.)

I'll submit a new PR for this change ASAP.

--Chun

Il 20/09/19 03:03, Norrish, Michael (Data61, Acton) ha scritto:
> Fair enough.  It seems clear that this is not a huge problem (using a 
> function such as this outside of its intended domain is a bad idea), but on 
> the other hand, it also seems clear that needlessly having it return the 
> wrong value is a bug. 
> 
> Having said all that, getting suminf (\x. -1) to return -1 doesn't seem much 
> of a win: the sum of an infinite sequence of -1s is hardly -1.
> 
> I think it would be better style to use new_specification so as to avoid 
> giving a specific value when the argument is not always positive.
> 
> Michael
> 
> 
> On 20/9/19, 09:51, "Chun Tian (binghe)"  wrote:
> 
> In fact, even for arbitrary functions with both positive and negative 
> values, if the partial sum ever reached +/-Inf, further adding finite values 
> on the other side cannot “pull” the result back to “normal”. For instance, 
> suppose at some moment the partial sum is +inf, adding any normal reals will 
> not change it, it’s then not allowed to add -Inf on it, because under the 
> textbook definition of `+`, PosInf + NegInf is unspecified.  Thus, in some 
> sense the suminf of possible limiting values has a very different behavior 
> with the real version.
> 
> Chun
>     
> Inviato da iPad
> 
> > Il giorno 20 set 2019, alle ore 01:33, Chun Tian (binghe) 
>  ha scritto:
> > 
> > Hi,
> > 
> > The extreal version of `suminf` is only “correct” and equivalent with 
> the real version when the involved function is positive - the partial sum is 
> mono-increasing. Its relatively simple definition serves the current need (in 
> measure and probability theories). Fully mimicking the real version requires 
> a (full) porting of seqTheory (and limTheory, netsTheory, eventually 
> metricTheory) to extreals, which is an almost impossible task in my opinion.
> > 
> > Besides, I think it’s also not needed to do so, because if the sum 
> limit never reaches +Inf, one can just reduce the work back to the ‘suminf’ 
> of reals. On the hand, If the partial sum ever reached +Inf, assuming it’s 
> monotonic, then the limit value must be also +Inf, it’s reduced to a finite 
> sum.
> > 
> > Chun
> > 
> >> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61, 
> Acton)  ha scritto:
> >> 
> >> The definition of suminf over the reals (in seqTheory) is completely 
> different; is it clear that the extreal version can't mimic the original?
> >> 
> >> Michael
> >> 
> >> On 18/9/19, 06:18, "Chun Tian (binghe)"  wrote:
> >> 
> >>   Hi,
> >> 
> >>   I occasionally found that HOL's current definition of ext_suminf 
> (extrealTheory) has a bug:
> >> 
> >>  [ext_suminf_def]  Definition  
> >> ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))
> >> 
> >>   The purpose of `suminf f` is to calculate an infinite sum: f(0) + 
> f(1) +  To make the resulting summation "meaningful", all lemmas about 
> ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how 
> it's used in all applications.  For instance, one lemma says, if f is 
> positive, so is `suminf f`:
> >> 
> >>  [ext_suminf_pos]  Theorem
> >> ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
> >> 
> >>   However, I found that the above lemma can be proved even without 
> knowing anything of `f`, see the following proofs:
> >> 
> >>   Theorem ext_suminf_pos_bug :
> >>   !f. 0 <= ext_suminf f
> >>   Proof
> >>   RW_TAC std_ss [ext_suminf_def]
> >>>> MATCH_MP_TAC le_sup_imp'
> >>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
> >>>> Q.EXISTS_TAC `0` >> BETA_TAC
> >>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
> >>   QED
> >> 
> >>   where [le_sup_imp'] is a version of [le_sup_imp] before applying 
> IN

Re: [Hol-info] A possible bug in ext_suminf (extrealTheory)?

[Chun Tian (binghe)]

In fact, even for arbitrary functions with both positive and negative values, 
if the partial sum ever reached +/-Inf, further adding finite values on the 
other side cannot “pull” the result back to “normal”. For instance, suppose at 
some moment the partial sum is +inf, adding any normal reals will not change 
it, it’s then not allowed to add -Inf on it, because under the textbook 
definition of `+`, PosInf + NegInf is unspecified.  Thus, in some sense the 
suminf of possible limiting values has a very different behavior with the real 
version.

Chun

Inviato da iPad

> Il giorno 20 set 2019, alle ore 01:33, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> The extreal version of `suminf` is only “correct” and equivalent with the 
> real version when the involved function is positive - the partial sum is 
> mono-increasing. Its relatively simple definition serves the current need (in 
> measure and probability theories). Fully mimicking the real version requires 
> a (full) porting of seqTheory (and limTheory, netsTheory, eventually 
> metricTheory) to extreals, which is an almost impossible task in my opinion.
> 
> Besides, I think it’s also not needed to do so, because if the sum limit 
> never reaches +Inf, one can just reduce the work back to the ‘suminf’ of 
> reals. On the hand, If the partial sum ever reached +Inf, assuming it’s 
> monotonic, then the limit value must be also +Inf, it’s reduced to a finite 
> sum.
> 
> Chun
> 
>> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61, Acton) 
>>  ha scritto:
>> 
>> The definition of suminf over the reals (in seqTheory) is completely 
>> different; is it clear that the extreal version can't mimic the original?
>> 
>> Michael
>> 
>> On 18/9/19, 06:18, "Chun Tian (binghe)"  wrote:
>> 
>>   Hi,
>> 
>>   I occasionally found that HOL's current definition of ext_suminf 
>> (extrealTheory) has a bug:
>> 
>>  [ext_suminf_def]  Definition  
>> ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))
>> 
>>   The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1) + 
>>  To make the resulting summation "meaningful", all lemmas about 
>> ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how 
>> it's used in all applications.  For instance, one lemma says, if f is 
>> positive, so is `suminf f`:
>> 
>>  [ext_suminf_pos]  Theorem
>> ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
>> 
>>   However, I found that the above lemma can be proved even without knowing 
>> anything of `f`, see the following proofs:
>> 
>>   Theorem ext_suminf_pos_bug :
>>   !f. 0 <= ext_suminf f
>>   Proof
>>   RW_TAC std_ss [ext_suminf_def]
>>>> MATCH_MP_TAC le_sup_imp'
>>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
>>>> Q.EXISTS_TAC `0` >> BETA_TAC
>>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
>>   QED
>> 
>>   where [le_sup_imp'] is a version of [le_sup_imp] before applying IN_APP:
>> 
>>  [le_sup_imp']  Theorem
>> 
>> ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
>> 
>>   For the reason, ext_suminf is actually calculating the sup of the 
>> following values:
>> 
>>   0
>>   f(0)
>>   f(0) + f(1)
>>   f(0) + f(1) + f(2)
>>   ...
>> 
>>   The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`, then 
>> SUM_IMAGE f {} = 0.
>> 
>>   Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3 
>>   But since the sup of a set containing 0 is at least 0, the `suminf f` 
>> in this case will be 0 (instead of the correct value -1).  This is why `0 <= 
>> suminf f` holds for whatever f.
>> 
>>   I believe Isabelle's suminf (in Extended_Real.thy) has the same problem 
>> (but I can't find its definition, correct me if I'm wrong here), i.e. the 
>> following theorem holds even without the "assumes":
>> 
>>   lemma suminf_0_le:
>> fixes f :: "nat ⇒ ereal"
>> assumes "⋀n. 0 ≤ f n"
>> shows "0 ≤ (∑n. f n)"
>> using suminf_upper[of f 0, OF assms]
>> by simp
>> 
>>   The solution is quite obvious. I'm going to fix HOL's definition of 
>> ext_suminf with the following one:
>> 
>>   val ext_suminf_def = Define
>>  `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;
>> 
>>   That is, using `SUC n` intead of `n` to eliminate the fake base case (0). 
>> I believe this change only causes minor incompatibilities.
>> 
>>   Any comment?
>> 
>>   Regards,
>> 
>>   Chun Tian
>> 
>> 
>> 
>> 
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] A possible bug in ext_suminf (extrealTheory)?

[Chun Tian (binghe)]

Hi,

The extreal version of `suminf` is only “correct” and equivalent with the real 
version when the involved function is positive - the partial sum is 
mono-increasing. Its relatively simple definition serves the current need (in 
measure and probability theories). Fully mimicking the real version requires a 
(full) porting of seqTheory (and limTheory, netsTheory, eventually 
metricTheory) to extreals, which is an almost impossible task in my opinion.

Besides, I think it’s also not needed to do so, because if the sum limit never 
reaches +Inf, one can just reduce the work back to the ‘suminf’ of reals. On 
the hand, If the partial sum ever reached +Inf, assuming it’s monotonic, then 
the limit value must be also +Inf, it’s reduced to a finite sum.

Chun

> Il giorno 20 set 2019, alle ore 01:00, Norrish, Michael (Data61, Acton) 
>  ha scritto:
> 
> The definition of suminf over the reals (in seqTheory) is completely 
> different; is it clear that the extreal version can't mimic the original?
> 
> Michael
> 
> On 18/9/19, 06:18, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>I occasionally found that HOL's current definition of ext_suminf 
> (extrealTheory) has a bug:
> 
>   [ext_suminf_def]  Definition  
>  ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))
> 
>The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1) + 
>  To make the resulting summation "meaningful", all lemmas about 
> ext_suminf assume that (!n. 0 <= f n) (f is positive). This also indeed how 
> it's used in all applications.  For instance, one lemma says, if f is 
> positive, so is `suminf f`:
> 
>   [ext_suminf_pos]  Theorem
>  ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f
> 
>However, I found that the above lemma can be proved even without knowing 
> anything of `f`, see the following proofs:
> 
>Theorem ext_suminf_pos_bug :
>!f. 0 <= ext_suminf f
>Proof
>RW_TAC std_ss [ext_suminf_def]
>>> MATCH_MP_TAC le_sup_imp'
>>> REWRITE_TAC [IN_IMAGE, IN_UNIV]
>>> Q.EXISTS_TAC `0` >> BETA_TAC
>>> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
>QED
> 
>where [le_sup_imp'] is a version of [le_sup_imp] before applying IN_APP:
> 
>   [le_sup_imp']  Theorem
> 
>  ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p
> 
>For the reason, ext_suminf is actually calculating the sup of the 
> following values:
> 
>0
>f(0)
>f(0) + f(1)
>f(0) + f(1) + f(2)
>...
> 
>The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`, then 
> SUM_IMAGE f {} = 0.
> 
>Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3 
>   But since the sup of a set containing 0 is at least 0, the `suminf f` 
> in this case will be 0 (instead of the correct value -1).  This is why `0 <= 
> suminf f` holds for whatever f.
> 
>I believe Isabelle's suminf (in Extended_Real.thy) has the same problem 
> (but I can't find its definition, correct me if I'm wrong here), i.e. the 
> following theorem holds even without the "assumes":
> 
>lemma suminf_0_le:
>  fixes f :: "nat ⇒ ereal"
>  assumes "⋀n. 0 ≤ f n"
>  shows "0 ≤ (∑n. f n)"
>  using suminf_upper[of f 0, OF assms]
>  by simp
> 
>The solution is quite obvious. I'm going to fix HOL's definition of 
> ext_suminf with the following one:
> 
>val ext_suminf_def = Define
>   `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;
> 
>That is, using `SUC n` intead of `n` to eliminate the fake base case (0). 
> I believe this change only causes minor incompatibilities.
> 
>Any comment?
> 
>Regards,
> 
>Chun Tian
> 
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info


___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] A possible bug in ext_suminf (extrealTheory)?

[Chun Tian (binghe)]

Hi,

I occasionally found that HOL's current definition of ext_suminf 
(extrealTheory) has a bug:

   [ext_suminf_def]  Definition  
  ⊢ ∀f. suminf f = sup (IMAGE (λn. ∑ f (count n)) 핌(:num))

The purpose of `suminf f` is to calculate an infinite sum: f(0) + f(1) +  
To make the resulting summation "meaningful", all lemmas about ext_suminf 
assume that (!n. 0 <= f n) (f is positive). This also indeed how it's used in 
all applications.  For instance, one lemma says, if f is positive, so is 
`suminf f`:

   [ext_suminf_pos]  Theorem
  ⊢ ∀f. (∀n. 0 ≤ f n) ⇒ 0 ≤ suminf f

However, I found that the above lemma can be proved even without knowing 
anything of `f`, see the following proofs:

Theorem ext_suminf_pos_bug :
!f. 0 <= ext_suminf f
Proof
RW_TAC std_ss [ext_suminf_def]
 >> MATCH_MP_TAC le_sup_imp'
 >> REWRITE_TAC [IN_IMAGE, IN_UNIV]
 >> Q.EXISTS_TAC `0` >> BETA_TAC
 >> REWRITE_TAC [COUNT_ZERO, EXTREAL_SUM_IMAGE_EMPTY]
QED

where [le_sup_imp'] is a version of [le_sup_imp] before applying IN_APP:

   [le_sup_imp']  Theorem
  
  ⊢ ∀p x. x ∈ p ⇒ x ≤ sup p

For the reason, ext_suminf is actually calculating the sup of the following 
values:

0
f(0)
f(0) + f(1)
f(0) + f(1) + f(2)
...

The first line (0) comes from `count 0 = {}` where `0 IN univ(:num)`, then 
SUM_IMAGE f {} = 0.

Now consider f = (\n. -1), the above list of values are: 0, -1, -2, -3   
But since the sup of a set containing 0 is at least 0, the `suminf f` in this 
case will be 0 (instead of the correct value -1).  This is why `0 <= suminf f` 
holds for whatever f.

I believe Isabelle's suminf (in Extended_Real.thy) has the same problem (but I 
can't find its definition, correct me if I'm wrong here), i.e. the following 
theorem holds even without the "assumes":

lemma suminf_0_le:
  fixes f :: "nat ⇒ ereal"
  assumes "⋀n. 0 ≤ f n"
  shows "0 ≤ (∑n. f n)"
  using suminf_upper[of f 0, OF assms]
  by simp

The solution is quite obvious. I'm going to fix HOL's definition of ext_suminf 
with the following one:

val ext_suminf_def = Define
   `ext_suminf f = sup (IMAGE (\n. SIGMA f (count (SUC n))) UNIV)`;

That is, using `SUC n` intead of `n` to eliminate the fake base case (0). I 
believe this change only causes minor incompatibilities.

Any comment?

Regards,

Chun Tian



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

A follow-up of this old topic:

Finally I found the following definitions of `extreal_inv` and `extreal_div` 
based on new_specification():

local
  val lemma = Q.prove (
 `?i. (i NegInf = Normal 0) /\
  (i PosInf = Normal 0) /\
  (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`,
   (* proof *)
  Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0
else if x = Normal 0 then ARB
else Normal (inv (real x))` \\
  RW_TAC std_ss [extreal_not_infty, real_normal]);
in
  (* |- extreal_inv NegInf = Normal 0 /\
extreal_inv PosInf = Normal 0 /\
!r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r)
   *)
  val extreal_inv_def = new_specification
("extreal_inv_def", ["extreal_inv"], lemma);
end;

local
  val lemma = Q.prove (
 `?d. (!r. d (Normal r) PosInf = Normal 0) /\
  (!r. d (Normal r) NegInf = Normal 0) /\
  (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv 
(Normal r`,
   (* proof *)
  Q.EXISTS_TAC `\x y.
if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0
else if y = Normal 0 then ARB
else extreal_mul x (extreal_inv y)` \\
  RW_TAC std_ss [extreal_not_infty, real_normal]);
in
  (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\
(!r. extreal_div (Normal r) NegInf = Normal 0) /\
!x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r)
   *)
  val extreal_div_def = new_specification
("extreal_div_def", ["extreal_div"], lemma);
end;

In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* 
undefined.

--Chun

Il 20/02/19 06:48, michael.norr...@data61.csiro.au ha scritto:
> Your right hand side is no better than ARB really.  You say that your aim is 
> to avoid x/0 = y, with y a literal extreal.  But if you believe ARB is a 
> literal extreal, then I will define
> 
>   val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`;
> 
> and then I can certainly prove that x/0 = pni.  If ARB is a literal extreal, 
> surely pni is too.
> 
> (Recall that ARB's definition is `ARB = @x. T`.)
> 
> Michael
> 
> 
> On 20/2/19, 09:31, "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

Re: [Hol-info] How to express a finite_map or alist using a key list and a value list?

[Chun Tian (binghe)]

Hi Konrad,

thanks for pointing me to balanced_mapTheory, where I found some useful 
LIST_REL related theorems, but the "fromList" is not what I can use.

After another look into listTheory, I think my previous alist built by MAP2 can 
be also done by ZIP. So I'm going to use ZIP for now.

--Chun

Il 07/08/19 20:05, Konrad Slind ha scritto:
> See also examples/balanced_bst/balanced_mapTheory, which has a "fromList" 
> construct.
> That does have the requirement of having the domain type capable of being 
> ordered.
> 
> Konrad.
> 
> 
> On Wed, Aug 7, 2019 at 3:45 AM Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> I wonder what's the most natural/native way to express a finite_map or 
> alist, using a key list and a value list (assuming their lengths are the 
> same, and the key list is all distinct)?
> 
> My current idea is to use MAP2 to build an alist of type ``:('a # 'b) 
> list``:
> 
>         MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)
> 
> then (if needed), `alist_to_fmap` will lead me to a finite_map. But 
> shouldn't it be already provided by a definition in alistTheory (or 
> finite_mapTheory) that I just didn't find out?
> 
> --Chun
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] How to express a finite_map or alist using a key list and a value list?

[Chun Tian (binghe)]

Hi,

I wonder what's the most natural/native way to express a finite_map or alist, 
using a key list and a value list (assuming their lengths are the same, and the 
key list is all distinct)?

My current idea is to use MAP2 to build an alist of type ``:('a # 'b) list``:

MAP2 (\k v. (k,v)) (ks :'a list) (vs :'b list)

then (if needed), `alist_to_fmap` will lead me to a finite_map. But shouldn't 
it be already provided by a definition in alistTheory (or finite_mapTheory) 
that I just didn't find out?

--Chun



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] "Wrong" definitions of transcendental functions (sin, cos, exp)?

[Chun Tian (binghe)]

Sorry... I'm wrong, these definitions are correct.  I was confused by
the definition of "suminf" for reals with the one for extreals.   The
one for reals is based on "sums" and "convergent", should be able to
handle negative values.

So, it should be possible to prove a full version of EXP_LE_X.

--Chun

Il 18/03/19 20:05, Chun Tian (binghe) ha scritto:
> Hi,
> 
> does anyone notice that, the 3 basic transcendental functions (sin, cos,
> exp) in HOL4 are only correctly defined on positive inputs?
> 
> I say this because all these definitions are based on suminf which gives
> desired results only for all positive summations:
> 
>[exp]  Definition
> 
>   ⊢ ∀x. exp x = suminf (λn. (λn. ( n)⁻¹) n * x pow n)
> 
>[sin]  Definition
> 
>⊢ ∀x.
>  sin x =
>  suminf
>(λn.
>  (λn. if EVEN n then 0
>   else -1 pow ((n − 1) DIV 2) /  n) n * x pow n)
> 
>[cos]  Definition
> 
>⊢ ∀x.
>  cos x =
>  suminf
>(λn.
>  (λn. if EVEN n then -1 pow (n DIV 2) /  n else 0) n *
> x pow n)
> 
> where suminf is the sup of partial sums of first n items:
> 
>> suminf;
> val it = ⊢ ∀f. suminf f = @s. f sums s: thm
>> sums;
> val it = ⊢ ∀f s. f sums s ⇔ (λn. sum (0,n) f) ⟶ s: thm
> 
> by definition, exp x = 1 + x + x^2/2! + x^3/3! + ..., but if x < 0, the
> summation will be alternatively positive and negative, the "sup" should
> be the first item, i.e. with some efforts one should be able to prove:
> !x. x < 0 ==> (exp(x) = 1)
> 
> --Chun
> 
> - below are some background story 
> 
> yesterday I started to need a small result of exponential function
> (exp), namely:
> 
> |- !x. &0 <= x ==> (&1 - x) <= exp (-x)
> 
> I noticed that, HOL Light has a theorem (REAL_EXP_LE_X) in its
> "Multivariate/transcendental.ml" saying:
> 
> |- !x. &1 + x <= exp(x)
> 
> this would be one I need (by instantiating `x` to `-x`) but in HOL4 I
> only see a restricted version (EXP_LE_X) with antecedents `0 <= x` in
> "src/real/transcScript.sml":
> 
> |- !x. &0 <= x ==> (&1 + x) <= exp(x)
> 
> Obviously this theorem (and the whole transcTheory) was ported from HOL
> Light's "Library/transc.ml" (REAL_EXP_LE_X), because all definitions and
> proofs are essentially identical.
> 
> I can't easily port REAL_EXP_LE_X from HOL Light's
> "Multivariate/transcendental.ml", because the "exp" there was defined as
> the real part of complex-valued "exp". So I started to prove the full
> version of EXP_LE_X by myself.  My idea was to use the existing EXP_LE_X
> for the case "0 <= x", and the case `x < -1` is trivial, because `1 + x
> < 0` and `0 <= exp(x)`. Thus I only need to prove for the case `-1 <= x
> < 0`:
> 
>0 ≤ f x
>
>  0.  x < 0
>  1.  -1 < x
>  2.  Abbrev (f = (λx. exp x − (1 + x)))
>  3.  Abbrev (g = (λx. exp x − 1))
>  4.  ∀x. (f diffl g x) x
>  5.  ∀x. x ≤ 0 ⇒ g x ≤ 0
>  6.  f 0 = 0
>: proof
> 
> so far so good, I have proved that, the differentiation 'g' of f(x) =
> exp(x) - (1+x) is negative in [-1,0], and f(0) = 0. Then I was going to
> look into my calculus books to find proofs that f() is mono-decreasing
> in [-1,0] to finish the entire proof. Then, I suddenly found the sad
> news, that HOL4's "exp" function is not correctly defined on negative
> inputs.
> 
> 
> 
> 
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] "Wrong" definitions of transcendental functions (sin, cos, exp)?

[Chun Tian (binghe)]

Hi,

does anyone notice that, the 3 basic transcendental functions (sin, cos,
exp) in HOL4 are only correctly defined on positive inputs?

I say this because all these definitions are based on suminf which gives
desired results only for all positive summations:

   [exp]  Definition

  ⊢ ∀x. exp x = suminf (λn. (λn. ( n)⁻¹) n * x pow n)

   [sin]  Definition

   ⊢ ∀x.
 sin x =
 suminf
   (λn.
 (λn. if EVEN n then 0
  else -1 pow ((n − 1) DIV 2) /  n) n * x pow n)

   [cos]  Definition

   ⊢ ∀x.
 cos x =
 suminf
   (λn.
 (λn. if EVEN n then -1 pow (n DIV 2) /  n else 0) n *
x pow n)

where suminf is the sup of partial sums of first n items:

> suminf;
val it = ⊢ ∀f. suminf f = @s. f sums s: thm
> sums;
val it = ⊢ ∀f s. f sums s ⇔ (λn. sum (0,n) f) ⟶ s: thm

by definition, exp x = 1 + x + x^2/2! + x^3/3! + ..., but if x < 0, the
summation will be alternatively positive and negative, the "sup" should
be the first item, i.e. with some efforts one should be able to prove:
!x. x < 0 ==> (exp(x) = 1)

--Chun

- below are some background story 

yesterday I started to need a small result of exponential function
(exp), namely:

|- !x. &0 <= x ==> (&1 - x) <= exp (-x)

I noticed that, HOL Light has a theorem (REAL_EXP_LE_X) in its
"Multivariate/transcendental.ml" saying:

|- !x. &1 + x <= exp(x)

this would be one I need (by instantiating `x` to `-x`) but in HOL4 I
only see a restricted version (EXP_LE_X) with antecedents `0 <= x` in
"src/real/transcScript.sml":

|- !x. &0 <= x ==> (&1 + x) <= exp(x)

Obviously this theorem (and the whole transcTheory) was ported from HOL
Light's "Library/transc.ml" (REAL_EXP_LE_X), because all definitions and
proofs are essentially identical.

I can't easily port REAL_EXP_LE_X from HOL Light's
"Multivariate/transcendental.ml", because the "exp" there was defined as
the real part of complex-valued "exp". So I started to prove the full
version of EXP_LE_X by myself.  My idea was to use the existing EXP_LE_X
for the case "0 <= x", and the case `x < -1` is trivial, because `1 + x
< 0` and `0 <= exp(x)`. Thus I only need to prove for the case `-1 <= x
< 0`:

   0 ≤ f x
   
 0.  x < 0
 1.  -1 < x
 2.  Abbrev (f = (λx. exp x − (1 + x)))
 3.  Abbrev (g = (λx. exp x − 1))
 4.  ∀x. (f diffl g x) x
 5.  ∀x. x ≤ 0 ⇒ g x ≤ 0
 6.  f 0 = 0
   : proof

so far so good, I have proved that, the differentiation 'g' of f(x) =
exp(x) - (1+x) is negative in [-1,0], and f(0) = 0. Then I was going to
look into my calculus books to find proofs that f() is mono-decreasing
in [-1,0] to finish the entire proof. Then, I suddenly found the sad
news, that HOL4's "exp" function is not correctly defined on negative
inputs.







signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

[Chun Tian (binghe)]

Thanks, my problem has been resolved using inductions.

I'm actually using extrealTheory. All I have for the necessary and
sufficient condition of a suminf being PosInf is the following:

   [ext_suminf_eq_infty]  Theorem

  ⊢ ∀f.
(∀n. 0 ≤ f n) ∧ (∀e. e < PosInf ⇒ ∃n. e ≤ ∑ f (count n)) ⇒
(suminf f = PosInf)

   [ext_suminf_eq_infty_imp]  Theorem

  ⊢ ∀f.
(∀n. 0 ≤ f n) ∧ (suminf f = PosInf) ⇒
∀e. e < PosInf ⇒ ∃n. e ≤ ∑ f (count n)

In my case, given any `e < PosInf`, it's very hard to construct such a
`n` directly, but, as I found before (based on your approach), an
induction approach works, and it turns out that the proof is quite
straightforward although not very short.

--Chun

Il 02/03/19 03:05, Haitao Zhang ha scritto:
> I assume you are using the theory from src/real/seqScript.sml and it
> looks like that summable is defined as a convergence of partial sums.
> That means you should be able to directly contradict the convergence
> criterion if (f n) does not go to 0. For example, SER_CAUCHY gives you:
> 
> “!f. summable f =
>   !e. &0 < e ==> ?N. !m n. m >= N ==> abs(sum(m,n) f) < e”
> 
> Choose e < 1, for any N, find n>N such that f n = 1, then abs(sum(n,n+1)
> f)=1 > e and contradiction. (I don't know the indexing of sum so it
> could be sum(n,n)).
> 
> Hope this helps,
> Haitao
> 
> 
> 
> On Fri, Mar 1, 2019 at 12:46 PM Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> wrote:
> 
> there’s is a typo in my previous post. I wanted to ask “…, why f
> must *not* be summable?” (i.e. divergent)
> 
> On a second thought, your approach could work for proving the
> partial sum is unbounded: for any real number e > 0, I can first use
> Archimedean property (simple version) of reals to find an integer N
> such that e < N, then I repeat N times your approach, first let the
> partial sum >= 1, then >= 2, … finally >= N, by induction, then the
> whole proof finished.  However to implement this idea it’s not easy
> to me. Still want to know better proofs.
> 
> —Chun
> 
> > Il giorno 01 mar 2019, alle ore 20:54, Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> ha scritto:
> >
> > Hi Haitao,
> >
> > thanks, and yes, f is a sequence of reals.  I'm following a
> similar path
> > (proof by contradiction), but I don't understand the last step:
> for any
> > m, the partial sum of f goes up by 1 at n > m, why f must be
> summable? I
> > think for every monotonic sequence such properties hold.
> >
> > --Chun
> >
> > Il 01/03/19 17:24, Haitao Zhang ha scritto:
> >> You say f is a function. From the context I assume the domain is
> Nat or
> >> f is a sequence. Mathematically speaking, you should form the partial
> >> sums of f ( sum f from 1 to n), which is a monotonic sequence of
> nats.
> >> Now proof by contradiction: if your conclusion doesn’t hold, for
> any m,
> >> you can find n > m, such that f n = 1. Then the partial sum goes
> up by 1
> >> at n. As m is arbitrary, f is not summable.
> >>
> >> However I don’t know what is the best way to carry out the above
> proof
> >> in hol as I am not familiar with the relevant libraries yet.
> >>
> >> Haitao
> >>
> >> On Friday, March 1, 2019, Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>
> >> <mailto:binghe.l...@gmail.com <mailto:binghe.l...@gmail.com>>> wrote:
> >>
> >>    Hi,
> >>
> >>    I'm blocked at the following goal:
> >>
> >>    I have a function f returning either 0 or 1.  Now I know the
> infinite
> >>    sum of f is finite, i.e.
> >>
> >>            suminf f < PosInf       (or `summable f` speaking reals)
> >>
> >>    How can I prove the set of {x | f x = 1} is finite, or after
> certain
> >>    index m all the rest f(n) are zeros?
> >>
> >>            ∃m. ∀n. m ≤ n ⇒ (f n = 0)
> >>
> >>    If I use CCONTR_TAC (proof by contradiction), I can easily
> derive the
> >>    following 2 assumptions using results I established in my previous
> >>    similar questions:
> >>
> >>            INFINITE N
> >>            ∀n. n ∈ N ⇒ (f n = 1)
> >>
> >>    but still I've no idea how to derive a contradiction with
> `suminf f <
> >>    PosInf` by proving `suminf f = PosInf`...
> >>
> >>    Thanks,
> >>
> >>    Chun Tian
> >>
> >
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

[Chun Tian (binghe)]

Hello Mr. Saitoh,

1. I'm not professor, I'm first-year PhD.
2. your recent behaviors on Isabelle and HOL's mailing list have hurt the
reputation of Japanese (or even Asian) researchers.
3. I'm not interested in your paper - actually I'm against any arithmetic
with division-by-zero.

So please don't do this again.

--Chun


On Fri, Mar 1, 2019 at 10:12 PM Saburou Saitoh 
wrote:

> Dear Professors Tian and Zhang:
>
> I am very interesting your communication on summable, however, I would
> like to read them carefully.
> We got a new idea; the area of disc with radius r is of course \pi r^2,
> however for r = infinity; in the entire plane, its area is zero!!.
>
> I will send some related article by separate e-mail.
>
> However, please look this:
>
> [5] *viXra:1902.0240 <http://vixra.org/abs/1902.0240>* *submitted on
> 2019-02-13 22:57:25*, (0 unique-IP downloads)
>
> *Zero and Infinity; Their Interrelation by Means of Division by Zero*
>
> *Authors:* *Saburou Saitoh <http://vixra.org/author/saburou_saitoh>*
> *Category:* General Mathematics <http://vixra.org/math>
>
>
>
> With best regards,
>
> Sincerely yours,
>
>
> Saburou Saitoh
>
> 2019.3.2.6:11
>
>
>
>
> 2019年3月2日(土) 5:47 Chun Tian (binghe) :
>
>> there’s is a typo in my previous post. I wanted to ask “…, why f must
>> *not* be summable?” (i.e. divergent)
>>
>> On a second thought, your approach could work for proving the partial sum
>> is unbounded: for any real number e > 0, I can first use
>> Archimedean property (simple version) of reals to find an integer N such
>> that e < N, then I repeat N times your approach, first let the partial sum
>> >= 1, then >= 2, … finally >= N, by induction, then the whole proof
>> finished.  However to implement this idea it’s not easy to me. Still want
>> to know better proofs.
>>
>> —Chun
>>
>> > Il giorno 01 mar 2019, alle ore 20:54, Chun Tian (binghe) <
>> binghe.l...@gmail.com> ha scritto:
>> >
>> > Hi Haitao,
>> >
>> > thanks, and yes, f is a sequence of reals.  I'm following a similar path
>> > (proof by contradiction), but I don't understand the last step: for any
>> > m, the partial sum of f goes up by 1 at n > m, why f must be summable? I
>> > think for every monotonic sequence such properties hold.
>> >
>> > --Chun
>> >
>> > Il 01/03/19 17:24, Haitao Zhang ha scritto:
>> >> You say f is a function. From the context I assume the domain is Nat or
>> >> f is a sequence. Mathematically speaking, you should form the partial
>> >> sums of f ( sum f from 1 to n), which is a monotonic sequence of nats.
>> >> Now proof by contradiction: if your conclusion doesn’t hold, for any m,
>> >> you can find n > m, such that f n = 1. Then the partial sum goes up by
>> 1
>> >> at n. As m is arbitrary, f is not summable.
>> >>
>> >> However I don’t know what is the best way to carry out the above proof
>> >> in hol as I am not familiar with the relevant libraries yet.
>> >>
>> >> Haitao
>> >>
>> >> On Friday, March 1, 2019, Chun Tian (binghe) > >> <mailto:binghe.l...@gmail.com>> wrote:
>> >>
>> >>Hi,
>> >>
>> >>I'm blocked at the following goal:
>> >>
>> >>I have a function f returning either 0 or 1.  Now I know the
>> infinite
>> >>sum of f is finite, i.e.
>> >>
>> >>suminf f < PosInf   (or `summable f` speaking reals)
>> >>
>> >>How can I prove the set of {x | f x = 1} is finite, or after certain
>> >>index m all the rest f(n) are zeros?
>> >>
>> >>∃m. ∀n. m ≤ n ⇒ (f n = 0)
>> >>
>> >>If I use CCONTR_TAC (proof by contradiction), I can easily derive
>> the
>> >>following 2 assumptions using results I established in my previous
>> >>similar questions:
>> >>
>> >>INFINITE N
>> >>∀n. n ∈ N ⇒ (f n = 1)
>> >>
>> >>but still I've no idea how to derive a contradiction with `suminf f
>> <
>> >>PosInf` by proving `suminf f = PosInf`...
>> >>
>> >>Thanks,
>> >>
>> >>Chun Tian
>> >>
>> >
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>

-- 

Chun Tian (binghe)
Fondazione Bruno Kessler (Italy)
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

[Chun Tian (binghe)]

there’s is a typo in my previous post. I wanted to ask “…, why f must *not* be 
summable?” (i.e. divergent)

On a second thought, your approach could work for proving the partial sum is 
unbounded: for any real number e > 0, I can first use
Archimedean property (simple version) of reals to find an integer N such that e 
< N, then I repeat N times your approach, first let the partial sum >= 1, then 
>= 2, … finally >= N, by induction, then the whole proof finished.  However to 
implement this idea it’s not easy to me. Still want to know better proofs.

—Chun

> Il giorno 01 mar 2019, alle ore 20:54, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi Haitao,
> 
> thanks, and yes, f is a sequence of reals.  I'm following a similar path
> (proof by contradiction), but I don't understand the last step: for any
> m, the partial sum of f goes up by 1 at n > m, why f must be summable? I
> think for every monotonic sequence such properties hold.
> 
> --Chun
> 
> Il 01/03/19 17:24, Haitao Zhang ha scritto:
>> You say f is a function. From the context I assume the domain is Nat or
>> f is a sequence. Mathematically speaking, you should form the partial
>> sums of f ( sum f from 1 to n), which is a monotonic sequence of nats.
>> Now proof by contradiction: if your conclusion doesn’t hold, for any m,
>> you can find n > m, such that f n = 1. Then the partial sum goes up by 1
>> at n. As m is arbitrary, f is not summable.
>> 
>> However I don’t know what is the best way to carry out the above proof
>> in hol as I am not familiar with the relevant libraries yet.
>> 
>> Haitao
>> 
>> On Friday, March 1, 2019, Chun Tian (binghe) > <mailto:binghe.l...@gmail.com>> wrote:
>> 
>>Hi,
>> 
>>I'm blocked at the following goal:
>> 
>>I have a function f returning either 0 or 1.  Now I know the infinite
>>sum of f is finite, i.e.
>> 
>>suminf f < PosInf   (or `summable f` speaking reals)
>> 
>>How can I prove the set of {x | f x = 1} is finite, or after certain
>>index m all the rest f(n) are zeros?
>> 
>>∃m. ∀n. m ≤ n ⇒ (f n = 0)
>> 
>>If I use CCONTR_TAC (proof by contradiction), I can easily derive the
>>following 2 assumptions using results I established in my previous
>>similar questions:
>> 
>>INFINITE N
>>∀n. n ∈ N ⇒ (f n = 1)
>> 
>>but still I've no idea how to derive a contradiction with `suminf f <
>>PosInf` by proving `suminf f = PosInf`...
>> 
>>Thanks,
>> 
>>Chun Tian
>> 
> 



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

Re: [Hol-info] An infinite sum of 0 or 1 is finite, then ...

[Chun Tian (binghe)]

Hi Haitao,

thanks, and yes, f is a sequence of reals.  I'm following a similar path
(proof by contradiction), but I don't understand the last step: for any
m, the partial sum of f goes up by 1 at n > m, why f must be summable? I
think for every monotonic sequence such properties hold.

--Chun

Il 01/03/19 17:24, Haitao Zhang ha scritto:
> You say f is a function. From the context I assume the domain is Nat or
> f is a sequence. Mathematically speaking, you should form the partial
> sums of f ( sum f from 1 to n), which is a monotonic sequence of nats.
> Now proof by contradiction: if your conclusion doesn’t hold, for any m,
> you can find n > m, such that f n = 1. Then the partial sum goes up by 1
> at n. As m is arbitrary, f is not summable.
> 
> However I don’t know what is the best way to carry out the above proof
> in hol as I am not familiar with the relevant libraries yet.
> 
> Haitao
> 
> On Friday, March 1, 2019, Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> I'm blocked at the following goal:
> 
> I have a function f returning either 0 or 1.  Now I know the infinite
> sum of f is finite, i.e.
> 
>         suminf f < PosInf       (or `summable f` speaking reals)
> 
> How can I prove the set of {x | f x = 1} is finite, or after certain
> index m all the rest f(n) are zeros?
> 
>         ∃m. ∀n. m ≤ n ⇒ (f n = 0)
> 
> If I use CCONTR_TAC (proof by contradiction), I can easily derive the
> following 2 assumptions using results I established in my previous
> similar questions:
> 
>         INFINITE N
>         ∀n. n ∈ N ⇒ (f n = 1)
> 
> but still I've no idea how to derive a contradiction with `suminf f <
> PosInf` by proving `suminf f = PosInf`...
> 
> Thanks,
> 
> Chun Tian
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] An infinite sum of 0 or 1 is finite, then ...

[Chun Tian (binghe)]

Hi,

I'm blocked at the following goal:

I have a function f returning either 0 or 1.  Now I know the infinite
sum of f is finite, i.e.

suminf f < PosInf   (or `summable f` speaking reals)

How can I prove the set of {x | f x = 1} is finite, or after certain
index m all the rest f(n) are zeros?

∃m. ∀n. m ≤ n ⇒ (f n = 0)

If I use CCONTR_TAC (proof by contradiction), I can easily derive the
following 2 assumptions using results I established in my previous
similar questions:

INFINITE N
∀n. n ∈ N ⇒ (f n = 1)

but still I've no idea how to derive a contradiction with `suminf f <
PosInf` by proving `suminf f = PosInf`...

Thanks,

Chun Tian



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Sorting a finite sequence of disjoint sets?

[Chun Tian (binghe)]

Hi Thomas,

thanks! Now I see the chances to solve my problem using sortingTheory.

--Chun

Il 25/02/19 20:46, Thomas Sewell ha scritto:
> I think that the set type here is irrelevant. You have a relation for
> sorting elements in the range of f. Construct the list of applications
> of f to 0..(n-1), sort that using the sort operation from sortingTheory,
> and make g from the list index operator applied to that. 
> 
> Cheers, 
>     Thomas. 
> 
> 
> 
> Sent from my Samsung Galaxy smartphone.
> 
> 
> ---- Original message 
> From: "Chun Tian (binghe)" 
> Date: 25/02/2019 15:02 (GMT+01:00)
> To: HOL-info list 
> Subject: [Hol-info] Sorting a finite sequence of disjoint sets?
> 
> Hi,
> 
> suppose I have a finite sequence of n disjoint sets, given by a function
> (f :num -> ‘a -> bool), and their union is BIGUNION (IMAGE f (count n)),
> and an order R (antisymmetric
> , transitive) on these sets.
> 
> Is it possible to assert the existence of another function (g :num -> ‘a
> -> bool) such that:
> 
>     BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))
> 
> and
> 
>     !i j. i < n /\ j < n ==> R (g i) (g j)
> 
> ?
> 
> That’s, I want to “sort” these set according to this order. Does it
> exist for sure?  Is there anything from the existing “sortingTheory”
> that I can leverage?
> 
> Regards,
> 
> Chun Tian
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Sorting a finite sequence of disjoint sets?

[Chun Tian (binghe)]

Hi,

suppose I have a finite sequence of n disjoint sets, given by a function (f 
:num -> ‘a -> bool), and their union is BIGUNION (IMAGE f (count n)), and an 
order R (antisymmetric
, transitive) on these sets.

Is it possible to assert the existence of another function (g :num -> ‘a -> 
bool) such that:

BIGUNION (IMAGE f (count n)) = BIGUNION (IMAGE g (count n))

and

!i j. i < n /\ j < n ==> R (g i) (g j)

?

That’s, I want to “sort” these set according to this order. Does it exist for 
sure?  Is there anything from the existing “sortingTheory” that I can leverage?

Regards,

Chun Tian



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

Re: [Hol-info] The equivalence of two definitions of "inf" (infimum) of real sets?

[Chun Tian (binghe)]

Hi Michael,

thanks for the explanation in details! Now I finally understand why the
two versions of `sup` can be proved equivalent, while the two "inf"
cannot.  Any way, I'll follow your idea and submit a fix of the
duplicated definitions of `inf` soon.

--Chun

Il 23/02/19 07:00, michael.norr...@data61.csiro.au ha scritto:
> It’s possible that both definitions will turn into applications of
> Hilbert choice applied to equivalent predicates. 
> 
>  
> 
> If inf1 s = @x. P x, and inf2 s = @x. Q x, but it happens that !x. P x
> <=> Q x, then it is indeed the case that inf1 = inf2, even on arguments
> where you’d prefer them not to be defined.  Equally though, it’s quite
> reasonable to imagine that they weren’t defined so conveniently, and you
> will just have
> 
>  
> 
>    s has-a-lower-bound ==> (inf1 s = inf2 s)
> 
>  
> 
> In this situation, I might prove the above, and then replace all the
> occurrences of one with the other under the expectation that the
> theorems about the one that is replaced are just as true of the other.
> 
>  
> 
> Michael
> 
>  
> 
> *From: *"Chun Tian (binghe)" 
> *Date: *Thursday, 21 February 2019 at 20:52
> *To: *hol-info 
> *Subject: *[Hol-info] The equivalence of two definitions of "inf"
> (infimum) of real sets?
> 
>  
> 
> Hi,
> 
>  
> 
> (this is another (strange) question about undefined values in total
> functions)
> 
>  
> 
> currently there’re two definitions of “inf” (infimum) for real sets in
> HOL4, one is at “src/real/realScript.sml”:
> 
>    [*inf_def*]  Definition
> 
>   
> 
>   ⊢ ∀p. inf p = -sup (λr. p (-r))
> 
> The other is at “src/probability/iterateScript.sml”, ported from HOL Light:
> 
>  
> 
>    [*inf*]  Definition
> 
>   
> 
>   ⊢ ∀s.
> 
>     inf s =
> 
>     @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
> 
> I believe they’re both correct definitions, as the related theorems
> derived from them all make senses. However, if I load “iterateTheory”,
> or “real_topologyTheory” which in turn uses “iterateTheory”, than all
> theorems about the “inf” defined at “realTheory” would be invalid, as
> they’re not for the latest “inf”.  Thus my goal is to merge the two
> definitions of “inf” and have a precise union of all theorems about them.
> 
>  
> 
> Usually this kind of definition merging is done by changing the later
> definition (in iterateTheory) into an equivalent theorem, i.e. to prove that
> 
>  
> 
> |- ∀s. inf s = @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
> 
>  
> 
> given the definition: inf p = -sup (λr. p (-r))
> 
>  
> 
> But I *feel* this is impossible, because “inf” of real set is not
> defined on all real sets. If I temporarily use ``inf’`` as the
> alternative definition of “inf” in iterateTheory, the above equivalent
> theorem becomes:
> 
>  
> 
> |- ∀s. inf s = inf’ s
> 
>  
> 
> but for s = {}, or any real sets without a lower bound, either “inf s”
> or “inf’ s” is not defined, should above theorem still be proved?  If
> not, then I have to re-prove all “inf” theorems in iterateTheory using
> lemmas from realTheory. This is more difficult.
> 
>  
> 
> Regards,
> 
>  
> 
> Chun Tian
> 
>  
> 
> P. S. in extrealTheory, “sup” and “inf” are really total functions, thus
> much easier to work with, e.g. I can prove things like: (in at least one
> of my Math book, it said “inf {} = PosInf” must be specially defined,
> but this is actually not needed)
> 
>    [*sup_empty*]  Theorem
> 
>   
> 
>   ⊢ sup ∅ = NegInf
> 
>    [*inf_empty*]  Theorem
> 
>   
> 
>   ⊢ inf ∅ = PosInf
> 
>    [*inf_univ*]  Theorem
> 
>   
> 
>   ⊢ inf 핌(:extreal) = NegInf
> 
>    [*sup_univ*]  Theorem
> 
>   
> 
>   ⊢ sup 핌(:extreal) = PosInf
> 
>  
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] The equivalence of two definitions of "inf" (infimum) of real sets?

[Chun Tian (binghe)]

Hi,

(this is another (strange) question about undefined values in total functions)

currently there’re two definitions of “inf” (infimum) for real sets in HOL4, 
one is at “src/real/realScript.sml”:
   [inf_def <>]  Definition

  ⊢ ∀p. inf p = -sup (λr. p (-r))
The other is at “src/probability/iterateScript.sml”, ported from HOL Light:

   [inf <>]  Definition

  ⊢ ∀s.
inf s =
@a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a
I believe they’re both correct definitions, as the related theorems derived 
from them all make senses. However, if I load “iterateTheory”, or 
“real_topologyTheory” which in turn uses “iterateTheory”, than all theorems 
about the “inf” defined at “realTheory” would be invalid, as they’re not for 
the latest “inf”.  Thus my goal is to merge the two definitions of “inf” and 
have a precise union of all theorems about them.

Usually this kind of definition merging is done by changing the later 
definition (in iterateTheory) into an equivalent theorem, i.e. to prove that

|- ∀s. inf s = @a. (∀x. x ∈ s ⇒ a ≤ x) ∧ ∀b. (∀x. x ∈ s ⇒ b ≤ x) ⇒ b ≤ a

given the definition: inf p = -sup (λr. p (-r))

But I *feel* this is impossible, because “inf” of real set is not defined on 
all real sets. If I temporarily use ``inf’`` as the alternative definition of 
“inf” in iterateTheory, the above equivalent theorem becomes:

|- ∀s. inf s = inf’ s

but for s = {}, or any real sets without a lower bound, either “inf s” or “inf’ 
s” is not defined, should above theorem still be proved?  If not, then I have 
to re-prove all “inf” theorems in iterateTheory using lemmas from realTheory. 
This is more difficult.

Regards,

Chun Tian

P. S. in extrealTheory, “sup” and “inf” are really total functions, thus much 
easier to work with, e.g. I can prove things like: (in at least one of my Math 
book, it said “inf {} = PosInf” must be specially defined, but this is actually 
not needed)
   [sup_empty <>]  Theorem

  ⊢ sup ∅ = NegInf
   [inf_empty <>]  Theorem

  ⊢ inf ∅ = PosInf
   [inf_univ <>]  Theorem

  ⊢ inf 핌(:extreal) = NegInf
   [sup_univ <>]  Theorem

  ⊢ sup 핌(:extreal) = PosInf



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

[Hol-info] subtypeTools (was Re: 0 / 0 = 0 ???)

[Chun Tian (binghe)]

Thanks for the paper links.

Actually I was long wondering what was under HOL’s "examples/miller/subtypes/“ 
folder, now I realized it’s the implementation of the idea in this paper.

There’re some example code at the end of subtypeTools.sml in that folder:

tt prove
(``~3 IN nzreal``,
 SUBTYPE_TAC (context_subtypes hol_c));

tt prove
(``(MAP inv (CONS (~1) (MAP sqrt [3; 1]))) IN list nzreal``,
 SUBTYPE_TAC (context_subtypes hol_c));

tt prove
(``(\x :: negreal. FUNPOW inv n x) IN negreal -> negreal``,
 SUBTYPE_TAC (context_subtypes hol_c));

tt prove
(``(!x :: nzreal. x / x = 1) ==> (5 / 5 = 3 / 3)``,
 SIMPLIFY_TAC hol_c []);

I wonder if this whole technique could also support parameters in the subtype, 
e.g. using n-length real-number lists as the type of points in n-dimension 
Euclidean space - the idea I learnt from hol-light’s Multivariate analysis 
formalization.  Things like ``!(x :: real^M) (y :: real^N). P x y`` would be 
nice.

P. S. currently HOL’s “real_topologyTheory” (ported from hol-light) only 
supports one-dimensional real number set, but the whole theory (and its 
original proof scripts in hol-light) were actually valid for arbitrary higher 
dimensions.   I’d like to have the same thing for HOL4 if possible.

—Chun

> Il giorno 20 feb 2019, alle ore 22:10, Umair Siddique  
> ha scritto:
> 
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101=rep1=pdf
>  
> 
> 
> http://www.gilith.com/talks/tphols2001-subtypes.pdf 
> 
> 
> 
> - Umair
> 
> On Wed, Feb 20, 2019 at 4:02 PM Freek Wiedijk  > wrote:
> Hi Ramana,
> 
> >I think this is exactly what is impossible to do in HOL:
> >it is a logic of total functions.
> 
> I think that in PVS you _can_ do something like that, right?
> Using the predicate subtypes.  Even though PVS _also_
> only has total functions.
> 
> And I _think_ there was a paper once about how to mimic
> predicate subtypes in HOL.  Does anyone remember the
> reference?
> 
> Freek
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> 
> ___
> 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

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

Well, as the purpose of optionTheory is to augment any type with one more 
value, for (at least) extreals, it would be equivalent to have that “undefined” 
thing defined as part of the datatype definition:

val extreal_def = Datatype
   `extreal = NegInf | PosInf | Normal real | Undefined`;

However, once “Undefined” is actually defined, it’s then a disaster to affect 
almost all arithmetic laws. For a number which is either PosInf nor NegInf, now 
we can’t say it must be a (Normal x) any more, and many theorems will be 
broken.  To fix it, we have to treat this “Undefined” as something like those 
NaNs in IEEE 754 standard and define their orders and arithmetic laws, then all 
these work are unnecessary for formalization of pure math theorems.

So I think the key is to make sure that “undefined” thing really undefined, 
such that whenever it appears, the proof cannot proceed any more, except for 
syntactic rewriting, which is inevitable in HOL.   Keeping ``0 / 0 = 0`` as 
before, could be another option, but I have concerns to convince mathematicians 
to accept this fact since I aim at precisely reproduce those pure math proofs 
under the “same” formal system with math books (except for the subtle 
differences between ZFC and HOL not affecting the math theories that I’m 
working with.)

—Chun

> Il giorno 20 feb 2019, alle ore 13:16, Ramana Kumar 
>  ha scritto:
> 
> I'd say one of the stronger ways to get "undefined" is to add an element to 
> your type representing undefinedness, e.g., make it (/) : real option -> real 
> option -> real option, where NONE represents "undefined". But then you will 
> have a lot of bookkeeping to deal with...
> I don't suggest this seriously in the case of division -- I would rather 
> suggest accepting the usual treatment of these partial functions as a small 
> price for the benefits of working in a logic of (only) total functions.
> 
> On Wed, 20 Feb 2019 at 12:00, Lawrence Paulson  > wrote:
> None of these attempts make any sense. In HOL and similar systems (including 
> Isabelle/HOL), it’s *impossible* to arrange for x/0 to be undefined in any 
> strong sense. Fortunately, it’s consistent and harmless to put x/0 = 0.
> 
> Larry Paulson
> 
> 
> > On 20 Feb 2019, at 05:48, hol-info-requ...@lists.sourceforge.net 
> >  wrote:
> >
> > I run some experiments so to check if it is violating any fundamental rule.
> > So far it went good.
> 
> 
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net 
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> 
> ___
> 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

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

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
>>>>

Re: [Hol-info] The remainder (tail) of an positive infinite summation?

[Chun Tian (binghe)]

Ha! that’s smart … thanks!

—Chun

> Il giorno 19 feb 2019, alle ore 17:23, buday.gerg...@uni-eszterhazy.hu ha 
> scritto:
> 
> Chun,
> 
> how about defining the sum of the tail as Limit minus the finite sum of the 
> first n elements?
> 
> - Gergely
> 
> Az Android Outlook <https://aka.ms/ghei36> letöltése
> 
> 
> 
> 
> On Tue, Feb 19, 2019 at 5:10 PM +0100, "Chun Tian (binghe)" 
> mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> I need to prove and then use a simple property of positive infinite 
> summations, i.e. if the summation `f(0)+f(1)+...` converges, the limit of its 
> "remainder after item n", i.e. `f(n)+f(n+1)+...` must be zero.  Current HOL4 
> doesn't provide this lemma, I haven't looked into Isabelle yet (don’t know 
> which file to look at …)
> 
> I know how to prove it by pencil and paper, but I don't know how to express 
> "remainder after item n" and its limit in a good way.
> 
> I'm dealing with extended reals, thus if that limit is `suminf_tail f`, my 
> desired lemma would be like this:
> 
> |- !f. (!n. 0 <= f n) /\ suminf f < PosInf ==> (suminf_tail f = 0)
> 
> So far I found two ways to define `f(n)+f(n+1)+...` given f and n. The first 
> way is to shift the argument by n:
> 
> (\n. suminf (\i. f (n + i
> 
> the second way is to forcely change the value of f(i) to zero if it's less 
> than n:
> 
> (\n. suminf (\i. if i < n then 0 else f i))
> 
> when n increasing above remainder as a function of n must decrease, thus to 
> get the limit ("-->" is not available in extrealTheory) I can use "inf" 
> instead:
> 
> suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. f (n + i))) UNIV)
> 
> or
> 
> suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. if i < n then 0 else 
> f i)) UNIV)
> 
> In the first way, I worry about the (n + i) part, which may brings 
> difficulties apply arithmetic laws. In the second way, case analysis at such 
> a deep nested level also scares me.
> 
> Does anyone have similar experiences?  Which one of the two definitions above 
> may be easier to handle? Are they correct? Is there any better way?
> 
> Regards,
> 
> Chun Tian
> 



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

[Hol-info] The remainder (tail) of an positive infinite summation?

[Chun Tian (binghe)]

Hi,

I need to prove and then use a simple property of positive infinite summations, 
i.e. if the summation `f(0)+f(1)+...` converges, the limit of its "remainder 
after item n", i.e. `f(n)+f(n+1)+...` must be zero.  Current HOL4 doesn't 
provide this lemma, I haven't looked into Isabelle yet (don’t know which file 
to look at …)

I know how to prove it by pencil and paper, but I don't know how to express 
"remainder after item n" and its limit in a good way.

I'm dealing with extended reals, thus if that limit is `suminf_tail f`, my 
desired lemma would be like this:

|- !f. (!n. 0 <= f n) /\ suminf f < PosInf ==> (suminf_tail f = 0)

So far I found two ways to define `f(n)+f(n+1)+...` given f and n. The first 
way is to shift the argument by n:

(\n. suminf (\i. f (n + i

the second way is to forcely change the value of f(i) to zero if it's less than 
n:

(\n. suminf (\i. if i < n then 0 else f i))

when n increasing above remainder as a function of n must decrease, thus to get 
the limit ("-->" is not available in extrealTheory) I can use "inf" instead:

suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. f (n + i))) UNIV)

or

suminf_tail f = extreal_inf (IMAGE (\n. suminf (\i. if i < n then 0 else f 
i)) UNIV)

In the first way, I worry about the (n + i) part, which may brings difficulties 
apply arithmetic laws. In the second way, case analysis at such a deep nested 
level also scares me.

Does anyone have similar experiences?  Which one of the two definitions above 
may be easier to handle? Are they correct? Is there any better way?

Regards,

Chun Tian



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

Re: [Hol-info] Dealing with INFINITE num set ...

[Chun Tian (binghe)]

Ah, thanks! sorry, I didn't see your replies before posting my last one.

Your proofs are much much shorter than mine, I'll use your versions instead!

--Chun

Il 16/02/19 22:48, Konrad Slind ha scritto:
> Rephrasing things might bring clarity:
> 
> load "pred_setLib";
> open pred_setTheory;
> 
> val set_ss = (arith_ss ++ pred_setLib.PRED_SET_ss);
> 
> val lem = Q.prove
> (`~(?N. INFINITE N /\ !n. N n ==> P n) <=> !N. N SUBSET P ==> FINITE N`,
>  rw_tac set_ss [EQ_IMP_THM,SUBSET_DEF,IN_DEF]
>   >- (`FINITE P \/ ?n. P n /\ ~P n` by metis_tac []
>        >> imp_res_tac SUBSET_FINITE
>        >> full_simp_tac std_ss [SUBSET_DEF, IN_DEF])
>   >- metis_tac[]);
> 
> From this and the original assumption, you should be able to get that P
> is finite, so has a maximum element.
> 
> Konrad.
> 
> 
> 
> On Fri, Feb 15, 2019 at 1:12 PM Chun Tian (binghe)
> mailto:binghe.l...@gmail.com>> wrote:
> 
> Hi,
> 
> I'm blocked at the following (strange) situation:
> 
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
> 
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
> 
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
> 
> ?m. !n. m <= n ==> ~(P n)
> 
> Thanks in advance,
> 
> Chun Tian
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Dealing with INFINITE num set ...

[Chun Tian (binghe)]

Cancel above questions. They're finally proved by myself using
FINITE_WEAK_ENUMERATE, FINITE_BIJ_COUNT_EQ, etc. [1]

   [infinity_bound_lemma]  Theorem

  ⊢ ∀N m. INFINITE N ⇒ ∃n. m ≤ n ∧ n ∈ N

   [infinity_often_lemma]  Theorem

  ⊢ ∀P. ¬(∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n) ⇔ ∃m. ∀n. m ≤ n ⇒ ¬P n

(they are related to Borel-Cantelli Lemma in Probability Theory)

Still want to know if there're shorter, more elegant proofs ... and
thanks all the same.

--Chun

[1]
https://github.com/binghe/HOL/blob/Probability-11/src/probability/util_probScript.sml
(line 1595-1638)

Il 15/02/19 20:46, Chun Tian (binghe) ha scritto:
> And also this one:
> 
> Given `INFINITE N` and a fixed number `m`, how can I assert the
> existence of another number `n` such that,
> 
> m <= n /\ n IN N
> 
> i.e. prove that
> 
> ``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``
> 
> --Chun
> 
> Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
>> Hi,
>>
>> I'm blocked at the following (strange) situation:
>>
>> I have an infinite set of integers (num) in which each integer n
>> satisfies a property P(n):
>>
>> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
>>
>> Suppose above proposition is NOT true, how can I derive that, there must
>> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
>>
>> ?m. !n. m <= n ==> ~(P n)
>>
>> Thanks in advance,
>>
>> Chun Tian
>>
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

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, since the
>>> definition
>>>     of `*` finally reduces to `*` of real numbers)
>>>
>>>     Regards,
>>>
>>>     Chun Tian
>>>
>>>     ___
>>>     hol-info mailing list
>>>     hol-info@lists.sourceforge.net
>>> <mailto:hol-info@lists.sourceforge.net>
>>>     https://lists.sourceforge.net/lists/listinfo/hol-info
>>>
>>
>>
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net
>> https://lists.sourceforge.net/lists/listinfo/hol-info



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Dealing with INFINITE num set ...

[Chun Tian (binghe)]

And also this one:

Given `INFINITE N` and a fixed number `m`, how can I assert the
existence of another number `n` such that,

m <= n /\ n IN N

i.e. prove that

``!N m. INFINITE N ==> ?n. m <= n /\ n IN N``

--Chun

Il 15/02/19 20:11, Chun Tian (binghe) ha scritto:
> Hi,
> 
> I'm blocked at the following (strange) situation:
> 
> I have an infinite set of integers (num) in which each integer n
> satisfies a property P(n):
> 
> ∃N. INFINITE N ∧ ∀n. n ∈ N ⇒ P n
> 
> Suppose above proposition is NOT true, how can I derive that, there must
> exist a number m such that for all n >= m, P(n) does NOT hold? i.e.
> 
> ?m. !n. m <= n ==> ~(P n)
> 
> Thanks in advance,
> 
> Chun Tian
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

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, since the definition
> of `*` finally reduces to `*` of real numbers)
> 
> Regards,
> 
> Chun Tian
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info
> 



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] 0 / 0 = 0 ???

[Chun Tian (binghe)]

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, since the definition
of `*` finally reduces to `*` of real numbers)

Regards,

Chun Tian



signature.asc
Description: OpenPGP digital signature
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Confused about Induct_on

[Chun Tian (binghe)]

Hi,

I think you should use HO_MATCH_MP_TAC (together with your induction theorem of 
“Gm”, of the form ``!Gm. X ==> P Gm``) in this case.  I only use Induct and 
Induct_on on simple variables like your Γ Γ’ A.

—Chun

> Il giorno 15 gen 2019, alle ore 14:49, Alexander Cox  ha 
> scritto:
> 
> I am having an issue using Induct_on on a Hol_reln called Gm.
> 
> If I try to use it on a trivial goal it works, e.g.
> 
> > g `!Γ A. Gm Γ A ==> Gm Γ A`;
> …
> > e (Induct_on `Gm`);
> OK..
> 1 subgoal:
> val it =
> 
> 
>(∀A. Gm {|A|} A) ∧ …
> 
> but if I use on a useful goal such as:
> 
> g `!Γ Γ' A. Gm Γ A ==> Gm (Γ' + Γ) A`;
> …
> e (Induct_on `Gm`);
> OK..
> 
> Exception raised at BasicProvers.Induct_on:
> at BasicProvers.induct_on_type:
> Type: :(α formula -> num) -> α formula -> bool is not registered in the types 
> database
> 
> Any ideas where I’m going wrong? Is the latter the goal in the wrong form? 
> Where should I look to figure this out?
> 
> Thank you,
> Alex
> 
> ___
> 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

Re: [Hol-info] How to prove basic equivalency of rational?

[Chun Tian (binghe)]

Some additional findings:

1. ``1/10 = 10/100 <=> T`` seems indeed possible, see theorem RAT_EQ_ALT and 
the following tests:

REWRITE_RULE [rat_nmr_def, rat_dnm_def]
 (SPECL [``1/10``, ``10/100``] RAT_EQ_ALT)

val it =
   ⊢ (0.1 = 0.10 ) ⇔
 (frac_nmr (rep_rat 0.1 ) * frac_dnm (rep_rat 0.10 ) =
  frac_nmr (rep_rat 0.10 ) * frac_dnm (rep_rat 0.1 )): thm

but I don’t know how to reduce the result to T…

2. RAT_ADD_CONV seems more powerful:

RAT_ADD_CONV ``1/10q + -10/100``;
val it = ⊢ 0.1 + -10 / 100 = 0: thm

In theory we can detect if the RHS is “0 :rat”, but I failed to implement a 
working RAT_EQ_CONV by reducing ``r1 = r2`` to ``r1 + -r2``. (once 1/10 becomes 
0.1 and 10/100 becomes 0.10, RAT_ADD_CONV doesn’t work any more, strange…)

—Chun

> Il giorno 14 gen 2019, alle ore 15:45, Heiko Becker  ha 
> scritto:
> 
> Hello,
> 
> I am not an expert on ratTheory itself but I briefly looked at your goal. To 
> me it feels like `1/10:rat = 10/100` is the wrong goal to prove.
> Looking at the documentation of ratTheory some theorems use `rat_equiv` 
> instead. If I restate your goal as
> 
> `rat_equiv (abs_frac (1,10)) (abs_frac (10,100))`
> 
> it can be proven by
> 
> fs[rat_equiv_def, NMR, DNM]
> 
> My guess is that your goal is not provable because `1/10` and `10/100` 
> represent different rational "objects" though they are equivalent (as 
> captured by `rat_equiv`).
> But I am not sure about this. Maybe someone more experienced can comment on 
> this.
> 
> 
> 
> Best regards,
> 
> Heiko
> 
> 
> On 1/14/19 6:24 AM, Xero Essential wrote:
>> Hi, every expert.
>> 
>> Maybe I'm a little new to the HOL4 libraries.
>> 
>> But, how could I prove the basic equivalency of rational like `1q / 10 = 
>> 10 / 100`?
>> The documentation is little and I have searched all the source, but 
>> related conversions and tactics like `RAT_EQ_TAC` are all failed and throw 
>> an empty error.
>> I looked the source about `RAT_EQ_TAC`, which something about  
>> `abs_rat`, and then I become confused.
>> 
>> Sorry for my bothering, and hope the suggestion.
>> 
>> Thanks.
>> Qiyuan Xu.
>> 
>> 
>> 
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net 
>> https://lists.sourceforge.net/lists/listinfo/hol-info 
>> 
> ___
> 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

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

I quote the beginning of the 2nd paragraph of Chapter 4 (Goal Directed Proof: 
Tactics and Tacticals) in The HOL System DESCRIPTION:

"Even with recourse to derived inference rules, it is still surprisingly 
awkward to work
*forward*, to find a chain of theorems that culminates in a desired theorem. …"

This is where the keyword “forward” comes from.

—Chun

> Il giorno 08 gen 2019, alle ore 02:38, Chun Tian (binghe) 
>  ha scritto:
> 
> Hmmm, well… all theorems are essentially *derived* from earlier theorems or 
> axioms, thus it seems (to me) that the word “derived” still doesn’t capture 
> the characterization of “save_thm” from “store_thm”.   But the word “dervied” 
> makes more senses than previous “calculated” as “save_thm”’s body is mainly 
> using “derived rules” instead of “tactics”. However, I see the essential 
> difference is the direction in the proof: from proof goal to existing 
> theorems, or from existing theorems to proof goal.
> 
> This whole mail thread is not really a technical discussion, thus whatever I 
> said here must be highly subjective, however I suggest the following:
> 
> 1. using keyword “forward” and “backward” to distinguish theorems built by 
> “save_thm” and “store_thm”, respectively:
> 
> - Theorem(forward) name (MLcode);
> - Theorem(backward) name tmquote (MLcode);
> 
> 2. the keyword (backward) is optional (simply because this is the most case), 
> thus backward theorems can also be expressed (if detected the tmquote part, 
> somehow) in your current way:
> 
> - Theorem name tmquote (MLcode);
> 
> 3. if ML’s parser is smart enough, even the keyword (forward) can be 
> eliminated, because the number of arguments is different: in forward proof it 
> is 2, in backward proof it is 3:
> 
> - Theorem name (MLcode);
> - Theorem name tmquote (MLcode);
> 
> How much you can go with above idea, depends on how powerful the ML quotation 
> code can be.
> 
> Hope this helps,
> 
> —Chun
> 
>> Il giorno 08 gen 2019, alle ore 02:10, michael.norr...@data61.csiro.au ha 
>> scritto:
>> 
>> Indeed, they are both calculated.  In one, you state the desired end-state 
>> and head towards it with a tactic.  In the other, you transform existing 
>> theorems with rules of inference and derive a final statement (hence the 
>> good practice, which you mentioned, of putting the statement into a comment).
>> 
>> Given that, what about
>> 
>>  Theorem(derived) name (MLcode);
>> 
>> ?
>> 
>> Michael
>> 
>> On 7/1/19, 20:31, "Chun Tian (binghe)"  wrote:
>> 
>>   Hi Michael,
>> 
>>   Thanks, now I see your points: if it’s really a “lemma”, then there’s no 
>> need to export it, thus `Q.prove` (or `prove`) should just do the job.
>> 
>>   Among the two syntactic sugars, I personally like your first version 
>> (Theorem(calculated) …), because it emphasized that, a `Theorem` generated 
>> by `save_thm` has no differences (in use) with a `Theorem` generated by 
>> `store_thm`, just the word “calculated” could have a better name, as both 
>> kinds of theorems are essentially calculated.
>> 
>>   —Chun
>> 
>>> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au ha 
>>> scritto:
>>> 
>>> The Theorem keyword is a prettier way of writing `store_thm`, which, as the 
>>> name suggests, is indeed for theorems.  In other words, the choice of 
>>> Theorem merely reflects our existing naming convention.
>>> 
>>> If you have a lemma that shouldn’t be “stored”, then you should probably be 
>>> using `Q.prove` (or `prove`).  The use of theory files that make theorem 
>>> values persistent is the way in which users can distinguish important 
>>> results that should persist (that is, “theorems”), and those that should be 
>>> more ephemeral.
>>> 
>>> The existing `save_thm` entrypoint has the same problem with requiring 
>>> redundant typing of names. I’m thus tempted to invent a Theorem analogue to 
>>> map to it.  My current feeling is to go for something like
>>> 
>>>  Theorem(calculated) thmname (ML code);
>>> 
>>> Or
>>> 
>>> Computed_Theorem thmname (ML code)
>>> 
>>> Or …?
>>> 
>>> Suggestions welcome.
>>> 
>>> Michael
>>> 
>>> From: "Chun Tian (binghe)" 
>>> Date: Thursday, 3 January 2019 at 23:20
>>> To: Makarius 
>>> Cc: Michael Norrish , hol-info 
>>> 
>>> Subject: Re: [Hol-info] New grammar of defining theorems?
>>> 
>>> S

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

Hmmm, well… all theorems are essentially *derived* from earlier theorems or 
axioms, thus it seems (to me) that the word “derived” still doesn’t capture the 
characterization of “save_thm” from “store_thm”.   But the word “dervied” makes 
more senses than previous “calculated” as “save_thm”’s body is mainly using 
“derived rules” instead of “tactics”. However, I see the essential difference 
is the direction in the proof: from proof goal to existing theorems, or from 
existing theorems to proof goal.

This whole mail thread is not really a technical discussion, thus whatever I 
said here must be highly subjective, however I suggest the following:

1. using keyword “forward” and “backward” to distinguish theorems built by 
“save_thm” and “store_thm”, respectively:

- Theorem(forward) name (MLcode);
- Theorem(backward) name tmquote (MLcode);

2. the keyword (backward) is optional (simply because this is the most case), 
thus backward theorems can also be expressed (if detected the tmquote part, 
somehow) in your current way:

- Theorem name tmquote (MLcode);

3. if ML’s parser is smart enough, even the keyword (forward) can be 
eliminated, because the number of arguments is different: in forward proof it 
is 2, in backward proof it is 3:

- Theorem name (MLcode);
- Theorem name tmquote (MLcode);

How much you can go with above idea, depends on how powerful the ML quotation 
code can be.

Hope this helps,

—Chun

> Il giorno 08 gen 2019, alle ore 02:10, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> Indeed, they are both calculated.  In one, you state the desired end-state 
> and head towards it with a tactic.  In the other, you transform existing 
> theorems with rules of inference and derive a final statement (hence the good 
> practice, which you mentioned, of putting the statement into a comment).
> 
> Given that, what about
> 
>   Theorem(derived) name (MLcode);
> 
> ?
> 
> Michael
> 
> On 7/1/19, 20:31, "Chun Tian (binghe)"  wrote:
> 
>Hi Michael,
> 
>Thanks, now I see your points: if it’s really a “lemma”, then there’s no 
> need to export it, thus `Q.prove` (or `prove`) should just do the job.
> 
>Among the two syntactic sugars, I personally like your first version 
> (Theorem(calculated) …), because it emphasized that, a `Theorem` generated by 
> `save_thm` has no differences (in use) with a `Theorem` generated by 
> `store_thm`, just the word “calculated” could have a better name, as both 
> kinds of theorems are essentially calculated.
> 
>—Chun
> 
>> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au ha 
>> scritto:
>> 
>> The Theorem keyword is a prettier way of writing `store_thm`, which, as the 
>> name suggests, is indeed for theorems.  In other words, the choice of 
>> Theorem merely reflects our existing naming convention.
>> 
>> If you have a lemma that shouldn’t be “stored”, then you should probably be 
>> using `Q.prove` (or `prove`).  The use of theory files that make theorem 
>> values persistent is the way in which users can distinguish important 
>> results that should persist (that is, “theorems”), and those that should be 
>> more ephemeral.
>> 
>> The existing `save_thm` entrypoint has the same problem with requiring 
>> redundant typing of names. I’m thus tempted to invent a Theorem analogue to 
>> map to it.  My current feeling is to go for something like
>> 
>>   Theorem(calculated) thmname (ML code);
>> 
>> Or
>> 
>>  Computed_Theorem thmname (ML code)
>> 
>> Or …?
>> 
>> Suggestions welcome.
>> 
>> Michael
>> 
>> From: "Chun Tian (binghe)" 
>> Date: Thursday, 3 January 2019 at 23:20
>> To: Makarius 
>> Cc: Michael Norrish , hol-info 
>> 
>> Subject: Re: [Hol-info] New grammar of defining theorems?
>> 
>> So the key is to make sure that they’re not distinguished internally by some 
>> tools, and if some tools do, it’s their problems but HOL’s.
>> 
>> I personally don’t like the keyword “Theorem” because I think many small 
>> theorems with 3 lines of tactics do not deserve the name “Theorem”. The 
>> correct way of using these conventions should be aligned with majority math 
>> books, which I believe there must be some “rules” mentioned somewhere.
>> 
>> On the other side, HOL4 users always have multiple ways to build a theorem. 
>> For example, sometimes I perfer using “save_thm” to build theorems forwardly 
>> and put the statement as comments before it, sometimes multiple theorems 
>> were put into a “local” block sharing common tactics. As a result, HOL4 
>> proof scripts were *not* documents but essentially raw ML programs, th

Re: [Hol-info] HOL's new measure theory (in progress)

[Chun Tian (binghe)]

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) 
>  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)"  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 f

Re: [Hol-info] HOL's new measure theory (in progress)

[Chun Tian (binghe)]

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)"  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-value

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

Hi Michael,

Thanks, now I see your points: if it’s really a “lemma”, then there’s no need 
to export it, thus `Q.prove` (or `prove`) should just do the job.

Among the two syntactic sugars, I personally like your first version 
(Theorem(calculated) …), because it emphasized that, a `Theorem` generated by 
`save_thm` has no differences (in use) with a `Theorem` generated by 
`store_thm`, just the word “calculated” could have a better name, as both kinds 
of theorems are essentially calculated.

—Chun

> Il giorno 07 gen 2019, alle ore 01:16, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> The Theorem keyword is a prettier way of writing `store_thm`, which, as the 
> name suggests, is indeed for theorems.  In other words, the choice of Theorem 
> merely reflects our existing naming convention.
> 
> If you have a lemma that shouldn’t be “stored”, then you should probably be 
> using `Q.prove` (or `prove`).  The use of theory files that make theorem 
> values persistent is the way in which users can distinguish important results 
> that should persist (that is, “theorems”), and those that should be more 
> ephemeral.
> 
> The existing `save_thm` entrypoint has the same problem with requiring 
> redundant typing of names. I’m thus tempted to invent a Theorem analogue to 
> map to it.  My current feeling is to go for something like
> 
>Theorem(calculated) thmname (ML code);
> 
> Or
> 
>   Computed_Theorem thmname (ML code)
> 
> Or …?
> 
> Suggestions welcome.
> 
> Michael
> 
> From: "Chun Tian (binghe)" 
> Date: Thursday, 3 January 2019 at 23:20
> To: Makarius 
> Cc: Michael Norrish , hol-info 
> 
> Subject: Re: [Hol-info] New grammar of defining theorems?
> 
> So the key is to make sure that they’re not distinguished internally by some 
> tools, and if some tools do, it’s their problems but HOL’s.
> 
> I personally don’t like the keyword “Theorem” because I think many small 
> theorems with 3 lines of tactics do not deserve the name “Theorem”. The 
> correct way of using these conventions should be aligned with majority math 
> books, which I believe there must be some “rules” mentioned somewhere.
> 
> On the other side, HOL4 users always have multiple ways to build a theorem. 
> For example, sometimes I perfer using “save_thm” to build theorems forwardly 
> and put the statement as comments before it, sometimes multiple theorems were 
> put into a “local” block sharing common tactics. As a result, HOL4 proof 
> scripts were *not* documents but essentially raw ML programs, thus extremely 
> flexible.  I may not adopt this new grammar in a complex proof script in 
> which different ways of building theorems were used together.
> 
> —Chun
> 
> P. S. Coq seems to have even more synonyms: (do Coq users here share the same 
> concerns?)
> 
> Lemma ident [binders] : type.
> Remark ident [binders] : type.
> Fact ident [binders] : type.
> Corollary ident [binders] : type.
> Proposition ident [binders] : type.
> 
> These commands are synonyms of Theorem ident [binders] : type.
> 
> Il giorno 03 gen 2019, alle ore 12:23, Makarius  ha 
> scritto:
> 
> On 03/01/2019 11:23, Chun Tian (binghe) wrote:
> 
> Hi Michael,
> 
> thanks for fixing the bugs. (now I see why I can’t find its definition…)
> 
> Going in this direction, have you considered adding also “Lemma” and 
> “Corollary”? Internally they're equivalent with “Theorem”, but they could 
> literally help writers (and readers) identifying different levels of 
> theorems, like those in math books.
> 
> This reminds me of Isabelle/Isar. Some decades ago I introduced these
> variants of 'theorem' and it became a running gag of confusion and
> unclear corner cases, because aliases were not really identical, but
> distinguished internally by some tools.
> 
> Recently, we even introduced 'proposition' as another variant, but it is
> unclear if it is more prominent than 'theorem' or less prominent than
> 'lemma'. Thus it depends on local conventions of particular
> formalization projects how to treat it, e.g. in document presentation.
> 
> If I had another chance today, I would probably eliminate all funny
> aliases of Isar commands.
> 
> 
> Makarius
> 
> 
> 
> ___
> 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

Re: [Hol-info] HOL's new measure theory (in progress)

[Chun Tian (binghe)]

> Il giorno 07 gen 2019, alle ore 01:52, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> 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.

Where’re the measures of real and extreal-valued in Isabelle’s measure theory?  
I only saw one version based on Extended Non-Negative Reals ('a set ⇒ ennreal) 
in “src/HOL/Analysis/Measure_Space.thy)

—Chun



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

Re: [Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

Hi,

thanks, I should really again the Euclid's Theorem tutorial.   I fixed `i` and 
directly do induction on `j`, then it also worked with some cases analysis.

—Chun

> Il giorno 05 gen 2019, alle ore 22:20, Konrad Slind  
> ha scritto:
> 
> There is discussion of something like this in the Euclid's Theorem tutorial. 
> You can do Induct_on `j - i` or do the trick where you prove ?k. j = i + SUC 
> k, eliminate j, and then induct on k.
> 
> Konrad.
> 
> 
> On Sat, Jan 5, 2019 at 12:35 PM Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> sorry, "i ≤ j” should be “i < j” actually:
> 
>∀i j. i < j ⇒ f (SUC i) ⊆ f j
>
>  0.  ∀n. f n ⊆ f (SUC n)
>  1.  ∀n. 0 < n ⇒ f 0 ⊆ f n
> 
> > Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) 
> > mailto:binghe.l...@gmail.com>> ha scritto:
> >
> > Hi,
> >
> > I have the following goal to prove: (f : num -> ‘a set)
> >
> >   ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
> >   
> > 0.  ∀n. f n ⊆ f (SUC n)
> >
> > but how can I do the induction on … e.g. `j - i`?
> >
> > —Chun
> >
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> <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

Re: [Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

sorry, "i ≤ j” should be “i < j” actually:

   ∀i j. i < j ⇒ f (SUC i) ⊆ f j
   
 0.  ∀n. f n ⊆ f (SUC n)
 1.  ∀n. 0 < n ⇒ f 0 ⊆ f n

> Il giorno 05 gen 2019, alle ore 19:32, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> I have the following goal to prove: (f : num -> ‘a set)
> 
>   ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
>   
> 0.  ∀n. f n ⊆ f (SUC n)
> 
> but how can I do the induction on … e.g. `j - i`?
> 
> —Chun
> 



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

[Hol-info] How to do this kind of induction?

[Chun Tian (binghe)]

Hi,

I have the following goal to prove: (f : num -> ‘a set)

   ∀i j. i ≤ j ⇒ f (SUC i) ⊆ f j
   
 0.  ∀n. f n ⊆ f (SUC n)

but how can I do the induction on … e.g. `j - i`?

—Chun



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

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

So the key is to make sure that they’re not distinguished internally by some 
tools, and if some tools do, it’s their problems but HOL’s.

I personally don’t like the keyword “Theorem” because I think many small 
theorems with 3 lines of tactics do not deserve the name “Theorem”. The correct 
way of using these conventions should be aligned with majority math books, 
which I believe there must be some “rules” mentioned somewhere.

On the other side, HOL4 users always have multiple ways to build a theorem. For 
example, sometimes I perfer using “save_thm” to build theorems forwardly and 
put the statement as comments before it, sometimes multiple theorems were put 
into a “local” block sharing common tactics. As a result, HOL4 proof scripts 
were *not* documents but essentially raw ML programs, thus extremely flexible.  
I may not adopt this new grammar in a complex proof script in which different 
ways of building theorems were used together.

—Chun

P. S. Coq seems to have even more synonyms: (do Coq users here share the same 
concerns?)

Lemma ident [binders] : type.
Remark ident [binders] : type.
Fact ident [binders] : type.
Corollary ident [binders] : type.
Proposition ident [binders] : type.

These commands are synonyms of Theorem ident [binders] : type.

> Il giorno 03 gen 2019, alle ore 12:23, Makarius  ha 
> scritto:
> 
> On 03/01/2019 11:23, Chun Tian (binghe) wrote:
>> Hi Michael,
>> 
>> thanks for fixing the bugs. (now I see why I can’t find its definition…)
>> 
>> Going in this direction, have you considered adding also “Lemma” and 
>> “Corollary”? Internally they're equivalent with “Theorem”, but they could 
>> literally help writers (and readers) identifying different levels of 
>> theorems, like those in math books.
> 
> This reminds me of Isabelle/Isar. Some decades ago I introduced these
> variants of 'theorem' and it became a running gag of confusion and
> unclear corner cases, because aliases were not really identical, but
> distinguished internally by some tools.
> 
> Recently, we even introduced 'proposition' as another variant, but it is
> unclear if it is more prominent than 'theorem' or less prominent than
> 'lemma'. Thus it depends on local conventions of particular
> formalization projects how to treat it, e.g. in document presentation.
> 
> If I had another chance today, I would probably eliminate all funny
> aliases of Isar commands.
> 
> 
>   Makarius
> 



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

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

Hi Michael,

thanks for fixing the bugs. (now I see why I can’t find its definition…)

Going in this direction, have you considered adding also “Lemma” and 
“Corollary”? Internally they're equivalent with “Theorem”, but they could 
literally help writers (and readers) identifying different levels of theorems, 
like those in math books.

—Chun

> Il giorno 02 gen 2019, alle ore 15:44,  
>  ha scritto:
> 
> Dear Chun,
> 
> This is indeed a new feature of the quotation filter.  Its purpose is to keep 
> names consistent, and to reduce the amount of boilerplate typing that 
> script-writers have to generate.
> 
> It's as yet undocumented, but I hope to get to that soon.
> 
> Michael
> 
> On 2/1/19, 06:20, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>(Happy New Year) I found the following code in 
> src/patricia/sptreeScript.sml (added in commit 
> 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)
> 
>Theorem list_to_num_set_append
>  `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) 
> (list_to_num_set l2)`
> (Induct \\ rw[list_to_num_set_def]
>  \\ rw[Once insert_union]
>  \\ rw[Once insert_union,SimpRHS]
>  \\ rw[union_assoc]);
> 
>Where is the definition of the keyword “Theorem”? Is this a new grammar of 
> defining theroems, aiming at preventing inconsistent theorem names in 
> exported theories?
> 
>Regards,
> 
>Chun
> 
> 
> 
> 
> ___
> 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

Re: [Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

I see… thanks, but currently Moscow ML cannot compile that file [1], and I 
can’t even find the definition of this new feature …

—Chun

[1] https://github.com/HOL-Theorem-Prover/HOL/pull/634

> Il giorno 02 gen 2019, alle ore 15:44,  
>  ha scritto:
> 
> Dear Chun,
> 
> This is indeed a new feature of the quotation filter.  Its purpose is to keep 
> names consistent, and to reduce the amount of boilerplate typing that 
> script-writers have to generate.
> 
> It's as yet undocumented, but I hope to get to that soon.
> 
> Michael
> 
> On 2/1/19, 06:20, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>(Happy New Year) I found the following code in 
> src/patricia/sptreeScript.sml (added in commit 
> 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)
> 
>Theorem list_to_num_set_append
>  `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) 
> (list_to_num_set l2)`
> (Induct \\ rw[list_to_num_set_def]
>  \\ rw[Once insert_union]
>  \\ rw[Once insert_union,SimpRHS]
>  \\ rw[union_assoc]);
> 
>Where is the definition of the keyword “Theorem”? Is this a new grammar of 
> defining theroems, aiming at preventing inconsistent theorem names in 
> exported theories?
> 
>Regards,
> 
>Chun
> 
> 
> 
> 
> ___
> 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

[Hol-info] New grammar of defining theorems?

[Chun Tian (binghe)]

Hi,

(Happy New Year) I found the following code in src/patricia/sptreeScript.sml 
(added in commit 2b78a8b8ac22b0686a5964a64f79fa8a8a17375e)

Theorem list_to_num_set_append
  `!l1 l2. list_to_num_set (l1 ++ l2) = union (list_to_num_set l1) 
(list_to_num_set l2)`
 (Induct \\ rw[list_to_num_set_def]
  \\ rw[Once insert_union]
  \\ rw[Once insert_union,SimpRHS]
  \\ rw[union_assoc]);

Where is the definition of the keyword “Theorem”? Is this a new grammar of 
defining theroems, aiming at preventing inconsistent theorem names in exported 
theories?

Regards,

Chun



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

Re: [Hol-info] (no subject)

[Chun Tian (binghe)]

Hi,

this is not an HOL question any more, and now you should learn some Standard ML 
first. Maybe the following book is a good start:

Harper, R.: Programming in Standard ML. 
http://www.cs.cmu.edu/~rwh/isml/book.pdf 


I??m sure the answer of your question (plus many other questions) is in it.

??Chun

> Il giorno 20 dic 2018, alle ore 07:23,  <849678...@qq.com> ha scritto:
> 
> 
> Here is the following code
> datatype temp =
>  C of real
>  | F of real;
> 
>  fun temp_to_f t =
> case t of
>C x => x * (9.0 / 5.0) + 32.0
>   | F x => x;
> What is the function of the function temp_to_f ? How to use this function 
> specifically?
> ___
> 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

Re: [Hol-info] On summation of 2-dimensional sequences

[Chun Tian (binghe)]

Hmmm… I just found NUMINF_2D in seqTheory: (actually it’s me who moved this 
theorem from util_probTheory here)

[SUMINF_2D]  Theorem

  ⊢ ∀f g h.
(∀m n. 0 ≤ f m n) ∧ (∀n. f n sums g n) ∧ summable g ∧
BIJ h 핌(:num) (핌(:num) × 핌(:num)) ⇒
UNCURRY f ∘ h sums suminf g

sorry for disturbing…

—Chun

> Il giorno 04 ott 2018, alle ore 20:41, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> suppose I have a function (f :num -> num -> real), and I want to calculate 
> the sum of (f i j) on the entire plane, one way is to use double suminf: 
> (assuming it is always summable, i.e. any sum is finite)
> 
>  suminf (λi. suminf (λj. f i j))) (1)
> 
> However, there’s another way using single suminf, based on numpairTheory:
> 
>  suminf (λn. f (nfst n) (nsnd n)) (2)
> 
> My question is: how can I prove (1) and (2) are equal, i.e.:
> 
>  suminf (λi. suminf (λj. f i j))) = suminf (λn. f (nfst n) (nsnd n))
> 
> ?
> 
> --Chun
> 



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

[Hol-info] On summation of 2-dimensional sequences

[Chun Tian (binghe)]

Hi,

suppose I have a function (f :num -> num -> real), and I want to calculate the 
sum of (f i j) on the entire plane, one way is to use double suminf: (assuming 
it is always summable, i.e. any sum is finite)

  suminf (λi. suminf (λj. f i j)))  (1)

However, there’s another way using single suminf, based on numpairTheory:

  suminf (λn. f (nfst n) (nsnd n))  (2)

My question is: how can I prove (1) and (2) are equal, i.e.:

  suminf (λi. suminf (λj. f i j))) = suminf (λn. f (nfst n) (nsnd n))

?

--Chun



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

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

> Il giorno 18 set 2018, alle ore 11:15, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi Thomas,
> 
> yes, you’re totally right.   My original problem cannot be resolved just in 
> scope of set theory. I’m trying to prove the uniqueness of measure:
> 
> [UNIQUENESS_OF_MEASURE]
> ∀sp sts f u v.
> sp ∈ sts ∧ subset_class sp sts ∧
> (∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (핌(:num) -> sts) ∧
> (∀n. f n ⊆ f (SUC n)) ∧ (sp = BIGUNION (IMAGE f 핌(:num))) ∧
> measure_space (sp,subsets (sigma sp sts),u) ∧
> measure_space (sp,subsets (sigma sp sts),v) ∧
> (∀n. u (f n) < PosInf) ∧ (∀s. s ∈ sts ⇒ (u s = v s)) ⇒
> ∀s. s ∈ subsets (sigma sp sts) ⇒ (u s = v s)
> 
> And I was approaching a measure (u a) using the sup of an image:
> 
> u a = sup (IMAGE (u ∘ (λi. f i ∩ a)) 핌(:num))
> 
> in which (u :’a set -> extreal) is a measure function, f is the increasing 
> sequence that I mentioned before. Now I believe the correct way to reduce 
> “sup” is to use the following non-trivial monotone convergence theorem 
> already in HOL’s measureTheory:
> 
> [MONOTONE_CONVERGENCE]
>⊢ ∀m s f.
>  measure_space m ∧ f ∈ (핌(:num) -> measurable_sets m) ∧
>  (∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 핌(:num))) ⇒
>  (sup (IMAGE (measure m ∘ f) 핌(:num)) = measure m s)
> 
> Above theorem does require that (f 0 = EMPTY), as I expected. Now I have 
> confidence to finish the whole proof.

*does NOT require that (f 0 = EMPTY).

> 
> —Chun
> 
>> Il giorno 18 set 2018, alle ore 10:36, Thomas Tuerk > <mailto:tho...@tuerk-brechen.de>> ha scritto:
>> 
>> Hi Chun,
>> 
>> no, it still does not hold. The problem is that case that "a" might be 
>> infinite and while there is for every element 'e' of 'a' an 'n' with 'e IN f 
>> n' you need arbitrary large ones.
>> 
>> A tiny modification of Ramana's counterexample is
>> 
>> f x := count x
>> sp := UNIV
>> a := { n | even n }
>> Cheers
>> 
>> Thomas
>> 
>> On 18.09.2018 10:25, Chun Tian (binghe) wrote:
>>> Hi Ramana,
>>> 
>>> thanks for your help. Sorry, I realized that the case “a = sp” can be 
>>> eliminated from other assumptions, thus I actually have another constraint 
>>> “a ≠ sp” in my original goals:
>>> 
>>>∃x. a ⊆ f x
>>>
>>>  4.  f 0 = ∅
>>>  5.  ∀i j. i ≤ j ⇒ f i ⊆ f j
>>>  6.  BIGUNION (IMAGE f 핌(:num)) = sp
>>> 21.  a ≠ sp
>>> 23.  ∀n. f n ⊆ sp
>>> 24.  a ⊆ sp
>>> 
>>> in this case your opposite proof doesn’t work any more. Also, I replaced 
>>> the monotonicity of f into another form, I don’t know which one is easier 
>>> to use. The assumption "f 0 = ∅” should be optional, I guess.
>>> 
>>> Now this should be a true statement, right?
>>> 
>>> —Chun
>>> 
>>>> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar >>> <mailto:ram...@kumar.id.au>> ha scritto:
>>>> 
>>>> I think this is false. Here's a proof of the opposite, with the type of f 
>>>> instantiated to a num set generator:
>>>> 
>>>> val thm = Q.prove(
>>>> `¬(
>>>>   ∀(f:num->num->bool) a sp.
>>>>   (f 0 = ∅) ∧
>>>>   (∀n. f n ⊆ f (SUC n)) ∧
>>>>   (∀n. f n ⊆ sp) ∧
>>>>   (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
>>>>   (a ⊆ sp) ⇒
>>>>  ∃x. a ⊆ f x)`,
>>>>   rw[]
>>>>   \\ qexists_tac`count`
>>>>   \\ qexists_tac`UNIV`
>>>>   \\ rw[SUBSET_DEF, PULL_EXISTS]
>>>>   >- metis_tac[]
>>>>   >- (
>>>> rw[Once EXTENSION]
>>>> \\ qexists_tac`count (SUC x)`
>>>> \\ rw[] )
>>>>   >- (
>>>> rw[EXTENSION]
>>>> \\ qexists_tac`SUC x`
>>>> \\ rw[] ));
>>>> 
>>>> 
>>>> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) >>> <mailto:binghe.l...@gmail.com>> wrote:
>>>> sorry, I also have this necessary assumption:
>>>> 
>>>>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
>>>> 
>>>> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
>>>> > mailto:binghe.l...@gmail.com>> ha scritto:
>>>> >
>>>> > Hi,
>>>> >
>>>> > I ran into the followi

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

Hi Thomas,

yes, you’re totally right.   My original problem cannot be resolved just in 
scope of set theory. I’m trying to prove the uniqueness of measure:

[UNIQUENESS_OF_MEASURE]
∀sp sts f u v.
sp ∈ sts ∧ subset_class sp sts ∧
(∀s t. s ∈ sts ∧ t ∈ sts ⇒ s ∩ t ∈ sts) ∧ f ∈ (핌(:num) -> sts) ∧
(∀n. f n ⊆ f (SUC n)) ∧ (sp = BIGUNION (IMAGE f 핌(:num))) ∧
measure_space (sp,subsets (sigma sp sts),u) ∧
measure_space (sp,subsets (sigma sp sts),v) ∧
(∀n. u (f n) < PosInf) ∧ (∀s. s ∈ sts ⇒ (u s = v s)) ⇒
∀s. s ∈ subsets (sigma sp sts) ⇒ (u s = v s)

And I was approaching a measure (u a) using the sup of an image:

u a = sup (IMAGE (u ∘ (λi. f i ∩ a)) 핌(:num))

in which (u :’a set -> extreal) is a measure function, f is the increasing 
sequence that I mentioned before. Now I believe the correct way to reduce “sup” 
is to use the following non-trivial monotone convergence theorem already in 
HOL’s measureTheory:

[MONOTONE_CONVERGENCE]
   ⊢ ∀m s f.
 measure_space m ∧ f ∈ (핌(:num) -> measurable_sets m) ∧
 (∀n. f n ⊆ f (SUC n)) ∧ (s = BIGUNION (IMAGE f 핌(:num))) ⇒
 (sup (IMAGE (measure m ∘ f) 핌(:num)) = measure m s)

Above theorem does require that (f 0 = EMPTY), as I expected. Now I have 
confidence to finish the whole proof.

—Chun

> Il giorno 18 set 2018, alle ore 10:36, Thomas Tuerk  
> ha scritto:
> 
> Hi Chun,
> 
> no, it still does not hold. The problem is that case that "a" might be 
> infinite and while there is for every element 'e' of 'a' an 'n' with 'e IN f 
> n' you need arbitrary large ones.
> 
> A tiny modification of Ramana's counterexample is
> 
> f x := count x
> sp := UNIV
> a := { n | even n }
> Cheers
> 
> Thomas
> 
> On 18.09.2018 10:25, Chun Tian (binghe) wrote:
>> Hi Ramana,
>> 
>> thanks for your help. Sorry, I realized that the case “a = sp” can be 
>> eliminated from other assumptions, thus I actually have another constraint 
>> “a ≠ sp” in my original goals:
>> 
>>∃x. a ⊆ f x
>>
>>  4.  f 0 = ∅
>>  5.  ∀i j. i ≤ j ⇒ f i ⊆ f j
>>  6.  BIGUNION (IMAGE f 핌(:num)) = sp
>> 21.  a ≠ sp
>> 23.  ∀n. f n ⊆ sp
>> 24.  a ⊆ sp
>> 
>> in this case your opposite proof doesn’t work any more. Also, I replaced the 
>> monotonicity of f into another form, I don’t know which one is easier to 
>> use. The assumption "f 0 = ∅” should be optional, I guess.
>> 
>> Now this should be a true statement, right?
>> 
>> —Chun
>> 
>>> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar >> <mailto:ram...@kumar.id.au>> ha scritto:
>>> 
>>> I think this is false. Here's a proof of the opposite, with the type of f 
>>> instantiated to a num set generator:
>>> 
>>> val thm = Q.prove(
>>> `¬(
>>>   ∀(f:num->num->bool) a sp.
>>>   (f 0 = ∅) ∧
>>>   (∀n. f n ⊆ f (SUC n)) ∧
>>>   (∀n. f n ⊆ sp) ∧
>>>   (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
>>>   (a ⊆ sp) ⇒
>>>  ∃x. a ⊆ f x)`,
>>>   rw[]
>>>   \\ qexists_tac`count`
>>>   \\ qexists_tac`UNIV`
>>>   \\ rw[SUBSET_DEF, PULL_EXISTS]
>>>   >- metis_tac[]
>>>   >- (
>>> rw[Once EXTENSION]
>>> \\ qexists_tac`count (SUC x)`
>>> \\ rw[] )
>>>   >- (
>>> rw[EXTENSION]
>>> \\ qexists_tac`SUC x`
>>> \\ rw[] ));
>>> 
>>> 
>>> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) >> <mailto:binghe.l...@gmail.com>> wrote:
>>> sorry, I also have this necessary assumption:
>>> 
>>>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
>>> 
>>> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
>>> > mailto:binghe.l...@gmail.com>> ha scritto:
>>> >
>>> > Hi,
>>> >
>>> > I ran into the following goal in the proof of a big theorem:
>>> >
>>> >   ∃x. a ⊆ f x
>>> >   
>>> > 3.  f 0 = ∅
>>> > 4.  ∀n. f n ⊆ f (SUC n)
>>> >20.  ∀n. f n ⊆ sp
>>> >21.  a ⊆ sp
>>> >
>>> > I have an increasing sequence of sets (f n) from empty to the whole space 
>>> > (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can 
>>> > always choose a big enough index x such that (f x) will contain “a”. But 
>>> > how can I make this argument formal?
>>> >
>

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

no… by drawing pictures and think it more, this statement is still not true, if 
the set is general (of type ‘a -> bool).

please forget the whole question. I must have assumed something wrong in 
earlier places. thanks all the same.

—Chun

> Il giorno 18 set 2018, alle ore 10:25, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi Ramana,
> 
> thanks for your help. Sorry, I realized that the case “a = sp” can be 
> eliminated from other assumptions, thus I actually have another constraint “a 
> ≠ sp” in my original goals:
> 
>∃x. a ⊆ f x
>
>  4.  f 0 = ∅
>  5.  ∀i j. i ≤ j ⇒ f i ⊆ f j
>  6.  BIGUNION (IMAGE f 핌(:num)) = sp
> 21.  a ≠ sp
> 23.  ∀n. f n ⊆ sp
> 24.  a ⊆ sp
> 
> in this case your opposite proof doesn’t work any more. Also, I replaced the 
> monotonicity of f into another form, I don’t know which one is easier to use. 
> The assumption "f 0 = ∅” should be optional, I guess.
> 
> Now this should be a true statement, right?
> 
> —Chun
> 
>> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar > <mailto:ram...@kumar.id.au>> ha scritto:
>> 
>> I think this is false. Here's a proof of the opposite, with the type of f 
>> instantiated to a num set generator:
>> 
>> val thm = Q.prove(
>> `¬(
>>   ∀(f:num->num->bool) a sp.
>>   (f 0 = ∅) ∧
>>   (∀n. f n ⊆ f (SUC n)) ∧
>>   (∀n. f n ⊆ sp) ∧
>>   (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
>>   (a ⊆ sp) ⇒
>>  ∃x. a ⊆ f x)`,
>>   rw[]
>>   \\ qexists_tac`count`
>>   \\ qexists_tac`UNIV`
>>   \\ rw[SUBSET_DEF, PULL_EXISTS]
>>   >- metis_tac[]
>>   >- (
>> rw[Once EXTENSION]
>> \\ qexists_tac`count (SUC x)`
>> \\ rw[] )
>>   >- (
>> rw[EXTENSION]
>> \\ qexists_tac`SUC x`
>> \\ rw[] ));
>> 
>> 
>> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe) > <mailto:binghe.l...@gmail.com>> wrote:
>> sorry, I also have this necessary assumption:
>> 
>>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
>> 
>> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
>> > mailto:binghe.l...@gmail.com>> ha scritto:
>> >
>> > Hi,
>> >
>> > I ran into the following goal in the proof of a big theorem:
>> >
>> >   ∃x. a ⊆ f x
>> >   
>> > 3.  f 0 = ∅
>> > 4.  ∀n. f n ⊆ f (SUC n)
>> >20.  ∀n. f n ⊆ sp
>> >21.  a ⊆ sp
>> >
>> > I have an increasing sequence of sets (f n) from empty to the whole space 
>> > (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can 
>> > always choose a big enough index x such that (f x) will contain “a”. But 
>> > how can I make this argument formal?
>> >
>> > thanks,
>> >
>> > Chun
>> >
>> 
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info 
>> <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

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

Hi Ramana,

thanks for your help. Sorry, I realized that the case “a = sp” can be 
eliminated from other assumptions, thus I actually have another constraint “a ≠ 
sp” in my original goals:

   ∃x. a ⊆ f x
   
 4.  f 0 = ∅
 5.  ∀i j. i ≤ j ⇒ f i ⊆ f j
 6.  BIGUNION (IMAGE f 핌(:num)) = sp
21.  a ≠ sp
23.  ∀n. f n ⊆ sp
24.  a ⊆ sp

in this case your opposite proof doesn’t work any more. Also, I replaced the 
monotonicity of f into another form, I don’t know which one is easier to use. 
The assumption "f 0 = ∅” should be optional, I guess.

Now this should be a true statement, right?

—Chun

> Il giorno 18 set 2018, alle ore 01:26, Ramana Kumar  ha 
> scritto:
> 
> I think this is false. Here's a proof of the opposite, with the type of f 
> instantiated to a num set generator:
> 
> val thm = Q.prove(
> `¬(
>   ∀(f:num->num->bool) a sp.
>   (f 0 = ∅) ∧
>   (∀n. f n ⊆ f (SUC n)) ∧
>   (∀n. f n ⊆ sp) ∧
>   (BIGUNION (IMAGE f 핌(:num)) = sp) ∧
>   (a ⊆ sp) ⇒
>  ∃x. a ⊆ f x)`,
>   rw[]
>   \\ qexists_tac`count`
>   \\ qexists_tac`UNIV`
>   \\ rw[SUBSET_DEF, PULL_EXISTS]
>   >- metis_tac[]
>   >- (
> rw[Once EXTENSION]
> \\ qexists_tac`count (SUC x)`
> \\ rw[] )
>   >- (
> rw[EXTENSION]
> \\ qexists_tac`SUC x`
> \\ rw[] ));
> 
> 
> On Tue, 18 Sep 2018 at 00:01, Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> sorry, I also have this necessary assumption:
> 
>  5.  BIGUNION (IMAGE f 핌(:num)) = sp
> 
> > Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
> > mailto:binghe.l...@gmail.com>> ha scritto:
> >
> > Hi,
> >
> > I ran into the following goal in the proof of a big theorem:
> >
> >   ∃x. a ⊆ f x
> >   
> > 3.  f 0 = ∅
> > 4.  ∀n. f n ⊆ f (SUC n)
> >20.  ∀n. f n ⊆ sp
> >21.  a ⊆ sp
> >
> > I have an increasing sequence of sets (f n) from empty to the whole space 
> > (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can 
> > always choose a big enough index x such that (f x) will contain “a”. But 
> > how can I make this argument formal?
> >
> > thanks,
> >
> > Chun
> >
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> <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

Re: [Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

sorry, I also have this necessary assumption:

 5.  BIGUNION (IMAGE f 핌(:num)) = sp

> Il giorno 18 set 2018, alle ore 01:00, Chun Tian (binghe) 
>  ha scritto:
> 
> Hi,
> 
> I ran into the following goal in the proof of a big theorem:
> 
>   ∃x. a ⊆ f x
>   
> 3.  f 0 = ∅
> 4.  ∀n. f n ⊆ f (SUC n)
>20.  ∀n. f n ⊆ sp
>21.  a ⊆ sp
> 
> I have an increasing sequence of sets (f n) from empty to the whole space 
> (sp), and I have a single set “a” (⊆ sp). It looks *obvious* that, I can 
> always choose a big enough index x such that (f x) will contain “a”. But how 
> can I make this argument formal?
> 
> thanks,
> 
> Chun
> 



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

[Hol-info] Choosing an element in an increasing sequence of sets

[Chun Tian (binghe)]

Hi,

I ran into the following goal in the proof of a big theorem:

   ∃x. a ⊆ f x
   
 3.  f 0 = ∅
 4.  ∀n. f n ⊆ f (SUC n)
20.  ∀n. f n ⊆ sp
21.  a ⊆ sp

I have an increasing sequence of sets (f n) from empty to the whole space (sp), 
and I have a single set “a” (⊆ sp). It looks *obvious* that, I can always 
choose a big enough index x such that (f x) will contain “a”. But how can I 
make this argument formal?

thanks,

Chun



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

Re: [Hol-info] Prove BIGUNION (IMAGE f 핌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

Hi again,

It seems that my original question has a positive answer. I got a proof from 
Thomas Tuerk saying:

val BIGUNION_IMAGE_COUNT_IMP_UNIV =
   ⊢ ∀f g.
 (∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ⇒
 (BIGUNION (IMAGE f 핌(:num)) = BIGUNION (IMAGE g 핌(:num)))

that’s amazing...

—Chun


(* provided by Thomas Tuerk, amazing! *)
val BIGUNION_IMAGE_COUNT_IMP_UNIV = store_thm
  ("BIGUNION_IMAGE_COUNT_IMP_UNIV",
  ``!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
  (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``,
 (* proof *)
   `!f g. (!n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))) ==>
  (BIGUNION (IMAGE f UNIV) SUBSET BIGUNION (IMAGE g UNIV))`
   suffices_by PROVE_TAC [SUBSET_ANTISYM]
 >> REWRITE_TAC [SUBSET_DEF]
 >> REPEAT STRIP_TAC
 >> rename1 `e IN BIGUNION _`
 >> Know `?n. e IN BIGUNION (IMAGE f (count n))`
 >- (FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_COUNT] \\
 rename1 `e IN f n'` \\
 Q.EXISTS_TAC `SUC n'` \\
 Q.EXISTS_TAC `n'` \\
 ASM_SIMP_TAC arith_ss [])
 >> STRIP_TAC
 >> `e IN BIGUNION (IMAGE g (count n))` by PROVE_TAC []
 >> FULL_SIMP_TAC std_ss [IN_BIGUNION, IN_IMAGE, PULL_EXISTS, IN_UNIV]
 >> METIS_TAC []);


> Il giorno 16 set 2018, alle ore 08:37, Chun Tian (binghe) 
>  ha scritto:
> 
> Cancel this question. Finally I found a way to reduce the original goal to
> 
>   ∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))
> 
> but it deeply relies on the definition of g, otherwise it seems impossible.  
> Sorry for disturbing.
> 
> —Chun
> 
>> Il giorno 15 set 2018, alle ore 22:26, Chun Tian (binghe) 
>>  ha scritto:
>> 
>> 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
>> 
> 



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

Re: [Hol-info] Prove BIGUNION (IMAGE f 핌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

Cancel this question. Finally I found a way to reduce the original goal to

∀n. BIGUNION (IMAGE g (count n)) = BIGUNION (IMAGE f (count n))

but it deeply relies on the definition of g, otherwise it seems impossible.  
Sorry for disturbing.

—Chun

> Il giorno 15 set 2018, alle ore 22:26, Chun Tian (binghe) 
>  ha scritto:
> 
> 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
> 



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

Re: [Hol-info] Prove BIGUNION (IMAGE f 핌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

Hi,

I’m afraid this idea doesn’t work, this is basically like using EXTENSION 
first, then EQ_TAC to prove two directions separately. But in my case, one 
direction cannot be proved. (I’ve been trying for 2 days), here is the full 
statements (it requires HOL’s existing measureTheory to be loaded):

val SETS_TO_DISJOINT_SETS = store_thm
  ("SETS_TO_DISJOINT_SETS",
  ``!sp sts f. subset_class sp sts /\ f IN (UNIV -> sts) ==>
   ?g. (g 0 = f 0) /\
   (!n. 0 < n ==> (g n = f n INTER (BIGINTER (IMAGE (\i. sp DIFF f i) 
(count n) /\
   (!i j :num. i <> j ==> DISJOINT (g i) (g j)) /\
   (BIGUNION (IMAGE f UNIV) = BIGUNION (IMAGE g UNIV))``,
  …);

More importantly, I’m trying to figure out why an informal math proof cannot be 
translated into a formal one, at least I don’t know how.In general, a 
statement about (count n) doesn’t hold automatically for univ(:num), but in 
above case I think yes, just I don’t know how.

—Chun

> Il giorno 15 set 2018, alle ore 22:40, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> 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 
> <http://hvg.ece.concordia.ca/code/hol/DFT/index.php>
> On Sat, Sep 15, 2018 at 4:27 PM Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> 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 <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> <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/ 
> <http://save.seecs.nust.edu.pk/waqar-ahmad/>
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

[Hol-info] Prove BIGUNION (IMAGE f 핌(:num)) by induction on (count n)?

[Chun Tian (binghe)]

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



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

[Hol-info] Uninterruptible PROVE_TAC []

[Chun Tian (binghe)]

Hi Michael,

with recent commits in HOL’s Git master, I found that I cannot easily interrupt 
the proof searching underly PROVE_TAC (or maybe also METIS_TAC). In another 
words, if I didn’t provide enough lemmas when calling PROVE_TAC [] and have 
caused the proof searching goes into infinite loops, I will *not* be able to 
interrupt HOL any more, by "Meta-H Ctrl-C” in Emacs, unless I do it early 
(still after calling PROVE_TAC but not that late somehow).   Then I have to 
kill HOL process in Emacs, then restart it, replay my proof scripts so far.

Do you have any clue on the root causes?(I also want to know if other HOL 
users met the same issues, by CC to hol-info mailing list)

Regards,

Chun



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

Re: [Hol-info] The "limit" of a ``:'num->'a set`` function?

[Chun Tian (binghe)]

Thanks, now I realized that, to have a meaningful “limit" on a sequence of 
sets, such a sequence must be either increasing or decreasing (f n SUBSET f 
(SUC n), or the other direction), then the “limit” is either BIGUNION (IMAGE f 
univ(:num)) or BIGINTER (IMAGE f univ(:num)).

—Chun

> Il giorno 14 set 2018, alle ore 04:53, michael.norr...@data61.csiro.au ha 
> scritto:
> 
> You don't just want something like
> 
>   BIGUNION (IMAGE f univ(:num))
> 
> ?
> 
> Michael
> 
> On 14/9/18, 05:02, "Chun Tian (binghe)"  wrote:
> 
>Hi,
> 
>I want to express the existence of a function (f :’num -> ‘a set) such 
> that, whenever the number n goes to “infinite”, ``f n`` equals to a given set 
> ``X :’a set``.
> 
>This looks like something in limTheory, but I have nothing to do with real 
> numbers here.
> 
>Does anyone know which definition in HOL4’s existing libraries should I 
> look for?
> 
>Regards,
> 
>Chun Tian
> 
> 
> 
> 



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

[Hol-info] The "limit" of a ``:'num->'a set`` function?

[Chun Tian (binghe)]

Hi,

I want to express the existence of a function (f :’num -> ‘a set) such that, 
whenever the number n goes to “infinite”, ``f n`` equals to a given set ``X :’a 
set``.

This looks like something in limTheory, but I have nothing to do with real 
numbers here.

Does anyone know which definition in HOL4’s existing libraries should I look 
for?

Regards,

Chun Tian




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

Re: [Hol-info] Two definitions of wellfoundedness

[Chun Tian (binghe)]

Hi,

ah... thanks, I didn’t see this theorem before.

—Chun

> Il giorno 11 set 2018, alle ore 10:08, Lorenz Leutgeb  ha 
> scritto:
> 
> Hi,
> 
> they are the same. Use the following theorem from prim_rec:
> 
> WF_IFF_WELLFOUNDED
> ⊢ ∀R. WF R ⇔ wellfounded R
> 
> Best,
> Lorenz
> 
> On Tue, 11 Sep 2018 at 17:59 Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> Hi,
> 
> in prim_recTheory, there’s a definition of ``wellfounded``:
> 
> [wellfounded_def]  Definition
> 
>   ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)
> 
> In relationTheory, there’s a definition of ``WF``:
> 
> [WF_DEF]  Definition
> 
>   ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b
> 
> are they essentially the same thing? (and if so, how to prove?)
> 
> —Chun
> 
> ___
> hol-info mailing list
> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
> https://lists.sourceforge.net/lists/listinfo/hol-info 
> <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

[Hol-info] Two definitions of wellfoundedness

[Chun Tian (binghe)]

Hi,

in prim_recTheory, there’s a definition of ``wellfounded``:

[wellfounded_def]  Definition

  ⊢ ∀R. wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)

In relationTheory, there’s a definition of ``WF``:

[WF_DEF]  Definition

  ⊢ ∀R. WF R ⇔ ∀B. (∃w. B w) ⇒ ∃min. B min ∧ ∀b. R b min ⇒ ¬B b

are they essentially the same thing? (and if so, how to prove?)

—Chun



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

Re: [Hol-info] Using Assumptions

[Chun Tian (binghe)]

Hi.

you can use PAT_ASSUM or PAT_X_ASSUM (or their versions in Q structure) to 
match an assumption and then use it as a theorem for your next tactic. 
PAT_ASSUM will keep the assumption untouched, while PAT_X_ASSUM will remove it, 
both are useful in certain cases.

For example, if there’s an assumption like ``!x. P x`` (P could be anything), 
and you want to move it to goal as an antecedent, a tactic like:

Q.PAT_X_ASSUM `!x. P x` MP_TAC

or

Q.PAT_X_ASSUM `!x. P x` (fn thm => MP_TAC thm)

will do the job. In case you want to further treatment of that theorem before 
calling MP_TAC, just expand above 2nd form inside the lambda-function. Check 
reference manual for more details.

Hope this helps,

—Chun

> Il giorno 16 ago 2018, alle ore 18:07, Dylan Melville 
>  ha scritto:
> 
> Is there anyway to reference a specific assumption of the current goal as a 
> theorem?
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] measureTheory (was: Re: New extrealTheory)

[Chun Tian (binghe)]

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.

—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
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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?)

[Chun Tian (binghe)]

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

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

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

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

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

—Chun

> Il giorno 10 ago 2018, alle ore 00:20, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> Hi,
> 
> I appreciate the changes that you are making but I'm still not sure that why 
> are you re-proving the existing properties that are present in the latest 
> version [1]. For instance, EXTREAL_SUM_IMAGE_INSERT is already existed in [1] 
> in different forms:
> 
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> NegInf) \/
>(!x. x IN e INSERT s ==> f x <> PosInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> 
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_NEG (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> NegInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> 
> extreal_hvgTheory.EXTREAL_SUM_IMAGE_PROPERTY_POS (THEOREM)
> --
> |- !f s.
>FINITE s ==>
>!e.
>(!x. x IN e INSERT s ==> f x <> PosInf) ==>
>(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> You can simply merge the latest extrealTheory (extreal_hvgTheory) with the 
> HOL sources and that will be it?
> 
> 
> [1] http://hvg.ece.concordia.ca/code/hol/DFT/index.php 
> <http://hvg.ece.concordia.ca/code/hol/DFT/index.php>
> 
> 
> On Thu, Aug 9, 2018 at 5:26 PM Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> Hi,
> 
> I’ve done some rework on EXTREAL_SUM_IMAGE (or SIGMA) of extrealTheory.
> 
> My general idea is: SIGMA of extreal can only be defined when there’s no 
> mixing of +inf and -inf in the summation. So I start with the old definition 
> based on ITSET:
> 
>[EXTREAL_SUM_IMAGE_def]  Definition
> 
>   ⊢ ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0
> 
> And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all its 
> properties (thus all remaining results should be derived from just this 
> single theorem without using the original definition):
> 
>[EXTREAL_SUM_IMAGE_THM]  Theorem
> 
>   ⊢ ∀f.
> (SIGMA f ∅ = 0) ∧
> ∀e s.
> ((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
>  ∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> a weaker (but practical) corollary is the following one (see the differences 
> of function f):
> 
>[EXTREAL_SUM_IMAGE_INSERT]  Theorem
> 
>   ⊢ ∀f s.
> (∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
> ∀e s.
> FINITE s ⇒
> (SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))
> 
> once I got EXTREAL_SUM_IMAGE_THM  almost all other SIGMA theorems either has 
> trivial proofs or their existing proofs still work. But the proof of above 
> theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3 for -inf), 
> I show the ones for +inf here:
> 
> [lemma1]
> ⊢ ∀f s.
>  FINITE s ⇒
>  ∀x b.
>  (∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
>  (ITSET (λe acc. f e + acc) (x INSERT s) b =
>   ITSET (λe acc. f e + acc) (s DELETE x)
> ((λe acc. f e + acc) x b))
> 
> [lemma2]
> ⊢ ∀f s.
>  (∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
>  ∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf
> 
> [lemma3]
> ⊢ ∀b f x s.
> 

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

[Chun Tian (binghe)]

Hi,

I’ve done some rework on EXTREAL_SUM_IMAGE (or SIGMA) of extrealTheory.

My general idea is: SIGMA of extreal can only be defined when there’s no mixing 
of +inf and -inf in the summation. So I start with the old definition based on 
ITSET:

   [EXTREAL_SUM_IMAGE_def]  Definition

  ⊢ ∀f s. SIGMA f s = ITSET (λe acc. f e + acc) s 0

And I proved a general theorem EXTREAL_SUM_IMAGE_THM which captures all its 
properties (thus all remaining results should be derived from just this single 
theorem without using the original definition):

   [EXTREAL_SUM_IMAGE_THM]  Theorem

  ⊢ ∀f.
(SIGMA f ∅ = 0) ∧
∀e s.
((∀x. x ∈ e INSERT s ⇒ f x ≠ PosInf) ∨
 ∀x. x ∈ e INSERT s ⇒ f x ≠ NegInf) ∧ FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

a weaker (but practical) corollary is the following one (see the differences of 
function f):

   [EXTREAL_SUM_IMAGE_INSERT]  Theorem

  ⊢ ∀f s.
(∀x. f x ≠ PosInf) ∨ (∀x. f x ≠ NegInf) ⇒
∀e s.
FINITE s ⇒
(SIGMA f (e INSERT s) = f e + SIGMA f (s DELETE e))

once I got EXTREAL_SUM_IMAGE_THM  almost all other SIGMA theorems either has 
trivial proofs or their existing proofs still work. But the proof of above 
theorem is not easy, I have to prove 6 lemmas first (3 for +inf, 3 for -inf), I 
show the ones for +inf here:

[lemma1]
⊢ ∀f s.
 FINITE s ⇒
 ∀x b.
 (∀z. z ∈ x INSERT s ⇒ f z ≠ PosInf) ∧ b ≠ PosInf ⇒
 (ITSET (λe acc. f e + acc) (x INSERT s) b =
  ITSET (λe acc. f e + acc) (s DELETE x)
((λe acc. f e + acc) x b))

[lemma2]
⊢ ∀f s.
 (∀x. x ∈ s ⇒ f x ≠ PosInf) ∧ FINITE s ⇒
 ∀b. b ≠ PosInf ⇒ ITSET (λe acc. f e + acc) s b ≠ PosInf

[lemma3]
⊢ ∀b f x s.
 (∀y. y ∈ x INSERT s ⇒ f y ≠ PosInf) ∧ b ≠ PosInf ∧ FINITE s ⇒
 (ITSET (λe acc. f e + acc) (x INSERT s) b =
  (λe acc. f e + acc) x (ITSET (λe acc. f e + acc) (s DELETE x) b))

These proofs were learnt from similar proofs in pred_setTheory and digged into 
the nature of extreal. Noticed that they are all lemmas about ITSET 
(pred_setTheory), λ-function (λe acc. f e + acc), and a extreal `b`, and once I 
set `b = 0` the whole ITSET just become SIGMA for extreals.  Thus these proofs 
were done even before EXTREAL_SUM_IMAGE is defined.

Then I re-used most proofs from the new version of extrealTheory, with almost 
all new theorems originally in HOL4’s version preserved (sometimes re-proved).

The new “extrealScript.sml” can be found here [1]. Now I have a satisfied 
extended real theory and have switched to merge the new measureTheory (with 
measure type ``:‘a set -> extreal`` instead of old ``:’a set -> real``) into 
HOL4.

[1] 
https://github.com/binghe/HOL/blob/HOL-Probability/src/probability/extrealScript.sml

Feel free to comment, I’ll be appreciated if you could let the original authors 
know these changes.

Regards,

Chun

> Il giorno 07 ago 2018, alle ore 18:35, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> Hi,
> 
> You're welcome to suggest improvements.. maybe step forward to put the 
> extrealTheory on right footings.. I'll be more than happy, if I could be of 
> any help to you at any point.
> 
> On Tue, Aug 7, 2018 at 11:56 AM Chun Tian (binghe)  <mailto:binghe.l...@gmail.com>> wrote:
> Hi,
> 
> I just want to see a textbook-correct theory of extended reals. Actually I’m 
> not quite sure how the improved measureTheory (of extreal) is connected with 
> the improved extrealTheory (with different definitions on +, -, inv). What I 
> observed so far is, the new measureTheory does use some new theorems from the 
> new extrealTheory, but those theorems should be also proved in the old 
> version of extrealTheory.
> 
> Of course the consequent formalization must be consistent, as long as we 
> don’t use axioms and cheats in the proof scripts.  The biggest enemy in 
> formalizations is the “wrong” definition, a correctly proved theorem based on 
> wrongly defined things would be useless. (but here it’s not that “wrong” 
> actually, because in probability measure there’s no mixing of PosInf and 
> NegInf at all; on the other side I’m not sure how the changes in 
> “extreal_inv” affects the new measureTheory.)
> 
>> Skipping the PosInf + a = PosInf requires to prove the termination of 
>> "EXTREAL_SUM_IMAGE" function as it has been done.
> 
> 
> I don’t think so. The termination of both old and new definition comes from 
> the finiteness of sets involved. A proper subset of finite set always has 
> smaller (by one) cardinality (CARD_PSUBSET), as shown in the following proof 
> scripts:
> 
> (WF_REL_TAC `measure (CARD o SND)` THEN
>METIS_TAC [CARD_PSUBSET, REST_PSUBSET])
> 
> Actually under th

Re: [Hol-info] conflicts auto-resolved by Define?

[Chun Tian (binghe)]

Hi,

I just want to see a textbook-correct theory of extended reals. Actually I’m 
not quite sure how the improved measureTheory (of extreal) is connected with 
the improved extrealTheory (with different definitions on +, -, inv). What I 
observed so far is, the new measureTheory does use some new theorems from the 
new extrealTheory, but those theorems should be also proved in the old version 
of extrealTheory.

Of course the consequent formalization must be consistent, as long as we don’t 
use axioms and cheats in the proof scripts.  The biggest enemy in 
formalizations is the “wrong” definition, a correctly proved theorem based on 
wrongly defined things would be useless. (but here it’s not that “wrong” 
actually, because in probability measure there’s no mixing of PosInf and NegInf 
at all; on the other side I’m not sure how the changes in “extreal_inv” affects 
the new measureTheory.)

> Skipping the PosInf + a = PosInf requires to prove the termination of 
> "EXTREAL_SUM_IMAGE" function as it has been done.


I don’t think so. The termination of both old and new definition comes from the 
finiteness of sets involved. A proper subset of finite set always has smaller 
(by one) cardinality (CARD_PSUBSET), as shown in the following proof scripts:

(WF_REL_TAC `measure (CARD o SND)` THEN
   METIS_TAC [CARD_PSUBSET, REST_PSUBSET])

Actually under the new definition of ``extreal_add``, we can’t prove the 
following theorem (EXTREAL_SUM_IMAGE_THM in old version):

  ``!f. (EXTREAL_SUM_IMAGE f {} = 0) /\
(!e s. FINITE s ==>
   (EXTREAL_SUM_IMAGE f (e INSERT s) =
f e + EXTREAL_SUM_IMAGE f (s DELETE e)))``,

why? because there could be mixing of PosInf and NegInf returned by the 
function f, and the resulting sum is not defined. The proof of above theorem 
used to depend on COMMUTING_ITSET_RECURSES (pred_setTheory):

!f e s b. (!x y z. f x (f y z) = f y (f x z)) /\ FINITE s ==>
  (ITSET f (e INSERT s) b = f e (ITSET f (s DELETE e) b))

but now the antecedent "(!x y z. f x (f y z) = f y (f x z))” is not satisfiable 
any more. (i.e. can’t be directly proved by “add_assoc” and “add_comm” of 
extreals)

—Chun

> Il giorno 07 ago 2018, alle ore 17:27, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> Hi,
> 
> let me make a little more comments to the formalized extended reals.
> 
> I’m actually reviewing the improved version of extrealTheory as part of [1] 
> (the link "Required Theories”). I don’t know if there’re further updates, but 
> comparing with the existing definitions shipped in HOL4, I think the new 
> version fixed some issue yet introduced more others. For example, the 
> definition of extreal_inv now allows division by zero:
> 
> val extreal_inv_def = Define
>   `(extreal_inv NegInf = Normal 0) /\
>(extreal_inv PosInf = Normal 0) /\
>(extreal_inv (Normal x) = (if x = 0 then PosInf else Normal (inv x)))`;
> 
> This is not aligned with any textbook, and it doesn’t make sense to let 
> ``(Normal _) / 0 = PosInf``, because I think PosInf and NegInf should have 
> equal positions in the formal theory. It may look like PosInf is more 
> important than NegInf (as measureTheory only uses PosInf) but for the theory 
> of extended real itself, they should be of the same importance.
> 
> Actually, both version of extrealtheory are developed by the original authors 
> (maybe at the same time) but for some reason the version that is little more 
> flexible is made part of HOL repositories. The source files that you're 
> referring are the latest one. The major difference is that the measure can 
> now be of type extreal, which is essential to reason about Lebesgue integral 
> properties in particular.  I'm not sure what made you worry about the less 
> use of NegInf. Is this makes the consequent formalization inconsistent?
> 
> 
> The other thing is, once it’s not allowed to have “PosInf + NegInf” with a 
> defined value, the arithmetic of extended reals are not commutative and 
> associative without further restrictions (e.g. mixing of PosInf and NegInf 
> must be disabled, as the resulting summation has no definition).  The 
> consequence is, summation over finite sets are hard to formalize now, because 
> theorems like COMMUTING_ITSET_RECURSES (pred_setTheory) depends on the 
> commutativity of summation.  But syntactically, the following (old) 
> definition should still be true:
> 
> val EXTREAL_SUM_IMAGE_DEF = new_definition
>   ("EXTREAL_SUM_IMAGE_DEF",
>   ``EXTREAL_SUM_IMAGE f s = ITSET (\e acc. f e + acc) s (0:extreal)``);
> 
> because re-proving deep lemmas about ITSET is not that easy.  The improved 
> version now defines EXTREAL_SUM_IMAGE from grounds:
> 
> val EXTREAL_SUM_IMAGE_def =
>  let open TotalDefn
>  in
>tDefine "EXTREAL_SUM_IMAGE"
> `EXTREAL_SUM_IMAGE (f:'a -> extreal) (s: 'a -> bool) =
>if FINITE s then
>   if s={} then 0:extreal
>   else f (CHOICE s) + EXTREAL_SUM_IMAGE f (REST s)
>else 

Re: [Hol-info] conflicts auto-resolved by Define?

[Chun Tian (binghe)]

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.

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.

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 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 

Re: [Hol-info] conflicts auto-resolved by Define?

[Chun Tian (binghe)]

Hi,

is the improved version you’re using available somewhere?

—Chun

> Il giorno 05 ago 2018, alle ore 18:09, Waqar Ahmad <12phdwah...@seecs.edu.pk> 
> ha scritto:
> 
> Hi Chun,
> 
> I'm not sure about your potential conflict question but we are now using an 
> improved definition of "extreal_add_def"
> 
> val extreal_add_def = Define`
>(extreal_add (Normal x) (Normal y) = (Normal (x + y))) /\
>(extreal_add (Normal _) a = a) /\
>(extreal_add b (Normal _) = b) /\
>(extreal_add NegInf NegInf = NegInf) /\
>(extreal_add PosInf PosInf = PosInf)`;
> 
> This will rule out the possibility of PosInf + a= PosInf... We do have a plan 
> to update the probability theory to the latest version in the near future 
> (Speaking on the behalf of original authors).
> 
> 
> 
> On Sun, Aug 5, 2018 at 11:14 AM Chun Tian  > 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/ 
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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?

[Chun Tian (binghe)]

Hi Thomas,

thanks for detailed explanations!

—Chun

> Il giorno 05 ago 2018, alle ore 19:58, Thomas Tuerk  
> ha scritto:
> 
> Hi Chun, Waqar,
> 
> "Define" does indeed give priority to earlier clauses. Under the hood pattern 
> compilation takes place. So what is actually is going on for
>> 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)`;
> 
> Is similar to what would happen for
> 
> val extreal_add_def = Define`
>   (extreal_add a b = case (a, b) of
>  (Normal x, Normal y) => (Normal (x + y))
>| (PosInf, _) => PosInf
>| (_, PosInf) => PosInf
>| (NegInf, _) => NegInf
>| (_, NegInf) => NegInf
> 
> In both cases, the pattern match (case-expression) is compiled to a decision 
> tree using various heuristics. This tree contains implicitly a complete list 
> of distinct patterns.
> Distinct means that the patterns don't overlap. Complete means that they 
> cover every possible value. For case-expressions you get the decision tree 
> itself back. For top-level pattern matches you get a list of non-overlapping 
> patterns back that are used for the returned definition theorem. If you look 
> at the result of the original definition, you will see that the actual 
> definition theorem is
> 
>   |- !y x v5 v3 v2 a.
>   (extreal_add (Normal x) (Normal y) = Normal (x + y)) /\
>   (extreal_add PosInf a = PosInf) /\
>   (extreal_add NegInf PosInf = PosInf) /\
>   (extreal_add (Normal v2) PosInf = PosInf) /\
>   (extreal_add NegInf NegInf = NegInf) /\
>   (extreal_add NegInf (Normal v5) = NegInf) /\
>   (extreal_add (Normal v3) NegInf = NegInf)
> 
> Here you see that the original clauses disappeared. Instead patterns from 
> resulting from this pattern compilation are used. Notice that similar to SML 
> and other functional languages, Define gives precedence to earlier clauses.
> 
> Most case-expressions are simple and pattern compilation is not an issue. 
> However, for more complicated cases it can be hard to predict what the 
> results will be. If you are interested, I recommend having a look at section 
> 6.4 of the description manual. I personally try not to use non-trivial 
> definitions directly, but use the theorems produced by Define to prove 
> simple, manually stated sanity check lemmata. I believe this makes proofs 
> more robust and helps me detect problems with my definitions earlier.
> 
> Best
> 
> Thomas
> 
> 
> On 05.08.2018 18:09, Waqar Ahmad via hol-info wrote:
>> 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 

Re: [Hol-info] How to (automatically) change the names of quantified variables in a theorem?

[Chun Tian (binghe)]

Hi Thomas,

thanks very much, now I see the possibility of changing whatever variable names 
I want!  (I never knew nor needed ALPHA before, although alpha-conversion is 
familiar to me)

—Chun

> Il giorno 03 ago 2018, alle ore 15:03, Thomas Tuerk  
> ha scritto:
> 
> Hi Chun,
> 
> the easiest way is using alpha-equivalence. If you really just want to rename 
> vars, you can state the new form explicitly and use apha-equivalence via e.g. 
> ALPHA directly. Tools like METIS_TAC should in theory be able to do it, but 
> in practice try to do too much and therefore time out, I fear.
> 
> There are also tools for renaming bound vars. "rename_bvar" for example is a 
> conversion for renaming an outermost bound var.
> Variables at subpositions can also be renamed using the quantifier heuristics 
> lib (see, e.g. INST_QUANT_CONV)
> 
> Vaguely related are tools for renaming free vars during a tactical proof. 
> There are various related tactics for this, e.g. RENAME_TAC. However, since 
> these deal with free vars during a proof, this does not fit really here.
> 
> So, there are plenty of options. Looking at your description, I expect using 
> ALPHA is the easiest and fasted possibility for your problem. I would use 
> something like
> 
> fun ALPHA_RULE t thm = let
>   val t0 = concl thm
>   val thm1 = ALPHA t0 t
>   val thm2 = EQ_MP thm1 thm
> in
>   thm2
> end
> 
> 
> val t0 = ``?A.  A  \/ !B  C. ?D.  D  B  C``
> val t  = ``?A'. A' \/ !B' C. ?DD. DD B' C``
> 
> val thm0 = METIS_PROVE [] t0
> val thm = ALPHA_RULE t thm0
> 
> Best
> 
> Thomas
> 
> 
> 
> On 03.08.2018 14:34, Chun Tian (binghe) wrote:
>> Hi,
>> 
>> suppose I have proved (or generated) a theorem like this:
>> 
>>  ⊢ ∀a0 a1.
>>  a0 ∼ a1 ⇔
>>  ∀u.
>>  (∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
>>  ∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2
>> 
>> but I don’t like the variables names (a0, a1, E1, E2), I want a new theorem, 
>> essentially the same one, but with variables names same as in text book:
>> 
>> ⊢ ∀P Q.
>>  P ∼ Q ⇔
>>  ∀u.
>>  (∀P'. P --u-> P' ⇒ ∃Q'. Q --u-> Q' ∧ P' ∼ Q') ∧
>>  ∀Q'. Q --u-> Q' ⇒ ∃P'. P --u-> P' ∧ P' ∼ Q’
>> 
>> if I understood HOL correctly, it is impossible to directly modify any 
>> theorem (as first-class object), replacing its bound variables with 
>> different names (if not conflicting others).
>> 
>> Actually, changing the outside universal quantifiers is easy, as I just need 
>> to do a SPEC with new variables, then GEN them. On the other side, I don’t 
>> see any automatic way to replace inner variables.   I also tried to prove 
>> the new theorem by PROVE_TAC or METIS_TAC with the old theorem, sometimes 
>> the theorem can be directly proved, but most of time it fails, I think 
>> because of  those existential quantifiers.
>> 
>> Does anyone have such experiences? (it’s a painful process to go over all 
>> proofs again, fixing almost every step with different variable names)
>> 
>> 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 
>> <http://sdm.link/slashdot>
>> 
>> ___
>> hol-info mailing list
>> hol-info@lists.sourceforge.net <mailto:hol-info@lists.sourceforge.net>
>> https://lists.sourceforge.net/lists/listinfo/hol-info 
>> <https://lists.sourceforge.net/lists/listinfo/hol-info>
> 
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] How to (automatically) change the names of quantified variables in a theorem?

[Chun Tian (binghe)]

Hi,

suppose I have proved (or generated) a theorem like this:

 ⊢ ∀a0 a1.
 a0 ∼ a1 ⇔
 ∀u.
 (∀E1. a0 --u-> E1 ⇒ ∃E2. a1 --u-> E2 ∧ E1 ∼ E2) ∧
 ∀E2. a1 --u-> E2 ⇒ ∃E1. a0 --u-> E1 ∧ E1 ∼ E2

but I don’t like the variables names (a0, a1, E1, E2), I want a new theorem, 
essentially the same one, but with variables names same as in text book:

⊢ ∀P Q.
 P ∼ Q ⇔
 ∀u.
 (∀P'. P --u-> P' ⇒ ∃Q'. Q --u-> Q' ∧ P' ∼ Q') ∧
 ∀Q'. Q --u-> Q' ⇒ ∃P'. P --u-> P' ∧ P' ∼ Q’

if I understood HOL correctly, it is impossible to directly modify any theorem 
(as first-class object), replacing its bound variables with different names (if 
not conflicting others).

Actually, changing the outside universal quantifiers is easy, as I just need to 
do a SPEC with new variables, then GEN them. On the other side, I don’t see any 
automatic way to replace inner variables.   I also tried to prove the new 
theorem by PROVE_TAC or METIS_TAC with the old theorem, sometimes the theorem 
can be directly proved, but most of time it fails, I think because of  those 
existential quantifiers.

Does anyone have such experiences? (it’s a painful process to go over all 
proofs again, fixing almost every step with different variable names)

Regards,

Chun Tian



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] INST on a theorem

[Chun Tian (binghe)]

> show_types := true;
val it = (): unit
> INFINITY_AX;
val it = ⊢ ∃(f :ind -> ind). ONE_ONE f ∧ ¬ONTO f: thm

> Il giorno 23 lug 2018, alle ore 18:22, Dylan Melville 
>  ha scritto:
> 
> Is there a way to print theorems with types displayed?
> 
>> On Jul 23, 2018, at 12:20 PM, Thomas Tuerk  wrote:
>> 
>> Hi,
>> 
>> hard to say, why it does not work without further details. However, one 
>> guess is that types do not match. I would recommend showing the types when 
>> printing the theorem. I expect that P might be of type `'a -> bool`. In this 
>> case you need to instantiate 'a to string first.
>> 
>> Best
>> 
>> Thomas
>> 
>> On 23.07.2018 18:10, Dylan Melville wrote:
>>> I have a theorem called EX which returns true when a value is an element of 
>>> a list. It is defined as:
>>> 
>>> thm = |- (EX P [] <=> F) /\ (EX P (CONS h t) <=> P h \/ EX P t)
>>> 
>>> I am trying to use this theorem with `P` being `(\x. x = “T”)` and `t` 
>>> being a long list of strings which contains “T”.  Unfortunately my attempts 
>>> to use INST on this theorem haven’t worked. Why doesn’t the following work?
>>> 
>>> INST [`(\x:string. x = “T")`,`P:(string->bool)`] EX;;
>>> 
>>> Thank you.
>>> 
>>> -Dylan Melville (McMaster University)
>>> 
>>> 
>>> --
>>> 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
>> 
>> --
>> 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
> 
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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

[Chun Tian (binghe)]

Hi Waqar,

I think you’re looking for a datatype package in which induction and 
coinduction types can be mixed naturally. This is currently not possible in 
HOL4, but it’s not the fault of Higher Order Logic itself. According to Andrei 
Popescu et al. [1] it’s in theory possible to port or (re)implement their BNF 
work in HOL4 as it doesn’t depend on Isabelle's type extensions to Higher Order 
Logic. However this is a huge work, nobody is doing this porting, as far as I 
know, although it is supposed to be a huge contribution once it’s done.

—Chun

[1] Traytel, D., Popescu, A.: Foundational, compositional (co) datatypes for 
higher-order logic: Category theory applied to theorem proving. 2012 27th 
Annual IEEE Symposium on Logic in Computer Science. 596–605 (2012).

> Il giorno 03 lug 2018, alle ore 17:09, Waqar Ahmad via hol-info 
>  ha scritto:
> 
> Hi,
> 
> In Isabelle, besides coinduction, the normal induction procedure on 
> lazylist/stream datatype appears to be allowed.. Can a same behaviour is 
> possible with the 'a llist type in HOL4.
> 
> Secondly, unlike lazy list, the "stream" are defined without having the empty 
> "LNIL". I see a similar formalization in  HOL example directory 
> "...examples/Crypto/TEA/lazy_teaScript.sml"
> 
> 
> val RoundFun_def =
>  Define
>`RoundFun (s: state) = SOME (Round s, FST (Round s))`;
> 
> val StreamG_def = new_specification
>  ("StreamG",
>   ["StreamG"],
>   ISPEC ``RoundFun`` llist_Axiom_1);
> 
> I defined it using LUNFOLD as
> 
> StreamD xs = LUNFOLD (λn. SOME (THE (LTL n),THE (LHD n))) x
> 
> Is it possible, that when an induction scheme is applied, the base case 
> (LNIL) can be discharged/skipped? I'm aware of llist_bisumulation, which is 
> extremely useful in proving that two lazy lists are equal. However, in many 
> cases, its not applicable
> 
> 
> 
> On Sun, May 13, 2018 at 6:19 AM  > wrote:
> If you want the coinductively defined streams predicate over lllist, you can 
> write
> 
> 
> 
> >  CoIndDefLib.Hol_coreln `!a s. a IN A /\ streams A s ==> streams A (LCONS a 
> > s)`;
> 
> <>
> 
> <>
> 
> val it =
> 
>(⊢ ∀A a s. a ∈ A ∧ streams A s ⇒ streams A (a:::s),
> 
> ⊢ ∀A streams'.
> 
>   (∀a0. streams' a0 ⇒ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams' s) ⇒
> 
>   ∀a0. streams' a0 ⇒ streams A a0,
> 
> ⊢ ∀A a0. streams A a0 ⇔ ∃a s. (a0 = a:::s) ∧ a ∈ A ∧ streams A s):
> 
> 
> 
> I think the last theorem of the triple is the cases theorem you want.
> 
> 
> 
> Note that if you are going to define Stream with
> 
> 
> 
>   Stream L = LFILTER (\n. T) L
> 
> 
> 
> You might as well write the equivalent
> 
> 
> 
>   Stream L = L
> 
> 
> 
> Best wishes,
> 
> Michael
> 
> 
> 
> 
> 
> 
> 
> From: Waqar Ahmad <12phdwah...@seecs.edu.pk >
> Date: Saturday, 12 May 2018 at 05:45
> To: "Norrish, Michael (Data61, Acton)"  >
> Cc: hol-info  >
> Subject: 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 

[Hol-info] tacticoe

[Chun Tian (binghe)]

The author (Thibault Gauthier) should learn how to correctly use Git *first*, 
before committing directly to ‘master’.

—Chun



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] INVERSE of function?

[Chun Tian (binghe)]

Hi prof. Dawson,

thank you very much. With your given new definition (of INVERSE) I believe the 
proofs of some related lemmas now become trivial (using theorems of LINV, et 
al. in pred_setTheory).

Regards,

Chun

> Il giorno 28 mag 2018, alle ore 04:35, Jeremy Dawson 
>  ha scritto:
> 
> Hi Chun,
> 
> See LINV and RINV in pred_set.
> 
> I found the definitions of these pointlessly restrictive since they only 
> applied for an injective/surjective function.  So I changed things to define 
> them both in terms of LINV_OPT which I defined.  (Hence the old theorem names 
> LINV_DEF and RINV_DEF.)
> 
> see my commits
> 4e806d114105079ead99b4a27a86c08dd5515d68
> f3fcad057ccfff3130edc82912ec54155901f085
> 
> So, rather than a multiplicity of similarly defined functions (where the 
> obvious relations between them would not be provable because of the 
> indeterminacy of @), I'd suggest defining INVERSE in terms of LINV
> (eg, I think it would be INVERSE f y = LINV f UNIV y)
> 
> Jeremy
> 
>> On 05/28/2018 12:01 PM, Chun Tian wrote:
>> Hi,
>> I saw the following definition in the current pending request  (vector 
>> theory #513):
>>val INVERSE_DEF = Define `INVERSE f = \y. @x. f x = y`;
>> But isn’t this too common to be already somewhere in HOL’s theory library? 
>> If so, where is it?
>> Regards,
>> Chun
>> --
>> 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
> 
> --
> 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

--
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] HOL 4 Kananaskis 11 Installation Problem

[Chun Tian (binghe)]

Hi,

I think you should use Poly/ML 5.6 to build Kananaskis 11. (and Poly/ML
5.6 or5.7 to build latest HOL on GitHub)

Regards,

Chun

Ashish Darbari wrote:
> I'm running into this problem on Cent OS 7. No issues reported with
> Poly ML installation (installation from sources).
>
> When running either smart-configure or tweaking by hand the
> configure.sml file I get Static Errors.
>
> Any idea how to fix this?
>
>
> Ashish
>
> [adarbari@localhost hol-kananaskis-11]$ poly
>  Poly/ML 5.7.1 Release
>
> HOL smart configuration.
>
> Determining configuration parameters: holdir OS poly polymllibdir 
> OS: linux
> poly:   /usr/local/bin/poly
> polyc:  /usr/local/bin/polyc
> polymllibdir:   /usr/local/lib
> holdir: /home/adarbari/hol-kananaskis-11
> DOT_PATH:   /usr/bin/dot
>
> Configuration will begin with above values.  If they are wrong
> press Control-C.
>
> Will continue in 1 seconds.
>
> Loading system specific functions
> /home/adarbari/hol-kananaskis-11/tools-poly/configure.sml:283: error:
> Type error in function application.
>Function: > : Position.int * Position.int -> bool
>Argument: (OS.FileSys.fileSize uifile, size uifile_content) :
>   Position.int * int
>Reason:
>   Can't unify Position.int (*In Basis*) with int (*In Basis*)
>  (Different type constructors)
> Found near
>   Time.> (modTime sigfile, modTime uifile)
>  orelse
>  OS.FileSys.fileSize uifile > size uifile_content
> Static Errors
>
>
>
>
> --
> 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


--
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] Poly/ML debugging facility does not work in HOL4

[Chun Tian (binghe)]

It works for me, when I was debugging SML functions manipulating HOL terms, in 
whatever mode. I think you should provide details to let other help you 
figuring out the mistakes in your steps.

—Chun

> Il giorno 19/apr/2018, alle ore 20:42, Mario Xerxes Castelán Castro 
>  ha scritto:
> 
> Hello.
> 
> When I tried to use the Poly/ML debugger as described in
> 
> breakpoints do not work. “breakIn” does not raise an exception, but when
> applying the exception, the debugger is not entered. I check this within
> the HOL mode for Emacs, running “hol.bare” from the command like and
> running “poly” from the command line (to confirm that debugging works as
> intended without HOL). Only the later (Poly/ML without HOL4) worked.
> 
> Is there a way to use the debugger from within HOL4?
> 
> Thanks.
> 
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
> 
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] How to define term-like multi-recursive structures?

[Chun Tian (binghe)]

Hi again,

I'm surprised that, ``('a, 'b) alist`` (or ``('a # 'b) list``) is supported
by datatype package. So I'm going to have the following datatype in the
future:

val _ = Datatype `CCS = nil
 | var 'a
 | prefix ('b Action) CCS
 | sum CCS CCS
 | par CCS CCS
 | restr (('b Label) set) CCS
 | relab CCS ('b Relabeling)
 | fix (('a # CCS) list) 'a `;

I wanted to use finite_map (learnt from Konrad Slind) but datatype package
doesn't support it, however alist is a prefect replacement.

Thus I would say my question can be closed, if there's no other suggestions.

Regards,

Chun Tian



On Thu, Oct 26, 2017 at 10:56 AM, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:

> Let me describe the problem again: (actually I have a candidate solution)
>
> The central idea in the CCS grammar designed by Robin Milner is to use
> inductively defined finite structures to represent potential infinite
> structures. If I have the following equation of CCS:
>
> X = a + X
>
> The only solution would be an infinite sum of a:
>
> X = a + a + a + ...
>
> But we don't really need the infinite sum as part of CCS grammar, we can
> write this form instead:
>
> rec X (a + var X)
>
> So the "equation with single variable" itself can be treated as a CCS
> process.   But if I have multi-variable equations:
>
> X = a + Y
> Y = b + X
>
> the solution should be:
>
> X = a + b + a + b + ...
> Y = b + a + b + a + ...
>
> to represent the equation itself as a CCS process, I should at least put
> the following "fix" constructor into the datatype:
>
> fix ('a list) (CCS list) 'a
>
> so that I can write a term
>
> ``fix [X; Y] [a + var Y; b + var X] X``
>
> which means "the value of X in the equation group in which X and Y are
> unknown variables".  But if I write only partially:
>
> ``fix [X; Y] [a + var Y; b + var X]``
>
> above term should have the type ``:'a -> ('a, 'b) CCS``, which works like
> a choice function, given any variable it returns the corresponding value of
> that variable.
>
> In my initial question, I wanted to put only ``fix ('a list) (CCS list)``
> into the CCS datatype, and that was wrong because the type of ``fix ('a
> list) (CCS list)`` is not CCS, but (CCS list).
>
> Can you see a better way to have a similar datatype?
>
> Regards,
>
> Chun Tian
>
>
> On Thu, Oct 26, 2017 at 1:20 AM, <michael.norr...@data61.csiro.au> wrote:
>
>> I’m not sure why you say that you can’t add “fix” to the datatype
>> declaration.
>>
>> A line like
>>
>>| fix (CCS list)
>>
>> would be accepted by Datatype.  Then the type of the constructor “fix”
>> would be
>>
>>   fix : ('a,'b) CCS list -> ('a,'b) CCS
>>
>> In short, I don't understand why you write "the type of ``fix …`` is
>> *not* CCS at all".
>>
>> If your underlying constructors don't allow for "infinite" CCS terms (or
>> their encoding), then it's hard to know how you would ever define the sorts
>> of CCS constants that have infinite behaviours in time.  Perhaps one
>> approach would be to define the syntax as a co-datatype, allowing the
>> syntax itself to be infinite.  This'd be a bit weird though…
>>
>> Michael
>>
>> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
>> Date: Thursday, 26 October 2017 at 00:05
>> To: hol-info <hol-info@lists.sourceforge.net>
>> Subject: [Hol-info] How to define term-like multi-recursive structures?
>>
>> Hi,
>>
>> sorry for keeping asking questions.  In my current CCS datatype, there's
>> a recursive constructor:
>>
>> val _ = Datatype `CCS = nil
>>  | var 'a
>> ...
>>  | rec 'a CCS `;
>>
>> A term ``rec X (f (var X))`` is like the solution of an equation X =
>> f(X), or the fixed-point of f(), and its behavior is then defined by a set
>> of rules.  What the Datatype package gives me, is to make sure "rec" and
>> "var" are kind of *primitive* constants, such that they're part of the
>> one_one and distinctness theorems of the CCS. (if I simply define a
>> constant outside of the datatype, I don't have such benefits at all, and
>> many theorems will not be proved)
>>
>> Now  (as a long-term plan) I want to implement the ultimate, original
>> form of Milner's CCS [1], in which there's a "fix" (fixed-point)
>> constructor.  It's like a multi-variable version of above "rec" costructor,
>> something like:
>>
>> fix X p1 Y p2 Z p3 ...
>>
>> If you think above term as a multi-variable equat

Re: [Hol-info] How to define term-like multi-recursive structures?

[Chun Tian (binghe)]

Let me describe the problem again: (actually I have a candidate solution)

The central idea in the CCS grammar designed by Robin Milner is to use
inductively defined finite structures to represent potential infinite
structures. If I have the following equation of CCS:

X = a + X

The only solution would be an infinite sum of a:

X = a + a + a + ...

But we don't really need the infinite sum as part of CCS grammar, we can
write this form instead:

rec X (a + var X)

So the "equation with single variable" itself can be treated as a CCS
process.   But if I have multi-variable equations:

X = a + Y
Y = b + X

the solution should be:

X = a + b + a + b + ...
Y = b + a + b + a + ...

to represent the equation itself as a CCS process, I should at least put
the following "fix" constructor into the datatype:

fix ('a list) (CCS list) 'a

so that I can write a term

``fix [X; Y] [a + var Y; b + var X] X``

which means "the value of X in the equation group in which X and Y are
unknown variables".  But if I write only partially:

``fix [X; Y] [a + var Y; b + var X]``

above term should have the type ``:'a -> ('a, 'b) CCS``, which works like a
choice function, given any variable it returns the corresponding value of
that variable.

In my initial question, I wanted to put only ``fix ('a list) (CCS list)``
into the CCS datatype, and that was wrong because the type of ``fix ('a
list) (CCS list)`` is not CCS, but (CCS list).

Can you see a better way to have a similar datatype?

Regards,

Chun Tian


On Thu, Oct 26, 2017 at 1:20 AM, <michael.norr...@data61.csiro.au> wrote:

> I’m not sure why you say that you can’t add “fix” to the datatype
> declaration.
>
> A line like
>
>| fix (CCS list)
>
> would be accepted by Datatype.  Then the type of the constructor “fix”
> would be
>
>   fix : ('a,'b) CCS list -> ('a,'b) CCS
>
> In short, I don't understand why you write "the type of ``fix …`` is *not*
> CCS at all".
>
> If your underlying constructors don't allow for "infinite" CCS terms (or
> their encoding), then it's hard to know how you would ever define the sorts
> of CCS constants that have infinite behaviours in time.  Perhaps one
> approach would be to define the syntax as a co-datatype, allowing the
> syntax itself to be infinite.  This'd be a bit weird though…
>
> Michael
>
> From: "Chun Tian (binghe)" <binghe.l...@gmail.com>
> Date: Thursday, 26 October 2017 at 00:05
> To: hol-info <hol-info@lists.sourceforge.net>
> Subject: [Hol-info] How to define term-like multi-recursive structures?
>
> Hi,
>
> sorry for keeping asking questions.  In my current CCS datatype, there's a
> recursive constructor:
>
> val _ = Datatype `CCS = nil
>  | var 'a
> ...
>  | rec 'a CCS `;
>
> A term ``rec X (f (var X))`` is like the solution of an equation X = f(X),
> or the fixed-point of f(), and its behavior is then defined by a set of
> rules.  What the Datatype package gives me, is to make sure "rec" and "var"
> are kind of *primitive* constants, such that they're part of the one_one
> and distinctness theorems of the CCS. (if I simply define a constant
> outside of the datatype, I don't have such benefits at all, and many
> theorems will not be proved)
>
> Now  (as a long-term plan) I want to implement the ultimate, original form
> of Milner's CCS [1], in which there's a "fix" (fixed-point) constructor.
> It's like a multi-variable version of above "rec" costructor, something
> like:
>
> fix X p1 Y p2 Z p3 ...
>
> If you think above term as a multi-variable equation groups, then each
> part in its solution will be defined as a valid CCS term.  Such a
> "solution" (as a container of CCS terms) may be represented as a finite_map
> ``:('a |-> ('a, 'b) CCS)`` or simply a list ``:('a, 'b) CCS list``.
>
> Obviously I can't put this "fix" directly into the definition of above CCS
> datatype (let's assume HOL4 can do support nesting recursive datatype),
> because the type of ``fix ...`` is *not* CCS at all.   But what is it if I
> want such a constant? some kind of specification?
>
> Regards,
>
> Chun Tian
>
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
>
> [1] Milner, R.: Operational and Algebraic Semantics of Concurrent
> Processes. 1–41 (2017).
>
>
>
> --------
> --
> 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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Chun Tian (binghe)]

I'm fine with constant overloading. But I think the "term_name" used in
add_rule() doesn't know constant overloading at all. After realaxTheory is
loaded, the previous rule defined in relationTheory has absolutely no
effects, even I'm using "inv" for relations.

But I don't mind if relation "inv" also uses "^{-1}" (so we should move the
rule from realaxTheory to relationTheory and remove the existing one in
relationTheory).

---
Chun

On 16 October 2017 at 16:02, Mario Castelán Castro <marioxcc...@yandex.com>
wrote:

> On 16/10/17 08:23, Chun Tian (binghe) wrote:
> > Is this something can be fixed? (I don't know how) i.e. preserving the
> > pp_setting of  "inv" for relations and correctly define TeX notations for
> > both of them.
>
> “inv” has 2 possible resolutions after loading realTheory:
>
> > overload_info_for "inv";
> inv parses to:
>   realax$inv
>   (relation$inv :(α -> α -> bool) -> α -> α -> bool)
> inv might be printed from:
>   (relation$inv :(α -> α -> bool) -> α -> α -> bool)
>   realax$inv
> val it = (): unit
>
> Typically the correct one will be chosen by the parser because of type
> constraints. If you want to force one of them, you can write
> “relation$inv” or “realax$inv”. If you want to make the one from
> “relation” the default, then do “overload_on("inv",“relation$inv”):”. I
> do not know how to manipulate the TeX mapping.
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> 
> --
> 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
>
>


-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] Conflicted "inv" pp_elements in relationTheory and realaxTheory

[Chun Tian (binghe)]

Hi,

In relationTheory there's a "inv" operatior for inverting a relation:

(* --
inverting a relation
   -- *)

val inv_DEF = new_definition(
  "inv_DEF",
  ``inv (R:'a->'b->bool) x y = R y x``);
(* superscript suffix T, for "transpose" *)
val _ = add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
   fixity = Suffix 2100,
   paren_style = OnlyIfNecessary,
   pp_elements = [TOK (UTF8.chr 0x1D40)],
   term_name = "inv"}

while there's another rule in realaxTheory, setting it differently:

val _ =
   add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
  fixity = Suffix 2100,
  paren_style = OnlyIfNecessary,
  pp_elements = [TOK (UnicodeChars.sup_minus ^
UnicodeChars.sup_1)],
  term_name = "inv"}

As a result, when I start HOL (in which relationTheory is loaded by
default), I see the "transpose" representation of ``inv R``:

-
   HOL-4 [Kananaskis 11 (expknl, built Mon Oct 16 12:19:37 2017)]
   For introductory HOL help, type: help "hol";
   To exit type -D
-
> ``inv R``;
<>
val it = “Rᵀ”: term

But after loading realTheory (directly or indirectly), it permanently
becomes $R^{-1}$:

> load "realTheory";
val it = (): unit
> ``inv R``;
<>
val it = “R⁻¹”: term
> ``inv (R :'a -> 'a -> bool)``;
val it = “R⁻¹”: term

Further more, their TeX notations were never defined, thus in TeX-based PDF
it simply shows "inv R".

Is this something can be fixed? (I don't know how) i.e. preserving the
pp_setting of  "inv" for relations and correctly define TeX notations for
both of them.

Regards,

Chun Tian

--
Chun Tian (binghe)
University of Bologna (Italy)
--
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] Converting ordinals from different type variables?

[Chun Tian (binghe)]

Hi Michael,

Thanks very much, this saves me lots of time trying to prove something
impossible.

Regards,

Chun Tian


On 16 October 2017 at 00:59, <michael.norr...@data61.csiro.au> wrote:

> The definition is fine, but will not have the nice properties you want
> (e.g., monotonicity) if the domain type is bigger than the range.  In
> particular if your domain includes \omega_1 and the range only has
> countable ordinals, then the result of c2a on \omega_1 will be
> unspecified.  This is because the RHS of the limit case will be invoking
> sup on the set of all possible ordinals in the range type.  Given that, you
> will not be able to prove that monotonicity holds.
>
> Michael
>
> On 15/10/17, 18:26, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> Hi,
>
> If I have the following recursive function on ordinals, simply
> converting ‘c ordinals into the “same” ‘a ordinals:
>
> (* Construct a 'c ordinal from 'a ordinal *)
> val c2a_def = new_specification (
>"c2a_def", ["c2a"],
> ord_RECURSION |> INST_TYPE [``:'a`` |-> ``:'c``]
>   |> ISPEC ``0 :'a ordinal``(* z *)
>   |> Q.SPEC `\x r. ordSUC r`(* sf *)
>   |> Q.SPEC `\x rs. sup rs` (* lf *)
>   |> SIMP_RULE (srw_ss()) []);
>
> val it =
>|- (c2a 0o = 0) ∧ (∀α. c2a α⁺ = (c2a α)⁺) ∧
>∀α. 0o < α ∧ islimit α ⇒ (c2a α = sup (IMAGE c2a (preds α))):
>thm
>
> Is my definition correct? (especially for the “lf” part using “sup”)
>  And if so, what properties can I expect from this function?   Is it at
> least monotone? i.e.
>
>  ∀m n. m ≤ n ⇒ c2a m ≤ c2a n
>
> 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
>



-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] What's the recommended way to delete elements from list?

[Chun Tian (binghe)]

By the way, it's amazing that your original definition (based on FILTER)
can be used to prove the following theorem so easily:

val DELETE_ELEMENT_APPEND = store_thm (
   "DELETE_ELEMENT_APPEND",
  ``!a L L'. DELETE_ELEMENT a (L ++ L') = DELETE_ELEMENT a L ++
DELETE_ELEMENT a L'``,
REWRITE_TAC [DELETE_ELEMENT_FILTER]
 >> REWRITE_TAC [GSYM FILTER_APPEND_DISTRIB]);

Regards,

Chun Tian


On 11 October 2017 at 13:41, Ramana Kumar <ramana.ku...@cl.cam.ac.uk> wrote:

> Oh whoops I misunderstood - it deletes all of them. Never mind.
>
> On 11 October 2017 at 22:38, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>
> wrote:
>
>> Just based on your final question, I suggest:
>> ?l1 l2. (DELETE_ELEMENT e L = l1 ++ l2) /\ (L = l1 ++ [e] ++ l2)
>>
>> On 11 October 2017 at 22:34, <michael.norr...@data61.csiro.au> wrote:
>>
>>> You might define the sublist relation :
>>>
>>>   Sublist [] l = T
>>>   Sublist _ [] = F
>>>   Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist
>>> (h1::t1) t2
>>>
>>> And show that
>>>
>>>   Sublist (DELETE_ELEMENT e l) l
>>>
>>> This doesn’t capture the idea that the only missing elements are e’s
>>> though.  This definition of Sublist might not be the easiest to work with…
>>>
>>> Michael
>>>
>>> On 11/10/17, 22:31, "Chun Tian" <binghe.l...@gmail.com> wrote:
>>>
>>> Hi,
>>>
>>> I’d like to close an old question.  3 months ago I was trying to
>>> define the free names in CCS process but failed to deal with list
>>> deletions.   Today I found another way to delete elements from list,
>>> inspired by DROP:
>>>
>>> val DELETE_ELEMENT_def = Define `
>>>(DELETE_ELEMENT e [] = []) /\
>>>(DELETE_ELEMENT e (x::l) = if (e = x) then DELETE_ELEMENT e l
>>>  else x::DELETE_ELEMENT e l)`;
>>>
>>> And the previous definition suggested by Ramana based on FILTER now
>>> becomes a theorem as alternative definition:
>>>
>>>[DELETE_ELEMENT_FILTER]  Theorem
>>>
>>>   |- ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
>>>
>>> I found it’s easier to use the recursive definition, because many
>>> useful results can be proved easily by induction on the list. For example:
>>>
>>>[EVERY_DELETE_ELEMENT]  Theorem
>>>
>>>   |- ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L
>>>
>>>[LENGTH_DELETE_ELEMENT_LE]  Theorem
>>>
>>>   |- ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
>>>
>>>[LENGTH_DELETE_ELEMENT_LEQ]  Theorem
>>>
>>>   |- ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
>>>
>>>[NOT_MEM_DELETE_ELEMENT]  Theorem
>>>
>>>   |- ∀e L. ¬MEM e (DELETE_ELEMENT e L)
>>>
>>> What I actually needed is LENGTH_DELETE_ELEMENT_LE, but 3 months ago
>>> I just couldn’t prove it!
>>>
>>> However, I still have one more question: how can I express the fact
>>> that all elements in (DELETE_ELEMENT e L) are also elements of L, with
>>> exactly the same order and number of appearances?   In another words, by
>>> inserting some “e” into (DELETE_ELEMENT e L) I got the original list L?
>>>
>>> Regards,
>>>
>>> Chun Tian
>>>
>>> > Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar <
>>> ramana.ku...@cl.cam.ac.uk> ha scritto:
>>> >
>>> > Sure, that's fine. I probably wouldn't even define such a constant
>>> but would instead use ``FILTER ((<>) x) ls`` in place.
>>> >
>>> > Stylistically it's usually better to use Define instead of
>>> new_definition, and to name defining theorems with a "_def" suffix. I'd
>>> also keep the name short like "DELETE" or even "delete".
>>> >
>>> > On 2 Jul 2017 17:04, "Chun Tian (binghe)" <binghe.l...@gmail.com>
>>> wrote:
>>> > Hi,
>>> >
>>> > It seems that ListTheory didn’t provide a way to remove elements
>>> from list? What’s the recommended way to do such operation? Should I use
>>> FILTER, for example, like this?
>>> >
>>> > val DELETE_FROM_LIST = new_definition (
>>> >"DELETE

Re: [Hol-info] What's the recommended way to delete elements from list?

[Chun Tian (binghe)]

Hi Michael,

Thanks, this SUBLIST relation is good enough for my potential needs.

Regards,

Chun Tian


On 11 October 2017 at 13:34, <michael.norr...@data61.csiro.au> wrote:

> You might define the sublist relation :
>
>   Sublist [] l = T
>   Sublist _ [] = F
>   Sublist (h1::t1) (h2::t2) = if h1 = h2 then Sublist t1 t2 else Sublist
> (h1::t1) t2
>
> And show that
>
>   Sublist (DELETE_ELEMENT e l) l
>
> This doesn’t capture the idea that the only missing elements are e’s
> though.  This definition of Sublist might not be the easiest to work with…
>
> Michael
>
> On 11/10/17, 22:31, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> Hi,
>
> I’d like to close an old question.  3 months ago I was trying to
> define the free names in CCS process but failed to deal with list
> deletions.   Today I found another way to delete elements from list,
> inspired by DROP:
>
> val DELETE_ELEMENT_def = Define `
>(DELETE_ELEMENT e [] = []) /\
>(DELETE_ELEMENT e (x::l) = if (e = x) then DELETE_ELEMENT e l
>  else x::DELETE_ELEMENT e l)`;
>
> And the previous definition suggested by Ramana based on FILTER now
> becomes a theorem as alternative definition:
>
>[DELETE_ELEMENT_FILTER]  Theorem
>
>   |- ∀e L. DELETE_ELEMENT e L = FILTER (λy. e ≠ y) L
>
> I found it’s easier to use the recursive definition, because many
> useful results can be proved easily by induction on the list. For example:
>
>[EVERY_DELETE_ELEMENT]  Theorem
>
>   |- ∀e L P. P e ∧ EVERY P (DELETE_ELEMENT e L) ⇒ EVERY P L
>
>[LENGTH_DELETE_ELEMENT_LE]  Theorem
>
>   |- ∀e L. MEM e L ⇒ LENGTH (DELETE_ELEMENT e L) < LENGTH L
>
>[LENGTH_DELETE_ELEMENT_LEQ]  Theorem
>
>   |- ∀e L. LENGTH (DELETE_ELEMENT e L) ≤ LENGTH L
>
>[NOT_MEM_DELETE_ELEMENT]  Theorem
>
>   |- ∀e L. ¬MEM e (DELETE_ELEMENT e L)
>
> What I actually needed is LENGTH_DELETE_ELEMENT_LE, but 3 months ago I
> just couldn’t prove it!
>
> However, I still have one more question: how can I express the fact
> that all elements in (DELETE_ELEMENT e L) are also elements of L, with
> exactly the same order and number of appearances?   In another words, by
> inserting some “e” into (DELETE_ELEMENT e L) I got the original list L?
>
> Regards,
>
> Chun Tian
>
> > Il giorno 02 lug 2017, alle ore 10:23, Ramana Kumar <
> ramana.ku...@cl.cam.ac.uk> ha scritto:
> >
> > Sure, that's fine. I probably wouldn't even define such a constant
> but would instead use ``FILTER ((<>) x) ls`` in place.
> >
> > Stylistically it's usually better to use Define instead of
> new_definition, and to name defining theorems with a "_def" suffix. I'd
> also keep the name short like "DELETE" or even "delete".
> >
> > On 2 Jul 2017 17:04, "Chun Tian (binghe)" <binghe.l...@gmail.com>
> wrote:
> > Hi,
> >
> > It seems that ListTheory didn’t provide a way to remove elements
> from list? What’s the recommended way to do such operation? Should I use
> FILTER, for example, like this?
> >
> > val DELETE_FROM_LIST = new_definition (
> >"DELETE_FROM_LIST", ``DELETE_FROM_LIST x list = (FILTER (\i. ~(i
> = x)) list)``);
> >
> > Regards,
> >
> > Chun
> >
> >
> > 
> --
> > 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
> >
>
>
>
> 
> --
> 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
>



-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] Is ``:string ordinal`` uncountable or not?

[Chun Tian (binghe)]

Hi Michael,

Thanks very much, it helps a lot. I took me some time to digest all the
words, that's why I reply late.

Regards,

Chun


On 10 October 2017 at 00:26, <michael.norr...@data61.csiro.au> wrote:

> Strings have the same cardinality as numbers (there is a bijection between
> them established in string_numTheory), so string ordinal will be the same
> type (up to isomorphism) as num ordinal.  There’s no general way to know
> what the cardinality of a type is unless you have theorems to hand that
> make it clear.
>
>
> In other words, the collection of countable ordinals is an uncountable
> set, so every ordinal type will have uncountably many elements. The first
> uncountable ordinal is that which has uncountably many predecessors, and
> will only be present if the type parameter has cardinality greater than
> aleph-0.
>
> To be pedantic about your last question: in the HOL formalisation all
> ordinal types are uncountable; not all ordinal types contain ω₁. In other
> words, the collection of countable ordinals is an uncountable set, so every
> ordinal type will have uncountably many elements. The first uncountable
> ordinal is that which has uncountably many predecessors, and will only be
> present if the type parameter has cardinality greater than aleph-0.
>
> Hope this helps,
> Michael
>
> On 10/10/17, 08:40, "Chun Tian" <binghe.l...@gmail.com> wrote:
>
> Hi,
>
> In Michael Norrish and Brian Huffman's paper [1] about HOL’s ordinals,
> it’s said, “the distinct types ``:unit ordinal``, ``:bool ordinal``, and
> ``:num ordinal`` will all be isomorphic (they will all be copies of the
> countable ordinals).”  “On the other hand, the type “:(num -> bool)
> ordinal” is large enough to include the first uncountable ordinal, w1.”
>
> I have a strange question here: what about “:string ordinal”? Is it
> large enough to include the first uncountable ordinal?  (or generally
> speaking, how can I know if an ordinal type based on an infinite type is
> large enough to be uncountable?)
>
> Regards,
>
> Chun Tian
>
> [1] Norrish, M., Huffman, B.: Ordinals in HOL: Transfinite Arithmetic
> up to (and Beyond) w1. (2013).
>
>
> 
> --
> 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
>



-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] The use of optionTheory for representing invisible actions in transition systems

[Chun Tian (binghe)]

Hi again,

For example, if I use pairTheory to represent my Label type, something like:

val _ = type_abbrev ("Label", ``'b # bool``);
val _ = overload_on ("name", ``\s. (s, T)``);
val _ = overload_on ("coname", ``\s. (s, F)``);

then retrieving the underlying names is simply the FST of the pair, and
relabeling operation is inverting the SND of pairs.  Is this idea
recommended? (although I see no benefits other than shorter generated
theory files)

Regards,

Chun Tian



On 9 October 2017 at 13:58, Chun Tian (binghe) <binghe.l...@gmail.com>
wrote:

> Hi,
>
> I was having the following two Datatype definitions for representing
> "labels" and "actions" in transition systems like CCS/LTS:
>
> val _ = Datatype `Label = name 'b | coname 'b`;
> val _ = Datatype `Action = tau | label ('b Label)`;
>
> But yesterday, after my thesis work has been committed into HOL's example
> directory, I suddenly realized: isn't the "Action" type a perfect case to
> use HOL's optionTheory? that is, using NONE as tau (invisible action), and
> SOME for all others:
>
> val _ = type_abbrev ("Action", ``:'b Label option``);
> val _ = overload_on ("tau", ``NONE :'b Action``); (* NONE is invisible
> (tau) *)
> val _ = overload_on ("label", ``\(l :'b Label). SOME l``);
>
> optionTheory provided already the induction, nchotomy, one_one, ...
> theorems, so all I need to do is to use INST_TYPE to convert them into
> theorems for my fake "Action" type, e. g.
>
> (* Define structural induction on actions
>|- ∀P. P tau ∧ (∀L. P (label L)) ⇒ ∀A. P A
>  *)
> val Action_induction = save_thm (
>"Action_induction", INST_TYPE [``:'a`` |-> ``:'b Label``]
> option_induction);
>
> So I've made the changes, and it works amazingly well.  Isn't this too
> perfect?
>
> P. S. Is there any existing "simple" type in HOL such that I can prevent
> using Datatype for defining the "Label" type?
>
> Regards,
>
> Chun Tian
> University of Bologna (Italy)
>
>


-- 
Chun Tian (binghe)
University of Bologna (Italy)
--
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] The use of optionTheory for representing invisible actions in transition systems

[Chun Tian (binghe)]

Hi,

I was having the following two Datatype definitions for representing
"labels" and "actions" in transition systems like CCS/LTS:

val _ = Datatype `Label = name 'b | coname 'b`;
val _ = Datatype `Action = tau | label ('b Label)`;

But yesterday, after my thesis work has been committed into HOL's example
directory, I suddenly realized: isn't the "Action" type a perfect case to
use HOL's optionTheory? that is, using NONE as tau (invisible action), and
SOME for all others:

val _ = type_abbrev ("Action", ``:'b Label option``);
val _ = overload_on ("tau", ``NONE :'b Action``); (* NONE is invisible
(tau) *)
val _ = overload_on ("label", ``\(l :'b Label). SOME l``);

optionTheory provided already the induction, nchotomy, one_one, ...
theorems, so all I need to do is to use INST_TYPE to convert them into
theorems for my fake "Action" type, e. g.

(* Define structural induction on actions
   |- ∀P. P tau ∧ (∀L. P (label L)) ⇒ ∀A. P A
 *)
val Action_induction = save_thm (
   "Action_induction", INST_TYPE [``:'a`` |-> ``:'b Label``]
option_induction);

So I've made the changes, and it works amazingly well.  Isn't this too
perfect?

P. S. Is there any existing "simple" type in HOL such that I can prevent
using Datatype for defining the "Label" type?

Regards,

Chun Tian
University of Bologna (Italy)
--
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] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Great! sure, I’ll do that! —Chun

> Il giorno 05 ott 2017, alle ore 23:16, Ramana Kumar 
> <ramana.ku...@cl.cam.ac.uk> ha scritto:
> 
> I think it would be good to add this UNIQUE constant to listTheory, if you 
> have time to make a pull request.
> 
> On 6 October 2017 at 01:49, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
> Let me close this question (further comments are welcome, of course).
> 
> I actually got another good definition from Robert Beers in a private email:
> 
>[UNIQUE_DEF]  Definition
> 
>   |- ∀x L.
>UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2
> 
> This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is exactly 
> what I needed from the uniqueness. Then I tried to prove the following two 
> alternative definitions using above definition, with success:
> 
>[UNIQUE_ALT]  Theorem
> 
>   |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])
> 
>[UNIQUE_ALT_COUNT]  Theorem
> 
>   |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)
> 
> where LIST_ELEM_COUNT is a constant defined in rich_listTheory:
> 
> [LIST_ELEM_COUNT_DEF]  Definition
> 
>   |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)
> 
> From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other direction 
> is more difficult. I attached my proof scripts in case anyone needs it. But 
> I’m new to listTheory, my scripts are very ugly, sorry for that (they will 
> become better once I’ve learnt more).
> 
> Regards,
> 
> Chun Tian
> 
> 
> 
> > Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) 
> > <binghe.l...@gmail.com> ha scritto:
> >
> > Hi,
> >
> > (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> > possibly duplicated elements, and I want to express certain element X is 
> > unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> > "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> >
> > Regards,
> >
> > Chun Tian
> >
> > --
> > Chun Tian (binghe)
> > University of Bologna (Italy)
> >
> 
> 
> --
> 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
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Let me close this question (further comments are welcome, of course).

I actually got another good definition from Robert Beers in a private email:

   [UNIQUE_DEF]  Definition

  |- ∀x L.
   UNIQUE x L ⇔ ∃L1 L2. (L1 ⧺ [x] ⧺ L2 = L) ∧ ¬MEM x L1 ∧ ¬MEM x L2

This form is very useful for me, because "¬MEM x L1 ∧ ¬MEM x L2” is exactly 
what I needed from the uniqueness. Then I tried to prove the following two 
alternative definitions using above definition, with success:

   [UNIQUE_ALT]  Theorem

  |- ∀x L. UNIQUE x L ⇔ (FILTER ($= x) L = [x])

   [UNIQUE_ALT_COUNT]  Theorem

  |- ∀x L. UNIQUE x L ⇔ (LIST_ELEM_COUNT x L = 1)

where LIST_ELEM_COUNT is a constant defined in rich_listTheory:

[LIST_ELEM_COUNT_DEF]  Definition

  |- ∀e l. LIST_ELEM_COUNT e l = LENGTH (FILTER (λx. x = e) l)

From UNIQUE_ALT it’s easy to derive UNIQUE_ALT_COUNT, but the other direction 
is more difficult. I attached my proof scripts in case anyone needs it. But I’m 
new to listTheory, my scripts are very ugly, sorry for that (they will become 
better once I’ve learnt more).

Regards,

Chun Tian



extra_listScript.sml
Description: application/smil

> Il giorno 05 ott 2017, alle ore 16:03, Chun Tian (binghe) 
> <binghe.l...@gmail.com> ha scritto:
> 
> Hi,
> 
> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> possibly duplicated elements, and I want to express certain element X is 
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> 
> Regards,
> 
> Chun Tian
> 
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] Experience and opinions on proof assistants with “rich” type systems

[Chun Tian (binghe)]

Hi Jeremy,

I have a relevant question: one time we talked about the differences between 
Coq and HOL (thread title: "Difficulties when migrating proof scripts from 
Coq”), and you said:

"There's a distinction between an inductively defined set (in Isabelle or
HOL) and a datatype, though they can look similar.  I don't know which
corresponds better to your Coq code

You can model a proof by a proof tree "object" by using a datatype
definition - then you have something of which you can define functions
to give, eg, its' height, number of rule applications, etc.”

Is the ability for theorem provers to do reasoning directly on “proofs” (or can 
we say “proofs” are 1st-class objects?) also a consequence of “rich” type 
systems?

Regards,

Chun Tian

> Il giorno 05 ott 2017, alle ore 18:53, Jeremy Dawson 
>  ha scritto:
> 
> Hi Mario,
> 
> Slightly off-topic, I had experience with the type system of HOL-Omega 
> (system F, if I recall the terminology right, not dependent types, so my 
> experience may not be very relevant)
> 
> My dominant recollection is the difficulty of getting the system to do the 
> right type inference, and getting terms to typecheck.  I was forever working 
> out where I needed to put in type annotations.  Quite frustrating after my 
> experience with regular HOL, and Isabelle.
> 
> It led me to conclude that the systems offering automatic inference of a 
> principal type really occupy a "sweet spot", ie the best compromise between 
> ease of use and expressive power.
> 
> Cheers,
> 
> Jeremy Dawson
> 
> On 06/10/17 03:46, Mario Castelán Castro wrote:
>> On 04/10/17 20:09, Ramana Kumar wrote:
>>> Perhaps it would make more sense to ask people who are using rich type
>>> systems what their motivations are :)
>>> (On this list it's probably mostly people who are satisfied with simple
>>> type theory.)
>> 
>> Yes, you are right. I wrote to this list because I am interesting in the
>> opinion of informed “outsiders”, not only “insiders”, so to speak.
>> 
>> 
>> 
>> --
>> 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
>> 
> 
> --
> 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



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

OK, thanks everyone!  So FILTER is what I must use.

I think I’m going to use ``(FILTER (\e. e = X) L = [X])`` to assert the unique 
appearance of X in list L, and after I split the list using MEM_SPLIT, my 
target props (~MEM X l1) could be re-expressed by EVERY and FILTER, then it may 
be provable for me.

—Chun

> Il giorno 05 ott 2017, alle ore 17:03, Scott Owens <s.a.ow...@kent.ac.uk> ha 
> scritto:
> 
> Among others, LENGTH (FILTER (\e. X = e)) = 1
> 
> Scott
> 
>> On 2017/10/05, at 15:55, Chun Tian (binghe) <binghe.l...@gmail.com> wrote:
>> 
>> But my list is not ALL_DISTINCT … there’re duplicated elements for sure, 
>> just the appearance of certain element is only one. —Chun
>> 
>>> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind 
>>> <konrad.sl...@gmail.com> ha scritto:
>>> 
>>> Hi Chun Tian,
>>> 
>>> The constant ALL_DISTINCT in listTheory is what you are looking for, I 
>>> think.
>>> 
>>> Konrad.
>>> 
>>> 
>>> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) <binghe.l...@gmail.com> 
>>> wrote:
>>> Hi,
>>> 
>>> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
>>> possibly duplicated elements, and I want to express certain element X is 
>>> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
>>> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
>>> 
>>> Regards,
>>> 
>>> Chun Tian
>>> 
>>> --
>>> Chun Tian (binghe)
>>> University of Bologna (Italy)
>>> 
>>> 
>>> --
>>> 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
>>> 
>>> 
>> 
>> --
>> 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
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

But my list is not ALL_DISTINCT … there’re duplicated elements for sure, just 
the appearance of certain element is only one. —Chun

> Il giorno 05 ott 2017, alle ore 16:48, Konrad Slind <konrad.sl...@gmail.com> 
> ha scritto:
> 
> Hi Chun Tian,
> 
>   The constant ALL_DISTINCT in listTheory is what you are looking for, I 
> think.
> 
> Konrad.
> 
> 
> On Thu, Oct 5, 2017 at 9:03 AM, Chun Tian (binghe) <binghe.l...@gmail.com> 
> wrote:
> Hi,
> 
> (I'm new to HOL's listTheory). Suppose I have a list L which contains 
> possibly duplicated elements, and I want to express certain element X is 
> unique (i.e. has only one copy) in that list.  How can I do this?  It seems 
> "?!" doesn't work here, e.g. ``?!e. MEM e L /\ (e = X)``.
> 
> Regards,
> 
> Chun Tian
> 
> --
> Chun Tian (binghe)
> University of Bologna (Italy)
> 
> 
> --
> 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
> 
> 



signature.asc
Description: Message signed with OpenPGP using GPGMail
--
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