Re: [Hol-info] Definitions of partial functions (incl. predicates)

[Ramana Kumar]

My intuition says that working with total functions (and especially
predicates) will be easier.
Why? I don't know exactly, but here are some possible reasons:
you can just use plain rewriting rather than conditional rewriting,
and you don't need to state so many assumptions explicitly on your
theorems.

I also want to make a point against the supposed elegance of partial
definitions. My understanding is that it seems more elegant to not
specify a function on inputs that are supposed to be "invalid" for
that function, because then you know your proofs don't depend on how
the function behaves on those inputs. In theory you could substitute
any function which agrees only on the valid inputs. However,
practically, I've never seen this work out. Nobody takes a proof on
an underspecified function and transports it to another setting with
another function that's the same on valid inputs, at least not
without doing substantial work. But often people do run into annoying
problems due to underspecification.


On 6 October 2017 at 06:04, Mario Castelán Castro 
wrote:

> Hello.
>
> What is the preferred way to define functions only for some values? For
> example, as in arithmetic$DIV in HOL?:
>
>   ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)
>
> Here nothing is asserted for the value of DIV for n = 0, thus it is
> “undefined” in some sense. I know that this can be done with
> “new_specification” but proving _trivial_ existence theorems seems like
> something that should be automatized.
>
> I am writing a formalization of elementary topology[1]. I have to define
> the concept of the interior, closure, etc. Currently I use total
> definitions. I am thinking that it may be more elegant to use a partial
> definition like the above.
>
> For example, currently I have the definition:
>
> interior To X r ⇔
>   is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
>   ∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To
>
> I want to change this to:
>
> is_topo To ∧ X ⊆ space To ⇒
>   interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}
>
> Is there some expected difficulty with this under-specification?
>
> Thanks.
>
> [1]  (work in progress).
>
> --
> 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
>
>
--
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 
>  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)  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) 
> >  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?

[Ramana Kumar]

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) 
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
>
>
--
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] Definitions of partial functions (incl. predicates)

[Mario Castelán Castro]

Hello.

What is the preferred way to define functions only for some values? For
example, as in arithmetic$DIV in HOL?:

  ⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)

Here nothing is asserted for the value of DIV for n = 0, thus it is
“undefined” in some sense. I know that this can be done with
“new_specification” but proving _trivial_ existence theorems seems like
something that should be automatized.

I am writing a formalization of elementary topology[1]. I have to define
the concept of the interior, closure, etc. Currently I use total
definitions. I am thinking that it may be more elegant to use a partial
definition like the above.

For example, currently I have the definition:

interior To X r ⇔
  is_topo To ∧ X ⊆ space To ∧ r ∈ space To ∧
  ∃Y. r ∈ Y ∧ Y ⊆ X ∧ Y open_in To

I want to change this to:

is_topo To ∧ X ⊆ space To ⇒
  interior To X = ⋃ {Y | Y ⊆ X ∧ Y open_in To}

Is there some expected difficulty with this under-specification?

Thanks.

[1]  (work in progress).

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Freek Wiedijk]

Hi Jeremy,

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

In Coq and Mizar I don't have this experience, in the sense
that I hardly ever need type annotations where I don't expect
them.  In occasionally have problems with "match ... with
..." typing, getting that to work can be very frustrating.
But apart from that, I don't have much of a problem.

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

I don't mind so much explicitly typing my variables
where they are bound.  So I don't share this feeling of
Hindley-Milner style polymorphism being a "sweet spot".
I'd rather have full polymorphism and dependent types
as well.

Freek

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

[Mario Castelán Castro]

On 05/10/17 11:53, Jeremy Dawson wrote:
> 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.

Hello Jeremy. Thanks for your answer! If you do not mind an off-topic
question, what differences in terms of usability and ease of formalizing
pure mathematics did you experience find between Isabelle and HOL4 (or
HOL Light if that is the one you use)?.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



signature.asc
Description: OpenPGP digital signature
--
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

[Jeremy Dawson]

Hi Chun Tian,

I don't know much about rich(er) type systems, and I'm not well 
acquainted with Coq, but I'd say that what can be done in Isabelle or 
HOL should be possible also in richer type systems.


Regarding modelling of a proof, the context of what I said is 
describing, in HOL or Isabelle, a proof system for some logic, and 
describing proofs in that proof system.


This is to be contrasted with an approach which I believe may be 
available in constructive logic systems, which is to do a proof in (say) 
Coq, then from that proof, to obtain a function which implements that 
proof, so in a sense you are getting an object representing the proof.


But I may be talking nonsense here, so you need the comments of someone 
more familiar with Coq or similar systems


Cheers,

Jeremy


On 06/10/17 05:38, Chun Tian (binghe) wrote:

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




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

