opaque recursion definitions break mergeSort decidability

Stream: lean4

[Tristan Figueroa-Reid]

I decided on Finset.sort which broke in the recent Lean 4.19 update. This is an MRE of the issue:

example : ([1] : List Nat).mergeSort (· ≤ ·) = [1] := by
  unfold List.mergeSort
  decide +kernel

/-
tactic 'decide' failed for proposition
  ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)) = [1]
since its 'Decidable' instance
  instDecidableEqList ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)) [1]
did not reduce to 'isTrue' or 'isFalse'.

Reduction got stuck at the 'Decidable' instance
  ([1].mergeSort fun x1 x2 => decide (x1 ≤ x2)).hasDecEq [1]
-/
example : ([1] : List Nat).mergeSort (· ≤ ·) = [1] := by
  decide +kernel

[Eric Wieser]

In the past I think the suggestion was to keep these functions defined in a way that is reducible, and then use csimp to link them to their irreducible optimized versions.

[Eric Wieser]

I think src#List.mergeSort hasn't changed, but the rules for reducibility have

[Tristan Figueroa-Reid]

Eric Wieser said:

In the past I think the suggestion was to keep these functions defined in a way that is reducible, and then use csimp to link them to their irreducible optimized versions.

I do believe that mergeSort already has a irreducible optimized version linked by csimp

[Tristan Figueroa-Reid]

I believe the rules for reducibility changed (which broke this well-founded definition of List.mergeSort) changed in #5182.

[Tristan Figueroa-Reid]

I don't know much of anything regarding reducibility with csimp, but given that List.mergeSort already has a csimp-linked tail-recursive definition, would it make sense to mark it as semireducible?

[Tristan Figueroa-Reid]

Actually, should decide follow csimp marked theorems?

[Eric Wieser]

I don't think that would be useful, the runtime-optimal version is less likely to reduce well

[Eric Wieser]

And following them in reverse would also not be very useful, because the runtime version should never appear in any theorem statements

[Joachim Breitner]

Copying from a discussion with @Bhavik Mehta right now

Oof, is there really no way of making it temporarily semireducible after the fact for decide?

Yes, and after having tiptoed around this issue for a while I believe that reducing proofs in the kernel (as it necessary for well-founded recursion) is just too big of a footgun to be allowed. It may have worked ok in a number of cases so far, but every so often it goes horribly wrong (kernel heartbeat timeout, hard to debug).
Also with the upcoming module system we really want proofs to be irrelevant, so that they can be omitted from interface files, maybe even omitted from downloaded olean etc.
So the conclusion is that well-founded recursion should only be used when you really only care about the classical existence of a function with that specification, and never when you want to get any kind of useful defeqs.

So conversely, if you have a function that you want to have useful defeqs, then don't use well-founded recursion. One way is to use a helper definition that is built to reduce nicely, e.g. using fuel, like I did here: https://github.com/leanprover/lean4/pull/7558

This should be possible for any function that's currently defined by wf recursion with a single Nat measure.

We could even consider having a termination_by fuel … variant that uses that construction internally.

(I don’t know how well this fares when reducing larger inputs, because I assume that although it won’t reduce proofs, the kernel will still construct a large proof for the fuel argument, so it may not scale to large number of recursions either.)

Another alternative is not to use decide, but rewriting, when doing the proof. But I understand that our rewriting tractics (simp, rw) are not great for the use case of “do cbv normalization by rewriting” yet. I did some steps in that direction in https://github.com/leanprover/lean4/pull/5977, but it wasn't quite convincing yet.

I agree that this is all a bit unsatisfactory until we are weaned off reducing wf proofs…

This is orthogonal, but I don't actually understand why reducing defs which use wfrec needs reduction of proofs at all?

Defs using well-founded recursion use WellFounded.fix which is essentially structural recursion on the Acc predicate, and to reduce these definitions by more than one step, the proof of Acc x y needs to be reduce to the Acc.intro constructor. Depending how your well-founded definition is defined, this may involve reducing Nat.le or stuff like that, and can be very expensive, exponential even.

