Hello
I have just broken through the second milestone in the development for a
CAS system over Metamath (or MM0).
Basically, now it can do this
"sum_ ∨1s e. ( 1 ... 5 ) ∨1s".test("; 1 5")
"sum_ ∨1s e. ( 1 ... 5 ) ( ( 2 x. ∨1s ) + 1 )".test("; 3 5")
"sum_ ∨1s e. ( 1 ... 9 ) ( ∨1s ^ 2 )".test("; ; 2 8 5")
"sum_ ∨1s e. ( 1 ... 4 ) ( ( 1 / 2 ) ^ ∨1s )".test("( ; 1 5 / ; 1 6 )")
where test just applies a "reduce" method on the left term and checks that
it leads to the second term (and proofs it)
More generally, the nice API of Milestone 1 evolved to be able to handle
statements with antecedents.
Basically, through the M2 API, you can :
1) take any statement like "A. v1s e. ZZ 0 < ( v1s ^ 2)"
2) apply some (or many) change like NN C_ ZZ
3) you get the statement "A. v1s e. NN 0 < ( v1s ^ 2)"
AND you have proved that |- ( A. v1s e. ZZ 0 < ( v1s ^ 2) -> A. v1s e. NN 0
< ( v1s ^ 2) )
EVEN if it has antecedents, it should handle those just fine (or if it
still doesn't I'll fix it and it will)
For example, this test just does that (it also adds antecedents to see if
it works with those)
"A. ∨1s e. ZZ 0 <_ ( ∨1s ^ 2 )".impTest("A. ∨1s e. NN 0 <_ ( ∨1s ^ 2 )") {
it.imp(P.b + "|- NN C_ ZZ") }
But basically, what a developer needs to do steps 1, 2, 3 requires only 1
line of code which is
"A. ∨1s e. ZZ 0 <_ ( ∨1s ^ 2 )".toAssertion().imp(P.b + "|- NN C_ ZZ")
P.b tells the node of the statement where the change should happend
|- NN C_ ZZ tells the code, what (proved) changed should be used to
transform the statement
And the code does the necessary to get the result AND the proof of the
transformation
Basically, you point to the place where you want to change something and
you give the system the tiny step you want to apply
the system figures out if you get a ->, a <- or a <-> for the transformation
(you use eq for <->, imp for -> and limp for <- if you want the sytem to
check that you get the result that you expect)
some other examples (in test form)
"( ( 1 + 2 ) = 3 /\\ ( 2 + 3 ) = 5 )".eqTest("( 3 = 3 /\\ 5 = 5 )") {
it.eq4(P.a.a * add(1, 2), P.b.a * add(2, 3)) }
assume("( ∨3w -> ( ∨6w -> ∨4w ) )")
assume("( ( ∨3w -> ∨6w ) -> ( ∨5w <-> ∨5w ) )")
"( ( ∨3w -> ∨4w ) -> ∨5w )".impTest("( ( ∨3w -> ∨6w ) -> ∨5w )") { it.imp(P.a.b
+ "( ∨6w -> ∨4w )") }
"-. 3 < 1".limpTest("-. 3 < 2") { it.limp(P.a.c + "|- 1 < 2") }
applying a theorem is quite simple as the system is usually able to infer
most arguments, from the statement and the place where you want to apply it
Like applying ( a * c / b * c ) = ( a / b) requires
- nothing if you apply it on ( 2 * 3 / 5 * 3 ) -> a = 2, c = 3, b = 5
- requires 1 argument if you apply it on ( 2 / 5) -> a= 2, b = 5 but what
do you want to take for c ?
The Api and the services that make it work (checking in which set,
statements are, checking that something is =/= 0, ...)
work quite nicely and make me think that I'll be able to provide a nice
user experiment doing maths through metamath,
especially since it will be possible to code a nice UI that makes things
simpler for the user (like providing suggestions of steps, theorems to
apply, ...)
I have not decided yet on what I want to work next.
My options are :
A) export proofs to metamath
B) research sequences and functions
C) try to write some simple and useful proofs
D) Improve the work already done on rationals, sums (like enable changing
the set variable used in sums...)
E) working on real and complex stuff, this requires more than reducing
(like factoring, developping, grouping...)
I think that it would be a waste to do A before C but I fear that I won't
find simple and usefull proofs before I do B
In order to develop the system further, I would really love to have some
(simple) target theorems that it should be able to prove.
Could someone, please, suggest me some simple theorems I could aim to prove
with my code ?
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/b9ca1a76-e5e8-4d7d-a29b-3e7d5577a8ed%40googlegroups.com.