[Mario Castelán Castro]

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.

-- 
Do not eat animals; respect them as you respect people.
https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan



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

[Jeremy Dawson]

Hi Mario,

I don't mind the question, but the answer may not be much use because 
it's a comparison between the 2005 version of Isabelle which I use and 
HOL4.


In terms of the type systems they are identical.

Isabelle has schematic variables and type classes, both of which can 
make proof easier.  Otherwise, I don't find major differences.


Turning to modern day Isabelle - other factors may be:

  - the extent of unnecessarily incompatible changes between one 
version of Isabelle and the next (which is in fact why I'm still using 
the 2005 version, when I'm not using HOL)


  - the difficulty of using ML to program complex proof tactics - 
mandatory for a small proportion of my work (I've had various and highly 
conflicting reports of whether this is possible or reasonably easy in 
current Isabelle)


  - documentation, and willingness of developers to help with questions 
(and for me, location at GMT+10 means I can often get an immediate answer)


In HOL4 the source code is effectively available for users to look at 
(in Isabelle they can look at it, but it - or a lot of it - is highly 
obfuscated).


Cheers,

Jeremy

On 06/10/17 04:49, Mario Castelán Castro wrote:

On 05/10/17 11:53, Jeremy Dawson wrote:

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.


Hello Jeremy. Thanks for your answer! If you do not mind an off-topic
question, what differences in terms of usability and ease of formalizing
pure mathematics did you experience find between Isabelle and HOL4 (or
HOL Light if that is the one you use)?.



--
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] Experience and opinions on proof assistants with “rich” type systems

[Jeremy Dawson]

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

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  ha 
> scritto:
> 
> Among others, LENGTH (FILTER (\e. X = e)) = 1
> 
> Scott
> 
>> On 2017/10/05, at 15:55, Chun Tian (binghe)  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 
>>>  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)  
>>> 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?

[Scott Owens]

Among others, LENGTH (FILTER (\e. X = e)) = 1

Scott

> On 2017/10/05, at 15:55, Chun Tian (binghe)  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  
>> 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)  
>> 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

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

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

Hi Anthony,

Thanks. This definition may work (at least I can see it’s correct), at least 
that’s what I can start with. But in my proof the next move will be using 
MEM_SPLIT to divide the list into three pieces:

[MEM_SPLIT]  Theorem

  |- ∀x l. MEM x l ⇔ ∃l1 l2. l = l1 ⧺ x::l2

and what I finally need are ``~MEM X l1`` and ``~MEM X l2``. But from FILTER 
and LENGTH how can I reach my targets? A little hints may help me a lot …

Regards,

Chun

> Il giorno 05 ott 2017, alle ore 16:21, Anthony Fox  ha 
> scritto:
> 
> Perhaps something like
> 
> val unique_def = Define`unique x l = LENGTH (FILTER ($= x) l) = 1`
> 
> is what you’re after?
> 
> Anthony
> 
>> On 5 Oct 2017, at 15:03, Chun Tian (binghe)  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

Re: [Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Konrad Slind]

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

[Hol-info] How to express the uniqueness of an (or a kind of) element(s) in a list?

[Chun Tian (binghe)]

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

[Hol-info] LRTC (Reflexive Transitive Closure with a List)

[Chun Tian (binghe)]

Hi,

In listTheory there's a concept called "LRC":

(* --
LRC
  Where NRC has the number of steps in a transitive path,
  LRC has a list of the elements in the path (excluding the rightmost)
   -- *)

val LRC_def = Define`
  (LRC R [] x y = (x = y)) /\
  (LRC R (h::t) x y =
   (x = h) /\ ?z. R x z /\ LRC R t z y)`;

