[opentheory-users] Importing proofs of version 6

Robert White ai.robert.wangshuai at gmail.com
Fri Jun 5 19:59:57 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 ]
:(

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 <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/20150605/5fe94842/attachment-0001.html>
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