tracing ring

Stream: new members

[Nathan Glenn]

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

[Johan Commelin]

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

lemma foo : blabla := blabla

#print foo -- see the generated proof

help a bit?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

tidy? does behave like this.

[Scott Morrison]

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".... :-(

[Kevin Buzzard]

@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

[Nathan Glenn]

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

[Nathan Glenn]

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?

[Johan Commelin]

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