seeing what a tactic did

Stream: general

[Matthew Pocock]

In the vs code view, it highlights parts of things touched by a tactic like simp, but I can't see way to see what the tactic actually did. Presumably simp or ring or whatever actually constructed some expression, which perform a series of rewrites. Is it possible to visualise these rewrites and/or the proofs that it used within the right-hand pannel?

[Anatole Dedecker]

Do you know about show_term?

[Damiano Testa]

You can use show_term [tactic] and it will display the term that the tactic created. However, as soon as there are rewrites, the output is fairly cluttered and rarely useful.

[Damiano Testa]

If you know what lemma you are looking for, show_term on some tactics can help. Specifically with simp, I would say that simp? is far superior to show_term and almost never worse.

[Kevin Buzzard]

Both simp and ring will produce disgusting terms -- they are high-powered tactics. simp is doing lots of rw, and rw is doing very clever application of Eq.rec with some appropriate motive. ring is much worse, it puts everything into some "Horner normal form": the actual term underlying a proof of $(x+y)^2=x^2+2xy+y^2$ is too big to post in Zulip.

[Damiano Testa]

Also, the idea of show_term is that you could replace the tactic with the given term, but, except for the most transparent tactics, the round-tripping almost never works.

[Kevin Buzzard]

import Mathlib.Tactic

