subject reduction

Stream: general

[Kevin Buzzard]

Jon Sterling (who is no mug) says on Twitter: "It’s funny how much is made of how Lean’s typechecking is undecidable, definitional equality intransitive, subject reduction failure… To those of us who know WHY these things fail in Lean it is quite clear that these things could be fixed in a semester’s internship project, without fundamentally changing the user experience of Lean (except, of course, to improve it)." He then goes on to sketch how to do this.

It’s funny how much is made of how Lean’s typechecking is undecidable, definitional equality intransitive, subject reduction failure… To those of us who know WHY these things fail in Lean it is quite clear that these things could be fixed in a semester’s internship project,

- Jon Sterling (@jonmsterling)

My experience is that when people who haven't written proof assistants start talking about how to "fix" a proof assistant, there is often some argument from the other side of the form "the problem with your "fix" is that actually it breaks X, Y and Z". But this is a long way from my area of expertise so I thought I may as well ask here, hoping that people who understand the subtleties might chime in. I have never had any interest in this subject reduction conversation because it seems that we have ample evidence that Lean is capable of doing proofs in hard modern mathematics (with classical axioms of course, as mainstream mathematicians believe that constructivism died 100 years ago) and thus any claim that it is "broken" in some way cannot be relevant to what I want to use Lean for. However perhaps it is relevant to others, especially if Lean 4 is wanting to broaden its remit beyond mathematics (and my understanding is that this is the case).

[Kevin Buzzard]

@Jonathan Sterling hopefully pinging the right person...(just occurred to me that you might be here)

[Martin Dvořák]

The fact that definitional equality is intransitive has nothing to do with equality being transitive in Lean, right?

[Jason Rute]

@Martin Dvořák equality is provably transitive even if definitional equality is sometimes (in rare cases) not transitive.

[Jason Rute]

I’d definitely love @Mario Carneiro’s feedback on Jon’s proposal. I’d also love to know how easy it would be to add Jon’s proposal to one of the external type checkers and just see how much of the current mathlib and core Lean 3 term proofs (if any) wouldn’t go through in his revised type system.

[Jonathan Sterling]

Kevin Buzzard said:

Jon Sterling (who is no mug) says on Twitter: "It’s funny how much is made of how Lean’s typechecking is undecidable, definitional equality intransitive, subject reduction failure… To those of us who know WHY these things fail in Lean it is quite clear that these things could be fixed in a semester’s internship project, without fundamentally changing the user experience of Lean (except, of course, to improve it)." He then goes on to sketch how to do this.

My experience is that when people who haven't written proof assistants start talking about how to "fix" a proof assistant, there is often some argument from the other side of the form "the problem with your "fix" is that actually it breaks X, Y and Z". But this is a long way from my area of expertise so I thought I may as well ask here, hoping that people who understand the subtleties might chime in. I have never had any interest in this subject reduction conversation because it seems that we have ample evidence that Lean is capable of doing proofs in hard modern mathematics (with classical axioms of course, as mainstream mathematicians believe that constructivism died 100 years ago) and thus any claim that it is "broken" in some way cannot be relevant to what I want to use Lean for. However perhaps it is relevant to others, especially if Lean 4 is wanting to broaden its remit beyond mathematics (and my understanding is that this is the case).

Hi Kevin, thanks for the ping! I generally agree about your experience with people who have some "great idea" but no experience, but in case it helps clarify things, I have extensive experience building proof assistants: I have been doing so for seven years and have built three of them. So while my familiarity with the Lean codebase itself is limited, my understanding of the subtlety of integrating various ideas in real code is deep and based on a lot of experience.

The proposal for fixing the quotients that I mentioned is not due to me, but rather to Mario Carneiro; as Mario pointed out years ago, this one thing could be fixed easily without anyone noticing. The proposal about fixing accessibility predicates is more invasive but likewise not due to me, but rather to Gilbert, Cockx, Sozeau, and Tabareau --- all of whom are proof assistant engineers extraordinaire with even more experience than me. Sozeau and Tabareau have been hardcore proof assistant builders for longer than Lean has even existed... It is perhaps worthwhile to listen to what they have to say.

[Jonathan Sterling]

My feeling about these things has always been (1) the problems are not so bad, so I don't know why people complain about them so much, and (2) the problems can be fixed and are not (contrary to what some people seem to like to say) part of a Great Tradeoff between Theory and Practice, or a tradeoff between the Goals of Lean and the Goals of Pointy-Headed Type Theorists.

My personal interest in this is not to gesticulate and demand that energy be devoted to work that will likely have a limited practical impact on Lean's users (as you say, people have been successfully working around conversion being broken for years without too much frustration). I am more reacting to some people (including but certainly not only @Kevin Buzzard) positioning what are some minor technical bugs that we know how to fix as if they are a political position, like "Maybe the type theorists need conversion to be transitive, but if we did that, we wouldn't be able to have X, Y, Z" — what I have been trying to explain for a while now is that there is no such tradeoff in play, so the only question is whether you want to devote time to fixing these bugs using the well-known solutions (which are completely compatible with Lean's goals and design to be an efficient proof assistant for classical mathematics with heavy use of proof-irrelevance).

