Lean's vs Coq' unfold and simpl

Stream: new members

[Daniel Fabian]

I've started going through the Software Foundations book series and I've got some observations and one question:

First of all, it seems very much like Lean was written for mathematicians whereas Coq was written for software verification. Even though their core calculi are virtually indistinguishable (modulo explicit vs. implicit universe levels, but I'm not sure how much it matters in practice), the proofs have a very different feel to them.

When proving things in Lean, it feels like most of the time you're hunting for the appropriate lemma to make progress (much like a normal math proof), in Coq it seems like you tend to do a lot more computationally, relying on the specific definition of a function and then letting beta-reductions do a lot of progress.

This leads to very asymmetrical and somewhat "unmathematical" feeling proof. E.g. with my mathematician's hat on, [] ++ l and l ++ [] should both be l reasoning that [] is the neutral element of list concatenation. Whereas computationally, one of them is trivial and one of them hard, requiring a proof by induction. In Coq you might prove that a number is a prime by defining a function is_prime : nat -> bool, perhaps have a lemma forall n, is_prime = true <-> prime n and then the "proof" would be "show is_prime 101 = true by reflexivity".

Furthermore Coq's very strong stance to rely much more heavily on constructive logic and computation for proofs makes the systems feel so incredibly different in practice.

Now for my questions; how are Lean's and Coq's unfold related? It seems to me that in Coq unfold literally unfolds a definition, whereas in Lean that's often not supported. E.g. if you define a function by cases (equation compiler, presumably), it won't let you unfold at all until you've already set up the preconditions such that you match a particular case at which point unfold behaves more like Coq's simpl (Lean's simp is a completely different beast applying all kinds of fancy lemma and transformations, much more complex than Coq's simpl.)

Do we have any basic unfold that can unfold definition of pattern matching? And do we have something to do beta reduction as a tactic?

[Reid Barton]

I'm not familiar with Coq's tactics, but if you want to literally just unfold a definition in Lean I think that's what delta does.

[Mario Carneiro]

unfold is actually simp with special settings btw

[Mario Carneiro]

While we could do something similar, it's not trivial in lean to obtain the equivalent of unfold on a coq Fixpoint definition, because lean doesn't have a fix combinator like coq

[Daniel Fabian]

is that a consequence of the equation compiler for defining functions by pattern matching?

[Mario Carneiro]

I think in coq you would first unfold to expose the match and then do case analysis, but in lean you have to do it the other way around because if you literally just delta it then you get this horrible mess of recursors

[Reid Barton]

hidden behind yet more definitions you would have to unfold first

[Mario Carneiro]

It's the other way around - the equation compiler defines functions using recursors because lean doesn't have fix

[Daniel Fabian]

gotcha

[Kevin Buzzard]

@Daniel Fabian what you say is interesting because I'm pretty sure Leo was not specifically targeting mathematicians when he wrote Lean. I had always assumed that the reason mathematics was growing faster in Lean than Coq was just that the user base was different and that this was perhaps just a historical fluke

[Kevin Buzzard]

The fact that nonconstructivism deeply permeates even undergraduate mathematics might be a reason though

[Kevin Buzzard]

The IVT is a nonconstructive theorem about a noncomputable object and these issues are never flagged to mathematics undergraduates when they are taught IVT in their first year. We don't care in mathematics departments

[Patrick Massot]

Daniel Fabian said:

First of all, it seems very much like Lean was written for mathematicians whereas Coq was written for software verification. Even though their core calculi are virtually indistinguishable (modulo explicit vs. implicit universe levels, but I'm not sure how much it matters in practice), the proofs have a very different feel to them.

When proving things in Lean, it feels like most of the time you're hunting for the appropriate lemma to make progress (much like a normal math proof), in Coq it seems like you tend to do a lot more computationally, relying on the specific definition of a function and then letting beta-reductions do a lot of progress.

I think what you wrote is literally false but of course it comes from something very real. First I don't think that Lean was written specifically for mathematicians. This would have been emphasized in the early papers and presentation you can find on the official website. Everything I see mention both kinds of applications. And I don't think there is much technical difference that explain what you see, although my understanding is that Coq is better at reflexivity heavy lifting. I think that what you describe is mostly a difference between user communities and libraries. It is well known that mathcomp loves definitional equality, and I guess Software Foundation also does. And of course they are deeply indoctrinated into constructivism, although this is slowly changing. But Coq itself is perfectly capable of being classical. In principle someone could go and write mathlib in Coq and it would feel Lean-like.

[Mario Carneiro]

I think setoid hell is an issue you would run into if you tried to just write mathlib in coq

[Mario Carneiro]

although perhaps it would be possible to live with quot.beta only being a propositional equality, in which case you can get away with a simple axiomatic definition of quotient types

[Kevin Buzzard]

I believe this is being tried in Coq

[Mario Carneiro]

it would also be interesting to know how well coq typeclass inference performs on typical mathlib style typeclass problems

[Daniel Fabian]

@Patrick Massot I find the choices Leo made quite interesting, to be honest. Z3 is after all heavily used in software verification in some pretty advanced projects. F* for instance is heavily automatised and it lets you prove whole invariants about programs very easily, often by merely stating them. Lean compared to that is very manual. Yet, Leo frames it at least in some earlier presentations as a next step up from Z3 to make software verification more scalable and robust.

Maybe it's that TPIL and Logic and Proof are specifically written with a math background whereas Software Foundations are written with a software verification background.

I was not asserting btw. that Lean and Coq are technically very different, but that the user experience, syntax choices, etc. give it a very different feel to it. And those things very much influence what can be done in a programming language in practice. As an analogy, even though to a first approximations all programming languages are equal in the sense that they are turing complete, assembly can be used for very, very different things than, say Java. Which in turn attracts a different community and reinforces the differences.

For instance this fixpoint operator vs recursors / equation compiler difference feels like something, we wouldn't care about unless we are trying to characterise the technical differences between the systems, yet it shows up naturally after trying to do case analysis on a piece of code that uses pattern matching.

Also interesting is the choice to separate computable from non-computable parts in Lean. So you may have a function which has computational meaning and prove a sophisticated property about it in a highly non-constructive way and Lean is quite happy with that.

It certainly feels valuable to experience theorem proving from both worlds as it helps building perspective ;-)

[Mario Carneiro]

I don't know enough about coq to say if this isn't already the case, but I imagine that Coq could fairly easily present recursive functions by pattern matching similar to how lean does it, which is probably more influenced by agda/haskell style

[Mario Carneiro]

The fact that you first unfold one iteration of the fix and then break up the match seems like exposing implementation details on coq's part

[Mario Carneiro]

the advantage of lean's approach is that you can't really tell how the recursive function is implemented, and indeed this is taken advantage of so that lean can support multiple compilation strategies depending on how the recursive calls look

[Daniel Fabian]

Kevin Buzzard said:

The IVT is a nonconstructive theorem about a noncomputable object and these issues are never flagged to mathematics undergraduates when they are taught IVT in their first year. We don't care in mathematics departments

When they were mentioning the AC to us, they did flag it up as being non-constructive, not really saying it was problematic, necessarily, though. When I learnt about intuitionistic logic, by that time, em was so ingrained that I found it quite difficult to have an intuition what is and isn't entailed, though, intuitionistically.

[Mario Carneiro]

IVT doesn't use AC, therefore it is constructive

[Mario Carneiro]

this is the way I learned it

[Daniel Fabian]

Mario Carneiro said:

the advantage of lean's approach is that you can't really tell how the recursive function is implemented, and indeed this is taken advantage of so that lean can support multiple compilation strategies depending on how the recursive calls look

This is in it's own right makes constructive reasoning harder, though. Precisely because you don't know the implementation details.

[Mario Carneiro]

well, lean does expose the fact that the equations it generates are definitional equalities

[Daniel Fabian]

@Mario Carneiro I remember the context when AC first came up. might have been the continuity, actually for picking a big enough N.

[Mario Carneiro]

at least, when they are (they are not necessarily in the case of well founded recursions)

[Mario Carneiro]

You mean for IVT?

[Mario Carneiro]

IVT doesn't need choice

[Mario Carneiro]

it's perfectly well definable in ZF

[Daniel Fabian]

it might have been for defining reals.

[Daniel Fabian]

really it's been a long time :P

[Mario Carneiro]

but the constructiveness meant by not using AC is more like "we have an explicit description of what we are talking about" so it includes things like the busy beaver function but not a well order of the reals

[Daniel Fabian]

And anyway, I expect in 5 years time, Lean will have more powerful tactics that will let us not think about fixpoint vs. recursors as some of the reasoning is fairly mechanical, anyway.

[Mario Carneiro]

I would say that lean has had that since almost the beginning

[Mario Carneiro]

the equation compiler is just about as powerful as fix/match

[Mario Carneiro]

I think it is noticeably less powerful than agda pattern matching in a few places

[Daniel Fabian]

I don't know about that, I've certainly run into loads of trouble trying to use match expressions inside of tactics mode.

[Mario Carneiro]

feel free to ask here :smile:

[Mario Carneiro]

But I think this might be a result of the clash between Coq tactics and Agda terms

[Mario Carneiro]

lean strikes a decent balance between them but they really are separate languages and they don't communicate too much

[Daniel Fabian]

I will at some point fight my way through that bloody rb-tree, lol. But I have to say I did hit a brick wall twice on it now in Lean, both intrinsically and extrinsically. I just somehow can't do the distinction by cases efficiently in Lean and since it's something like 125 cases, I'm not going to spell it out by hand :P

[Daniel Fabian]

maybe I'll be able to ask a more concrete thing, but it really boils do to the balance operation being defined as an 8-line pattern match, very simple.

[Mario Carneiro]

Ah, I've been there :)

[Daniel Fabian]

but it corresponds to 100+ cases and and I haven't been able to tell lean's tactics to the work for me.

[Mario Carneiro]

You shouldn't get that many cases if you set things up well, use lots of intermediate functions and such

[Daniel Fabian]

Ya, I'll work my way through Software Foundations, maybe I'll learn something that'll be useful in this context, specifically.
I'll get it done, eventually.