how do I step through proofs?

Stream: general

[Dan Abolafia]

I want to be able to step through the type checker on a proof the same way I could step through the execution of a program in a debugger. When reading a proof on paper, there is uncertainty about what exactly is going on and the meaning of symbols. In principle, the benefit of computer proofs is that this ambiguity goes away. I've been trying to understand the proofs in mathlib. For instance, the proof that sqrt(2) is irrational, and the proof that the reals are uncountable. I have VSCode setup with lean, and see the goal outputs and types when I put my cursor at places in these proofs. I'm finding that I'm still largely guessing at what each line is doing. In the end it seems no different than reading a proof on paper. I'm wondering if Lean provides any additional debugger tools that let me step through every single step the type checker goes through?

[Mario Carneiro]

Perhaps #explode might help break the proof down a bit more

[Kevin Buzzard]

If proofs are written in tactic mode then it's easy to step through them. If they're in term mode, or in tactic mode but with semicolon separators, then it's harder but you can often find out more by deleting terms and replacing them with a _, which can sometimes persuade lean to tell you the type of the term which is supposed to go in the hole.

[Mario Carneiro]

My understanding of the question is that he is not happy with the level of detail provided by tactic proofs

[Dan Abolafia]

#explode is helpful, but it is not interactive. I have to manually explode every definition used in the proof. Yes I wish it were possible to step through tactic meta programming, as well as see the proof checker state at every step, analogous to seeing all the local variable state in a debugger. That would at least allow me to figure out exactly what any line of code does in principle, though it may be very tedious.

[Andrew Ashworth]

When is Metamath proof explorer getting ported to Lean? :)

[Mario Carneiro]

This is a good question; I don't know how to reasonably support an explorer type interface to #explode using the tactic / vscode tricks available to us in lean. We could always generate tens of thousands of html files like metamath does, but I think it would be much more appropriate for lean to have some pull based API where the pages are only constructed as they are requested.

[Dan Abolafia]

Is there any thought being given to adding the kind of debugger I'm describing to lean in the future?

[Reid Barton]

I don't understand what this hypothetical feature does

[Dan Abolafia]

I suppose there are two features:
1) A debugger to step through tactic metaprogramming would be like a typical code debugger, if i understand the language correctly.
2) I think what I'm asking for is to be able to step through the execution of the proof checker, and have each step in that execution be tied to some position in user-facing code, i.e. any lean code involved in the proof (e.g. mathlib definitions, axioms, theorems, etc). Like a debugger, I would also want the checker state to be surfaced somehow, so that I can see what the checker sees. I don't have much of an understanding of the inner workings of the proof checker, so I don't know to what extent this is feasible.

[Reid Barton]

Two major difficulties with 2):