I think it is very reasonable if nobody here wants to devote time to that, and all I would appreciate is if people stop positioning these (relatively minor) design mistakes as if they are trade-offs between theory and practice, which they are not.

[Sebastien Gouezel]

Nice to have you here, and thanks for your comments. Maybe you can enlighten me on one of your sentences:
Jonathan Sterling said:

people have been successfully working around conversion being broken for years without too much frustration

In fact, people working with mathlib have never needed to work around conversion being broken for years, because there has never been any issue related to that, as far as I can tell, so no need to work anything around. Could you explain in laymen terms what conversion being broken means (by layman, I mean for someone understanding a lot of mathematics in the traditional sense and a very basic background in logic), and how it could manifest itself? Maybe in fact it already happened but we couldn't recognize it for what it was.

[Jonathan Sterling]

Good question, it is often hard to pinpoint the cause of some issue if you don't have some experience with it, and in a setting where there is heavy use of sophisticated automation like in Lean, it can be hard to tell whether some issue is caused by a bug or if it is a non-bug caused by some subtlety of the automation...

The usual thing that happens when conversion fails to be transitive is that you will have some equation that should hold by reflexivity according to the type theory of Lean, but Lean itself rejects reflexivity here --- so to prove your goal you instead break it up into several equational reasoning steps that are each solved by reflexivity and then composed by transitivity of (propositional) equality. This can also arise in cases that do not involve a goal of the form u = v, for instance when you have a predicate of the form P(u) and you want to solve it using a proof of P(v) where u and v are (should be) definitionally equal, but conversion fails to see this.

Last time I discussed this with Kevin he mentioned to me that he has seen things like this happen, and indeed, you just work around it by rephrasing (sometimes in an artificial way) the thing you were trying to write until the typechecker accepts it.

[Sebastien Gouezel]

ok, so conversion failure is when terms should be definitionally equal but the kernel fails to see that. Yes, that might have happened -- although the issues I remember were more mistakes on my side than on the kernel's :-)

[Jonathan Sterling]

Yeah... It is often really hard to figure out whether it is my own fault or the system's fault :) This is basically why type theorists have always had the design goals of conversion to be sound (never accepts something wrong), complete (always accepts something right), and efficient (doesn't take too long); I would personally like to add predictable to this list. The reason these things are important is that it is necessary, in my world, for users to be able to reliably determine whether they are the one who made a mistake, or the kernel is the one who made the mistake. If conversion does not claim to reliably implement definitional equality, there is no "ground source of truth" and no one component can be assigned blame for a failure.

I often hear "Well, we don't use reflexivity very often, since we try not to depend too much on definitional equality; so why does it matter if some random thing an be proved using reflexivity or if it requires a more complex argument that we can automate?" This is all true (and good proof engineering practice too!), but I think what is at stake is not so much the degree of power that we endow reflexivity with (e.g. what kinds of non-trivial things can it prove) but rather, no matter how weak or strong it is, how reliable and predictable it is.

[Sebastien Gouezel]

Things that clearly happen sometimes is cases where you build a proof using tactics, the proof is really quick, but then the proof checking by the kernel is really slow (but terminates eventually). Say 0.5s for proof building, 10s for proof checking. This is not a theoretical failure of whatever, because in the end the kernel works it out, but more of an engineering problem with different heuristics used on one side and the other. These ones are really frustrating from a practical point of view!

[Jonathan Sterling]

Yeah!! These are the kinds of questions that I am increasingly interested in, because it really gets right to the point... And I think that there is a lot of room to investigate the way that various theoretical concepts (e.g. completeness) influence the pragmatic aspects of the user experience.

[Sebastien Gouezel]

And often you can work them around by changing randomly your proof until the kernel is also quick.

[Jonathan Sterling]

That's true... I've experienced that problem a LOT when using Coq — you do this great proof, and then hit Qed. and the whole computer grinds to a halt :laughing:

[Sebastien Gouezel]

(By randomly, I mean, change a rewrite to a simplifier invocation or vice-versa).

[Eric Rodriguez]

I'm not sure whether this sort of issue falls under the "subject reduction" style stuff, but there is often cases where a proof term doesn't work, but writing by exact _ for the exact same proof term does. I'm told that this is to do with metavariables, but I don't fully understand it.

[Jonathan Sterling]

Yeah, I think these issues that we are now discussing a more subtle than the subject reduction stuff, and do not necessarily reflect a bug but just some engineering tradeoffs that are very hard to negotiate :)

[Johan Commelin]

@Jonathan Sterling Could you please explain what you have in mind by adding predictable to {sound, complete, efficient}? Naively, it sounds to me that predictable would be a consequence of the other three.

