Mephistolus (milestone 4)

[Olivier Binda]

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()
            }
        }
    }
}