I went for step C. I'm not very good at explaining what I want to achieve
but I may succeed with the following example.
I want to build a system (probably named "Mephistolus") that makes it easy
for humans (math students) to compute expressions and write computer
checked maths proofs
Here is my first go at writing a simple and useful proof (inspired by a
basic exercise I give to my 1st year students)
proving that ( A e. CC -> ( C e. NN0 -> ( ( 1 - A ) x. sum_ k e. ( 0 .. ∨C
) ( A ^ k ) ) = ( 1 - ( A ^ ( C + 1 ) ) ) ) )
// the comment are only here to help follow the computations and get what
the theorems do
/** proving that ( A e. CC -> ( C e. NN0 -> ( ( 1 - A ) x. sum_ k e. ( 0 .. ∨C
) ( A ^ k ) ) = ( 1 - ( A ^ ( C + 1 ) ) ) ) )
* or with A=v1c, C=v3c, k=v2s
* ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 .. ∨3c ) (
∨1c ^ ∨2s ) ) = ( 1 - ( ∨1c ^ ( ∨3c + 1 ) ) ) ) ) */
"( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) )".toAssertion("∨1c e.
CC", "∨2c e. NN0")
.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)).s(Sum_AsubB)
// 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) }
// ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( ( 0 + 1 ) .. (
∨3c + 1 ) ) ( ∨1c ^ ∨5s ) )
.eq(Change4(P.c.b.a, Engine::reduceAddition))
// ( sum_ ∨2s e. ( 0 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( ( 1 .. ( ∨3c +
1 ) ) ( ∨1c ^ ∨5s ) )
.eq(P.a.th(firstA_plus_Sum_ofA), P.c.th(Sum_ofA_plus_lastA))
// ( ( ( ∨1c ^ 0 ) + sum_ ∨2s e. ( ( 0 + 1 ) .. ∨3c ) ( ∨1c ^ ∨2s ) ) - (
sum_ ∨5s e. ( ( 1 .. ( ( ∨3c + 1 ) - 1 ) ) ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c +
1 ) ))
.eq(Change4(P.a.a, Engine::reduce), Change4(P.a.c.b, Engine::reduce),
P.c.b.c.th(A_plus_B_sub_C_ass))
// ( ( 1 + sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s e. ( ( 1
.. ( ∨3c + ( 1 - 1 ) ) ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ))
.eq(Change4(P.c.b.c, Engine::reduce))
// ( ( 1 + sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s e. ( 1 ..
∨3c ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ) )
.s(A_plus_B_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(Change4(P.c, Engine::reduce))
// ( 1 - ( ∨1c ^ ( ∨3c + 1 ) ) )
/** done */
Next, I'll try to make this test pass (I haven't run it yet)
And when it runs, I'll start working on step A (export of the Mephistolus
proofs to Metamath proofs).
That way, it won't just be vapourware and it'll maybee start being useful
to some people
Best regards,
Olivier
--
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/78712324-293e-4ec4-a714-ad72aece54c6%40googlegroups.com.