[Jonathan Sterling]

@Johan Commelin Good point, I think that what you say is true in a certain sense: if conversion correctly (soundly, completely) implements definitional equality, it is of course predictable if you understand definitional equality. So maybe it would have been better for me to say that predictability more pertains to the design of definitional equality than to the implementation of conversion.

[Jason Rute]

@Jonathan Sterling How much work work do you think this is, and would it be easier to implement a proof of concept in one of the external checkers?

[Jonathan Sterling]

Good question; the first part (fixing quotients) is almost certainly very easy (but we should check with Mario), but the broader issue is quite involved (but still doable if someone actually wanted to do it). The bigger issue is that singleton elimination (not sure what people call it in Lean world) for inductively defined propositions is not really compatible with having a working conversion algorithm, and the way to work around this is that the these inductively defined propositions can be replaced with recursively defined propositions in practice, and then the need for singleton elimination disappears. The main place where these inductively defined propositions occur today is in accessibility predicates, which are part of Lean's elaboration of well-founded recursive pattern-matching definitions.

[Jonathan Sterling]

The translation of these accessibility predicates to recursively defined predicates with their associated induction principles is quite complicated, to my recollection, and this is the place where most of the work would happen. There was a partially implemented prototype of this in Coq I think by Sozeau (because the Coq people experimenting with Lean's proof-irrelevant Prop universe), but I do not think it was ever really completed.

[Jonathan Sterling]

The idea that I am describing comes from this paper IIRC, which I found really impressive: https://dl.acm.org/doi/10.1145/3290316. Although the goals of the paper pertained to integrating proof irrelevance into a type theory that does not have UIP, the ideas of this paper also apply to systems like Lean where we take UIP for granted.

[Anne Baanen]

Eric Rodriguez said:

I'm not sure whether this sort of issue falls under the "subject reduction" style stuff, but there is often cases where a proof term doesn't work, but writing by exact _ for the exact same proof term does. I'm told that this is to do with metavariables, but I don't fully understand it.

If I may come back to this slightly off topic point, replacing t with by exact t should result in the exact same term being sent to the kernel. In particular, the kernel should not be sent any metavariables at all to check. Rather, (my entirely phenomenological understanding not tested against the actual source code is that) the by exact trick tells the elaborator to postpone its work on some parts of the expression that might get stuck, and first process some other subexpressions that cause the by exacted expression to become unstuck.

[Sebastian Ullrich]

Lean 4's generalized elaboration ordering should hopefully make that particular workaround obsolete

[Jonathan Sterling]

Sebastian Ullrich said:

Lean 4's generalized elaboration ordering should hopefully make that particular workaround obsolete

Sounds cooll!! Where can I learn more about the generalized elaboration ordering? (It's ok if nothing's written, I can also look at code :) )

[Sebastian Ullrich]

https://davidchristiansen.dk/pubs/tyde2020-predictable-macros-abstract.pdf describes a similar but more elegant design, and how Lean simplifies the implementation in exchange for a bit of redundant computation :)

[Reid Barton]

