Inferring Theorem from a Proof Term?

Stream: new members

[Joe Palermo (S2'17)]

I've noticed that in Lean, theorems are always stated and then proved, i.e. backwards reasoning is the norm. In The Hitchhiker's Guide to Logical Verification I read about structured proofs (i.e. forward proofs), but even in that case the theorem is always stated before the proof begins.

I understand why this is the case, but I'm interested in computational methods for randomly generating theorems, and for this purpose it would be helpful to have a method of pulling theorems statements directly from (randomly generated) proofs. In other words, given a randomly generated proof (generated without knowing what theorem it will be a proof of), it would be helpful to have a way of extracting the theorem statement it is a proof of.

In Lean can you infer a theorem (i.e. type) directly from a proof term that proves that theorem? If so, how?

I understand that #check can provide the type of any well-formed term, but sometimes Lean won't allow me to "#check" a proof term for instance if it is constructed with iff.dcases_on as in this example

Perhaps to fix this example I need a fully elaborated version of the proof term?

[Eric Wieser]

If you use def rather than lemma, lean will try to deduce the type (in this case, the statement) for you

[Kevin Buzzard]

set_option pp.all true
lemma iff_of_true2 {P : Prop}:
(P ↔ true) → P :=
λ H, iff.dcases_on H (λ H₁ H₂, H₂ trivial)

#print iff_of_true2

#check λ {P : Prop} (H : iff P true), @iff.dcases_on.{0} P true (λ (_x : iff P true), P) H (λ (H₁ : P → true) (H₂ : true → P), H₂ trivial)

It works if you give it the fully elaborated term.

[Joe Palermo (S2'17)]

Thanks! I didn't realize #print would do that

[Jason Rute]

Are you going to use Lean to randomly generate the proof or some external tool? In either case, I think you might quickly run into difficulties with dependent parameters but I suppose that will depend a lot on what terms you are using to generate your proofs. For example, consider randomly generating an induction proof using nat.rec (or similar theorem). Also, be considerate of rfl proofs, since you can prove 0 = 0+0 with rfl, but if you copy and paste the fully elaborated proof, you it will type check as0=0. (I don’t mean to discourage, just pointing out some considerations that I thought about when think through a similar project.)

[Lucas Allen]

You can also use infer_type to get the type of an expr, this lets you get the theorem statement from the proof term. I'm not on my Lean machine right now, but I think you can do something like,

infer_type `(\lambda x, rfl)

to get \forall x, x = x. I hope that's right.

[Jason Rute]

The reason for my question about what you are using to generate terms is that @Lucas Allen is correct that if you are looking to do this programmatically, then infer_type is one good way to go. Technically, there are two ways to programmatically work with Lean. You can use the language server. It is slow, but you can do anything you can do in VS Code (like #check). Or you can use the monadic tactic framework, including infer_type. If you do everything in the Lean programming language, this latter one is the way to go. If you are integrating with external tools, then it requires some finesse, but we did recently add to Lean a way to parse Lean text inside the tactic monad which should make some things easier. I'm happy to explain more, but I don't want to get ahead of myself here.

[Joe Palermo (S2'17)]

@Lucas Allen Thanks for the tip!

@Jason Rute I really appreciate for your words of advice and interest. My intention is use neural nets to generate the proof terms. I'm interested in the question of how to create a feedback loop between a model that generates theorems/proofs and a model that tries to reconstruct proofs given the theorem statement. Essentially the question is how to get asymmetric self-play to work in mathematics. I'm not entirely sure it makes sense to try doing this by simply generating proof terms, and then #check ing them to get theorems, but I'm not sure how else it could be done in Lean today. My understanding is that many tactics only work in a backwards proof style where the goal is known. If one is generating new theorems then the "goal" is not known. Hence why I'm thinking to work directly with proof terms instead of tactics.

Any idea how much slower the language server is? It seems like it might be a simpler interface to use.

Btw I read your recent PACT paper (really cool paper btw) and I see that the theorem proving environment is written entirely in Lean. Having read through some of the code, I'm curious to know how you feel about it. What are the limitations of working in Lean? I don't have much background in functional programming (by profession I'm a deep learning engineer) and I'm finding it hard to understand the code and to assess the pros/cons.

[Scott Morrison]

You can just make a metavariable goal, and work backwards even without knowing what the goal is:

import data.nat.factorial

def wrapper {α : Sort*} (a : α) : true := trivial

def ex : true :=
begin
  let x : _ := by {
    apply nat.factorial_pos,
    exact 7, },
  exact wrapper x,
end

#print ex

[Jason Rute]

Neat trick! intro n doesn't seem to work in such a proof (since it doesn't know the type of n), but you can use refine:

import data.nat.factorial

def wrapper {α : Sort*} (a : α) : true := trivial

def ex : true :=
begin
  let x : _ := by {
    refine λ n : ℕ, _,       -- basically `intro n`
    tactic.trace_result,     -- show proof so far
    apply nat.factorial_pos, -- apply theorem nat.factorial_pos
    tactic.trace_result,
    exact n,
    tactic.trace_result,
    },
  exact wrapper x,
end

#print ex

[Jason Rute]

You also might need to reorder the goals using tactic.rotate since some goals depend on others.

[Jason Rute]

Joe Palermo (S2'17) said:

My intention is use neural nets to generate the proof terms.

Neural nets would make a lot of sense. Our gptf/pact paper indeed shows that transformers can generate whole term proofs (in the form of exact ... directly, and I'm sure there are lots of other ways to apply neural nets into generators besides direct text generation. They would also probably be good at making sure that the various types match. If you are looking to do "math zero", you might have a bit of trouble getting the loop started, since for induction proofs (which are pretty common before you build up facts) you have to know what your induction hypothesis is at the beginning. This is true in dependent type theory (using nat.rec say) as well as first order logic (using say the Peano axioms or ZFC).

[Jason Rute]

Joe Palermo (S2'17) said:

I'm not entirely sure it makes sense to try doing this by simply generating proof terms, and then #check ing them to get theorems, but I'm not sure how else it could be done in Lean today.

I think there are a few considerations. You have a lot of options to generate terms. If you generate them as plain text you can use (1) pretty-printed human-style Lean, (2) fully elaborated lean, or (3) Lean expressions (more on this in a bit). For gptf, we used option 1 for the proof steps, but that was because we were using human written code. However, much of the time, the pretty printed output of a lean proof will not actually parse as you have already seen. The fully elaborated proofs (option 2) are more likely to parse, but also much longer and you have to fill in type information that Lean could do automatically. Human proofs of course use a mix. When it is possible to use the less verbose syntax, they use that, but then switch to the elaborated versions when needed. Note, however that at least in Lean 3 (everything I say is for Lean 3) what Lean shows as a fully elaborated proof might still not parse (there are cycle-consistency problems in Lean 3). For more security, you could build the proof as a Lean expression internally in Lean. You could build it externally as say an s-expression, or internally using Lean's metaprogramming framework to build a proof term possibly programming in something like Scott's example above to build a proof in stages instead of all at once. The advantage here is that Lean would stop you part way through a proof to say that one part of the proof can't unify with another.

[Jason Rute]

Then there is the question of how to check the terms. You can use the lean server, writing a file and #checking the proof. You asked how long that takes. It has a hard-coded speed limit of 200ms to process a file. (You can get around it a bit by putting in multiple #checks in on file, but this becomes a pain.) If you are interested in the Lean server, I'd recommend looking at my example here of using it in Python. Another, better way to use it in Python is via the lean-python client. That client really needs some love (my fault, hopefully this is motivation for me to put in some effort to fix it up).

[Jason Rute]

The other option is to learn to metaprogram in Lean. Then you can either (1) use Lean's metaprogramming framework to build proofs in stages (building on Scott's example), or (2) have Lean read a string, parse it, and check it. For the latter approach, I'd recommend looking at this thread as looking through my annotated examples in #new members > basic tactic writing & IO. Both approaches would involve learning to metaprogram in Lean. For that I recommend:

• https://leanprover-community.github.io/extras/tactic_writing.html
• https://agentultra.github.io/lean-for-hackers/

[Jason Rute]

When I said before that you should use the tactic framework, I really meant in general the metaprogramming framework. That is made up mostly of three monads: tactic, parser, io. All three have access to Lean's Environment, so they could be used to loop over, say, all Lean proofs. The io monad also supports IO, the parser monad is needed to read Lean code and parse it (which may be important to what you are doing), and the tactic monad, while often used for generating proofs, also just has a bunch of tools for interacting with the environment and type checker. One of these is the function infer_type which will let you take an expression (of say a proof term already parsed with the parser) and infer its type (i.e. the theorem it proves). Note, now all the monads can access all the other ones. That wasn't the case in the thread #new members > basic tactic writing & IO, so much of that thread was elaborate tricks to access the parser monad inside the io or tactic monads.

[Jason Rute]

Joe Palermo (S2'17) said:

Btw I read your recent PACT paper (really cool paper btw) and I see that the theorem proving environment is written entirely in Lean. Having read through some of the code, I'm curious to know how you feel about it. What are the limitations of working in Lean? I don't have much background in functional programming (by profession I'm a deep learning engineer) and I'm finding it hard to understand the code and to assess the pros/cons.

The advantage of working in Lean directly is that you can work with Lean objects directly, including Lean proofs. Also, Lean has a lot of tools for stuff like what you are doing. The disadvantage is that Lean 3 is hard to learn, and the notation is confusing. If you are new to functional programming (and even if you are not), it will honestly take some time. (Lean 4 is a better programming language, but I don't think it has as many tools right now.)

[Jason Rute]

Last, I want to again emphasize that rfl proofs are weird. Here is an example:

#check (rfl : nat.zero = 0 + 0)   -- rfl : 0 = 0
set_option pp.all true
#check (rfl : nat.zero = 0 + 0)   -- @rfl.{1} nat nat.zero : @eq.{1} nat nat.zero nat.zero

You would think this would type check as nat.zero = 0 + 0 or something like that, but rfl as a theorem can only prove a = a and that is what it type checks as. (Notice there is nothing in the proof, even the fully elaborated proof, about 0+0.) However, rfl is more than just a theorem. It is like a built in script in the proof term language that tells the type checker to identify things which are judgmentally equal. I think the idea is that this reduces the size of proof terms, since lean or an external proof checker can just check the rfl part on the fly by normalizing the expressions instead of saving the very long proof term that rfl would generate. Anyway, that means you might have to put in some extra work generating rfl proofs which are not just trivial identities.

[Bryan Gin-ge Chen]

(deleted)

[Jason Rute]

I realize this morning that my description of rfl is wrong. I no longer think the rfl (which is basically just the constructor eq.refl) is special in the way I said. Consider:

theorem ex (h : 1 * 1 < 0) : 1 < 0 + 0 := h
#print ex
-- The proof type checks to λ (h : 1 * 1 < 0), h : 1 * 1 < 0 → 1 * 1 < 0
#check (λ (h : 1 * 1 < 0), h : 1 * 1 < 0 → 1 < 0 + 0)

There is no rfl but the same thing is going on. Instead, now I think that judgmentally equal things are just treated as the same in Lean, and this is verified by the type checker. Anyway, the consequence is still the same. The same proof can be a proof for a number of theorems which all judgmentally equal. If you ask Lean to typecheck a proof without it being associated with a declaration (theorem/def) then it will pick one type of many equivalent possibilities.

[Joe Palermo (S2'17)]

Jason Rute said:

The other option is to learn to metaprogram in Lean. Then you can either (1) use Lean's metaprogramming framework to build proofs in stages (building on Scott's example), or (2) have Lean read a string, parse it, and check it. For the latter approach, I'd recommend looking through my annotated examples in #new members > basic tactic writing & IO. Both approaches would involve learning to metaprogram in Lean. For that I recommend:

• https://leanprover-community.github.io/extras/tactic_writing.html
• https://agentultra.github.io/lean-for-hackers/

These resources look super useful! Thanks very much for the abundance of information. I'm going to dive into these materials and re-assess those design choices once I have some more comfort with Lean.

[Joe Palermo (S2'17)]

#print command above in the meta variable goal example from @Jason Rute produces this:

def ex : true :=
let x : ∀ (n : ℕ), 0 < n.factorial := λ (n : ℕ), n.factorial_pos in wrapper x

I guess the whole thing let x : ∀ (n : ℕ), 0 < n.factorial := λ (n : ℕ), n.factorial_pos in wrapper x is a proof term. I didn't know proof terms could contain ":=". How would you get the theorem statement for this proof? If I run #check on the whole proof term. I just comes back as "true" which makes sense since that's the type that was declared for ex, but ideally I'd like to extract some more descriptive type. Not sure if it's possible.

[Greg Price]

The theorem that whole term is a proof of is the theorem whose statement is just true. It has some much shorter proofs, like trivial which is what appears in the implementation of wrapper.

[Greg Price]

There's a theorem embedded inside there, which is the part between let x : and :=. In other words, it's the type that's being ascribed to x.

That theorem isn't part of the type of the whole term, so you'd want to extract it from the term's syntax.

[Jason Rute]

@Joe Palermo (S2'17) I think there are two questions here. The first question is about this exact proof term. As Greg said, it is using let notation. For example, let x := 2 in x + x evaluates to 4, and you can also add in a type so let x : nat := 2 in 2 + 2 is the same thing but explicitly giving the type of x. The proof you showed should be read as "Let x be the element of type ∀ (n : ℕ), 0 < n.factorial whose value is λ (n : ℕ), n.factorial_pos (so λ (n : ℕ), n.factorial_pos is a proof of ∀ (n : ℕ), 0 < n.factorial) and put this in wrapper x (which remember is just a proof of true ignoring the input). Your second question is if you use that trick above, how do you get the inner proof being constructed (ignoring all the wrapping stuff). The inner theorem being proved is between x : and := and the proof is between := and in. (Of course, writing a parser for this that will be guaranteed to work in all situations could be complicated if the inner proof also uses letnotation.)

[Greg Price]

I think a very simple parser will work even if the proof uses let-notation -- as long as the theorem statement itself doesn't. It just has to look for the first :=.

[Greg Price]

If the (inner) theorem statement may use let-notation, then the easiest solution is probably to work out how to do the metaprogramming to ask Lean about the pieces of the expression object directly.

[Joe Palermo (S2'17)]

Ahh I see, it's a meaningful theorem wrapped in a dummy theorem. That clarifies things a lot.

[Joe Palermo (S2'17)]

Here's a followup question. Could you take any proof in mathlib and stick it into a wrapper like this? I picked a random theorem in data.nat.factorial (factorial_lt for example), and tried wrapping it up in the same way, but it fails.

import data.nat.factorial

def wrapper {α : Sort*} (a : α) : true := trivial

def ex : true :=
begin
  let x : _ := by {
    split; intro h,
    { rw [← not_le], intro hmn, apply not_le_of_lt h (factorial_le hmn) },
    { have : ∀(n : ℕ), 0 < n → n! < n.succ!,
    { intros k hk, rw [factorial_succ, succ_mul, lt_add_iff_pos_left],
      apply mul_pos hk (factorial_pos k) },
    induction h with k hnk generalizing h0,
    { exact this _ h0, },
    { refine lt_trans (h_ih h0) (this _ _), exact lt_trans h0 (lt_of_succ_le hnk) }}
    },
  exact wrapper x,
end

#print ex

It fails immediately on split because "constructor tactic failed, target is not an inductive datatype". So you can't just naively wrap a proof, but is there a simple procedure one could implement to do it? i.e. an algorithm to automatically put a wrapper around the proof, in such a way that everything checks out and one could #print and parse out the resulting theorem.

The context here is that I'm interested in ways of generating proofs with machine learning methods, but it's really critical that proofs in mathlib can be put into the same structure to serve as data for bootstrapping, otherwise there's no way to get off the ground.

[Eric Wieser]

an algorithm to automatically put a wrapper around the proof

Most tactics work by inspecting the current goal, and doing something based upon it - but your example fails, because the goal is just _, a wildcard with no information.

Perhaps more damningly to this idea, there is not a unique lemma statement corresponding to a tactic; by {ext, simp} is a proof of probably 100s of lemmas in mathlib.

[Joe Palermo (S2'17)]

@Eric Wieser Thanks for the input.

That's an important point. There isn't a unique lemma statement corresponding to the proofs of form by {ext, simp}, but I assume each such proof would have a unique proof term corresponding to it. That suggests to me that the only way to do something like this in Lean would be to use raw proof terms. But that's such a verbose representation, I wonder if it defeats the utility of it.

[Joe Palermo (S2'17)]

Tactic proofs nicely summarize proof terms which could be massive if fully elaborated

[Kevin Buzzard]

import data.real.basic

theorem foo (x y : ℝ) : (x+y)^3=x^3+3*x^2*y+3*x*y^2+y^3 := by ring

#print foo -- oof

[Eric Wieser]

~Note that~ As far as I'm aware, "raw" proof terms already contain the theorem statement. What you care about are "pretty printed" proof terms, which may or may not round-trip to the original proof term depending on how nasty the term is and whether you have set_option pp.implicit true (or worse) enabled.

[Jason Rute]

@Joe Palermo (S2'17) Again, I think it is helpful to step back and think through what you want to accomplish here. If your goal is to generate proofs, you have two options: Generate the whole proof in one go (maybe as a tree or as a Lean fully elaborated text), or generate the proofs in steps. For example, to generate λ (n : ℕ), n.factorial_pos you would do it in stages:

• λ (n : ℕ), _
• λ (n : ℕ), nat.factorial_pos _
• λ (n : ℕ), nat.factorial_pos n
  If you did it in stages that is when that trick would help you. But, no you can't use the typical tactics, you would have to work with a very small DSL of low-level tactics like apply and refine.

My personal thought is that if you are doing this as a supervised learning project and have access to a large language model, then try to generate whole proof terms. If you are doing this as a "math zero"reinforcement learning project where you are building up proofs from scratch or you don't have access to large language models, then breaking up the construction into steps would help your model. For example, one wrong character could cause a proof to not type check (and fully elaborated proofs can get really long). Doing this as a tree search over this tactic DSL gives your model the ability to backtrack.

However if you do the latter approach where you generate a proof in stages, then that is a lot of engineering to both create the DSL, convert your proofs to this DSL, and make your model work with this DSL, whereas large language models are easy (if you have the resources).

[Joe Palermo (S2'17)]

@Jason Rute Thanks again for your detailed advice. I have the skill set and resources to train reasonably large language models so I'm definitely inclined to that direction. I'm going to followup in my other thread (https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learning.20for.20Theorem.20Proving/topic/Lean.20client.20for.20Python), regarding some more specific questions about how one might do that.