I managed to pass the aforementioned (slightly changed) test
/** proving that ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. (
0 .. ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) */
val assertion = "( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s )
)".toAssertion("∨1c e. CC", "∨3c e. NN0")
val result = "( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )".toStatement()
val step = "|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0
... ∨3c ) ( ∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) )".toStatement()
val proof = assertion
.s(A_times_Sum) // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( 1 - ∨1c ) x. ( ∨1c ^ ∨2s ) )
.c(A_times_B_com) // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) x. ( 1 - ∨1c
) )
.c(A_times_BsubC) // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ( ∨1c ^ ∨2s ) x. 1 ) - (
( ∨1c ^ ∨2s ) x. ∨1c ) )
.eq(P.c.a.th(A_times_1), P.c.c.th(A_exp_Bplus1)) // sum_ ∨2s e. ( 0 .. ∨3c
) ( ( ∨1c ^ ∨2s ) - ( ∨1c ^ ( ∨2s + 1 ) ) )
.s(Sum_AsubB) // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨2s e. ( 0
.. ∨3c ) ( ∨1c ^ ( ∨2s + 1 ) ) )
.c(Sum_AplusB_in) { arrayOf("∨5s".toStatement(), statement1, "( ∨1c ^ ( (
∨5s - 1 ) + 1 ) )".toStatement()) } // ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s )
- sum_ ∨5s e. ( ( 0 + 1 ) .. ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 ) ) )
.eq(P.c.b.a.op(Engine::reduceAddition)) // ( sum_ ∨2s e. ( 0 ... ∨3c ) (
∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ( ∨5s - 1 ) + 1 )
.eq(P.c.c.c.th(AsubB_plus_C_rot)) // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^
∨2s ) - sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ( ∨5s - ( 1 - 1 ) ) )
.eq(P.c.c.op(Engine::reduce)) // ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s )
- sum_ ∨5s e. ( 1 ... ( ∨3c + 1 ) ) ( ∨1c ^ ∨5s ) )
.eq(P.a.th(firstA_plus_Sum_ofA) { arrayOf("( ∨1c ^ 0 )".toStatement()) },
P.c.th(Sum_ofA_plus_lastA) { arrayOf("( ∨1c ^ ( ∨3c + 1 ) )".toStatement()) })
// ( ( ( ∨1c ^ 0 ) + sum_ ∨2s e. ( ( 0 + 1 ) ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_
∨5s e. ( 1 ... ( ( ∨3c + 1 ) - 1 ) ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) )
.eq(P.a.a.op(Engine::reduce), P.a.c.b.op(Engine::reduce),
P.c.a.b.c.th(AplusB_sub_C_ass)) // ( ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^
∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ( ∨3c + ( 1 - 1 ) ) ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ (
∨3c + 1 ) ) ) )
.eq(P.c.a.b.c.op(Engine::reduce))// ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c
^ ∨2s ) ) - ( sum_ ∨5s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) )
)
.s(AplusB_sub_C_ass) // ( 1 + ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - (
sum_ ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ) )
.c(A_sub_BplusC_ass) // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) -
sum_ ∨5s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) )
.eq(P.c.a.c.th(Sum_AswitchB_in) { arrayOf("∨2s".toStatement(), "( ∨1c ^ ∨2s
)".toStatement()) }) // ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_
∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) )
.eq(P.c.op(Engine::reduce)) // ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )
/** done */
assertEquals(assertion.origin, proof.origin)
assertEquals(result, proof.result)
assertEquals(step, proof.step)
assertTrue(isProven(proof.step))
I had to improve a few parts of the system (including the part tracking in
what "closure" (NN0, NN, ZZ, QQ, RR, CC) things are)
and this test very efficiently showed places where things where lacking and
deserved a better handling.
Now, that I have a Mephistolus-Proof for a really interesting and high
level real world exercise,
I am going to work on
1) exporting Mephistolus-proofs to Metamath (this requires bootstrapping
Mephistolus theorems from Metamath ones)
2) write other Mephistolus-proofs for real world university level maths so
that I can test, debug and enhance progressively the system (hopefully,
writing them will become faster and faster).
This being said, I am quite happy with this result because, I posted 1 year
ago in this group to ask if the people there thought that it was possible to
do real maths, in a nice human friendly way, and I got my answer. It is
definately possible (but it requires quite a lot of man-month worth of work
to implement) .
The above test looks quite like real maths (especially if you consider that
the Mephistolus references for the used theorems will be set by users (with
sensible default) so that everyone can decently use stuff like A + B = B +
A with a label/id they like in their language.
But I think that it should be possible to slightly enhance the way the
proof is written further.
For example, when the last term of the sum is taken out, the system should
be able to compute what the value should be
So, there should be no need for specifying "( ∨1c ^ ( ∨3c + 1 ) )".
toStatement()
By only asking the user for values/parts that the system cannot compute,
should make things a lot easier for the human user.
Also, with some enhancements, the above proof can be shortened of a few
steps (only the important stuff should remain)
As I am not a mmj2 user, I was wondering how Mephistolus fares against mmj2.
How hard is it in mmj2 to write the above proof ? How many steps does it
require ?
Best regards ?
--
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/058bcb63-e3aa-4427-9bac-841536671850%40googlegroups.com.