This might be dumb for some reason I am missing, but it seems to me that definitions by well-founded recursion already do not compute and we are basically okay with that (for closed terms we have other methods to propositionally "compute" the value, and for open terms computation isn't likely to be useful).
In that case, how bad would it be to just discard the computation rule for acc.rec? That would fix the associated subject reduction issue right?

[Eric Rodriguez]

Sebastian Ullrich said:

Lean 4's generalized elaboration ordering should hopefully make that particular workaround obsolete

it's not perfect: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/logic.2Eequiv.2Ebasic.20mathlib4.23631/near/311869098

[Eric Rodriguez]

In my experience, acc.rec not computing has been really annoying when it actually matters; this is rarely though.

[Jonathan Sterling]

Reid Barton said:

This might be dumb for some reason I am missing, but it seems to me that definitions by well-founded recursion already do not compute and we are basically okay with that (for closed terms we have other methods to propositionally "compute" the value, and for open terms computation isn't likely to be useful).
In that case, how bad would it be to just discard the computation rule for acc.rec? That would fix the associated subject reduction issue right?

Oh, very interesting --- I didn't realize these things don't compute on their own. I'd have to think about it a little more, but your idea sounds potentially workable and nicely non-invasive. Maybe we can try it on a branch and see what happens?

[Jonathan Sterling]

Sebastian Ullrich said:

https://davidchristiansen.dk/pubs/tyde2020-predictable-macros-abstract.pdf describes a similar but more elegant design, and how Lean simplifies the implementation in exchange for a bit of redundant computation :)

Oh OK thanks! I was recently hanging out with David and he explained this idea to me. It sounds amazing.

[Sebastian Ullrich]

@Reid Barton This is basically https://github.com/leanprover/lean/pull/1803

[Reid Barton]

There is also https://github.com/leanprover-community/lean/pull/562

[Reid Barton]

I may have accidentally done some testing on a lean version which is older than that.

[Reid Barton]

OK I tested on lean-3.48.0, and

set_option pp.all true
#reduce @acc.rec ℕ (<) (λ _, ℕ) (λ x IH IH', 0) 1 (well_founded.apply has_well_founded.wf 1)

prints nat.zero (so the computation rule is still around in some form).

[Sebastian Ullrich]

Yes, since that change acc.rec computes only when applied to a syntactic acc.intro (which is how well_founded.fix_eq is derived). So if you work with well-founded recursion where well-foundedness comes from an external proof as usual, it should be basically impossible to observe this failure of transitivity unless you or a tactic explicitly unfold the major premise.

[Reid Barton]

And also the subject reduction failure from the paper Jon linked to still "works" (i.e., fails in the same way).

[Jonathan Sterling]

Sebastian Ullrich said:

Yes, since that change acc.rec computes only when applied to a syntactic acc.intro (which is how well_founded.fix_eq is derived). So if you work with well-founded recursion where well-foundedness comes from an external proof as usual, it should be basically impossible to observe this failure of transitivity unless you or a tactic explicitly unfold the major premise.

So I think this is not a good idea... haha.

[Reid Barton]

This sounds like "how to create subject reduction failure 101"

[Jonathan Sterling]

Precisely. It is absolutely a non-starter to have rules that distinguish between syntactic forms that are definitionally equivalent. Why bother putting in such a rule in the first place? It would be better to remove the computation entirely and generate unfolding axioms.

[Sebastian Ullrich]

I would have to check the code carefully, but I believe this is the natural emergent behavior from iota reduction + "do not reduce proofs". The rule specific to acc was removed.

[Sebastian Ullrich]

It certainly means that completely blocking computation like in the PR should not affect most code

[Reid Barton]

I see, so now that there is no longer special logic to reduce proofs that appear as arguments to acc.rec, it would make sense to consider that PR (or equivalent) again.

[Jonathan Sterling]

Oh, I think now I am starting to partly understanding what you folks are saying...

[Reid Barton]

If we give up the computation rule for acc, then I think one can argue (at least informally) that the type checker can operate without ever reducing a proof. In other words, proofs become "typechecker irrelevant" in the sense that once the type checker builds one, it never has to inspect it again. Here is the rough argument I have in mind:

• One reason we might need to reduce a proof is to check whether a reduction rule applies to an expression that contains it.

  • For the beta rule, if we are reducing h x and h is a proof, then the term h x we are reducing must also be a proof. In that case, we could not get into this situation in the first place (by assumption).

  • For the inductive proposition computation rules, if we are reducing T.rec ... h with h a proof, first note that there is again no problem if the elimination results in another proposition.

  So, we only need to consider propositions h : p where p supports large elimination. I will consider a few specific examples, and assume that all inductive propositions can be treated similarly. In case of doubt, one can always decline to support a computation rule (as in the case of acc).

  • If p is false then it has no constructors, so there are no computation rules to worry about.

  • If p is and q r then we should reduce and.rec f (and.mk hq hr) to f hq hr. Instead, we reduce and.rec f h to f h.fst h.snd (effectively eta-expanding h).

  • If p is x = y then eq.rec a h can only reduce when h reduces to rfl. In that case, x and y would be defeq. So instead, check whether x and y are defeq and if so reduce eq.rec a h to a. (This relies on UIP of course.)

  • If p is some other weird inductive proposition like acc then we declare that we're not going to have a computation rule for it, so there is nothing to do.

• The other situation in which we might need to reduce a proof h is to check whether it is defeq to something else. By definitional proof irrelevance, we can answer "yes" without inspecting h.

• Any other cases I forgot?

[Jonathan Sterling]

Just to be super clear on what you mean, when you say a proof you mean an element u:P where P:Prop?

[Reid Barton]

Yes, exactly

[Jonathan Sterling]

Cool! It would be a really fantastic step to get Lean to the point where it does not compute these proofs. If that invariant can be imposed, it will make a lot of other things easier to do :)

[Mario Carneiro]

It was definitely my understanding that this was the intent behind lean#568.

[Mario Carneiro]

Incidentally, this discussion came up in this week's lean 4 dev meeting (maybe @Sebastian Ullrich was reading your tweets?) and while there are a few hurdles to getting these issues fixed, I don't think we're really against it. The change to quot seems like the easy part, it would need to be tested / backported on mathlib3 first (that is, changing the type of quot from Sort u -> Sort u to Sort u -> Sort (max 1 u)) but I anticipate ~no breakage.

[Mario Carneiro]

The change to acc is quite a bit more invasive and it's not clear what approach would be best:

1. Make acc live in Type u; then well_founded is also a Type u and we would often want to use noncomputable stuff to prove it. This would still result in unpredictable computation of well-founded definitions.
2. Make acc not do reduction of proofs, as in lean#568. This makes well-founded definitions almost never compute, and this is what is currently used by mathlib3. It's still not quite as strong as @Reid Barton 's plan, since it would still reduce acc.rec_on ... (acc.intro ..).
3. Make acc never reduce. This would make well-founded definitions never compute, and matches Reid's plan.

I think that no matter what, we would want some tactic or mechanism for evaluating well founded definitions. I think that this is a major missing piece in lean's tactic story.

[Mario Carneiro]

@Jonathan Sterling

[Jonathan Sterling]

I'm really excited to here there is interest and internal discussion!! I agree with you that figuring out the right thing to do with acc is a bit tricky. Just to clarify, the three options you describe are OK, but the option I suggested is different — my proposal will allow wf-definitions to compute definitionally, without having any of the downsides. But my proposal is much harder to implement than any of your three, so I think it would be a good idea to start where you're at and see if one of those can work out well for Lean and its existing codebase.

[Jonathan Sterling]

I agree that having some kind of tactic mechanism to evaluate wf definitions should be a priority :)

