[opentheory-users] opentheory tool implementing eqMp incorrectly

[Joe Hurd]

Hi Ramana,

I think the opentheory tool is implementing eqMp correctly. I added
some new trace statements and a new tiny test example (example5) that
executes one eqMp, and together the following was output:

ObjectRead.execute: cmd = eqMp
ObjectRead.execute: stack = [|- a, |- a <=> b]
ObjectProv.mkEqMp = |- b

The stack shows |- a on the top (the second argument of eqMp),
followed by |- a <=> b (the first argument of eqMp). Perhaps the
confusion results from the fact that the first argument is buried more
deeply on the stack than the second argument?

Do you have an example where the opentheory tool seems to be working
incorrectly?

Cheers,

Joe

On Thu, Sep 8, 2011 at 6:06 AM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> I think there's an argument order problem. It's hard keeping track of
> which argument is which though :)
>
> The article file format says, roughly,
> a :: a = b :: stack --[eqMp]--> b :: stack
>
> Now in the opentheory tool source code,
> ...
>      | Command.EqMp =>
>        let
>          val (stack,objA,objB) = ObjectStack.pop2 stack
>
>          val obj = ObjectProv.mkEqMp {savable = savable} objA objB
> ...
>
> fun pop2 stack =
> ...
>      | obj1 :: obj0 :: objs =>
> ...
>        in
>          (stack,obj0,obj1)
>        end
> ...
>
> fun mkEqMp {savable} objA objB =
> ...
>          in
>            Object.Thm (Thm.eqMp a b)
>          end
> ...
>
> fun eqMp th1 th2 =
> ...
>      val (c2',concl) = Term.destEq c1
>
>      val () =
>          if Term.alphaEqual c2 c2' then ()
>          else raise Error "Thm.eqMp: not alpha equivalent"
> ...
>
> (c2 is the conclusion of th2, c1 of th1)
> But I think th2 will be the equality (a=b), not th1.
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>