Declarative Lean

Stream: general

[Brando Miranda]

I wanted to learn more about the options for Declarative Lean (e.g. like Isar or controlled natural language or Cezar https://kluedo.ub.uni-kl.de/frontdoor/deliver/index/docId/2100/file/B-065.pdf). Any pointers? Does this exist for Lean?

[Patrick Massot]

Everything I see when skimming this pdf is already possible with the tactics we have.

[Patrick Massot]

You don't need anything new , you only need to restrict to a subset of what is available

[Patrick Massot]

If you want to enforce using only this subset then you can have a dedicated tactic mode where you only copy the subset you want to enforce

[Patrick Massot]

For instance you can read the discussion at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Proposal.3A.20.60fix.20x.60.20for.20.60assume.20x.60. It will contains a lot of noise from your point of view, but also interesting things for you.

[Kevin Buzzard]

Here's the example on p4 of the pdf, in Lean:

import tactic

namespace hidden

def div2 : ℕ → ℕ
| 0 := 0
| 1 := 0
| (n+2) := div2 n + 1

def double (n : ℕ) := n + n

open nat

lemma double_div2: ∀ n, div2 (double n) = n :=
begin
  intro n,
  induction n with d hd,
  { refl},
  unfold double at hd ⊢,
  rw succ_add,
  show div2 (_ + 2) = _,
  rw div2,
  show div2 (d + d) + _ = _,
  rw hd,
end

lemma double_div2' : ∀ n, div2 (double n) = n :=
  assume n,
  nat.rec_on n
  ( show 0 = 0,
    from rfl)
  (assume m, assume Hrec,
   calc div2 (double (succ m)) = div2 (succ m + succ m) : rfl
   ... = div2 ((m + m) + 2) : congr_arg _ $ by simp [succ_add, add_succ]
   ... = succ (div2 (double m)) : by rw div2; refl
   ... = nat.succ m : by rw Hrec
  )

end hidden

Both modes are already available.

[Patrick Massot]

See also the example at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Lebesgue.20number.20lemma/near/194033514

[Patrick Massot]

The main difference with Isar (beyond the additional flexibility) is the lack of sledgehammer to proving proofs of each small step.

[Patrick Massot]

You can also mix Kevin's example, doing the structured tactic mode style.

[Jason Rute]

@Brando Miranda’s interests are in AI, so I don’t think he is asking from the point of a Lean user (i.e. how can I do this in practice), but for some other purpose (e.g. is there a formal declarative specification I can use to interact with Lean). Can you clarify your motivation Brando? (Also it is good to hear from you again.)

[Patrick Massot]

Wow. Thanks Jason, that was very hard to guess from his message and then disappearance.

[Brando Miranda]

Hi @Patrick Massot Thanks for your response. It's greatly appreciated. I'm curious, what do you mean by disappearance? I didn't know when I would get a response so I just closed the chat and would be back to it later as I have now.

My question has many facets. One of them is trying to understand what is the best representation from an interactive theorem prover side for machine learning (ML) systems to do proof search. I won't lie but with so many Interactive Theorem Provers (ITPs) in existence, it's been very hard for me to commit to any of them in depth (though Isabelle is the one I know best because it's the one taught in my university) because I just don't know which one is the best (especially for Machine Learning). I am not even sure what are all the features I should be considering when choosing one (especially for ML).

In addition, to discover that there is a declarative style ITP language added yet another layer of complexity that I didn't know existed. It's not entirely clear why to me what the main problem declarative proofs solve vs procedural (I will admit if I don't know if there are more styles I am not aware of).

Though, it was a pleasant surprise to hear that Lean has declarative proofs embedded in the language naturally, so I wouldn't have to worry about that if I were to choose Lean it seems, though I'm not an expert in ITPs, but I find them fascinating (and fun to use!).

[Brando Miranda]

@Jason Rute Thanks for the kind message Jason. I plan to be very active this summer, as soon as classes end next week. Excited! :)

[Patrick Massot]

Brando Miranda said:

Thanks for your response. It's greatly appreciated. I'm curious, what do you mean by disappearance? I didn't know when I would get a response so I just closed the chat and would be back to it later as I have now.

There is no problem. I was making fun of Kevin and I trying to answer very quickly without really knowing the question (but adding some context can often help)

[Brando Miranda]

@Patrick Massot Thanks! I didn't want to overwhelm people with every question I had but I am happy to start with a few first (and hopefully get them all cleared!). What problem are declarative style proofs suppose to solve (why were they invented for ITPs in particular)? Are they a good representation for proof search with respect to classical search methods or ML methods? Are they good at all for proof search?

[Mario Carneiro]

Declarative proof styles are intended for human readability. I think they are unlikely to be good for automatic search

[Mario Carneiro]

the idea is that you can get a formal proof that has the general structure of an informal maths proof

[Brando Miranda]

Are the grammars for procedural ITPS vs declarative ITPS usually completely separate?

[Mario Carneiro]

No, in fact they have significant overlap, which is what I think Kevin's original point was. Lean has tactics corresponding to all the different proof styles

[Brando Miranda]

Why does Lean have such a feature embedded, apparently, so naturally in it? Was that a major design point for Lean? It seems other languages make a big deal out of this feature (e.g. Cezar for Coq, Miz3 for HOL Light, Isar for Isabelle perhaps more out there) so I am trying to understanding it better.

[Mario Carneiro]

Lean was made with the benefit of hindsight, but I don't think it was a major design point, as much as the idea of having a dynamically extensible tactic language in the first place

[Brando Miranda]

Mario Carneiro said:

No, in fact they have significant overlap, which is what I think Kevin's original point was. Lean has tactics corresponding to all the different proof styles

But this isn't standard afaik. Otherwise why draw the distinction btw Isabelle vs Isar?

[Brando Miranda]

Mario Carneiro said:

Lean was made with the benefit of hindsight, but I don't think it was a major design point, as much as the idea of having a dynamically extensible tactic language in the first place

you mean we already know much more about ITPs before Lean was designed?

[Mario Carneiro]

Lean is only 5-6 years old. It's a baby compared to the others

[Brando Miranda]

Maybe this the wrong place to ask this (since the answer might be biased), but is due to this hindsight Lean the best ITP out there?

[Mario Carneiro]

That depends on what you mean by "best"

[Mario Carneiro]

I think in terms of user interface lean gets a lot of things right

[Brando Miranda]

Mario Carneiro said:

That depends on what you mean by "best"

Is it possible to learn more about the way "best" was defined for Lean? e.g. the main decision that came around for the design of Lean?

[Mario Carneiro]

There is a paper on metaprogramming in lean 3, that might be a good place to look for major design decisions

[Mario Carneiro]

that was when lean 3 first came out and differentiated itself from lean 2 with its much expanded tactic grammar

[Brando Miranda]

I am curious, what do you think is Lean's major advantages compared to Coq & Isabelle? (I will read that reference thanks!)

[Kevin Buzzard]

Different ITPs use different logics, e.g. some use higher order logic, some have the univalence axiom baked in, and so on. Hence it's difficult to say which is the "best" one -- it depends on what you plan on using it for. I have a hypothesis that Lean's particular choice of dependent type theory is the best one for doing a lot of different kinds of modern pure mathematics but it's difficult to "prove" this, other than by what we are doing, which is formalising lots of different kinds of pure mathematics and seeing what happens.

[Mario Carneiro]

https://leanprover.github.io/papers/tactic.pdf

[Kevin Buzzard]

Coq takes the concerns of constructivists more seriously, but because most mathematicians aren't constructivists I regard this as a hindrance. I don't really understand this link https://artagnon.com/articles/leancoq but perhaps you will.

[Kevin Buzzard]

Isabelle/HOL is higher order logic, not dependent type theory, so the foundations are very different. What it does, it does very well, and very quickly. But my worries when it comes to mathematics are about what it can't do well at all.

[Kevin Buzzard]

But these are just my personal opinions and they're highly skewed by my personal goal, which is to see e.g. an entire undergraduate pure maths degree in one system.

[Brando Miranda]

Which one is the easiest to write where things that are "obvious" or "intuitive" can be taken for granted? I am guessing Lean is the best at this from this quote from the link you sent https://artagnon.com/articles/leancoq

Quotient-reasoning makes formalizing commutative algebra painless, and it's baked into the Lean kernel.

[Mario Carneiro]

That's an eternal goal in any theorem prover

[Kevin Buzzard]

The way to prove an obvious thing is to apply the proof which someone else has already formalised in the maths library

[Kevin Buzzard]

however this only works for some values of obvious

[Kevin Buzzard]

and I've seen a lot of very complicated things being called obvious in research maths seminars in my time

[Brando Miranda]

I was surprised to read that Lean is slow? I would have thought it's really fast because of the C++

My inference is from this paragraph (https://artagnon.com/articles/leancoq):

One would think that Lean is an engineering feat, since it's written in C++: Coq's math-comp (90k loc) compares to Lean's mathlib (150k loc); math-comp builds in under ten minutes, while mathlib takes over thirty minutes to build! Indeed, due to their design decision to use a VM for computations, computation happens at a speed comparable to Python-bytecode evaluation — they seem to be overhauling this in Lean4 though, by compiling Lean code down to C before execution.

[Kevin Buzzard]

obvious can mean "known to the people in the room" sometimes.

[Brando Miranda]

Got it. I was just guessing based on the comment from the blog you sent me.

[Mario Carneiro]

Lean is surprisingly fast when you look at how much it is doing

[Brando Miranda]

hmm...What is it doing?

[Mario Carneiro]

The main slow things in lean are VM evaluation and typeclass inference

[Brando Miranda]

I guess from a proof search point of view (my interest mainly), I would be really happy if my ITP environment is fast. Very fast.

[Mario Carneiro]

VM evaluation is used for running tactics, which does impact your ML bottom line

[Brando Miranda]

But perhaps to focus only on fast is a naive goal. Hence the discussion I started and my interest in learning about Lean more (& declarative proofs).

[Brando Miranda]

Also, if proofs are going to be generated, it would be nice that they are human understandable, hence why I was curious about declarative style proofs (since that seems to be their main goal afaik).

[Mario Carneiro]

I think that a fast ITP is a great goal (which is why I built one). It's tough selling this to the community though

[Mario Carneiro]

I still have hope for post processing arbitrary proofs to make them more human readable / navigable / understandable

[Mario Carneiro]

the main downside of procedural proofs is that you have to have the proof state in your head at all times to read the proof, which in practice means they can't be read without the program running alongside

[Jannis Limperg]

Mario Carneiro said:

Lean is surprisingly fast when you look at how much it is doing

Is there any evidence for this? Coq also does typeclasses and tactic-based metaprogramming, and while Lean is not particularly slow, it also hasn't struck me as particularly fast. The mathlib compile times aren't great, but there is no direct comparison, so it's hard to evaluate these claims.

[Mario Carneiro]

That at least is easy enough to fix post facto

[Mario Carneiro]

The typeclass problems lean has to slog though are gigantic

[Mario Carneiro]

I don't think Coq does as much with dynamic tactics as lean

[Mario Carneiro]

most tactics are implemented in ML, certainly any of the "serious" ones. This gives them a big performance advantage

[Mario Carneiro]

Lean is definitely slow when you look at how many lines of source it goes through per second, but that is more reflective of the complexity of the problems it has set itself (dependent type theory, unification up to definitional reduction, typeclass searches all over the place, etc) than the implementation (which is quite efficient and well optimized)

[Mario Carneiro]

Put another way, I think you would have a hard time beating lean at its own game, that is, an alternate lean typechecker. If you change the game then you can get huge (orders of magnitude) wins, but you won't see that with e.g. better allocation strategies

[Mario Carneiro]

Jannis Limperg said:

Mario Carneiro said:

Lean is surprisingly fast when you look at how much it is doing

Is there any evidence for this? Coq also does typeclasses and tactic-based metaprogramming, and while Lean is not particularly slow, it also hasn't struck me as particularly fast. The mathlib compile times aren't great, but there is no direct comparison, so it's hard to evaluate these claims.

Note that I include busywork in this sense of "how much it is doing". E.g. superman took 2 hours to cross the town, which doesn't sound fast until you realize he circled the world a hundred times first

[Mario Carneiro]

The gains in lean 4 for typeclass inference are solidly in the realm of "eliminating busywork"

[Jannis Limperg]

On typeclasses, it would be interesting to know how Coq fares on similarly sized problems. Afaict, their algorithms are very similar, at least until we get the tabled stuff.

On tactics, Lean also delegates to C++ quite a bit; after all, the standard tactics library consists mainly of thin wrappers around C++. The big Coq projects (e.g. anything by Chiplala) also have a ton of custom Ltac, some of it very complex, so I'm not sure Lean is unique in this regard.

I'm not saying that Lean is slow, and I certainly couldn't develop a faster Lean typechecker. But in the absence of evidence, I'll remain skeptical that it's significantly faster than the competition at similar tasks.

[Mario Carneiro]

Coq doesn't use typeclasses nearly as pervasively as mathlib. math-comp uses canonical instances instead, which solve the problem in a different way with more up front work for the user and a better asymptotic behavior for the problems generated

[Mario Carneiro]

I would bet that if you ported mathlib to coq, using coq typeclasses, lean would outperform coq

[Mario Carneiro]

Lean's tactic mode is also seemingly more flexible than Coq's. In Coq you just start every proof in tactic mode, term proofs seem to be rare, and they are built right into the grammar. By contrast, in lean a begin end block can be anywhere in the term, and when it hits one it translates the tactic block into a term (running the tactic parsers in the VM), typechecks the term, then evaluates the result (also in the VM), eventually calling back in to C++. This setup is a lot more flexible but it comes at a noticeable performance cost

[Mario Carneiro]

In any case, I'm just speculating, and I don't have enough experience with coq to make a strong argument

[Brando Miranda]

Thanks for performance discussion! Very interesting for me as an ML person but back to declarative languages.

I was asking because Isabelle has sledgehammers and they often suggest Isar proofs. Which seem to outline the general shape of proofs + are more readable which made me think that perhaps declarative languages are just as easy to proof search. Which lead to this discussion. Is that true for Lean too? Why are Isar proofs so readily avaiable by the sledgehammer?

[Jannis Limperg]

Sorry Brando, I'll stop hijacking your thread now. ;)

For Sledgehammer, I'll try to summon @Jasmin Blanchette; he can probably tell you whether Isar makes this sort of thing easier.

[Mario Carneiro]

As they say, when all you have is a hammer, everything looks like a nail. I think it finds declarative proofs because that's the way isabelle is designed to present proofs. The things the ATPs are solving are full proofs anyway; you can present those proofs however you like.

[Jason Rute]

Does @Gabriel Ebner's Lean-hammer supply proofs? What do those look like?

[Jason Rute]

I think from the point of view of AI, Lean has certain advantages and disadvantages:
Advantages:

• It is very popular, partly because it has a lot of nice features which make proving things easy, and because it has a great active community.
• Lean has a lot of built in tools (like a tactic language, an io interface, a parser and a server) which make proof recording and interaction possible (not as nice as I'd like, but possible) without hacking the C++ code.
• It has a reasonable size library.

Disadvanatages

• All those "nice" features make Lean hard to parse. You can have by blocks in term mode in calc mode in begin...end blocks. This makes proof recording and other data-gathering tasks difficult.
• Also the behavior of tactics can change depending on attributes attached to theorems.
• There is nothing like it now, so it needs to be built from scratch.
• Everyone is telling me to wait for Lean 4 :slight_smile: but I don't listen.

[Jason Rute]

Also, this is really off-topic now, but as for speed and AI, I think I've found a performant way to interact with Lean as a gym environment and to call a trained AI from within Lean as a tactic. I'm playing around with it more, but it requires some more engineering. I think I'll have a prototype (only a subset of Lean tactics) in about 2 weeks.

[Jason Rute]

Ok, I think that last paragraph promises more than I intend. I won't have DeepHOL for Lean (or even TacticToe for Lean) anytime soon, but I'm saying I think I've found a path to making them and I'll create a small demo of that path soon.

[Yury G. Kudryashov]

Me when switching from Is {...} a tactic? to this thread: https://i.gifer.com/7Cca.mp4

[Jasmin Blanchette]

Sledgehammer sometimes suggest Isar proofs because these can then follow the structure of the ATP proofs step by step. I don't see a good way to do this with only tactics -- you'd quickly get out of sync with the ATP proof. My JAR article "Semi-intelligible ..." shows some examples of ATP vs. Isar proofs.

[Gabriel Ebner]

Jason Rute said:

Does Gabriel Ebner's Lean-hammer supply proofs? What do those look like?

I'm kind of waiting for Lean 4 at the moment, because I'm tired of the performance issues right now. The tactic scripts it produces are of the form by super [list, of, lemmas] (where super is a first-order prover). The proof terms produced by the tactic are semi-legible, at least you can make out the steps of the prover.

[Brando Miranda]

Jason Rute said:

Also, this is really off-topic now, but as for speed and AI, I think I've found a performant way to interact with Lean as a gym environment and to call a trained AI from within Lean as a tactic. I'm playing around with it more, but it requires some more engineering. I think I'll have a prototype (only a subset of Lean tactics) in about 2 weeks.

I'd like to get involved in some way with your Lean + AI hacking (though I might miss messages in this stream because I'm can't figure out how to mute all the general things without muting this one).

[Brando Miranda]

I'm trying to wrap my head around the discussion in the thread with respect to ATPs + Hammers + producing Declarative proofs in Lean. Is the consensus that it's not as straight forward as it is in Isabelle because Isabelle is by design intended to be a declarative ITP language?

[Brando Miranda]

Jason Rute said:

• Lean has a lot of built in tools (like a tactic language, an io interface, a parser and a server) which make proof recording and interaction possible (not as nice as I'd like, but possible) without hacking the C++ code.

This seems like a really big advantage from an ML perspective.