[opentheory-users] Importing proofs of version 6

Joe Leslie-Hurd joe at gilith.com
Sun Jun 7 06:56:56 UTC 2015
Previous message: [opentheory-users] Importing proofs of version 6
Next message: [opentheory-users] Importing proofs of version 6
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Hi Robert,

It turned out the import code didn't work very well, but I have fixed
it up and it seems to be doing the right thing. For each theory you
import, you have to first extend_the_interpretation so the importer
can give a HOL Light name to the OpenTheory symbols in the article.

Also, a nice feature is that imports build on each other, so you can
import a sequence of theories where assumptions in later theories are
satisfied by theorems in earlier theories.

Below is an example showing how to import theories - each article file
was generated by a command of the form:

opentheory info --article -o natural-prime.art natural-prime

This new import code is all checked in to my HOL Light fork available at

http://src.gilith.com/hol-light.html

Cheers,

Joe


(* ------------------------------------------------------------------------- *)
(* Importing a theory.                                                       *)
(* ------------------------------------------------------------------------- *)

extend_the_interpretation
  "opentheory/theories/natural-divides/natural-divides.int";;
import_article "natural-divides.art";;

extend_the_interpretation
  "opentheory/theories/stream/stream.int";;
import_article "stream.art";;

extend_the_interpretation
  "opentheory/theories/natural-prime/natural-prime.int";;
import_article "natural-prime.art";;

