[opentheory-users] Importing proofs of version 6

[Joe Leslie-Hurd]

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