[opentheory-users] opentheory tool implementing eqMp incorrectly

[Joe Hurd]

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.

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