Zulip Chat Archive

Stream: new members

Topic: tracing ring


view this post on Zulip Nathan Glenn (Jun 14 2020 at 11:22):

I'm working my way through tutorial 01_equality_rewriting.lean now. After watching Scott Morrison's "Infinitely Many Primes" video on YouTube, I was hoping that it would be simple to get traces for tactics like he shows for back? (which doesn't actually exist). I want to see the individual steps taken by the ring tactic. I tracked the core of ring down to simp_tactic.lean and tried to find trace options from there, but to no avail:

--- none of these options do what I want
set_option trace.simplify true
set_option trace.simp_lemmas true
set_option trace.algebra true
-- 0007
example (a b : ) : (a + b) + a = 2*a + b :=
begin
  ring, -- I want to trace this!
end

I'd like to be able to mouse over ring in VS Code and see the individual replacements done to solve the goal. I'd be okay with adding trace calls into my local copy of the core lean code, but I'm getting lost in it pretty quickly...

view this post on Zulip Johan Commelin (Jun 14 2020 at 11:34):

@Nathan Glenn It's not exactly what you want, but does

lemma foo : blabla := blabla

#print foo -- see the generated proof

help a bit?

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:35):

You can always try show_term { X }, where X is some tactic block.

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:36):

However many tactics, particularly ring will produce a giant non-human-readable mess.

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:36):

It is just not in the nature of decision procedure tactics to produce human readable accounts of their inner workings. :-)

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:36):

That said, there are plenty of other tactics that produces unpleasant to read terms, even just rw and simp.

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:38):

ring is not really something that you can "trace" in this sense, anyway. It goes off and does a bunch of unverified calculations, and then, knowing what it actually wants to prove, goes and proves that. It doesn't really "compile down to a list of invocations of simpler tactics".

view this post on Zulip Johan Commelin (Jun 14 2020 at 11:38):

I guess rw_search (once it's in mathlib) might give a readable trace in this example.

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:38):

tidy? does behave like this.

view this post on Zulip Scott Morrison (Jun 14 2020 at 11:39):

I'm not sure why when I sit down and think "ooh, what shall I do next?" I never seem to arrive at "work on getting rw_search merged".... :-(

view this post on Zulip Kevin Buzzard (Jun 14 2020 at 11:47):

@Nathan Glenn it's pretty clear how to prove anything which ring can do -- change all numerals to 1+1+...+1, expand out all brackets with mul_add and add_mul, do a bunch of applications of commutativity and associativity of + and *, sort out all the minus signs by multiplying them out and moving them to the other side of the equality, and after more commutativity and associativity you're done. It's not a mystery. This is in stark contrast to some of Scott's tactics, which are pooling ideas from a far wider collection of lemmas in the library

view this post on Zulip Nathan Glenn (Jun 14 2020 at 12:22):

Thanks, #print and show_term both work, although as indicated the output is not super human friendly.
I was doing exercise 0008, where you are supposed to not use the ring tactic just to see how tedious it was. I got stuck here:

-- 0008
example (a b : ) : (a + b)*(a - b) = a^2 - b^2 :=
begin
  repeat {rw pow_two},
    rw mul_sub (a + b) a b,
    repeat {rw add_mul},
    rw <- sub_sub,
    rw mul_comm b a,
    -- rw sub_self (a*b), -- doesn't match :(
    ring,-- shrug!
end

Of course, the answer is actually given above, but I couldn't quite follow how to apply the lemmas correctly. So my hope was to run ring and then copy it's strategy :D

view this post on Zulip Nathan Glenn (Jun 14 2020 at 12:24):

The goal at that point is a * a + a * b - a * b - b * b = a * a - b * b; I tried to apply sub_self, which is just a-a=0, but that failed to match. I guess because a*b - a*b is not in a parenthetical group?

view this post on Zulip Johan Commelin (Jun 14 2020 at 12:29):

I guess it would be nice to have set_option pp.parens true. (Maybe it even exists?)


Last updated: May 14 2021 at 03:27 UTC