• In practice the proof checker (I assume this means the kernel) takes many, many more "steps" than you would care to follow. You would need to somehow find the steps you're interested in, but this is probably a meaningless concept, because:
• Tactics, especially "higher-level" ones such as simp or ring, can produce proofs where even the proof term itself is essentially not comprehensible, let alone the process of checking the proof term. There simply is no more comprehensible layer below the level of these tactics. (That's not to say such a layer could not exist, just that it does not exist with the way these tactics are implemented currently.)

I think there is a fallacy here that if you have access to more detail, it will give you greater understanding of what is happening. That is not necessarily the case when the amount of information is overwhelming and where the nature of the information is not more humanly accessible than the original form.

[Reid Barton]

It would help to have some examples of what you would hope to get out of such a tool.

[Reid Barton]

For example if you're completely new to lean and you want to understand proofs of things like p ∧ (q ∧ r) ↔ (p ∧ q) ∧ r , that's a different matter.

[Reid Barton]

But no amount of tracing the type checking of quadratic_reciprocity is going to tell you why quadratic reciprocity is true.

[Mario Carneiro]

Needless to say, I beg to differ. While the way in which lean sees these proofs is not readily accessible to human readers, this is more a presentation issue than anything else. I strongly believe that it is important to retain some connection to what is happening at the low level. If you give that up, the proof checker starts to fall into "magic" territory, and there is no longer a reason to believe in its trustworthiness

[Mario Carneiro]

At the very least, there is an abstract formalism associated with lean (c.f. my thesis), and it should be possible to present any lean term as a proof in that system

[Kevin Buzzard]

Sure, it's just that quadratic reciprocity will be incomprehensible to a human if you look at it that way.

[Mario Carneiro]

currently we aren't there yet, because there is no way to trace definitional equality proofs

[Kevin Buzzard]

You're much better off reading a book.

[Mario Carneiro]

It is possible that the proof of quadratic reciprocity has gone past what people can read, but I would submit that if this is the case then it's a bad proof

[Reid Barton]

I'm very confused by all of this!

[Mario Carneiro]

There is no reason why a proof of quadratic reciprocity should be incomprehensible

[Mario Carneiro]

even in full formal detail

[Mario Carneiro]

If you look at a metamath proof, it is probably more than one would care to write by a factor of about 10 or so, but not more than that. This is within the range of human understanding

[Reid Barton]

All I'm saying is that the proof you actually write in the proof assistant is more comprehensible than what you get by trying to examine, say, the proof term generated by the tactic. Isn't that the purpose of a high-level proof language?

[Mario Carneiro]

the thing is, proof terms are not a good way to present proofs

[Mario Carneiro]

because what people actually care about are the types

[Reid Barton]

Right, but this is what was asked for.

[Reid Barton]

Well, not the term per se, but something even worse.

[Mario Carneiro]

something even better

[Reid Barton]

Well, maybe we have different interpretations of the question then.

[Mario Carneiro]

proof terms without the typing information requires the user to hold the whole context in their head at all times, which requires ridiculous attention to detail

[Mario Carneiro]

you can't jump around in a proof like that

[Mario Carneiro]

which is what humans do

[Mario Carneiro]

#explode tries to fill that gap by presenting the types of each intermediate term, and mostly hiding the proof term itself

[Mario Carneiro]

but it still has nothing to say about definitional unfolding

[Reid Barton]

I think the question asked is probably not the real intended question anyways

[Reid Barton]

and I think you're trying to answer the real intended question

[Reid Barton]

Or maybe not. I have no idea.

[Mario Carneiro]

I think that #explode has some limitations since it is non-interactive, and a more debugger like interface would be good, but there are a lot of unanswered UI and implementation details to that

[Mario Carneiro]

One maybe easy option would be a tactic-ifier that takes any lean proof (as a term), and reconstructs an apply based tactic proof of it

[Mario Carneiro]

then you could use the goal view to see all the intermediate states

[Bryan Gin-ge Chen]

That sounds really cool.

[Reid Barton]

I was responding to the statement of 2). I still am fairly certain that given a tactic mode proof, there is no amount of visibility into things which actually currently happen during the processing of that proof that will give a greater understanding of what is happening in the proof than to just step through the tactic steps and watch the goal window.

[Reid Barton]

maybe with some rare exceptions for tactics like solve_by_elim that tend to produce comprehensible proofs

[Mario Carneiro]

Many tactics are too high level to be able to follow how the goal changed

[Mario Carneiro]

And this will only get worse as tactics improve

[Mario Carneiro]

if I see a proof by magic then following your approach I have no recourse but to just believe

[Reid Barton]

I think the original question is based on a faulty analogy. If we pretend proofs are like programs then stepping through the checking of a proof is like stepping through the compilation of a program. This is not a good way to try to understand a program. (It might be a good way to debug your compiler.)

[Kevin Buzzard]

The computer says it's OK so it's OK. I can completely understand what ring is doing and I have no interest in learning about horner form.

[Mario Carneiro]

It's amusing that you say that because I find the analogy extremely accurate

[Kevin Buzzard]

That's because you're not a mathematician

[Reid Barton]

Right, but the proposed approach is not necessarily going to help with those mystery tactics either. That is what I tried to address with my parenthetical sentence.

[Kevin Buzzard]

so you think about maths in a different way. If you want to actually get somewhere you have to learn to fly.

[Reid Barton]

Which analogy is accurate?

[Mario Carneiro]

It's not so much stepping through the compilation but rather stepping through the low level assembly that comes out the other end

[Mario Carneiro]

stepping through the compilation would be debugging the tactic itself

[Reid Barton]

I still think you're reading the question as what you want it to be and not as what it actually says.

[Mario Carneiro]

that's quite possible. I have strong views on this topic and they may be clouding my reading

[Mario Carneiro]

2) I think what I'm asking for is to be able to step through the execution of the proof checker, and have each step in that execution be tied to some position in user-facing code, i.e. any lean code involved in the proof (e.g. mathlib definitions, axioms, theorems, etc). Like a debugger, I would also want the checker state to be surfaced somehow, so that I can see what the checker sees.

I think it would be hard to relate the steps in the checker (the kernel) to code written in the source text (the tactics), because of the two step compilation process. However, it should be possible to relate tactics to bits of the proof term, and bits of the proof term to checker steps

[Reid Barton]

It's also probably true that what you want the question to be is the same as what the asker wanted the question to be, but without the original asker here we can't really know.

[Mario Carneiro]

The recently added show_term tactic will show an individual tactic's contribution to the resulting proof term

[Reid Barton]

Another thing along these lines that would be neat is to make simp or rw (with many rewrite steps) output a calc-style proof

[Reid Barton]

I don't really know whether that's trivial or difficult.

[Mario Carneiro]