You can kick the can down the road by identifying all affected functions, define them as semireducible, and then right afterwards use attribute [irreducible] foo. This gives you the old behavior and you don’t need to fix all at once.

It works sometimes (for example, for technical reasons one unfolding is actually free), and when it works it’s annoyingly useful. But it shot a few legs, so we’d really like to pretend it never worked at all :-)

[Mario Carneiro]

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

[Edward van de Meent]

(what is Acc reduction?) i should read :see_no_evil:

[Aaron Liu]

Mario Carneiro said:

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

Why

[Joachim Breitner]

Mario Carneiro said:

If we really actually make Acc reduction not work, maybe we can finally actually fix the core reason why lean has undecidable typechecking and rip this out of the kernel?

Just to avoid confusion, what precisely is “this”?

(I can’t answer your question, but maybe we can at least make it an option by eventually removing all uses of reducible wf rec.)

[Mario Carneiro]

I'm thinking to change the inductive schema so that types like Acc do not have an iota rule, but possibly give you an iota axiom instead

[Mario Carneiro]

which is hopefully enough to prove WellFounded.fix

[Joachim Breitner]

While we are at it: What do you think of https://github.com/leanprover/lean4/issues/5234, @Mario Carneiro ?
Summary: When the measure of wf-recursion is just one Nat (not lexicographic, not a different order), use a Nat-specific fix-point operator that is a drop-in replacement for WellFounded.fix, but implemented by using Nat.rec on fuel that’s initialized by the measure.

It seems that this would be simple to implement, would let decide work for many (but not all) wf-rec function, and would avoid most (bot not all) “reduction bombs” because for neutral arguments, the intial fuel is neutral and reduction gets stuck, as it should.

[Mario Carneiro]

I don't see why to specialize on Nat here, you can do the same thing for any inductive type

[Mario Carneiro]

I'm sad about the general direction, it's making well founded recursion turn into a big bugaboo and discouraging people from using it

[Joachim Breitner]

I’m not particularly happy either (besides that this will make proofs even more irrelevant, which is great for the upcoming module system, smaller olean, less recompilation, and that we hopefully get rid of this sometimes hard-to-debug “reduction bombs”)

[Mario Carneiro]

I definitely think proofs should be irrelevant but I don't see why that means wf recursion has to suck

[Mario Carneiro]

this should never have been implemented by reducing proofs in the first place

[Joachim Breitner]

Mario Carneiro said:

I don't see why to specialize on Nat here, you can do the same thing for any inductive type

Can you? Maybe with an inductive type where the < relation that’s picked up by WellFoundedRelation contains the subterm-relation, unless I am missing something. Do you have concrete examples in mind?

[Mario Carneiro]

I was thinking you would not use a well founded relation at all, you would just use the subterm relation on an inductive type

[Joachim Breitner]

Mario Carneiro said:

this should never have been implemented by reducing proofs in the first place

What are the alternatives? We once discussed a world where Acc.rec reduces always, without looking at theAcc proof, but doesn’t that make the problem of the kernel reducing things ad infinitum even worse?

[Mario Carneiro]

you could reduce only closed terms

[Mario Carneiro]

I think we should kind of set Acc aside, because we actually care more about WellFounded (they are equivalent in strength) and WellFounded doesn't have the issue of a monotonically increasing proof term during reduction

[Mario Carneiro]

I think we're just reinventing fix + match here, we should just check what Rocq does

[Joachim Breitner]

Rocq has an in-kernel termination checker (the “guardedness checker”), AFAIR

[Mario Carneiro]

yeah but that's sort of separate from this

[Mario Carneiro]

the question is more about when reduction happens

[Joachim Breitner]

Mario Carneiro said:

I think we should kind of set Acc aside, because we actually care more about WellFounded (they are equivalent in strength) and WellFounded doesn't have the issue of a monotonically increasing proof term during reduction

