Let's make this the Thread about Mephistolus (it'll help prevent me
spamming the metamath group).
I'll report the Mephistolus progress in here and maybee also, post stuff
about it's internals and design decisions
( and ask a lot of help for metamath experts when I'm at a loss, I'll be
in you gentle care :))
Milestone 5 has been reached, with the first Mephistolus-proof exported and
proof checked in Metamath for an exercise I give to my students (now only
400+ more to go :) ) :
|- ( ∨1c e. CC -> ( ∨3c e. NN0 -> ( ( 1 - ∨1c ) x. sum_ ∨2s e. ( 0 ... ∨3c ) (
∨1c ^ ∨2s ) ) = ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) ) ) )
Here is the high level human proof :
/** 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 )
)".toSingle("∨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 i = "∨2s".toStatement()
val j = dummy(MType.S, assertion.origin, *assertion.context.toTypedArray())
val proof = assertion
.s(AxSum)
/*.s(A_times_Sum)*/ // sum_ ∨2s e. ( 0 .. ∨3c ) ( ( 1 - ∨1c ) x.
( ∨1c ^ ∨2s ) )
.c(rotX)
// sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ∨1c ^ ∨2s ) x. ( 1 - ∨1c ) )
.c(Ax_BsubC)
// sum_ ∨2s e. ( 0 .. ∨3c ) ( ( ( ∨1c ^ ∨2s ) x. 1 ) - ( ( ∨1c ^
∨2s ) x. ∨1c ) )
.eq(P.c.a.th(Ax1), P.c.c.th(Aexp_Bp1))
// 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_CDI) { arrayOf(j, statement1, "( ∨1c ^ ( ( $j - 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.mut(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(rotSubP))
// ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1
... ( ∨3c + 1 ) ) ( ∨1c ^ ( ∨5s - ( 1 - 1 ) ) )
.eq(P.c.c.mut(Engine::reduce))
// ( sum_ ∨2s e. ( 0 ... ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨5s e. ( 1
... ( ∨3c + 1 ) ) ( ∨1c ^ ∨5s ) )
.eq(P.a.th(ApSumA) { arrayOf("( ∨1c ^ 0 )".toStatement()) },
P.c.th(SumA_pA) { 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.mut(Engine::reduce), P.a.c.b.mut(Engine::reduce),
P.c.a.b.c.th(rotPSub)) // ( ( 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.mut(Engine::reduce))
// ( 1 + sum_ ∨2s e. ( 1 ... ∨3c ) ( ∨1c ^ ∨2s ) ) - ( sum_ ∨5s
e. ( 1 ... ∨3c ) ( ∨1c ^ ∨5s ) + ( ∨1c ^ ( ∨3c + 1 ) ) ) )
.s(rotPSub)
// ( 1 + ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - ( sum_ ∨5s e.
( 1 .. ∨3c ) ( ∨1c ^ ∨5s ) ) + ( ∨1c ^ ( ∨3c + 1 ) ) )
.c(rotSubSub)
// ( 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_CDV) { arrayOf(i, "( ∨1c ^ $i )".toStatement()) })
// ( 1 + ( ( sum_ ∨2s e. ( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) - sum_ ∨2s e.
( 1 .. ∨3c ) ( ∨1c ^ ∨2s ) ) - ( ∨1c ^ ( ∨3c + 1 ) ) )
.eq(P.c.mut(Engine::reduce))
// ( 1 + -u ( ∨1c ^ ( ∨3c + 1 ) ) )
/** done */
Here are the goals for Milestone 6 (let's make Mephistolus a concrete goal
driven development, instead of a feature driven development) :
context("Exo 2.7") {
it("a") {
val s = "sum_ ∨2s e. ( 1 ... ( ∨1c - 1 ) ) ( ( 5 x. ( 3 ^ -u ∨2s ) ) -
( 4 x. ( 2 ^ ( ( 2 x. ∨2s ) - 1 ) ) ) )".toSingle("∨1c e. NN")
}
it("b") {
val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( 1 / 4 ) ^ ( 2 x. ∨2s ) )
)".toSingle("∨1c e. NN0")
}
it("c") {
val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ( ( ( ( ∨1c ^ 2 ) x. ∨2s ) + ( ∨1c
x. ( ∨2s ^ 2 ) ) ) - ( 3 x. ( ∨2s ^ 3 ) ) ) / ( ∨1c ^ 4 ) )".toSingle("∨1c e.
NN0")
}
it("d") {
val s = "sum_ ∨2s e. ( 0 ... ∨1c ) ( ( ( ( ∨2s x. ( ∨2s - 1 ) ) x. ( 3
^ ∨2s ) ) - ( 5 ^ ( ∨2s - 1 ) ) ) / ( 3 ^ ∨2s ) )".toSingle("∨1c e. NN0")
}
it("e") {
val s = "sum_ ∨2s e. ( 0 ... ( ( 2 x. ∨1c ) - 1 ) ) ( 5 / ( 6 ^ ( ∨2s -
1 ) ) )".toSingle("∨1c e. NN0")
}
}
context("Exo 2.10") {
it("1 (induction)") {
val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s ) ) = ( ( ! ` (
∨2s + 1 ) ) - 1 )".toSingle("∨1c e. NN")
}
it("2 (telescopic sums)") {
val s = "sum_ ∨2s e. ( 1 ... ∨1c ) ( ∨2s x. ( ! ` ∨2s )
)".toSingle("∨1c e. NN")
}
}
Milestone 6 will be reached with 2 other real world proofs involving only
sums (say Exo2.7a and Exo 2.7b) and for 1 real world proof by induction
(say Exo 2.10.1)
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/3c43167b-f7ad-4eff-b90e-a75460fd5862%40googlegroups.com.
