[opentheory-users] opentheory tool implementing eqMp incorrectly

[Ramana Kumar]

On Sun, Sep 11, 2011 at 12:33 AM, Joe Hurd <joe at gilith.com> wrote:
> 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?

The best I have at the moment is an article file
(http://cam.xrchz.net/cl.art.gz)
for a relatively simple theory I logged in HOL4. I can read this
article in using the HOL4 reader successfully, so now I'm more
confident it might be valid. But opentheory complains about an eqMp
command failing. Perhaps you could show me the arguments on the stack
for which the command is failing in a more readable form than the way
they are currently printed? They look like good arguments for eqMp to
me, but I'm not sure.

>
> 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
>>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>