I’m sorry, but I think you have to spell this out some more for me. Is there another definition of WellFounded that doesn’t go through Acc and allows for recursion somehow?

[Mario Carneiro]

I think the definition of WellFounded is an implementation detail, it could be built in axiomatic

[Aaron Liu]

Mario Carneiro said:

I think the definition of WellFounded is an implementation detail, it could be built in axiomatic

How?

[Mario Carneiro]

That is, WellFounded is a primitive axiomatic constructor and so is WellFounded.fix and it has magic computation rules provided by the kernel. Whether it gets these computation rules because it's built in or because it has a definition that works out that way doesn't really matter for things built on top

[Mario Carneiro]

My point is that WellFounded.fix has better definitional reduction rules than Acc.rec does because Acc needs to manipulate a proof term in every step of the recursion

[Edward van de Meent]

ok, but then will we be able to create instances for WellFounded?

[Mario Carneiro]

sure, it can have a constructor that looks like WellFounded.mk too

[Mario Carneiro]

I'm saying to separate the API from the implementation

[Edward van de Meent]

i guess that makes sense

[Mario Carneiro]

the API of WellFounded includes WellFounded.mk and WellFounded.fix and possibly a defeq that looks like WellFounded.fix_eq, so it's worth talking about what kind of API here and what kind of restrictions on fix_eq give desirable behaviors for things on top

[Mario Carneiro]

and if at the end of that it turns out it can be defined in terms of something more basic, great, but if not, it can still be a built in primitive supplied by the kernel

[Mario Carneiro]

Acc is already super special and complicates the inductive schema for a case which has essentially only one practical application

[Mario Carneiro]

I would definitely trade having a simpler schema in exchange for needing another magic special type like Quot

[Edward van de Meent]

does making WellFounded internal/axiomatic let us make sure something like Acc can't be created, though?

[Mario Carneiro]

yeah, we would ban types like it and/or make them have crappy defeqs

[Aaron Liu]

Edward van de Meent said:

does making WellFounded internal/axiomatic let us make sure something like Acc can't be created, though?

You can do something like saying the subtype of stuff less than x is well-founded

[Mario Carneiro]

if it wasn't for Acc -> WellFounded -> every wf rec definition ever, we wouldn't care about Acc at all

[Aaron Liu]

Mario Carneiro said:

if it wasn't for Acc -> WellFounded -> every wf rec definition ever, we wouldn't care about Acc at all

We have this one file file#SetTheory/Ordinal/Rank

[Mario Carneiro]

Also, keep in mind that "Acc in Type" is one way of neutering Acc by making it act like a regular inductive

[Mario Carneiro]

and in the presence of the axiom of choice you can go back and forth with something that has the type of the current Acc

[Mario Carneiro]

so I think that rank file would be fine

[Edward van de Meent]

what is special about current Acc? as far as i can tell it's really just a normal inductive, so i don't get how you would even begin to ban "inductives like it"

[Mario Carneiro]

It's a large eliminating subsingleton type

[Edward van de Meent]

it's large eliminating!?

[Mario Carneiro]

it's the only large eliminating recursive inductive type in lean

[Edward van de Meent]

ah, i missed that bit

[Edward van de Meent]

so you don't even get to define something like Acc in lean as-is? that clears it up a bunch

[Mario Carneiro]

Equality is also a large eliminating inductive, but it's not recursive

[Mario Carneiro]

No, you can define something like Acc

[Mario Carneiro]

because it's not actually special cased

[Mario Carneiro]

but there is an additional clause in the inductive schema which allows "Acc and things like it" but in practice that means just Acc

[Mario Carneiro]

in fact, there is a proof in #leantt that Acc is universal for such types

[Mario Carneiro]

Edward van de Meent said:

it's large eliminating!?

It has to be large eliminating or else one can't define functions by well founded recursion, only prove theorems by well founded induction

[Joachim Breitner]

Mario Carneiro said:

Equality is also a large eliminating inductive, but it's not recursive

