Have you thought about providing a limited release, or a recording of you using the program? It's not really clear to me what the overall program is, and you post snippets that lack the context to make sense of them (I don't think you are expecting people to run them, but I don't even know what language they are written in). Is this the end user experience or is there some GUI front end? The code snippets on their own only provide a myopic view into the development process.
I know you want to ultimately sell this program, and I don't want to make you do anything to compromise that, but you might get more and better feedback if you provide a more comprehensive overview of what the program is. Mario On Tue, Nov 19, 2019 at 3:23 AM Olivier Binda <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/3c43167b-f7ad-4eff-b90e-a75460fd5862%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJStHoGFF4JBX801gHqkpSjrs0cR_2Q1TyPaq2jYWn%2BSRbA%40mail.gmail.com.
