[opentheory-users] Importing proofs of version 6

Robert White ai.robert.wangshuai at gmail.com
Sun Jun 7 10:56:15 UTC 2015
Previous message: [opentheory-users] Importing proofs of version 6
Next message: [opentheory-users] axioms or proofs?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Ok, I will try now.

Thanks a lot.

Regards,
Robert

On 7 June 2015 at 08:56, Joe Leslie-Hurd <joe at gilith.com> wrote:

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



-- 

Regards,
Robert White <http://www.dptinfo.ens-cachan.fr/~swang/>(Shuai Wang)
INRIA Deducteam <https://www.rocq.inria.fr/deducteam/>
[Moving to ILLC of UvA from this Sep. ]
[New email address will be shuai.wang at student.uva.nl]
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150607/d60414df/attachment-0001.html>
Previous message: [opentheory-users] Importing proofs of version 6
Next message: [opentheory-users] axioms or proofs?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the opentheory-users mailing list