[Junyan Xu]

I'm not an expert in type theory, but I did once investigate into some issues around docs#acc and dig up some old PR/issues from the early days of Lean 3.

[Junyan Xu]

Sebastien Gouezel said:

Things that clearly happen sometimes is cases where you build a proof using tactics, the proof is really quick, but then the proof checking by the kernel is really slow (but terminates eventually). Say 0.5s for proof building, 10s for proof checking.

Anne Baanen said:

Eric Rodriguez said:

I'm not sure whether this sort of issue falls under the "subject reduction" style stuff, but there is often cases where a proof term doesn't work, but writing by exact _ for the exact same proof term does.

... the by exact trick tells the elaborator to postpone its work on some parts of the expression that might get stuck, and first process some other subexpressions that cause the by exacted expression to become unstuck.

I've also once observed that adding by apply could sometimes speed up elaboration (not kernel checking) significantly in #14967

[Mario Carneiro]

Jonathan Sterling said:

I'm really excited to here there is interest and internal discussion!! I agree with you that figuring out the right thing to do with acc is a bit tricky. Just to clarify, the three options you describe are OK, but the option I suggested is different — my proposal will allow wf-definitions to compute definitionally, without having any of the downsides afaict (though personally I am not so sure that definitional computation with well-founded definitions is always desirable — it can sometimes be a bit hard to control). But my proposal is much harder to implement than any of your three, so I think it would be a good idea to start where you're at and see if one of those can work out well for Lean and its existing codebase.

To be clear, I don't actually know what you specifically have in mind here. You have only hinted that there is a better way here and in your twitter thread, and without the details it is hard to assess what the fallout is.

But more importantly, this issue is decidedly low priority, and people making noise about it can actually be harmful especially considering how much it is a non-issue in practice. I think it is great if people investigate potential solutions, if you would like to work on it or find someone else to work on it, but this is definitely a "merely theoretical" problem for we have long since come up with good enough workarounds so that we can move on to more pressing things.

[Mario Carneiro]

my proposal will allow wf-definitions to compute definitionally, without having any of the downsides afaict

By the way, this already sounds impossible given the results of my thesis. Because you can construct a wf-definition whose definitional computation simulates a turing machine. You have to break at least the type of acc.rec or proof irrelevance or the iota rule for some inductives and all of those options would have some real-world consequences

[Reid Barton]

I also didn't understand from the paper what the plan would be to replace definitions by wf recursion with.

[Chris Hughes]

I do find it annoying in Lean4 when a definition using pattern matching that is compiled to something with well_founded doesn't reduce. I think it would make sense for these automatically generated well founded proofs to use a Type version of Acc so that they do unfold. I don't think these automatically generated proofs use any axioms.

[Sebastian Ullrich]

No axioms probably, but they do case on predicates such as prod.lex that do not eliminate into Type. So either you need to lift them into Type as well or add some other sufficient side condition such as decidable equality on the type of the first element in order to fix acc instances.

[Mario Carneiro]

They also use a lot of arithmetic theorems on nat, because of simp_arith or its lean 3 approximation for reasoning about SizeOf expressions. IIRC these theorems do use propext in lean 3

[Chris Hughes]

Will using propext be a problem? The natural number lemmas will mainly be used for proving inequalities, not accessibility of a relation right? So it should be okay?

[Mario Carneiro]

Yes, propext will block computation if you require that the proof be reducible to an acc.intro constructor application

[Mario Carneiro]

and propext gets pulled in to all sorts of theorems because of simp and rw

[Mario Carneiro]

I don't think it would be a good thing for the library if we have to work under the constraint of no propext

[Mario Carneiro]

I would much rather set things up so that all well founded functions can compute in some sense, even if not by defeq

[Chris Hughes]

I definitely agree we need well-founded stuff to compute somehow. There're two separate problems here, closed terms and non-closed terms.

I'd like closed terms to compute regardless of axioms in the proof

For non-closed terms there is always going to be a problem about how far to unfold, so we can't have nice behaviour on non-closed terms except in certain cases, and I think a reasonable expectation is that things defined using pattern matching should unfold in the expected way

