Zulip Chat Archive

Stream: general

Topic: how do I step through proofs?


view this post on Zulip Dan Abolafia (Mar 19 2020 at 21:41):

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?

view this post on Zulip Mario Carneiro (Mar 19 2020 at 23:49):

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

view this post on Zulip Kevin Buzzard (Mar 20 2020 at 07:02):

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.

view this post on Zulip Mario Carneiro (Mar 20 2020 at 07:29):

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

view this post on Zulip Dan Abolafia (Mar 28 2020 at 18:20):

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

view this post on Zulip Andrew Ashworth (Mar 28 2020 at 18:28):

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

view this post on Zulip Mario Carneiro (Mar 28 2020 at 22:40):

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.

view this post on Zulip Dan Abolafia (Mar 28 2020 at 22:54):

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

view this post on Zulip Reid Barton (Mar 28 2020 at 22:56):

I don't understand what this hypothetical feature does

view this post on Zulip Dan Abolafia (Mar 29 2020 at 17:45):

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.

view this post on Zulip Reid Barton (Mar 29 2020 at 23:32):

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.

view this post on Zulip Reid Barton (Mar 29 2020 at 23:32):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 23:33):

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.

view this post on Zulip Reid Barton (Mar 29 2020 at 23:37):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:51):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:53):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 23:53):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:53):

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

view this post on Zulip Kevin Buzzard (Mar 29 2020 at 23:53):

You're much better off reading a book.

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:54):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 23:54):

I'm very confused by all of this!

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:54):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:54):

even in full formal detail

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:56):

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

view this post on Zulip Reid Barton (Mar 29 2020 at 23:56):

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?

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:57):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:57):

because what people actually care about are the types

view this post on Zulip Reid Barton (Mar 29 2020 at 23:57):

Right, but this is what was asked for.

view this post on Zulip Reid Barton (Mar 29 2020 at 23:57):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:57):

something even better

view this post on Zulip Reid Barton (Mar 29 2020 at 23:58):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:58):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:58):

you can't jump around in a proof like that

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:58):

which is what humans do

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:59):

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

view this post on Zulip Mario Carneiro (Mar 29 2020 at 23:59):

but it still has nothing to say about definitional unfolding

view this post on Zulip Reid Barton (Mar 29 2020 at 23:59):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:00):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:01):

Or maybe not. I have no idea.

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:01):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:03):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:03):

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

view this post on Zulip Bryan Gin-ge Chen (Mar 30 2020 at 00:04):

That sounds really cool.

view this post on Zulip Reid Barton (Mar 30 2020 at 00:05):

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.

view this post on Zulip Reid Barton (Mar 30 2020 at 00:06):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:23):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:23):

And this will only get worse as tactics improve

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:24):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:24):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 00:24):

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.

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:24):

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

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 00:25):

That's because you're not a mathematician

view this post on Zulip Reid Barton (Mar 30 2020 at 00:25):

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.

view this post on Zulip Kevin Buzzard (Mar 30 2020 at 00:25):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:25):

Which analogy is accurate?

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:25):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:26):

stepping through the compilation would be debugging the tactic itself

view this post on Zulip Reid Barton (Mar 30 2020 at 00:26):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:26):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:29):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:29):

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.

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:31):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:31):

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

view this post on Zulip Reid Barton (Mar 30 2020 at 00:32):

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

view this post on Zulip Mario Carneiro (Mar 30 2020 at 00:32):

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

view this post on Zulip Dan Abolafia (May 01 2020 at 21:13):

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

view this post on Zulip Dan Abolafia (May 01 2020 at 21:33):

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

view this post on Zulip Kevin Buzzard (May 01 2020 at 21:35):

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

view this post on Zulip Kevin Buzzard (May 01 2020 at 21:38):

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.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 21:39):

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

view this post on Zulip Dan Abolafia (May 01 2020 at 21:39):

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.

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 21:40):

Usually every step is obvious for a mathematician.

view this post on Zulip Kevin Buzzard (May 01 2020 at 21:40):

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.

view this post on Zulip Kevin Buzzard (May 01 2020 at 21:42):

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

view this post on Zulip Kevin Buzzard (May 01 2020 at 21:44):

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

view this post on Zulip Yury G. Kudryashov (May 01 2020 at 21:46):

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.

view this post on Zulip Kevin Buzzard (May 01 2020 at 22:27):

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

view this post on Zulip Dan Abolafia (May 01 2020 at 22:28):

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.

view this post on Zulip Kevin Buzzard (May 01 2020 at 22:31):

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?

view this post on Zulip Kevin Buzzard (May 01 2020 at 22:31):

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

view this post on Zulip Kevin Buzzard (May 01 2020 at 22:32):

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.

view this post on Zulip Dan Abolafia (May 01 2020 at 22:33):

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

view this post on Zulip Bryan Gin-ge Chen (May 01 2020 at 22:34):

Yes. Here's the doc entry on rcases.

view this post on Zulip Bryan Gin-ge Chen (May 01 2020 at 22:39):

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.

view this post on Zulip Dan Abolafia (May 01 2020 at 22:40):

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.

view this post on Zulip Reid Barton (May 02 2020 at 00:15):

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.

view this post on Zulip Reid Barton (May 02 2020 at 00:30):

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.

view this post on Zulip Scott Morrison (May 04 2020 at 03:57):

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.


Last updated: May 08 2021 at 02:46 UTC