Any interesting large eliminating inductives besides these two? Or put differently: If we didn’t need Acc, could Eq be the only large eliminating inductive?

[Mario Carneiro]

And is also large eliminating

[Mario Carneiro]

but it's not interesting

[Mario Carneiro]

True and False too

[Mario Carneiro]

only recursive large eliminating types are really problematic though

[Mario Carneiro]

Eq is semi-problematic :)

[Aaron Liu]

False, Eq, and Acc are interesting

[Aaron Liu]

With True you can't do anything with its large elimination and with And you can just use the projections

[Mario Carneiro]

False's large elimination is quite important but it usually is harmless from a type theory perspective because it has no iota rule (since it has no constructors to have iota rules for)

[Aaron Liu]

Mario Carneiro said:

False's large elimination is quite important but it usually is harmless from a type theory perspective because it has no iota rule (since it has no constructors to have iota rules for)

What does iota rule do (why is not having one harmless)?

[Mario Carneiro]

T.rec F (T.constructor x) = F x

[Mario Carneiro]

you have one of those for every constructor of an inductive type, so for False there are no rules

[Aaron Liu]

Is having these "harmful" then?

[Mario Carneiro]

it's what makes the theory interesting

[Mario Carneiro]

where "interesting" may go as far as "soundness is an open question"

[Mario Carneiro]

but it's not like we don't want to be able to make definitions by recursion on Nat

[Mario Carneiro]

Here's a proof (using AC) that it is possible to construct WellFounded.fix using a small-eliminating Acc:

import Mathlib.Logic.Unique

inductive SmallAcc {α} (r : α → α → Prop) : α → Prop
  | mk x : Unit → (∀ y, r y x → SmallAcc r y) → SmallAcc r x

def WellFounded' {α} (r : α → α → Prop) := ∀ x, SmallAcc r x

inductive FixOut {α} {C : α → Sort _} {r : α → α → Prop}
    (F : (x : α) → ((y : α) → r y x → C y) → C x) : ∀ x, C x → Prop
  | mk x f : (∀ y h, FixOut F y (f y h)) → FixOut F x (F x f)