I think a better primitive than calc would be a conv proof where the only steps are descending into subterms and transitivity

[Dan Abolafia]

@Reid Barton I've done the exercises in https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html through section 4, and I would understand a tactic-free proof of p ∧ (q ∧ r) ↔ (p ∧ q) ∧ r. The core language without tactics seems to satisfy what I am looking for. I can inspect the type signature of each expression in a proof and understand why the expression has that type signature. This is effectively stepping through a proof.

I think the original question is based on a faulty analogy. If we pretend proofs are like programs then stepping through the checking of a proof is like stepping through the compilation of a program. This is not a good way to try to understand a program. (It might be a good way to debug your compiler.)

Yes no one can understand a program fully by stepping through it. My intention is to use "stepping through the code" as a way to quickly ramp up my understanding of the language. But even an experienced user may wish to step through code they are reading to resolve confusions they may have, in lieu of talking to the code's author.

I agree with @Mario Carneiro "I strongly believe that it is important to retain some connection to what is happening at the low level. If you give that up, the proof checker starts to fall into "magic" territory, and there is no longer a reason to believe in its trustworthiness" The fact that what an expression does and represents is objective is immensely powerful (over informal mathematics in text), but only if I can actually have the computer tell me what is the case.

[Dan Abolafia]

@Reid Barton let me give you an example of what I'm trying to do.

I was looking at irr_sqrt_two in irrational.lean, which calls into irr_sqrt_of_prime which eventually calls into irr_nrt_of_n_not_dvd_multiplicity, which to me looks like a complicated mess. Are you telling me there is no way for me to fast track my understanding of this particular proof? That the tactics involved, with their nuances and idiosyncrasies, need to be fully comprehended through many hours of dedicated study just so I may understand the proof that sqrt(2) is irrational? And even then, I'll be relying on my interpretation of the code, and never get confirmation that what I think is happening is actually the case.

The fact that I cannot step through tactic metaprogramming exacerbates the situation because I effectively have to internalize the behavior of these tactics through encountering many examples. This reminds me of deep learning, where the various tools and methods are black boxes and cannot be understood formally, so practitioners and researchers are forced to acquire a heuristic understanding through long-term exposure. That is uncomfortable for me, and mathematics is my refuge from such messiness. It seems that lean is bringing the messiness of complex uninspectable black boxes into mathematics. Then the pedagogical benefits of computer proof checking are lost to me, and I'm not sure of what value lean is to me.

[Kevin Buzzard]

You can certainly understand the mathematics behind the proof and you can work your way down if you choose to. This sounds like a very long proof mathematically so the proof term will be gigantic. It will be like reading the machine code translation of a relatively simple python program

[Kevin Buzzard]

I have no idea what you mean when you call irr_nrt_of_n_not_dvd_multiplicity a complicated mess. It is a natural mathematical statement which can easily be interpreted, and the tactic mode proof is fairly short and natural.

[Yury G. Kudryashov]

And you can look at the proof state after each step.

[Dan Abolafia]

Python is not compiled, the analog would be stepping through the python interpreter at the assembly level. Frankly, if there were something screwy going on with the Python language itself that the python debugger can't resolve I might step through the interpreter at the C++ level. And for C++ code, I have indeed stepped through at the assembly level when things were weird. I don't see a reason to prefer machine code over assembly, and I suspect a similar first-pass translation can be done of raw proof code to something somewhat more human readable.

[Yury G. Kudryashov]

Usually every step is obvious for a mathematician.

[Kevin Buzzard]

All I'm saying is that the mathematical proof has a meaning, and sure you can keep digging and digging until you reach a level where it's just thousands of lines of elementary operations and all overall understanding is lost.

[Kevin Buzzard]

But if you want to understand this proof you should consult a mathematician, not keep digging

[Kevin Buzzard]

The tactics are conceptually meaningful and are manipulating mathematical objects in an intuitive way. Each individual step can be examined down to the core but to get an overall understanding of the proof you should first translate it into mathematics

[Yury G. Kudryashov]

BTW, studying mathlib proofs is definitely not the best way to learn math. In many cases we don't take the shortest route to an elementary statement but prove a very general version first.

[Kevin Buzzard]

Yes there are definitely easier ways to prove that the square root of two is irrational! This way has the advantage that you can also prove that the cube root of 691 is irrational with about as much work

[Dan Abolafia]

Let me elucidate why I described it as a complicated mess (I don't mean this as a jab at the authors, and I'm sure its very elegant lean code, but I am commenting on my experience as a novice jumping into the deep end).
Looking at the first line in irrational_nrt_of_n_not_dvd_multiplicity
https://github.com/leanprover-community/mathlib/blob/4daa7e8/src/data/real/irrational.lean#L57

