Zulip Chat Archive

Stream: general

Topic: Declarative Lean


view this post on Zulip Brando Miranda (May 06 2020 at 17:21):

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?

view this post on Zulip Patrick Massot (May 06 2020 at 17:32):

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

view this post on Zulip Patrick Massot (May 06 2020 at 17:33):

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

view this post on Zulip Patrick Massot (May 06 2020 at 17:34):

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

view this post on Zulip Patrick Massot (May 06 2020 at 17:37):

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.

view this post on Zulip Kevin Buzzard (May 06 2020 at 17:38):

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.

view this post on Zulip Patrick Massot (May 06 2020 at 17:38):

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

view this post on Zulip Patrick Massot (May 06 2020 at 17:39):

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

view this post on Zulip Patrick Massot (May 06 2020 at 17:40):

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

view this post on Zulip Jason Rute (May 06 2020 at 17:43):

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

view this post on Zulip Patrick Massot (May 06 2020 at 18:00):

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

view this post on Zulip Brando Miranda (May 06 2020 at 20:17):

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

view this post on Zulip Brando Miranda (May 06 2020 at 20:20):

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

view this post on Zulip Patrick Massot (May 06 2020 at 20:57):

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)

view this post on Zulip Brando Miranda (May 06 2020 at 21:29):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:30):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:31):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:32):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:33):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:33):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 21:35):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:35):

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?

view this post on Zulip Brando Miranda (May 06 2020 at 21:35):

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?

view this post on Zulip Mario Carneiro (May 06 2020 at 21:36):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:36):

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?

view this post on Zulip Mario Carneiro (May 06 2020 at 21:36):

That depends on what you mean by "best"

view this post on Zulip Mario Carneiro (May 06 2020 at 21:37):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:37):

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?

view this post on Zulip Mario Carneiro (May 06 2020 at 21:38):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:38):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:39):

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

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

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 21:41):

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

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

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.

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:43):

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.

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

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.

view this post on Zulip Brando Miranda (May 06 2020 at 21:49):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 21:51):

That's an eternal goal in any theorem prover

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:51):

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

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:51):

however this only works for some values of obvious

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:51):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:52):

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.

view this post on Zulip Kevin Buzzard (May 06 2020 at 21:52):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:52):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:52):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:53):

hmm...What is it doing?

view this post on Zulip Mario Carneiro (May 06 2020 at 21:53):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:53):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 21:54):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:54):

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

view this post on Zulip Brando Miranda (May 06 2020 at 21:55):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:55):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:57):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 21:58):

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

view this post on Zulip Jannis Limperg (May 06 2020 at 21:59):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 21:59):

That at least is easy enough to fix post facto

view this post on Zulip Mario Carneiro (May 06 2020 at 22:00):

The typeclass problems lean has to slog though are gigantic

view this post on Zulip Mario Carneiro (May 06 2020 at 22:02):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:02):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:05):

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)

view this post on Zulip Mario Carneiro (May 06 2020 at 22:07):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:14):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:15):

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

view this post on Zulip Jannis Limperg (May 06 2020 at 22:16):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 22:18):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:19):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:24):

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

view this post on Zulip Mario Carneiro (May 06 2020 at 22:26):

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

view this post on Zulip Brando Miranda (May 06 2020 at 22:47):

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?

view this post on Zulip Jannis Limperg (May 06 2020 at 22:52):

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.

view this post on Zulip Mario Carneiro (May 06 2020 at 23:06):

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.

view this post on Zulip Jason Rute (May 06 2020 at 23:26):

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

view this post on Zulip Jason Rute (May 06 2020 at 23:34):

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.

view this post on Zulip Jason Rute (May 06 2020 at 23:41):

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.

view this post on Zulip Jason Rute (May 06 2020 at 23:44):

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.

view this post on Zulip Yury G. Kudryashov (May 07 2020 at 03:08):

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

view this post on Zulip Jasmin Blanchette (May 07 2020 at 05:17):

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.

view this post on Zulip Gabriel Ebner (May 07 2020 at 07:50):

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.

view this post on Zulip Brando Miranda (May 09 2020 at 15:30):

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

view this post on Zulip Brando Miranda (May 09 2020 at 15:32):

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?

view this post on Zulip Brando Miranda (May 09 2020 at 15:39):

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.


Last updated: May 10 2021 at 18:22 UTC