See tactic source code

Stream: new members

[Chris M]

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]

Look in src/tactic/ring in mathlib

[Bryan Gin-ge Chen]

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

[Chris M]

got it! thanks

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

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

[Jalex Stark]

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