[Chris Hughes]

Mario Carneiro said:

I would much rather set things up so that all well founded functions can compute in some sense, even if not by defeq

I think I might come in and defend def-eq here. def-eq has the advantage that you don't need to use casts. I think that this is not a major difference for the sorts of things that we do in mathlib, but we really don't use any inductive types more complicated than a list. I'm surrounded by people trying to do compiler related things in Lean, and Lean has some shortcomings here compared with Coq, and I wouldn't be at all surprised if well-founded definitions not unfolding by def-eq caused someone a major headache somewhere.

[Reid Barton]

acc-in-Type doesn't require any special support does it? Aside from in the equation compiler I suppose.

[Reid Barton]

I guess I'm not really sure what path you're advocating for here

[Chris Hughes]

I'm advocating for using acc in Type for automatically generated well foundedness proofs that could presumably be done quite easily without axioms. Stuff like this is compiled to WellFounded.fix in Lean4 currently, and presumably it doesn't need axioms to prove this even if it does use them. Hopefully both the theorems below should be provable with rfl at some point, but not currently.

inductive T : Type
| mk : List Nat → T

open T

def thing : T → T
| mk (_ :: ns) => thing (mk ns)
| x => x

example (n : Nat) (ns : List Nat) :
  thing (mk (n :: ns)) = thing (mk ns) := rfl --fails

example : thing (mk [0]) = mk [] := rfl --fails

[Jonathan Sterling]

Mario Carneiro said:

Jonathan Sterling said:

I'm really excited to here there is interest and internal discussion!! I agree with you that figuring out the right thing to do with acc is a bit tricky. Just to clarify, the three options you describe are OK, but the option I suggested is different — my proposal will allow wf-definitions to compute definitionally, without having any of the downsides afaict (though personally I am not so sure that definitional computation with well-founded definitions is always desirable — it can sometimes be a bit hard to control). But my proposal is much harder to implement than any of your three, so I think it would be a good idea to start where you're at and see if one of those can work out well for Lean and its existing codebase.

To be clear, I don't actually know what you specifically have in mind here. You have only hinted that there is a better way here and in your twitter thread, and without the details it is hard to assess what the fallout is.

But more importantly, this issue is decidedly low priority, and people making noise about it can actually be harmful especially considering how much it is a non-issue in practice. I think it is great if people investigate potential solutions, if you would like to work on it or find someone else to work on it, but this is definitely a "merely theoretical" problem for we have long since come up with good enough workarounds so that we can move on to more pressing things.

Re: "people making noise about it can actually be harmful ", to be very clear, I would have been totally silent about it if I had not seen several unprovoked rants about it by Kevin Buzzard in the past year pushing disinformation about the issue. So if you are looking to keep the issue quiet, I would certainly recommend that you look to your camp first before coming after outsiders who are trying to correct the record. As I've said many times, we don't have any problem with you choosing that this is not a priority. We do have problems with repeated statements that spread disinformation on a subtle topic that concerns us. It is telling that people in this thread are saying things like "it's a non-issue, I've never encountered it" or whatever, but then admit that they actually have no idea what the consequences of it are, and admitting "oh yeah, that's probably happened" when I explain what the consequences are.