rcases nat.eq_zero_or_pos n with rfl | hnpos,
I can see that nat.eq_zero_or_pos has type ∀ (n : ℕ), n = 0 ∨ n > 0.
I can see that the result of this line is to create two goals from nat.eq_zero_or_pos, one where hnpos : n > 0 is an added proposition, and the other where n is replaced by 0 everywhere.
It took me a while to realize n was being replaced by 0 in the first goal, so I was at first confused about what happened to the n = 0 case.
The more verbose alternative is cases nat.eq_zero_or_pos n with H₁ hnpos, subst H₁, where I can see the goal state with H₁ : n = 0 as a proposition and then see the explicit substitution subst H₁,

So now I am curious exactly how rcases does the cases and substitution all in one swoop. How is rfl contributing here?
Turns out in rcases_core has special support for rfl as a name.

| ((rcases_patt.one `rfl, e) :: l) := do
  (t, e) ← get_local_and_type e,
  subst e,
  rcases.continue l

(credit to Jesse Han for helping me figure this out)

My point is that I wouldn't know why the rcases line works, and I had to rely on having a good eye just to catch exactly the effect of this tactic on the goals state (replacing n with 0 in one place). Not knowing why it works (without help), I would not learn anything about rcases, and I would not be able to use a similarly efficient line in my own proof. Yes I can play around with the line and surrounding code to get a sense for what rcases is doing by trial and error. That is indeed an important complement to stepping through code anyway. But not being able to step through code or get some information about what is going on internally is a handicap that I have to work around. I expect that I'll encounter a similar difficulty for every line in this proof, where I need to guess and check what the objects in the line are doing by carefully reading through their definitions and the goal state information, and hoping for the best.

[Kevin Buzzard]

There are just a finite number of tricks which you learn after some practice. I would recommend reading the docs to learn about what tactics do, not the source code! Do you know about the community docs?

[Kevin Buzzard]

Rcases docs explain what's going on much better than rcases source code

[Kevin Buzzard]

And reading simple use cases of rcases will teach you more about rcases than just leaping in and trying to understand a complex proof from a standing start.

[Dan Abolafia]

By community docs you mean the mathlib docs?
https://leanprover-community.github.io/mathlib_docs/

[Bryan Gin-ge Chen]

Yes. Here's the doc entry on rcases.

[Bryan Gin-ge Chen]

It does look like we need to add a mention of the way rfl is treated. I actually asked about that myself not too long ago.

[Dan Abolafia]

There are just a finite number of tricks which you learn after some practice.

Finite is not very reassuring, haha. Is there a short list of tricks that form a minimum set to get me going? I'm less likely to invest time in learning something if I don't know how deep the rabbit hole goes and what the payoff will be.

Yes I can read the docs. I'm making a point about pedagogy. The joy of learning a programming language is that you don't need to read the docs ;) Seems like there's a missed opportunity here for hacker types to get interested in pure math and proofs. I know plenty of very intelligent people who view theoretical work as inaccessible to them because of the formalities of reading large amounts of material without any interactivity.

[Reid Barton]

Dan Abolafia said:

Yes no one can understand a program fully by stepping through it. My intention is to use "stepping through the code" as a way to quickly ramp up my understanding of the language. But even an experienced user may wish to step through code they are reading to resolve confusions they may have, in lieu of talking to the code's author.

Thanks for clarifying, I had a quite different picture of what you were looking for before. In particular, I didn't realize the main issue is with understanding the language itself.

If I may offer another analogy, suppose you are reading an ordinary math proof in a language you do not speak well, let's say German. The proof will probably be rather hard to understand, but that is because of the language it is written in. The solution is not to find another proof also in German with more of the details expanded, but instead to consult a German textbook or speaker for help with the parts that are difficult. (Or just see if you can find a translation instead.)

But now you are saying something like: well if I did have an expanded version of the proof in German, there's a greater chance that my rudimentary German will enable me to pick up some understanding of the argument, and maybe in turn improve my German skills; and there is also sense to this.

[Reid Barton]

Anyways, long ago you posted two items 1) and 2). 1) was a debugger for the tactic state. Tactics are effectively imperative programs, so this is surely possible in principle (e.g., Haskell has a debugger although I think virtually no one uses it). 2) was about stepping through the "proof checker" which I interpreted, perhaps wrongly, as referring to the entire system from tactics to the elaborator to the kernel, and this is a very different beast and probably not profitable to understand in any kind of stepwise fashion.

[Scott Morrison]

This reminds me of the Berkeley PhD language exams, where (depending on some important details like who the examiners were for each language) a viable strategy was sometimes to translate the theorem statements, write your own proofs out (in English), and only then try to read the given proofs in German/French/Russian, and finally try to rephrase your proof along the lines of the given one. The key point being that understanding the maths is often easier than understanding the language.