import tactic
example (R : Type*) [comm_ring R] (a b c d : R) :
a + b + c + d = d + b + c + a :=
by ring
It takes about 50ms to parse, process, and type check this example, with the ring tactic running using some VM-compiled Lean code (in Lean 4, tactics will be compiled to native code).
The way the ring tactic works is that it puts both sides of the equality into some kind of normal form, and hopefully the normal forms are the same. And, honestly, even without the ring tactic, it's easy to use just the simplifier for this if you know the incantation: simp [add_assoc, add_left_comm, add_comm]. (The simplifier is not a simple piece of software, but it's built-in and it's able to run a rewrite system while being able to normalize things when the rewrites enter loops.)
To write CAS-like tactics, in principle "all you have to do" is write algorithms that simultaneously operate on expressions and construct proofs that the expressions represent what you need them to represent.
One example of this in mathlib is the norm_num tactic, which is supposed to take expressions involving numbers, operators, and other functions, then evaluate everything as far as possible. It's something like Mathematica's evaluator, though it only evaluates using rules specifically developed for norm_num. It turns out that norm_num, even though it is operating on expressions and constructing proofs the whole way, tends to be much faster than using kernel reductions (the gold standard for correctness). That's because it's able to use faster algorithms for various functions rather than the mathematically pristine ones, for example it does multiplication using a base-2 representation of a natural number rather than in terms of its unary representation, which is the definition for the natural numbers as an inductive type.
In fact, by using these sorts of tactics it's possible to calculate things that the kernel can't calculate itself. Here are some examples using top-level commands to invoke kernel reduction and the norm_num tactic:
#reduce 1000000 * 1000000
-- deep recursion was detected
#norm_num 1000000 * 1000000
-- 1000000000000
(This is something that lets you use Lean as a calculator with a "repl".)
Lean also has #eval to VM-compile an expression and evaluate it there, but what's interesting about #norm_num is that while evaluating it's also constructed a proof that the answer is correct. The VM compiler and VM are considered to be untrusted code, and they certainly have not been proved to be correct in any way.
Similar story in Isabelle/HOL - no special tactics required for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
by fastforce
Just for fun, I wrote up an equivalent but completely manual proof where every proof step consist of just one application of an existing fact - this is extremely verbose, but still quite short for this example:
lemma
fixes a :: "'a::comm_ring"
shows "a + b + c + d = d + b + c + a"
proof -
note assoc = ab_semigroup_add_class.add_ac(1)
have "a + b + c + d = a + (b + c + d)"
unfolding assoc[of a] by rule
also have "… = a + (d + (b + c))"
unfolding add.commute[of d "b + c"] by rule
also have "… = d + (b + c) + a"
unfolding add.commute[of a "d + (b + c)"] by rule
also have "… = d + b + c + a"
unfolding assoc by rule
finally show ?thesis .
qed
Here's a verbose Lean calc proof using single rewrites:
import tactic
example (R : Type*) [comm_ring R] (a b c d : R) :
a + b + c + d = d + b + c + a :=
calc a + b + c + d = a + b + (c + d) : by rw add_assoc
... = a + (b + (c + d)) : by rw add_assoc
... = b + (c + d) + a : by rw add_comm
... = c + d + b + a : by rw add_comm b
... = d + c + b + a : by rw add_comm c
... = d + (c + b) + a : by rw add_assoc d
... = d + (b + c) + a : by rw add_comm c
... = d + b + c + a : by rw ← add_assoc
(I didn't put any thought into trying to make it be efficient.)
The way the ring tactic works is that it puts both sides of the equality into some kind of normal form, and hopefully the normal forms are the same. And, honestly, even without the ring tactic, it's easy to use just the simplifier for this if you know the incantation: simp [add_assoc, add_left_comm, add_comm]. (The simplifier is not a simple piece of software, but it's built-in and it's able to run a rewrite system while being able to normalize things when the rewrites enter loops.)
To write CAS-like tactics, in principle "all you have to do" is write algorithms that simultaneously operate on expressions and construct proofs that the expressions represent what you need them to represent.
One example of this in mathlib is the norm_num tactic, which is supposed to take expressions involving numbers, operators, and other functions, then evaluate everything as far as possible. It's something like Mathematica's evaluator, though it only evaluates using rules specifically developed for norm_num. It turns out that norm_num, even though it is operating on expressions and constructing proofs the whole way, tends to be much faster than using kernel reductions (the gold standard for correctness). That's because it's able to use faster algorithms for various functions rather than the mathematically pristine ones, for example it does multiplication using a base-2 representation of a natural number rather than in terms of its unary representation, which is the definition for the natural numbers as an inductive type.
In fact, by using these sorts of tactics it's possible to calculate things that the kernel can't calculate itself. Here are some examples using top-level commands to invoke kernel reduction and the norm_num tactic:
(This is something that lets you use Lean as a calculator with a "repl".)Lean also has #eval to VM-compile an expression and evaluate it there, but what's interesting about #norm_num is that while evaluating it's also constructed a proof that the answer is correct. The VM compiler and VM are considered to be untrusted code, and they certainly have not been proved to be correct in any way.