But I think a more useful similar concept should be a Reflexive Transitive
Closure which is able to remember all the transition labels in a relation R
(of type 'a -> 'b -> 'a -> bool), that is:

val LRTC_DEF = new_definition ("LRTC_DEF",
  ``LRTC (R :'a -> 'b -> 'a -> bool) a l b =
  !P. (!x. P x [] x) /\
  (!x h y t z. R x h y /\ P y t z ==> P x (h :: t) z) ==> P a l
b``);

For example, if we have a relation R and things like P --a--> Q, Q --b-->
R,  the resulting closure (LRTC R) can be used to describe P --[a;b]--> R.

Following a similar path with RTC in relationTheory, I can prove the
following basic theorems:

   [LRTC0_NO_TRANS]  Theorem

  |- ∀R x y. LRTC R x [] y ⇔ (x = y)

   [LRTC_CASES1]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   if NULL l then x = y else ∃u. R x (HD l) u ∧ LRTC R u (TL l) y

   [LRTC_CASES2]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   if NULL l then x = y
   else ∃u. LRTC R x (FRONT l) u ∧ R u (LAST l) y

   [LRTC_CASES_LRTC_TWICE]  Theorem

  |- ∀R x l y.
   LRTC R x l y ⇔
   ∃u l1 l2. LRTC R x l1 u ∧ LRTC R u l2 y ∧ (l = l1 ⧺ l2)

   [LRTC_INDUCT]  Theorem

  |- ∀R P.
   (∀x. P x [] x) ∧
   (∀x h y t z. R x h y ∧ P y t z ⇒ P x (h::t) z) ⇒
   ∀x l y. LRTC R x l y ⇒ P x l y

   [LRTC_LRTC]  Theorem

  |- ∀R x m y. LRTC R x m y ⇒ ∀n z. LRTC R y n z ⇒ LRTC R x (m ⧺ n) z

   [LRTC_REFL]  Theorem

  |- ∀R. LRTC R x [] x

   [LRTC_RULES]  Theorem

  |- ∀R.
   (∀x. LRTC R x [] x) ∧
   ∀x h y t z. R x h y ∧ LRTC R y t z ⇒ LRTC R x (h::t) z

   [LRTC_SINGLE]  Theorem

  |- ∀R x t y. R x t y ⇒ LRTC R x [t] y

   [LRTC_STRONG_INDUCT]  Theorem

  |- ∀R P.
   (∀x. P x [] x) ∧
   (∀x h y t z. R x h y ∧ LRTC R y t z ∧ P y t z ⇒ P x (h::t) z) ⇒
   ∀x l y. LRTC R x l y ⇒ P x l y

   [LRTC_TRANS]  Theorem

  |- ∀R x m y n z. LRTC R x m y ∧ LRTC R y n z ⇒ LRTC R x (m ⧺ n) z

Is this something general enough for putting into, say, rich_listTheory?
(or has anyone already done a similar development?)

Regards,

-- 
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] Changing thms used by computeLib

[Ramana Kumar]

Unfortunately I don't know anything better than "run it again".

You could also maybe try an older HOL commit (maybe prior to
d52c7d66716ddd253b6fd40bd3d38b29a238c392) and see if that's any more
reliable.

This is all speculation on my part though. The problem could have nothing
to do with pointer equality.

On 5 October 2017 at 16:15, Heiko Becker  wrote:

> Hello Ramana,
>
> yes, the Mk_comb error occurs non-deterministic. Is there a temporary
> workaround for this, that I could make use of?
>
> Cheers,
>
> Heiko
>
> On 10/05/2017 12:43 PM, Ramana Kumar wrote:
>
> Hi Heiko,
>
> Does it fail every time when you try to run the proofs non-interactively
> (with Holmake)?
>
> I suspect the "Mk_comb" error, if it is non-deterministic, has to do with
> pointer equality problems, which are in the middle of being fixed.
>
> Cheers,
> Ramana
>
> On 5 October 2017 at 13:22, Heiko Becker  wrote:
>
>> Hello,
>>
>> I have some proofs that I could previously solve by running EVAL_TAC,
>> after modifying computeLib.the_compset with
>>
>>
>> val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>> val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>>
>>
>> As it turns out, the proofs still run fine when interactively run in an
>> HOL4 emacs session, but the proofs fail when run on the command line.
>>
>> The failure either is
>>
>> HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
>> m"}
>>  Uncaught exception: HOL_ERR {message = "", origin_function = "Mk_comb",
>> origin_structure = "Thm"}
>>
>> or
>>
>>  (∀k.
>> k = 1 ∨ k = 0 ⇒
>> lookup k (BS (BN LN (LS ())) () (LS ())) =
>> lookup k (BS LN () (LS (
>>
>> Previously it sufficed to have a file myComputeLib.sml declaring the
>> structure myComputeLib and adding the two val statements above there and
>> loading that file when doing the proof with "open". When trying to debug
>> this issue, I moved the val statements in a separate tactic, declaring
>>
>>   val my_eval_tac =
>>  let
>>val _ = computeLib.del_funs [sptreeTheory.subspt_def]
>>val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
>> sptreeTheory.subspt_eq]
>>  in
>>   EVAL_TAC
>>  end;
>>
>>
>> but that did not solve my problem either.
>>
>> Can someone help me resolve this or give me a hint on how to debug this
>> issue?
>>
>> Thanks,
>>
>> Heiko
>>
>>
>> 
>> --
>> 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] Changing thms used by computeLib

[Heiko Becker]

Hello Ramana,

yes, the Mk_comb error occurs non-deterministic. Is there a temporary 
workaround for this, that I could make use of?


Cheers,

Heiko

On 10/05/2017 12:43 PM, Ramana Kumar wrote:

Hi Heiko,

Does it fail every time when you try to run the proofs 
non-interactively (with Holmake)?


I suspect the "Mk_comb" error, if it is non-deterministic, has to do 
with pointer equality problems, which are in the middle of being fixed.


Cheers,
Ramana

On 5 October 2017 at 13:22, Heiko Becker > wrote:


Hello,

I have some proofs that I could previously solve by running
EVAL_TAC, after modifying computeLib.the_compset with


val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]


As it turns out, the proofs still run fine when interactively run
in an HOL4 emacs session, but the proofs fail when run on the
command line.

The failure either is

HOL_ERR {message = "", origin_function = "Mk_comb",
origin_structure = "T$
m"}
 Uncaught exception: HOL_ERR {message = "", origin_function =
"Mk_comb", origin_structure = "Thm"}

or

 (∀k.
k = 1 ∨ k = 0 ⇒
lookup k (BS (BN LN (LS ())) () (LS ())) =
lookup k (BS LN () (LS (

Previously it sufficed to have a file myComputeLib.sml declaring
the structure myComputeLib and adding the two val statements above
there and loading that file when doing the proof with "open". When
trying to debug this issue, I moved the val statements in a
separate tactic, declaring

  val my_eval_tac =
 let
   val _ = computeLib.del_funs [sptreeTheory.subspt_def]
   val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]
 in
  EVAL_TAC
 end;


but that did not solve my problem either.

Can someone help me resolve this or give me a hint on how to debug
this issue?

Thanks,

Heiko



--
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] Experience and opinions on proof assistants with “rich” type systems

[Freek Wiedijk]

Hi Ramana,

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

One can do everything with anything.  So dependent tpes
certainly are not _needed_ for formalization.  But dependent
types _are_ very convenient.  I know them both from Coq
and from Mizar.

In Mizar the foundations are untyped ZF-style set theory
(Josef Urban's PhD thesis is about cooking away all the
syntactic sugar), so you don't need an "an enormously
complex logic" (Mario's words) to get dependent types.

Examples of types that to me seem dependent in a natural
way are, in mathematics:

  element of the set X
  element of the carrier of the algebraic structure X
  vector space of dimension n
  normal subgroup of group G
  field of characteristic p
  field extension of field K
  simplicial k-complex
  morphism from A to B in a category

and in (theoretical) computer science:

  array of length n
  integer of signedness s and size n
  machine program of processor architecture P
  C program of implementation I
  normal form of term t under some reduction relation
  term of type A in a typed system

or in mathematical logic:

  proposition over a signature S
  proof of proposition A

Etcetera, etcetera.

The last actually _also_ has the signature S as an argument,
but it is "hidden" (implicit) because it can be inferred
from the type of A, so does not need to be written.
These implicit arguments are quite powerful.  For example,
when working in group theory, you can write x + y, but
actually it will be a ternary operation, with the group the
third argument that can be inferred from the type of x and y.

I know that John Harrison has a hack where he uses
type variables to simulate natural numbers, and you get
_something_ like dependent types in HOL that way.  But that
really only goes so far.

Now various of these types are sometimes in a natural way
empty (for example the type "normal form of term t", when t
does not have a normal form), which makes it so irritating
that Mizar doesn't allow for empty types.  Without dependent
arguments, not allowing for empty types is not a big deal
(like in HOL), but once you ahve dependent types you really
also have to allow for types being empty.

Even when you don't care at all (like I do, well maybe :-))
for the Curry-Howard isomorphism.

Freek

--
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] Changing thms used by computeLib

[Heiko Becker]

Hello,

I have some proofs that I could previously solve by running EVAL_TAC, 
after modifying computeLib.the_compset with



val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, 
sptreeTheory.subspt_eq]



As it turns out, the proofs still run fine when interactively run in an 
HOL4 emacs session, but the proofs fail when run on the command line.


The failure either is

HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
m"}
 Uncaught exception: HOL_ERR {message = "", origin_function = 
"Mk_comb", origin_structure = "Thm"}


or

 (∀k.
k = 1 ∨ k = 0 ⇒
lookup k (BS (BN LN (LS ())) () (LS ())) =
lookup k (BS LN () (LS (

Previously it sufficed to have a file myComputeLib.sml declaring the 
structure myComputeLib and adding the two val statements above there and 
loading that file when doing the proof with "open". When trying to debug 
this issue, I moved the val statements in a separate tactic, declaring


  val my_eval_tac =
 let
   val _ = computeLib.del_funs [sptreeTheory.subspt_def]
   val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER, 
sptreeTheory.subspt_eq]

 in
  EVAL_TAC
 end;


but that did not solve my problem either.

Can someone help me resolve this or give me a hint on how to debug this 
issue?


Thanks,

Heiko


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