## Stream: new members

### Topic: See tactic source code

#### Chris M (Jun 29 2020 at 08:39):

I'm doing the mathematics in lean tutorial. I'd like to see the source code that defines the tactic "ring", in the following code:

example : (c * b) * a = b * (a * c) :=
by ring


I'd like to understand what the ring tactic is doing internally (and similarly for other tactics), so is there a way to quickly look this up?

#### Johan Commelin (Jun 29 2020 at 08:41):

Look in src/tactic/ring in mathlib

#### Bryan Gin-ge Chen (Jun 29 2020 at 08:48):

If you're using VS Code, you should be able to right click and go to definition on most tactics.

got it! thanks

#### Mario Carneiro (Jun 29 2020 at 11:52):

Another thing you can do is look at the proof that ring generates. Even without reading the code, by looking at the proof you can get a pretty good idea of how it works. (You can use something like #explode to see the individual proof steps marked up)

#### Chris M (Jun 29 2020 at 15:05):

Mario Carneiro said:

Another thing you can do is look at the proof that ring generates. Even without reading the code, by looking at the proof you can get a pretty good idea of how it works. (You can use something like #explode to see the individual proof steps marked up)

Using #print theoremname you mean? This seems to generate the proof term but I'm not sure, because it's generating terms like tactic.ring.horner, which seem like tactic terms, not an actual proof term. The following code:

lemma test : (c * b) * a = b * (a * c) :=
by ring
#print test


Generates the following output:

theorem test : ∀ (a b c : ℝ), c * b * a = b * (a * c) :=
λ (a b c : ℝ),
(norm_num.subst_into_mul (c * b) a (tactic.ring.horner (tactic.ring.horner 1 b 1 0) c 1 0)
(tactic.ring.horner 1 a 1 0)
(tactic.ring.horner (tactic.ring.horner (tactic.ring.horner 1 a 1 0) b 1 0) c 1 0)
(norm_num.subst_into_mul c b (tactic.ring.horner 1 c 1 0) (tactic.ring.horner 1 b 1 0)
(tactic.ring.horner (tactic.ring.horner 1 b 1 0) c 1 0)
(tactic.ring.horner_atom c)
(tactic.ring.horner_atom b)
(tactic.ring.horner_mul_const 1 c 1 0 (tactic.ring.horner 1 b 1 0) (tactic.ring.horner 1 b 1 0) 0
(one_mul (tactic.ring.horner 1 b 1 0))
(zero_mul (tactic.ring.horner 1 b 1 0))))
(tactic.ring.horner_atom a)
(tactic.ring.horner_mul_const (tactic.ring.horner 1 b 1 0) c 1 0 (tactic.ring.horner 1 a 1 0)
(tactic.ring.horner (tactic.ring.horner 1 a 1 0) b 1 0)
0
(tactic.ring.horner_mul_const 1 b 1 0 (tactic.ring.horner 1 a 1 0) (tactic.ring.horner 1 a 1 0) 0
(one_mul (tactic.ring.horner 1 a 1 0))
(zero_mul (tactic.ring.horner 1 a 1 0)))
(zero_mul (tactic.ring.horner 1 a 1 0)))).trans
(norm_num.subst_into_mul b (a * c) (tactic.ring.horner 1 b 1 0)
(tactic.ring.horner (tactic.ring.horner 1 a 1 0) c 1 0)
(tactic.ring.horner (tactic.ring.horner (tactic.ring.horner 1 a 1 0) b 1 0) c 1 0)
(tactic.ring.horner_atom b)
(norm_num.subst_into_mul a c (tactic.ring.horner 1 a 1 0) (tactic.ring.horner 1 c 1 0)
(tactic.ring.horner (tactic.ring.horner 1 a 1 0) c 1 0)
(tactic.ring.horner_atom a)
(tactic.ring.horner_atom c)
(tactic.ring.horner_const_mul (tactic.ring.horner 1 a 1 0) 1 c 1 0 (tactic.ring.horner 1 a 1 0) 0
((mul_comm (tactic.ring.horner 1 a 1 0) 1).trans (one_mul (tactic.ring.horner 1 a 1 0)))
((mul_comm (tactic.ring.horner 1 a 1 0) 0).trans (zero_mul (tactic.ring.horner 1 a 1 0)))))
(tactic.ring.horner_const_mul (tactic.ring.horner 1 b 1 0) (tactic.ring.horner 1 a 1 0) c 1 0
(tactic.ring.horner (tactic.ring.horner 1 a 1 0) b 1 0)
0
(tactic.ring.horner_mul_const 1 b 1 0 (tactic.ring.horner 1 a 1 0) (tactic.ring.horner 1 a 1 0) 0
(one_mul (tactic.ring.horner 1 a 1 0))
(zero_mul (tactic.ring.horner 1 a 1 0)))
((mul_comm (tactic.ring.horner 1 b 1 0) 0).trans (zero_mul (tactic.ring.horner 1 b 1 0))))).symm


Is this something you would read and understand the point of?

#### Mario Carneiro (Jun 29 2020 at 15:22):

That's why I suggested #explode, it will show you step by step what is going on

#### Mario Carneiro (Jun 29 2020 at 15:23):

tactic.ring.horner is an actual term, you can look at the definition which is something like a * x ^ n + b

#### Mario Carneiro (Jun 29 2020 at 15:24):

I think you can add a notation for tactic.ring.horner to make it a bit nicer to look at

#### Mario Carneiro (Jun 29 2020 at 15:27):

import tactic
variables (a b c : ℤ)
notation [ a  *  b ^ c  +  d ] := tactic.ring.horner a b c d
lemma test : (c * b) * a = b * (a * c) :=
by ring
#print test
#explode test


#### Kevin Buzzard (Jun 29 2020 at 17:12):

Is this something you would read and understand the point of?

No -- tactics are not designed to make human-readable proofs.

#### Jalex Stark (Jun 29 2020 at 17:32):

this is why you should avoid using tactics to construct data --- the definition of a piece of data will get read by a human in the middle of a proof

Last updated: May 08 2021 at 04:14 UTC