# Zulip Chat Archive

## Stream: new members

### Topic: Lean's vs Coq' unfold and simpl

#### Daniel Fabian (Jul 01 2020 at 22:41):

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 (Jul 01 2020 at 22:44):

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 (Jul 01 2020 at 22:49):

`unfold`

is actually `simp`

with special settings btw

#### Mario Carneiro (Jul 01 2020 at 22:52):

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 (Jul 01 2020 at 22:53):

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

#### Mario Carneiro (Jul 01 2020 at 22:53):

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 (Jul 01 2020 at 22:53):

hidden behind yet more definitions you would have to unfold first

#### Mario Carneiro (Jul 01 2020 at 22:54):

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

#### Daniel Fabian (Jul 01 2020 at 22:54):

gotcha

#### Kevin Buzzard (Jul 02 2020 at 07:40):

@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 (Jul 02 2020 at 07:42):

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

#### Kevin Buzzard (Jul 02 2020 at 07:44):

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 (Jul 02 2020 at 08:02):

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 (Jul 02 2020 at 08:11):

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

#### Mario Carneiro (Jul 02 2020 at 08:12):

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 (Jul 02 2020 at 08:12):

I believe this is being tried in Coq

#### Mario Carneiro (Jul 02 2020 at 08:13):

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

#### Daniel Fabian (Jul 02 2020 at 10:14):

@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 (Jul 02 2020 at 10:17):

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 (Jul 02 2020 at 10:18):

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 (Jul 02 2020 at 10:19):

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 (Jul 02 2020 at 10:19):

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 (Jul 02 2020 at 10:20):

IVT doesn't use AC, therefore it is constructive

#### Mario Carneiro (Jul 02 2020 at 10:20):

this is the way I learned it

#### Daniel Fabian (Jul 02 2020 at 10:21):

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 (Jul 02 2020 at 10:22):

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

#### Daniel Fabian (Jul 02 2020 at 10:22):

@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 (Jul 02 2020 at 10:23):

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

#### Mario Carneiro (Jul 02 2020 at 10:23):

You mean for IVT?

#### Mario Carneiro (Jul 02 2020 at 10:23):

IVT doesn't need choice

#### Mario Carneiro (Jul 02 2020 at 10:23):

it's perfectly well definable in ZF

#### Daniel Fabian (Jul 02 2020 at 10:24):

it might have been for defining reals.

#### Daniel Fabian (Jul 02 2020 at 10:24):

really it's been a long time :P

#### Mario Carneiro (Jul 02 2020 at 10:24):

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 (Jul 02 2020 at 10:26):

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 (Jul 02 2020 at 10:26):

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

#### Mario Carneiro (Jul 02 2020 at 10:26):

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

#### Mario Carneiro (Jul 02 2020 at 10:27):

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

#### Daniel Fabian (Jul 02 2020 at 10:27):

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 (Jul 02 2020 at 10:28):

feel free to ask here :smile:

#### Mario Carneiro (Jul 02 2020 at 10:28):

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

#### Mario Carneiro (Jul 02 2020 at 10:29):

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

#### Daniel Fabian (Jul 02 2020 at 10:29):

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 (Jul 02 2020 at 10:30):

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 (Jul 02 2020 at 10:30):

Ah, I've been there :)

#### Daniel Fabian (Jul 02 2020 at 10:31):

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 (Jul 02 2020 at 10:31):

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

#### Daniel Fabian (Jul 02 2020 at 10:33):

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.

Last updated: Dec 20 2023 at 11:08 UTC