Mephistolus just reached it's 4th Milestone
Now, it allow it's single user (me) to :
produce a Mephistolus proof and a Metamath proof in a developer friendly way
for example, the command
"( ( ; 2 6 x. ( ( ( ( 7 x. ; 8 9 ) + ∨2c ) x. ( ; ; 1 2 3 + ( ( 7 - ∨1c )
x. ( ! ` 5 ) ) ) ) - ; ; 2 3 8 ) ) / ; 1 4 )" // stating the expression to
compute
.single("∨1c = 1", "∨2c = 2") // adding antecedents
.s(Engine::reduce) // the actual computation and proof process
proves that
|- ( ∨1c = 1 -> ( ∨2c = 2 -> ( ( ; 2 6 x. ( ( ( ( 7 x. ; 8 9 ) + ∨2c ) x. (
; ; 1 2 3 + ( ( 7 - ∨1c ) x. ( ! ` 5 ) ) ) ) - ; ; 2 3 8 ) ) / ; 1 4 ) = (
; ; ; ; ; ; 6 8 4 6 2 8 1 / 7 ) ) )
with a Mephistolus proof that is 2151 calls long
And it exports it to a Metamath proof that has 1845237 calls
And metamath-check-proofs it
in less than 8s (but those 8s is from a cold start with all initialisations
happening (the parser, parsing all theorems...)
To achieve that, after a few tries, I managed to implement a Mephistolus->
Metamath conversion process,
that is quite nice to use. I also had to metamath-prove the Mephistolus
theorems I was using (obviously).
When the mephistolus theorems were close from some metamath counterpart
(inference, deduction or implication), it was quite straightforward
And when I was ralying on Mephistolus theorem that had no equivalent in the
mm database; I had to work some more and prove them using other proven
Mephistolus theorems
For example, I needed this to be proven:
val impImp = mephistolusTheorem(aim="|- ( ( ∨1w -> ∨2w ) -> ( ∨3w -> ∨4w
) )", hypotheses = "|- ( ∨3w -> ∨1w )", "|- ( ∨1w -> ( ∨2w -> ∨4w ) )")
fun Proofers.proveCloser() {
// addition
MinZinZ.add1(mmMinZinZ)
N0pN0inN0.add1(mmN0pN0inNN0)
NpNinN.add1(mmNpNinNN)
ZpZinZ.add1(mmZpZinZ)
N0pNinN.add2(mmNpN0inN_imp, 1, 0) { it.a(rotP).proveResult() }
NexpN0inN.add1(mmNexpN0inN)
ZsubZinZ.add1(mmAsubB_e_ZZ)
Nsub1inN0.add2(mmAsub1_inNN0_imp)
QdivQinQ.add2(mmQdivQinQ_imp)
QexpN0inQ.add2(mmQexpN0inQ_imp)
MinQinQ.add2(mmMinA_in_QQd)
NxNinN.add01(mmNxNinN)
N0xN0inN0.add01(mmN0xN0inN0)
QxQinQ.add2(mmQxQinQ_imp)
IntRangecN.add2(mmIntRangecN)
MinCinC.add01(mmMinCinC)
ZxZinZ.add1(mmZxZinZ)
prove(N_N0inN) { (c, h) ->
val (a, b) = h
val s = A_B.mutation(c, a, b)
NxNinN.single(c, s10, a).result
N0pNinN.single(c, b, s.result.A).a(rotP).proveResult()
eqIn.mutation(c, s.origin, sNN, s.result, sNN).proveOrigin()
}
prove(N0_NinN) { (c, h) ->
val (a, b) = h
when (c.size) {
0 -> mmN0_NinN_i.call0(a, b)
else -> {
val s = A_B.mutation(c, a, b)
N0xN0inN0.call(c, s10, a)
N0pNinN.call(c, s.result.A, b)
eqIn.mutation(c, s.origin, sNN, s.result, sNN).proveOrigin()
}
}
}
}
--
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/0ec24187-2e3f-4693-9056-e0f957a96032%40googlegroups.com.
