# Zulip Chat Archive

## 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.

#### Chris M (Jun 29 2020 at 09:24):

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