theorem SmallAcc.fix_exists {α} {C : α → Sort _} {r : α → α → Prop}
    (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (hwf : SmallAcc r x) :
    ∃ y : C x, FixOut F x y :=
  hwf.rec fun _ _ _ IH =>
    ⟨F _ fun y h => (IH y h).choose, ⟨_, _, fun y h => (IH y h).choose_spec⟩⟩

noncomputable def WellFounded'.fix {α} {C : α → Sort _} {r : α → α → Prop}
    (hwf : WellFounded' r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x :=
  (SmallAcc.fix_exists F x (hwf x)).choose

theorem WellFounded'.fix_eq {α} {C : α → Sort _} {r : α → α → Prop}
    (hwf : WellFounded' r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) :
    fix hwf F x = F x (fun y _ => fix hwf F y) := by
  suffices ∀ y y', FixOut F x y → FixOut F x y' → y = y' from
    this _ _ (SmallAcc.fix_exists F x (hwf x)).choose_spec
      ⟨_, _, fun y _ => (SmallAcc.fix_exists F y (hwf y)).choose_spec⟩
  intro y y' H1 H2
  induction H1 with
  | _ x f h IH =>
    let ⟨_, f', h'⟩ := H2
    congr; ext; exact IH _ _ _ (h' ..)

[Aaron Liu]

No computation makes it slightly disappointing

[Mario Carneiro]

the point is that if one is willing to give up computation then we don't need this kind of inductive at all

[Mario Carneiro]

plus the compiler can of course support computation of this function anyway

[Mario Carneiro]

I don't think it's possible to get a version that computes in the kernel without kernel magic (either Acc-like types or primitive WellFounded.fix)

[Aaron Liu]

What would be the consequences of using a type-valued Acc?

[Mario Carneiro]

You would be able to define fix easily, but WellFounded would no longer be a Prop, and also the proof of well foundedness would not be erased

[Mario Carneiro]

If you make WellFounded a prop using Nonempty then you need the axiom of choice to define fix and you end up with something similar to the above

[Mario Carneiro]

It's possible you could make it work if we had erasure annotations and used them on well foundedness arguments

[Mario Carneiro]

which TBH sounds less scary than the alternatives that involve kernel magic

[Edward van de Meent]

so if i understand correctly, you're proposing to get rid of this rule:
image.png
and make WellFounded a built-in exception?

[Edward van de Meent]

(the image is from #leantt , i added the box)

[Mario Carneiro]

WellFounded isn't exactly an exception to this rule, since it's not an inductive type of this kind at all (it's a structure wrapping Acc)

[Edward van de Meent]

ah, that's fair

[Joachim Breitner]

Mario Carneiro said:

the proof of well foundedness would not be erased

Does that matter? At least if you refer to erasure in compiled code, because the compiler works on the recursive PreDefinition and doesn’t even see the kernel-facing construction we are discussing here. And the kernel doesn’t erase proofs, does it?

[Mario Carneiro]

Ah, I suppose that's true

[Mario Carneiro]

hm... let's try it and see what breaks?

[Joachim Breitner]

Making Acc a Type would allow simplifying the type theory, but not help with the other issues (slow reduction of Acc terms, for example), would it?

[Edward van de Meent]

it might force users to write better-reducing "proofs" though

[Edward van de Meent]

i.e. not use tactics

[Mario Carneiro]

I think it would mean that defeq would work reliably

[Mario Carneiro]

well foundedness proofs would have a similar status to Decidable proofs, you would want to avoid using rw except in the proof arguments

[Joachim Breitner]

I see – are saying we need WF proofs to be more carefully crafted, and that’s more likely to happen in Type

[Mario Carneiro]

Note that a (Type-valued) proof of well foundedness still contains a lot of proofs in it because the r argument is still a prop

[Mario Carneiro]

and unlike "reducing proofs", we can clearly separate out the spine of the WF proof from the side proofs showing individual relations hold

[Joachim Breitner]

Right, that’s my worry still

[Mario Carneiro]

you would not need to do anything special to tell lean to reduce the WF argument but not the side proofs

[Mario Carneiro]

I think it makes a difference in this setting whether you are doing well founded recursion over a relation or its transitive closure. Doing recursion on the transitive closure should be more efficient

[Mario Carneiro]

I'm trying it out now, and there is an issue: Acc in Type is a subsingleton but not definitionally so (because we don't have eta for "recursive structures" and that sounds scary), which means that fix_eq is not a defeq because it uses two different derivations for the well foundedness proof on each side of the equality

[Aaron Liu]

What if we add a rule that elements of a structurally subsingleton type are definitional equal?

[Aaron Liu]

Structural eta already does a lot of this, recursive types like Acc are sort of an exception now

[Mario Carneiro]

it could work

[Mario Carneiro]

I think it reintroduces the issue that makes Acc bad though

[Mario Carneiro]

you can use definitional equality to swap out constructors in an inconsistent context and so typing is undecidable

[Mario Carneiro]

I guess that's the whole point, WellFounded.fix_eq (which ignores its proof argument) can't be a defeq without implicating undecidability of typechecking

[Mario Carneiro]

note that Acc.fixF works just fine

[Edward van de Meent]

docs#Acc.fixF :looking:

[Edward van de Meent]

:man_shrugging:

[Mario Carneiro]

docs#WellFounded.fixF

[Mario Carneiro]

But actually, I think it doesn't matter that fix_eq isn't a defeq. It's already not a defeq. The question is whether it computes on closed terms, and I believe it should

[Bhavik Mehta]

So conversely, if you have a function that you want to have useful defeqs, then don't use well-founded recursion

I have made this change for Nat.xgcd here: #24514

[Aaron Liu]

Should we make everything come with fuel?

[Bhavik Mehta]

That's my conclusion from Joachim's message