[opentheory-users] opentheory tool implementing eqMp incorrectly

[Ramana Kumar]

On Wed, Sep 14, 2011 at 11:14 PM, Joe Hurd <joe at gilith.com> wrote:
> Hi Ramana,
>
> I added some more debugging information to the opentheory tool, so
> running it on your example article now produces the output below. The
> most important lines are the last ones:
>
> different constants:
>     combinatoryLogicExample.cl.rep
>  vs combinatoryLogicExample.cl.rep
> different constant provenances: defined vs undefined
>
> What may have caused this situation is that one of these constants is
> the result of a type definition, but the other has been created using
> a "const" command (which results in an "undefined" constant). If this
> is indeed the cause of your problem the way to solve it is to save
> into the dictionary the constants that appear on the stack as a result
> of definition commands, and consistently use these versions throughout
> the article.

Yes, you were right about this - thanks.

I find it mildly disturbing that constants aren't determined solely by
their names.

I've updated my article at http://cam.xrchz.net/cl.art.gz
Try reading it, if you want, and tell me what should be improved...
I got some warnings from the opentheory tool.

Also the tool is really slow! (I compiled with mosml though and maybe
should try mlton.)

A next step for me would be to upload my (locally installed) package
somewhere - the infrastructure is in place for that I presume..?

>
> Cheers,
>
> Joe
>
> _______________________________________________
>
> FATAL ERROR: opentheory failed:
> in Article.fromTextFile:
> error in file "-" around line 23288:
> eqMp
> 2767
> def
> while executing eqMp command:
>  stack =
>    [|- (let a0' <- r in
>         !'cl'.
>           (!a0'.
>              a0' =
>              HOL4.Datatype.CONSTR Number.Numeral.zero arb
>                (\n. HOL4.Datatype.BOTTOM) \/
>              a0' =
>              HOL4.Datatype.CONSTR (Number.Natural.suc Number.Numeral.zero)
>                arb (\n. HOL4.Datatype.BOTTOM) \/
>              (?a0 a1.
>                 a0' =
>                 (let a0 <- a0 in
>                  \a1.
>                    HOL4.Datatype.CONSTR
>                      (Number.Natural.suc
>                         (Number.Natural.suc Number.Numeral.zero)) arb
>                      (HOL4.Datatype.FCONS a0
>                         (HOL4.Datatype.FCONS a1
>                            (\n. HOL4.Datatype.BOTTOM)))) a1 /\ 'cl' a0 /\
>                 'cl' a1) ==> 'cl' a0') ==> 'cl' a0') <=>
>        combinatoryLogicExample.cl.rep (combinatoryLogicExample.cl.abs r) =
>        r,
>     |- ((let a0' <- r in
>          !'cl'.
>            (!a0'.
>               a0' =
>               HOL4.Datatype.CONSTR Number.Numeral.zero arb
>                 (\n. HOL4.Datatype.BOTTOM) \/
>               a0' =
>               HOL4.Datatype.CONSTR
>                 (Number.Natural.suc Number.Numeral.zero) arb
>                 (\n. HOL4.Datatype.BOTTOM) \/
>               (?a0 a1.
>                  a0' =
>                  (let a0 <- a0 in
>                   \a1.
>                     HOL4.Datatype.CONSTR
>                       (Number.Natural.suc
>                          (Number.Natural.suc Number.Numeral.zero)) arb
>                       (HOL4.Datatype.FCONS a0
>                          (HOL4.Datatype.FCONS a1
>                             (\n. HOL4.Datatype.BOTTOM)))) a1 /\ 'cl' a0 /\
>                  'cl' a1) ==> 'cl' a0') ==> 'cl' a0') <=>
>         combinatoryLogicExample.cl.rep
>           (combinatoryLogicExample.cl.abs r) = r) <=>
>        ((let a0' <- r in
>          !'cl'.
>            (!a0'.
>               a0' =
>               HOL4.Datatype.CONSTR Number.Numeral.zero arb
>                 (\n. HOL4.Datatype.BOTTOM) \/
>               a0' =
>               HOL4.Datatype.CONSTR
>                 (Number.Natural.suc Number.Numeral.zero) arb
>                 (\n. HOL4.Datatype.BOTTOM) \/
>               (?a0 a1.
>                  a0' =
>                  (let a0 <- a0 in
>                   \a1.
>                     HOL4.Datatype.CONSTR
>                       (Number.Natural.suc
>                          (Number.Natural.suc Number.Numeral.zero)) arb
>                       (HOL4.Datatype.FCONS a0
>                          (HOL4.Datatype.FCONS a1
>                             (\n. HOL4.Datatype.BOTTOM)))) a1 /\ 'cl' a0 /\
>                  'cl' a1) ==> 'cl' a0') ==> 'cl' a0') <=>
>         combinatoryLogicExample.cl.rep
>           (combinatoryLogicExample.cl.abs r) = r) <=> T, r]
> in ObjectProv.mkEqMp:
> in Thm.eqMp:
> terms not alpha-equivalent:
>     (let a0' <- r in
>      !'cl'.
>        (!a0'.
>           a0' =
>           HOL4.Datatype.CONSTR Number.Numeral.zero arb
>             (\n. HOL4.Datatype.BOTTOM) \/
>           a0' =
>           HOL4.Datatype.CONSTR (Number.Natural.suc Number.Numeral.zero)
>             arb (\n. HOL4.Datatype.BOTTOM) \/
>           (?a0 a1.
>              a0' =
>              (let a0 <- a0 in
>               \a1.
>                 HOL4.Datatype.CONSTR
>                   (Number.Natural.suc
>                      (Number.Natural.suc Number.Numeral.zero)) arb
>                   (HOL4.Datatype.FCONS a0
>                      (HOL4.Datatype.FCONS a1 (\n. HOL4.Datatype.BOTTOM))))
>                a1 /\ 'cl' a0 /\ 'cl' a1) ==> 'cl' a0') ==> 'cl' a0') <=>
>     combinatoryLogicExample.cl.rep (combinatoryLogicExample.cl.abs r) = r
>  vs (let a0' <- r in
>      !'cl'.
>        (!a0'.
>           a0' =
>           HOL4.Datatype.CONSTR Number.Numeral.zero arb
>             (\n. HOL4.Datatype.BOTTOM) \/
>           a0' =
>           HOL4.Datatype.CONSTR (Number.Natural.suc Number.Numeral.zero)
>             arb (\n. HOL4.Datatype.BOTTOM) \/
>           (?a0 a1.
>              a0' =
>              (let a0 <- a0 in
>               \a1.
>                 HOL4.Datatype.CONSTR
>                   (Number.Natural.suc
>                      (Number.Natural.suc Number.Numeral.zero)) arb
>                   (HOL4.Datatype.FCONS a0
>                      (HOL4.Datatype.FCONS a1 (\n. HOL4.Datatype.BOTTOM))))
>                a1 /\ 'cl' a0 /\ 'cl' a1) ==> 'cl' a0') ==> 'cl' a0') <=>
>     combinatoryLogicExample.cl.rep (combinatoryLogicExample.cl.abs r) = r
> different constants at path 1010 subterms:
>     combinatoryLogicExample.cl.rep
>  vs combinatoryLogicExample.cl.rep
> different constants:
>     combinatoryLogicExample.cl.rep
>  vs combinatoryLogicExample.cl.rep
> different constant provenances: defined vs undefined
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>