Zulip Chat Archive

Stream: new members

Topic: See tactic source code


view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jun 29 2020 at 08:41):

Look in src/tactic/ring in mathlib

view this post on Zulip 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.

view this post on Zulip Chris M (Jun 29 2020 at 09:24):

got it! thanks

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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