Regarding your thesis, the thing I describe is NOT impossible and it is not contradicted by your thesis. What is true is that you cannot use inductively defined accessibility predicates anymore; these can be replaced, however, with recursively defined ones. This is detailed in the paper I linked earlier in the thread. It is still unclear what the fallout is, which is why I did not advocate you to just blindly jump into it, and favored the more conservative ideas expressed in this thread by others (like Reid's comments on deleting some problematic rules, at the expense of some computation --- which sounded reasonable to me).

[Jonathan Sterling]

So my first suggestion would be to (1) stop spreading disinformation, and/or (2) start communicating with the team who wrote that paper. It's ok if this isn't a priority, but you must silence those who are spreading disinformation if you don't want it to come back to you.

[Martin Dvořák]

Well, that escalated quickly.

[Jonathan Sterling]

I apologize if I have ruined this thread, I felt that there was a lot of very productive discourse in it so far. I was reacting to Mario characterizing my intervention as "harmful", when I feel the harm began when disinformation was allowed to go out unchallenged. I have always felt that Mario's interventions in the past were of a very positive nature, as his writings clarified many of the underlying issues; my own comments were essentially based on Mario's.

I hope we can work collaboratively to a better mutual understanding of these issues, informed by the goals of the Lean project (which I certainly am not in a place to dictate, nor would I even advise paying too much attention to these metatheoretic issues when you've got more fun stuff to do).

[Jason Rute]

As for disinformation, which I may have spread, I’m not clear on the very simple question: does the current breakage of subject reduction effect Lean users? I’ve heard two conflicting things: (1) the only way to encounter this issue is to come up with a contrived example using something like acc and this just doesn’t occur in practice. (2) That it does occur in practice occasionally and when it does, people find workarounds, possibly painfully.

I think it is clear that not everything that should be defeq the kernel can compute in a reasonable time, but it is hard to know if it is because of SR/transitivity or just a slow kernel. (Mario also points out that if a=b and b=c are defeq and fast to compute, it may be that a=c maybe be really slow to compute and will timeout. I assume fixing transitivity and SR won’t fix this, right?)

[Jonathan Sterling]

Thanks @Jason Rute for bringing us back onto track :) I think (2) is probably the case (based on the conversations I've had with Lean users both here and elsewhere), but I would guess that the workaround are not too painful in most cases --- if they were very painful (rather than more like a little ant-bite, which is what I think they are like), we would probably be hearing more about it. So based on this, my estimation is that it might not be worthwhile to try and fix this, but it also would not be the hardest thing in the world to fix it. It is certainly not the case, as I have demonstrated, that fixing it would contradict the goals of Lean to have quotient types and proof irrelevance. It might contradict the goals of "not wasting time on stuff that doesn't matter too much", which I totally respect ;-)

Regarding your second paragraph, that is an excellent point, and it is indeed the case that whether "fast conversions" are closed under composition is orthogonal to the question of whether conversions in general are closed under composition. If the issues under discussion were fixed, it would still be the case that there are some things that fast when broken up into steps, but slow when composed --- and I think it is unclear whether that could ever be fixed, but it would certainly be a very deep and hard research question for someone to investigate.

[Jason Rute]

By the way, here is the previous discussion on subject reduction: #general > What is the subject reduction debate?

[Jason Rute]

Also, here is a stack exchange question on the matter. I tried to give what I felt at the time was my best answer given what I knew. Anyone is free to correct the record by adding their own answer, commenting on mine, or persuading me to edit (or delete) my answer: https://proofassistants.stackexchange.com/a/1194/122

[Jonathan Sterling]

I thought your PA.SE answer was mostly fine (for instance, your operative comment about syntactic subsingleton elimination for acc is correct!), with the caveat that the failure of a particular normalization algorithm does not imply that you cannot have a computational model --- as you know, your VM provides a computational model of some sort, and we can also do similar things on the mathematical side.

[Jonathan Sterling]

P.S. In case it did not come out in this thread, I want to say that I have so much admiration for Lean and especially the very innovative things happening in Lean 4. I can't believe my eyes when I see the macro tooling, custom elaboration, and editor integration, just to give a couple examples...

I have long felt that there was so much amazing and exciting work happening in Lean that there was no need for boosters of Lean to try and argue "against" other tools, or (much more bafflingly), "against" the idea of informing implementation through type theory (which I observed in the discussion of subject reduction, rhetorically transforming trade-offs that are really about time/effort into (non-)trade-offs that purport to be about theory/practice). The work speaks for itself, and it's amazing.

[Mario Carneiro]

@Jonathan Sterling I understand how you can translate some inductive predicates into recursive ones, but to do this for acc itself seems to invoke a regress because the recursion needs to be well founded somehow. Can you give a concrete example?

[Jonathan Sterling]

Thanks for your question, @Mario Carneiro. I will think about it, and also double-check that I have not made a mistake. I believe the general form of acc is not translatable in this sense, but that many common instances well-founded recursion (that would arise from defining recursive functions in practice) would be — of which the account of le (S m) n is the prototype. I'm sorry for adding to the confusion by making it sound like you could do this in general as opposed to case-by-case.

[Jonathan Sterling]

So part of the 'fallout' that would have to be investigated is to see how such a constraint really affects the existing library code.

[Jonathan Sterling]

I think that ultimately the idea of @Chris Hughes in this thread is probably the most broadly applicable and practical one.

[Jonathan Sterling]

Zooming out, if the general accessibility predicate is Type-valued, we still do not lose too much. There will be many cases (especially in the case of lexicographic induction) where a Prop-valued one can be defined, and you will obtain some additional definitional equalities in that case, but I am very doubtful that a Type-valued acc R predicate would be worse to use in practice than what is currently there. The VM can still be instrumented to erase it, if you want — there is a lot of literature on analyses that can automatically erase such things that I could suggest, but it is reasonable to just special-case it at first.

[Sebastian Ullrich]

Erasure at least is not a problem because we send the version of the definition before eliminating syntactic recursion to the code generator

[Jonathan Sterling]

Sebastian Ullrich said:

Erasure at least is not a problem because we send the version of the definition before eliminating syntactic recursion to the code generator

very smart idea!

[Jeremy Avigad]

I am sorry to have arrived late to this party. I have been trying to catch up on the discussion and read enough of the Gilbert et al. paper to at least have a general sense of what is being proposed. That paper describes an extension to MLTT (as well as an impredicative version thereof), and then proofs of consistency relative to ETT (resp. Voevodsky's resizing axioms). How does this translate to Lean?

My understanding is that the idea is to eliminate some of the problematic features of Lean's foundation (an elimination principle from Prop to type or definitional proof irrelevance or maybe both?), and then do something to patch the places in the library where these are currently used. What's not clear to me is whether this involves adding something new. In other words, it is not clear to me whether the proposal is to weaken Lean's type theory (by ruling out things that were allowed before) or modify it (by also allowing other things that were not allowed before or not there before). @Jonathan Sterling I'd be curious to see a sketch of the proposal, even if the details aren't fully worked out.

By the way, long ago, when Leo was first working out the mechanisms for handling well-founded recursion in Lean, he also experimented with putting acc R in Type. He characterized this as providing the recursive function with "fuel" to carry out the computation. My vague memory is that there were problems with that beyond merely adding irrelevant data to a computation, but I don't remember the details and I may be misremembering entirely. I'd be happy to see a solution like that if it could be made to work, if there are clear principles that dictate what is really computationally relevant and what can be erased in code extraction.

[Chris Hughes]

I did a bit of an experiment with the Acc in type idea. The code is here. It's not as good as it seems. The expected equalities are not definitional. Maybe by very carefully defining the proof that lt is well_founded on the natural numbers they could be made to be definitional. Probably it would require a carefully defined lt in Type with carefully written proofs of n < n + 1 etc to get the desired definitional equalities.

[Chris Hughes]

To be clear, the equality fib (n+2) = fin n + fib (n+1) is not definitional in my code.

[Chris Hughes]

Of course, this will still all compute on closed terms.

[Reid Barton]

I feel like it's unreasonable to expect that definitional equality but I don't know exactly why. Does it work in Coq?

[Jeremy Avigad]

Chris, thanks for working that out!

Isn't this whole discussion about definitional equality? If we don't care about that, we can use any definitions that work, even nonconstructive ones, and we can tune code extraction to do whatever we want it to do. That is Isabelle's approach:
https://isabelle.in.tum.de/dist/Isabelle2022/doc/functions.pdf
https://isabelle.in.tum.de/dist/Isabelle2022/doc/corec.pdf
The underlying definitions of the functions are arbitrary (as long as they satisfy the defining equations), and there is no concern with matching them up with any built-in notion of computation in the type theory.

[Chris Hughes]

Reid Barton said:

I feel like it's unreasonable to expect that definitional equality but I don't know exactly why. Does it work in Coq?

I think it gets stuck on a if n + 0 = n + 1 then _ else _

[Chris Hughes]

Jeremy Avigad said:

Chris, thanks for working that out!

Isn't this whole discussion about definitional equality? If we don't care about that, we can use any definitions that work, even nonconstructive ones, and we can tune code extraction to do whatever we want it to do. That is Isabelle's approach:
https://isabelle.in.tum.de/dist/Isabelle2022/doc/functions.pdf
https://isabelle.in.tum.de/dist/Isabelle2022/doc/corec.pdf
The underlying definitions of the functions are arbitrary (as long as they satisfy the defining equations), and there is no concern with matching them up with any built-in notion of computation in the type theory.

I think some people do care about definitional equality, even if those people aren't mathlib contributors. It came up in a toy project. I had where I wanted these things to be definitional equalities because I was using dependent types and didn't want to use casts.

[Reid Barton]

This paper seems to be related: https://hal.archives-ouvertes.fr/hal-03857705v2

[Chris Hughes]

Sorry to revive an old thread, but I couldn't figure out what @Jonathan Sterling's proposal was.

Is there a way of getting something like the below fibonacci definition or other recursive definitions on inductives where you call the function on a subtree of the current inductive tree to satisfy their defining equations definitionally. I think the proposal is that maybe you can define some clever relation that satisfies the property in this paper and the function can be defined by induction on that, but I couldn't figure out how to do it if that is the proposal.

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

Incidentally this definition does unfold nicely in Lean right now, because underneath it's defined using Nat.below and Nat.brecOn, which are autogenerated, but I wrote out pretty much the definitions below

def Nat.below {motive : ℕ → Sort _} : ℕ → Sort _
  | 0 => PUnit
  | n+1 => PProd (motive n) (@Nat.below motive n)

def Nat.brecOnAux {motive : ℕ → Sort _} :
    (t : ℕ) → ((t : ℕ) → @Nat.below motive t → motive t) → @Nat.below motive (t+1)
  | 0, f => ⟨f 0 ⟨⟩ , ⟨⟩⟩
  | t+1, f =>
    let ih := Nat.brecOnAux t f
    ⟨f (t+1) ih, ih⟩

def Nat.brecOn {motive : ℕ → Sort _} (t : ℕ)
    (f : ((t : ℕ) → @Nat.below motive t → motive t)) : motive t :=
  (@Nat.brecOnAux motive t f).fst

I don't know who came up with this Nat.below idea, but it looks fairly general.

[Jannis Limperg]

The below construction is probably from this paper. It indeed applies to any inductive type.