I might have just produced my first correct metamath proof from a
Mephistolus proof
When trying to prove ⊢ ( ( 1 + 1 ) + 1 ) = 3
The following test code
val step = "( ( 1 + 1 ) + 1 )".toAssertion().s(Engine::reduce).step
val proof = Mephistolus2Metamath.mmProofFor(step, this@with)
MetamathProofChecker.process("test", NormalizedTheorem(step, listOf(), 0,
setOf()), proof)
succeeds and produces the (uncompressed) metamath proof :
c1
c1
caddc
co
c1
caddc
co
c2
c1
caddc
co
c3
c1
c1
caddc
co
c2
c1
caddc
1p1e2apr1 (<- I know that it is deprecated but it should do for the
moment)
oveq1i
2p1e3
eqtri
Could someone proofcheck it with another metamath proofchecker (I recycled
a proof checker that I implemented a few months ago, there might be bugs as
the code has been lying untended a long time)
I'll now work on :
0) improving the coverage of tests for proof conversion
1) compressing metamath proofs
2) Improving the range of Mephistolus theorems converted to Metamath.
This might not be hard as Mephistolus theorems are just slightly different
from metamath ones
(a difference : I'm pretty sure that x. in Mephistolus will only be allowed
for complex numbers though and not for any class expression
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/e8ab72ec-4131-4aea-8bc9-ba695fc2d93c%40googlegroups.com.