On Fri, Jun 5, 2015 at 1:33 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> OK, that's not good. Let me take a look.
>
> Cheers,
>
> Joe
>
> On Fri, Jun 5, 2015 at 12:59 PM, Robert White
> <ai.robert.wangshuai at gmail.com> wrote:
>> :(
>>
>> looks it is not working that way.
>>
>> # import_article "../laholide/opentheory/natural-divides.art";;
>> Exception:
>> Failure
>>  "in article ../laholide/opentheory/natural-divides.art at line 159:
>> defineConst\nstack = [Term; \"Number.Natural.divides\"; Var; Var;
>> []]\nunknown constant \"Number.Natural.divides\"".
>> #
>>
>>
>> and when I load other files, say list.art. I get all the thm as None. OHHH
>> :(
>>
>> # import_article "../laholide/opentheory/list.art";;
>> val it :
>>   (term list * term) list * (thm option * (term list * term)) option list =
>>   ([([], `(!) = (\p. p = (\x. T))`);
>>     ([], `(/\) = (\p q. (\f. f p q) = (\f. f T T))`);
>>     ([], `!n. EVEN (SUC n) <=> ~EVEN n`);
>>     ([], `!n. EVEN (BIT0 (BIT1 _0) * n)`);
>>     ([], `!m n. SUC m = SUC n <=> m = n`);
>>     ([], `!m n p. m * n = m * p <=> m = _0 \/ n = p`);
>>     ([], `!m n. m <= n /\ n <= m <=> m = n`); ([], `BIT0 _0 = _0`);
>>     ([], `!n. _0 + n = n`); ([], `!n. BIT0 (SUC n) = SUC (SUC (BIT0 n))`);
>>     ([], `!m n. SUC m + n = SUC (m + n)`);
>>     ([], `!m n. m + SUC n = SUC (m + n)`);
>>     ([], `!p. p _0 /\ (!n. p n ==> p (SUC n)) ==> (!n. p n)`);
>>     ([], `!n. BIT1 n = SUC (BIT0 n)`); ([], `!n. _0 <= n`);
>>     ([], `!m. m <= _0 <=> m = _0`); ([], `!n. BIT0 (BIT1 _0) * n = n + n`);
>>     ([], `!m n. m <= SUC n <=> m = SUC n \/ m <= n`);
>>     ([], `!m n. m * n = _0 <=> m = _0 \/ n = _0`); ([], `!n. ~(SUC n =
>> _0)`);
>>     ([], `!m n p. m * n <= m * p <=> m = _0 \/ n <= p`);
>>     ([], `!m n. SUC m <= n <=> m < n`);
>>     ([], `!m n p. m * n < m * p <=> ~(m = _0) /\ n < p`);
>>     ([], `!m n. m <= n <=> m < n \/ m = n`);
>>     ([], `!m n. EVEN (m * n) <=> EVEN m \/ EVEN n`);
>>     ([], `!m n. EVEN (m + n) <=> EVEN m <=> EVEN n`);
>>     ([], `!m n. ~(m <= n /\ n < m)`); ([], `!m n. ~(m < n /\ n <= m)`);
>>     ([], `!m. m EXP _0 = BIT1 _0`); ([], `!m n. m EXP SUC n = m * m EXP n`);
>>     ([], `!m n p. m * n * p = (m * n) * p`);
>>     ([], `!m n. m EXP n = _0 <=> m = _0 /\ ~(n = _0)`);
>>     ([], `!p m n. m + p = n + p <=> m = n`);
>>     ([], `!e f. ?!fn. fn _0 = e /\ (!n. fn (SUC n) = f (fn n) n)`);
>>     ([], `!m n. ~(m <= n) <=> n < m`);
>>     ([], `!m n. m < n <=> (?d. n = m + SUC d)`); ([], `!m n. m + n = n +
>> m`);
>>     ([], `!m. m + _0 = m`); ([], `!m n. SUC m <= SUC n <=> m <= n`);
>>     ([], `CARD {} = _0`);
>>     ([],
>>      `!x s.
>>           FINITE s
>>           ==> CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD
>> s))`);
>>     ([], `!n. n <= SUC n`); ([], `!n. n <= n`);
>>     ([], `!m n p. m <= n /\ n <= p ==> m <= p`);
>>     ([], `!m n. (m + n) - m = n`); ([], `!n. n - n = _0`);
>>     ([], `!m n. m + n = _0 <=> m = _0 /\ n = _0`); ([], `!m n. m <= m + n`);
>>     ([], `!m n. m + n = n <=> m = _0`); ([], `!n. SUC n - BIT1 _0 = n`);
>>     ([], `!m. ~(m < _0)`); ([], `!m. m = _0 \/ (?n. m = SUC n)`);
>>     ([], `!m n. SUC m < SUC n <=> m < n`); ([], `!n. n < SUC n`);
>>     ([], `!p x. p x ==> p ((@) p)`);
>>     ([], `!n. {m | m < SUC n} = _0 INSERT {SUC m | m < n}`);
>>     ([], `!m n. n <= m + n`); ([], `!n. ~(n < n)`); ([], `!m. m - _0 = m`);
>>     ([], `!n. _0 < SUC n`); ([], `!m n. ~(m < n) <=> n <= m`);
>>     ([], `!m n. n <= m ==> SUC m - SUC n = m - n`);
>>     ([], `!m. SUC m = m + BIT1 _0`); ([], `!m n p. m + n + p = (m + n) +
>> p`);
>>     ([], `!m n p. m < n /\ n <= p ==> m < p`);
>>     ([], `!m n p. m + n <= m + p <=> n <= p`)],
>>    [None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; None; None; None; None; None; None; None; None; None;
>>     None; None; None; ...])
>>
>>
>>
>>
>> On 5 June 2015 at 19:14, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>>
>>> Hi Robert,
>>>
>>> Perhaps a more realistic case study would be to import a new theory
>>> from the OpenTheory repo:
>>>
>>> http://opentheory.gilith.com/
>>>
>>> For example,
>>>
>>> opentheory install natural-divides
>>> opentheory info --article -o natural-divides.art natural-divides
>>>
>>> and then import this article file?
>>>
>>> Cheers,
>>>
>>> Joe
>>>
>>> On Fri, Jun 5, 2015 at 10:04 AM, Robert White
>>> <ai.robert.wangshuai at gmail.com> wrote:
>>> > Hi Joe,
>>> >
>>> > At the moment I am only trying to load the old proofs. but if I don't
>>> > change
>>> > the hol.ml file there will be conflict then. So seems the only solution
>>> > is
>>> > that I completely comment out the rest of the files loaded in hol.ml if
>>> > so?
>>> >
>>> > No, I don't have new theories so far.
>>> > Regards,
>>> > Robert
>>> >
>>> > On 5 June 2015 at 19:00, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >>
>>> >> Hi Robert,
>>> >>
>>> >> You are using it correctly. The intent of the import facility is to
>>> >> extend the current logical context by bringing in a new theory, not to
>>> >> change the current logical context. The error that you are redefining
>>> >> the T constant is an indication that you are trying to change the
>>> >> current logical context.
>>> >>
>>> >> What is your eventual goal using the OpenTheory importer in HOL Light?
>>> >> I assume you have some new theories you want to import that are not
>>> >> already in HOL Light.
>>> >>
>>> >> Cheers,
>>> >>
>>> >> Joe
>>> >>
>>> >>
>>> >> On Fri, Jun 5, 2015 at 5:44 AM, Robert White
>>> >> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> > Dear Joe,
>>> >> >
>>> >> > I am wondering if I am using it correctly. I would like to load some
>>> >> > thm
>>> >> > in
>>> >> > and do some proof checking and proof optimisation. However, after
>>> >> > loading
>>> >> > the hol.ml and then do
>>> >> > let all = import_article "../../laholide/opentheory/bool.art";;
>>> >> > I get errors saying I am redefining constants. For instance, the
>>> >> > bool.art
>>> >> > file:
>>> >> >
>>> >> > # let all = import_article "../../laholide/opentheory/bool.art";;
>>> >> > Exception:
>>> >> > Failure
>>> >> >  "in article ../../laholide/opentheory/bool.art at line 89:
>>> >> > defineConst\nstack = [Term; \"Data.Bool.T\"; Thm]\nnew_constant:
>>> >> > constant T
>>> >> > has already been declared".
>>> >> >
>>> >> > I could solve the problem by either not loading some of the files in
>>> >> > HOL, so
>>> >> > constants won't be redefined, or try to detect the problems that are
>>> >> > defined
>>> >> > but going to be redefined the same way. I would you solve the problem
>>> >> > for
>>> >> > the OpenTheory version of HOL.
>>> >> >
>>> >> > Thanks
>>> >> > Regards,
>>> >> > Robert
>>> >> >
>>> >> >
>>> >> > On 5 June 2015 at 08:38, Robert White <ai.robert.wangshuai at gmail.com>
>>> >> > wrote:
>>> >> >>
>>> >> >> Thanks Joe!
>>> >> >>
>>> >> >> I will have to do some more test. I will let you know if I find any
>>> >> >> bug.
>>> >> >>
>>> >> >> Regards,
>>> >> >> Robert
>>> >> >>
>>> >> >> On 5 June 2015 at 04:55, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >> >>>
>>> >> >>> Robert and I have updated the HOL Light importer to work with
>>> >> >>> version
>>> >> >>> 6 articles, which is now available from
>>> >> >>>
>>> >> >>> http://src.gilith.com/hol-light.html
>>> >> >>>
>>> >> >>> It is very lightly tested at this point, so it may well be buggy. I
>>> >> >>> was able to read in the standard theory library as a version 6
>>> >> >>> article, which I generated using the command
>>> >> >>>
>>> >> >>> opentheory info --article -o base.art base
>>> >> >>>
>>> >> >>> but I didn't even look closely at the results.
>>> >> >>>
>>> >> >>> Cheers,
>>> >> >>>
>>> >> >>> Joe
>>> >> >>>
>>> >> >>>
>>> >> >>> On Wed, Jun 3, 2015 at 2:12 PM, Robert White
>>> >> >>> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> >>> > Thanks for the reply.
>>> >> >>> >
>>> >> >>> > I would like to give it a try so I choose option 3 for now. I
>>> >> >>> > will
>>> >> >>> > use
>>> >> >>> > option 1 to continue my project alongside.
>>> >> >>> >
>>> >> >>> > Regards,
>>> >> >>> > Robert
>>> >> >>> >
>>> >> >>> > On 3 June 2015 at 22:46, Joe Leslie-Hurd <joe at gilith.com> wrote:
>>> >> >>> >>
>>> >> >>> >> Hi Robert,
>>> >> >>> >>
>>> >> >>> >> Unfortunately I have not yet updated the import capability in my
>>> >> >>> >> HOL
>>> >> >>> >> Light fork to work with version 6 theories. You can either:
>>> >> >>> >>
>>> >> >>> >> 1. Use the command I showed you before to convert version 6
>>> >> >>> >> articles
>>> >> >>> >> to version 5 before importing them.
>>> >> >>> >> 2. Wait for me to implement this functionality.
>>> >> >>> >> 3. Implement it yourself and send me a pull request.
>>> >> >>> >>
>>> >> >>> >> Please let me know what you decide: it may affect the wait time
>>> >> >>> >> in
>>> >> >>> >> solution 2 :-)
>>> >> >>> >>
>>> >> >>> >> Cheers,
>>> >> >>> >>
>>> >> >>> >> Joe
>>> >> >>> >>
>>> >> >>> >> On Wed, Jun 3, 2015 at 7:58 AM, Robert White
>>> >> >>> >> <ai.robert.wangshuai at gmail.com> wrote:
>>> >> >>> >> > Dear Joe,
>>> >> >>> >> >
>>> >> >>> >> > I noticed that I can't using import for the current version
>>> >> >>> >> > (version
>>> >> >>> >> > 6).
>>> >> >>> >> > I
>>> >> >>> >> > am using the one from:
>>> >> >>> >> >
>>> >> >>> >> > git clone http://src.gilith.com/hol-light
>>> >> >>> >> >
>>> >> >>> >> >
>>> >> >>> >> > I wonder if you have implemented it/updated the import.ml
>>> >> >>> >> > file,
>>> >> >>> >> > so I
>>> >> >>> >> > won't
>>> >> >>> >> > have to redo your work.
>>> >> >>> >> >
>>> >> >>> >> >
>>> >> >>> >> > Thanks
>>> >> >>> >> >
>>> >> >>> >> > Robert
>>> >> >>> >> >
>>> >> >>> >> >
>>> >> >>> >
>>> >> >>> >
>>> >> >>> >
>>> >> >>> >
>>> >> >>> > --
>>> >> >>> >
>>> >> >>> > Regards,
>>> >> >>> > Robert White (Shuai Wang)
>>> >> >>> > INRIA Deducteam
>>> >> >>
>>> >> >>
>>> >> >>
>>> >> >>
>>> >> >> --
>>> >> >>
>>> >> >> Regards,
>>> >> >> Robert White (Shuai Wang)
>>> >> >> INRIA Deducteam
>>> >> >> [Moving to ILLC of UvA from this Sep. ]
>>> >> >> [New email address will be shuai.wang at student.uva.nl]
>>> >> >>
>>> >> >
>>> >> >
>>> >> >
>>> >> > --
>>> >> >
>>> >> > Regards,
>>> >> > Robert White (Shuai Wang)
>>> >> > INRIA Deducteam
>>> >> > [Moving to ILLC of UvA from this Sep. ]
>>> >> > [New email address will be shuai.wang at student.uva.nl]
>>> >> >
>>> >
>>> >
>>> >
>>> >
>>> > --
>>> >
>>> > Regards,
>>> > Robert White (Shuai Wang)
>>> > INRIA Deducteam
>>> > [Moving to ILLC of UvA from this Sep. ]
>>> > [New email address will be shuai.wang at student.uva.nl]
>>> >
>>
>>
>>
>>
>> --
>>
>> Regards,
>> Robert White (Shuai Wang)
>> INRIA Deducteam
>> [Moving to ILLC of UvA from this Sep. ]
>> [New email address will be shuai.wang at student.uva.nl]
>>
Previous message: [opentheory-users] Importing proofs of version 6
Next message: [opentheory-users] Importing proofs of version 6
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list