example (x y : ℤ) : (x+y)^2=x^2+2*x*y+y^2 := by show_term ring
/-
Try this: exact Mathlib.Tactic.Ring.of_eq
  (Mathlib.Tactic.Ring.pow_congr
    (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf x) (Mathlib.Tactic.Ring.atom_pf y)
      (Mathlib.Tactic.Ring.add_pf_add_lt (x ^ Nat.rawCast 1 * Nat.rawCast 1)
        (Mathlib.Tactic.Ring.add_pf_zero_add (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0))))
    (Mathlib.Tactic.Ring.cast_pos (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)))
    (Mathlib.Tactic.Ring.pow_add
      (Mathlib.Tactic.Ring.pow_nat (Mathlib.Tactic.Ring.coeff_one 2)
        (Mathlib.Tactic.Ring.pow_one_cast (x ^ Nat.rawCast 1 * Nat.rawCast 1 + (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
        (Mathlib.Tactic.Ring.pow_bit0
          (Mathlib.Tactic.Ring.pow_one (x ^ Nat.rawCast 1 * Nat.rawCast 1 + (y ^ Nat.rawCast 1 * Nat.rawCast 1 + 0)))
          (Mathlib.Tactic.Ring.add_mul
            (Mathlib.Tactic.Ring.mul_add
              (Mathlib.Tactic.Ring.mul_pp_pf_overlap x
                (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                  (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1)
                    (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2)))
                (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
              (Mathlib.Tactic.Ring.mul_add
                (Mathlib.Tactic.Ring.mul_pf_left x (Nat.rawCast 1)
                  (Mathlib.Tactic.Ring.mul_pf_right y (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
                (Mathlib.Tactic.Ring.mul_zero (x ^ Nat.rawCast 1 * Nat.rawCast 1))
                (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 1 * (y ^ Nat.rawCast 1 * Nat.rawCast 1) + 0)))
              (Mathlib.Tactic.Ring.add_pf_add_gt (x ^ Nat.rawCast 1 * (y ^ Nat.rawCast 1 * Nat.rawCast 1))
                (Mathlib.Tactic.Ring.add_pf_add_zero (x ^ Nat.rawCast 2 * Nat.rawCast 1 + 0))))
            (Mathlib.Tactic.Ring.add_mul
              (Mathlib.Tactic.Ring.mul_add
                (Mathlib.Tactic.Ring.mul_pf_right x (Nat.rawCast 1)
                  (Mathlib.Tactic.Ring.mul_pf_left y (Nat.rawCast 1) (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1))))
                (Mathlib.Tactic.Ring.mul_add
                  (Mathlib.Tactic.Ring.mul_pp_pf_overlap y
                    (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                      (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1)
                        (Mathlib.Meta.NormNum.IsNat.of_raw ℕ 1) (Eq.refl 2)))
                    (Mathlib.Tactic.Ring.one_mul (Nat.rawCast 1)))
                  (Mathlib.Tactic.Ring.mul_zero (y ^ Nat.rawCast 1 * Nat.rawCast 1))
                  (Mathlib.Tactic.Ring.add_pf_add_zero (y ^ Nat.rawCast 2 * Nat.rawCast 1 + 0)))
                (Mathlib.Tactic.Ring.add_pf_add_lt (x ^ Nat.rawCast 1 * (y ^ Nat.rawCast 1 * Nat.rawCast 1))
[90 or so more lines omitted]

[Matthew Pocock]

OK, so yeah the tactic-generated code I'm looking at is horrific. It may be informative if it could display a list, or a tree of transformed terms?

[Kevin Buzzard]

I'm not sure that this tree of transformed terms is ever generated by Lean.

[Damiano Testa]

I doubt that even that would be much more helpful: proof terms found automatically tend to be really unwieldy.

[Kevin Buzzard]

These tactics are not written with readable proof terms in mind. The reason is: what do you care as a human about how a computer is proving $(x+y)^2=x^2+2xy+y^2$? The paper proof is obvious, it doesn't matter what the machine is doing.

[Damiano Testa]

Also, keep in mind that probably also the actual target that you are looking at pretty-printed is probably completely unusable, if you inspect it with set_option pp.all true.

[Matthew Pocock]

That's a little sad - I was hoping to learn something about how to construct proofs by looking at them.

[Damiano Testa]

To me, looking at proof terms seems the wrong way to approach the problem...

[Kevin Buzzard]

Even a simple thing like changing an x to a y in the middle of a complex term under the hypothesis that x=y will be some horrific thing in Lean's type theory. The way to construct a proof of anything other than the most trivial thing is to use tactics. The underlying type theory is just an implementation detail.

[Damiano Testa]

If you look at the term-mode proofs in mathlib, you will find that they are typically really short, and often you can see that their equivalent tactic-mode was a chain of intro and refine.

[Kevin Buzzard]

The important thing is to have some kind of understanding that the type theory is capable of doing the mathematical "move" that you want to do. How it's doing it is only of interest if you are researching the foundations. For example it's useful to understand that the rw tactic can in theory exist, by examining the type of Eq.rec and seeing that it does precisely the concept of "substituting in". And it's useful to understand that you can compose tactics; this corresponds to composing functions. But looking at the details is like writing some python code, compiling to C or assembly, and then looking at the C/assembly code and expecting to get some insight into "how python works".

[Matthew Pocock]

Kevin Buzzard said:

But looking at the details is like writing some python code, compiling to C or assembly, and then looking at the C/assembly code and expecting to get some insight into "how python works".

I feel personally called out -- I have spent literally months doing this Rust to assembly.

[Damiano Testa]

... and what was the conclusion?

[Kevin Buzzard]

Heh, well whether you want to look at the actual term probably depends on what your interests are. I'm a mathematician with no interest in foundations; I once took a class which taught me they existed, and I convinced myself that they were strong enough to be able to do the mathematics I was interested in, and then I never looked back. Here's two ways of understanding how simp is doing something really simple:

import Mathlib.Tactic

example (x : ℤ) : x + 0 * 1 + 0 * 1 = x := by show_term simp
/-
Try this: exact of_eq_true
  (Eq.trans
    (congrFun
      (congrArg Eq
        (Eq.trans (congr (congrArg HAdd.hAdd (Eq.trans (congrArg (HAdd.hAdd x) (mul_one 0)) (add_zero x))) (mul_one 0))
          (add_zero x)))
      x)
    (eq_self x))
-/
example (x : ℤ) : x + 0 * 1 + 0 * 1 = x := by simp?
-- Try this: simp only [mul_one, add_zero]

and the second one is helpful ("oh, I see that actually continually rewriting those lemmas will work") but the first one just looks like a bunch of random noise to me and gives me much less information, other than the fact that I knew already which is that primitive operations like Eq.trans can be used to put arguments together etc.

[Matthew Pocock]

Damiano Testa said:

... and what was the conclusion?

It's a bit OT here, but I learned that modern x86 family chips are exceedingly good at referring to data by pointer, especially if you can limit gotos, so much so that I could often get a 30-50% speed improvement not caching values in a register. I think it gives the chip more freedom to compile it down from the assembly to whatever the chip actually does, and frees up its data fetch pipeline.

[Damiano Testa]

Ok, without knowing anything about Rust or assembly, is it fair to summarize that you learned more about assembly than about Rust? I would say that exploring proof terms would gain you a knowledge of terms, not of proofs.

[Matthew Pocock]

Damiano Testa said:

Ok, without knowing anything about Rust or assembly, is it fair to summarize that you learned more about assembly than about Rust? I would say that exploring proof terms would gain you a knowledge of terms, not of proofs.

That's probably fair -- I was learning how to write highly speed-optimized rust but yes, I learned mainly about what modern CPUs like to eat. I'm only a week old in lean, so the difference between terms and proofs and tactics is still a bit hazy to me in practice.

[Kevin Buzzard]

I think that this thread shows you really clearly what the difference is. A proof is a mathematical idea, mathematically trivial proofs can be realised directly as terms but the moment you're doing anything nontrivial you can use tactics to manipulate and generate terms in ways where the underlying concepts are human-understandable but the terms themselves might be pretty nasty in the actual type theory.

[Damiano Testa]

I would say that looking at one or two layers inside can be beneficial, so knowing something about proof terms can be helpful for constructing proofs. However, looking very deeply inside them will likely not give too much understanding of higher level arguments. Maybe it is a little like trying to read a poem, where you only have access to the coordinates of the pixels that make up its words: the information is there, but it is presented in a very inconvenient way!

[Kevin Buzzard]

You might find the first few chapters of #tpil of interest. This goes through a whole bunch of mathematically completely trivial stuff showing how to make terms corresponding to the proofs.

[Matthew Pocock]

Kevin Buzzard said:

You might find the first few chapters of #tpil of interest.

Yeah - I did that book on Wednesday/Thursday. The exercise were really fun.

[Kevin Buzzard]

People with a computer science background tend to really appreciate Theorem Proving In Lean. I was kind of intrigued by it, writing these spaghetti terms to prove things like associativity of \and -- and then I got to the chapter about tactics and was like "wtf? why didn't they tell me this before? I've been wasting my time!". The natural number game is written for mathematicians, and it doesn't explain terms at all, I just start by introducing tactics right from the start, and it's basically impossible to exit tactic mode in that game. I think my vehemently anti-term opinion just comes from the fact that I know that for any mathemtical question I'm interested in, the underlying term for a proof will be incomprehensible to a human so why bother even looking at it. But if you are only interested in trivial statements (perhaps because you are interested in implementation details) then perhaps the terms will be more enlightening.

[Matthew Pocock]

I totally get the cultural difference. At the moment I'm just wasting time playing with the collatz conjecture to keep my brain active, and I quickly realised that without some mechanical assistance that I couldn't trust myself. I am definitely not a mathematician.

[Kevin Buzzard]

More philosophically, if I am formalising a mathematical proof in Lean then I already understand the proof (if I didn't know how to prove it then I certainly wouldn't be trying to figure it out using Lean -- I'd be using pencil and paper). Tactics are a far more appropriate language for translating the mathematical argument in my head into a Lean proof, and the term can't teach me anything because I already understand the proof and the term is probably gobbledegook anyway.

[Kevin Buzzard]

My understanding is that there are people using homotopy type theory provers who really do use ITPs as an experimental tool for research, perhaps because the questions they're interested in involve keeping track of higher types (i.e. infinity groupoids) and then the ITP does actually help with keeping track of what's going on. But for classical mathematics of the type we're developing in mathlib, paper and pencil is still king, and will remain so for a while I think.

[Alex Kontorovich]

I'm actually hoping that mathlib eventually gets good enough that it can indeed be used for real-time research, not just when you're done understanding the math. Certainly when I'm writing some god-awful 100 page analytic number theory paper with 30 parameters that need to be carefully balanced at the end for it all to work out, I wish there was a more robust mechanism for keeping it all straight than merely relying on my brain and reams of paper...

[Kevin Buzzard]

Maybe at some point in the future there will be a crossover; I would not like to conjecture when it will happen, and it might happen at different times for different subject areas in mathematics.

[Matthew Pocock]

What does it mean for it to help you do research rather than to document what you've already researched? Is it that it offers suggestions about what you could explore next? Or visualisation tools? I don't really know.

[Matthew Pocock]

Mind, I don't really know what research is in maths. I'm a biologist.

[Bolton Bailey]

I recently found myself getting confused by a strange idea I had relating to the random oracle model (the random oracle model is a technique in cryptography which assumes a particular function being used in a cryptographic protocol is drawn uniformly at random from the space of all functions of a given type). I eventually resorted to trying to work it out in lean notation (even though I was writing in a google doc). I wonder if I would have had more success actually using a lean environment.

[Bolton Bailey]

In this case, the issue was that there were two instantiations of the ROM at play, and I hoped that explicitly writing down what functions were calling what would help me keep track of the distinctions.

[Bolton Bailey]

I have also found lean helpful for understanding Löb's theorem in the past.

[Bolton Bailey]

Kevin Buzzard said:

Maybe at some point in the future there will be a crossover; I would not like to conjecture when it will happen, and it might happen at different times for different subject areas in mathematics.

I agree with this and with the sentiment that this crossover will probably come sooner for field more closely related to logic.

[Jireh Loreaux]

@Alex Kontorovich without any more information about specifics, it seems to me like you might actually be able to have Lean help you with that task. At least, you could outline parts of the proof with sorry and axiomatize things we don't have in mathlib. You could verify select portions of the proof. It would be the same as a full formalization, but it could help you with organization and keeping track of balancing quantities. On the other hand, perhaps I'm just misunderstanding your actual situation and it's not really feasible.

[Joachim Breitner]

I thought I saw someone demo a tactic that synthesizes calc proofs from simp (or from rw or proof terms)? Or maybe I was dreaming, but maybe it's possible, at least for common cases?

[Henrik Böving]

Matthew Pocock said:

Damiano Testa said:

Ok, without knowing anything about Rust or assembly, is it fair to summarize that you learned more about assembly than about Rust? I would say that exploring proof terms would gain you a knowledge of terms, not of proofs.

That's probably fair -- I was learning how to write highly speed-optimized rust but yes, I learned mainly about what modern CPUs like to eat. I'm only a week old in lean, so the difference between terms and proofs and tactics is still a bit hazy to me in practice.

Tactics are the things that you use to produce a certificate (in the form of a term) that you have indeed a proof of something. The reason that both tactics and terms exist is because we want Lean to have a minimal piece of software (the kernel) that only has to check these certificates in order to verify that you indeed have a proof. This is useful because we can extend the tools that produce these terms with arbitrary algorithms without having to trust them as we have a minimal core to check their output. If you wish to understand how the proof terms are generated it is much more useful to read the implementation of the tactics than the proof terms themselves. That said meta programming is a rather advanced topic so you might want to get comfortable with Lean as a theorem prover and programming language before venturing that way.

[Henrik Böving]

Kevin Buzzard said:

My understanding is that there are people using homotopy type theory provers who really do use ITPs as an experimental tool for research, perhaps because the questions they're interested in involve keeping track of higher types (i.e. infinity groupoids) and then the ITP does actually help with keeping track of what's going on. But for classical mathematics of the type we're developing in mathlib, paper and pencil is still king, and will remain so for a while I think.

I've read that Emily Riehl is using rzk (https://github.com/rzk-lang/rzk) for her research although rzk seems very custom tailored to a specific mathematical field (as far as I can tell as an outsider to both rzk and non-functional-programming-category-theory) as opposed to Lean/mathlib

[Kevin Buzzard]

Right but she is doing mathematics where the basic object out of which everything is built is the infinity groupoid (which mathematicians struggled with a definition of for decades), whereas in mathlib the basic object is the set level type (which is trivial to understand -- it's just a collection of terms).

[Kevin Buzzard]

Once you have decided that the basic object of study is this fantastically complicated thing, then the kinds of questions you want to think about change completely, e.g. groups are boring and arguably not even the right objects to study, because group theory does not play well with this higher type structure; a group is a set-level object.

[Kevin Buzzard]

so all the questions you have now involve morphisms and morphisms between morphisms and morphisms between these things and... , and now you can imagine that having a theorem prover keeping track of all this infinite amount of data is really useful! Because every object looks like this.

[Kevin Buzzard]

You could say that the fact that x = y is a subsingleton in Lean means that Lean's types are "lower types" whereas in a univalent theory (where this is not the case) you study "higher types" and things get super-complicated very quickly.

[Mario Carneiro]

Kevin Buzzard said:

These tactics are not written with readable proof terms in mind. The reason is: what do you care as a human about how a computer is proving $(x+y)^2=x^2+2xy+y^2$? The paper proof is obvious, it doesn't matter what the machine is doing.

Actually, it may surprise you to know that ring is designed to produce readable (or at least straightforward) proof terms. The thing is, it's not the proof expression itself you should be reading but rather the sequence of subgoals produced, i.e. using #explode to view the proof. (You might also need to use some notations to hide things like rawCast which would normally be displayed as just ↑.)

[Mario Carneiro]

Matthew Pocock said:

Damiano Testa said:

Ok, without knowing anything about Rust or assembly, is it fair to summarize that you learned more about assembly than about Rust? I would say that exploring proof terms would gain you a knowledge of terms, not of proofs.

That's probably fair -- I was learning how to write highly speed-optimized rust but yes, I learned mainly about what modern CPUs like to eat. I'm only a week old in lean, so the difference between terms and proofs and tactics is still a bit hazy to me in practice.

Put another way, ring is designed to produce terms that the kernel likes to eat. This means it has very simple defeq problems (essentially syntactic only), a minimum of rewriting steps like Eq.trans or congrFun like you see in simp, and yet it does not optimize the names of lemmas because these are stored once and reused as many times as necessary, so they are essentially free (although big namespaced names contribute a lot to the "busy-ness" of the output of ring; opening the relevant namespace helps a lot)

[Matthew Pocock]

Mario Carneiro said:

but rather the sequence of subgoals produced, i.e. using #explode to view the proof.

I think #explode may have been what I was hoping for all-along :D Thank you for this.

[Alex Kontorovich]

Jireh Loreaux said:

Alex Kontorovich without any more information about specifics, it seems to me like you might actually be able to have Lean help you with that task. At least, you could outline parts of the proof with sorry and axiomatize things we don't have in mathlib. You could verify select portions of the proof. It would be the same as a full formalization, but it could help you with organization and keeping track of balancing quantities. On the other hand, perhaps I'm just misunderstanding your actual situation and it's not really feasible.

Indeed, I had a student look into formalizing the "formalizable" parts of a recent (long) paper of mine, with sorrys at the parts that involved objects not in mathlib; but for now, even that is still too hard and we gave up. Once that's possible without too much difficulty, I can foresee being able to write such little lemmata up as I work, so I don't have to go back and recheck if it's really true, in the process of scrambling to some other part of the proof...

[Mario Carneiro]

Here's a cleaned up version of Kevin's example:

import Mathlib.Tactic

namespace Mathlib.Tactic.Ring
open Meta.NormNum Lean PrettyPrinter.Delaborator SubExpr
@[delab app.Nat.rawCast]
def delabNatCast : Delab := do
  let e ← getExpr
  guard $ e.isAppOfArity' ``Nat.rawCast 3
  withNaryArg 2 delab

theorem T (x y : ℤ): (x+y)^2=x^2+2*x*y+y^2 := by ring
#explode T