feat: drop support for termination_by' #3033

nomeata · 2023-12-06T09:46:58Z

until around 7fe6881 the way to define well-founded recursions was to
specify a WellFoundedRelation on the argument explicitly. This was
rather low-level, for example one had to predict the packing of multiple
arguments into PProds, the packing of mutual functions into PSums,
and the cliques that were calculated.

Then the current termination_by syntax was introduced, where you
specify the termination argument at a higher level (one clause per
functions, unpacked arguments), and the WellFoundedRelation is found
using type class resolution.

The old syntax was kept around as termination_by'. This is not used
anywhere in the lean, std, mathlib or the theorem-proving-in-lean repositories,
and three occurrences I found in the wild can do without

In particular, it should be possible to express anything that the old syntax
supported also with the new one, possibly requiring a helper type with a
suitable instance, or the following generic wrapper that now lives in std

def wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : {x : α // Acc r x}

Since the old syntax is unused, has an unhelpful name and relies on
internals, this removes the support. Now is a good time before the
refactoring that's planned in #2921.

The test suite was updated without particular surprises.

The parametric terminationHint parser is gone, which means we can
match on syntax more easily now, in expandDecreasingBy?.

until around 7fe6881 the way to define well-founded recursions was to specify a `WellFoundedRelation` on the argument explicitly. This was rather low-level, for example one had to predict the packing of multiple arguments into `PProd`s, the packing of mutual functions into `PSum`s, and the cliques that were calculated. Then the current `termination_by` syntax was introduced, where you sepecify the termination argument at a higher level (one clause per functions, unpacked arguments), and the `WellFoundedRelation` is found using type class resolution. The old syntax was kept around as `termination_by'`. But at the time of writing, this is not used anywhere in the lean, std, mathlib or the theroem-proving-in-lean repositories. Also, should be possible to express anything that the old syntax supported also with the new one, possibly requiring a helper type with a suitable instance, or a very generic wrapper like ``` inductive WithWFRel {a : Type _} {rel : a → a → Prop} (h : WellFounded rel) where | mk : a -> WithWFRel h instance : WellFoundedRelation (WithWFRel h) := invImage (fun x => match x with | .mk x => x) ⟨_, h⟩ ``` Since the old syntax is unused, has an unhelpful name and relies on internals, this removes the support. Now is a good time before the refactoring that's planned in #2921. The test suite was updated without particular surprises. The parametric `terminationHint` parser is gone, which means we can match on syntax more easily now, in `expandDecreasingBy?`.

nomeata · 2023-12-06T09:51:47Z

Silly commit convention, removal of a feature is strange feat :-)

digama0 · 2023-12-06T09:59:39Z

I think this should not be done without a clear deprecation and migration strategy, including the WithWFRel type.

nomeata · 2023-12-06T10:08:01Z

I think this should not be done without a clear deprecation and migration strategy, including the WithWFRel type.

Yeah, that is something I wonder as well: How fast can we still move? Do you have evidence that this is used anywhere? And moreover that any of these theses are not better served by termination_by (rather than WithWFRel)?

You are probably not on board with “Renaming the old syntax as termination_by', so that users start using termination_by is the deprecation strategy, and two years was enough” :-)?

Also, would you argue we need a migration strategy for #2921 as well?

leanprover-community-mathlib4-bot · 2023-12-06T10:11:18Z

💥 Mathlib branch lean-pr-testing-3033 build failed against this PR. (2023-12-06 10:11:16) View Log
💥 Mathlib branch lean-pr-testing-3033 build failed against this PR. (2023-12-06 10:48:22) View Log
💥 Mathlib branch lean-pr-testing-3033 build failed against this PR. (2023-12-06 14:57:32) View Log
✅ Mathlib branch lean-pr-testing-3033 has successfully built against this PR. (2023-12-06 18:37:29) View Log
✅ Mathlib branch lean-pr-testing-3033 has successfully built against this PR. (2023-12-06 19:17:12) View Log
💥 Mathlib branch lean-pr-testing-3033 build failed against this PR. (2023-12-08 08:45:15) View Log
❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-12-08' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-12-08 09:16:00)
❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-08 18:41:55)
💥 Mathlib branch lean-pr-testing-3033 build failed against this PR. (2023-12-09 12:34:03) View Log
✅ Mathlib branch lean-pr-testing-3033 has successfully built against this PR. (2023-12-09 14:27:41) View Log
✅ Mathlib branch lean-pr-testing-3033 has successfully built against this PR. (2023-12-09 15:32:26) View Log

digama0 · 2023-12-06T10:31:55Z

You are probably not on board with “Renaming the old syntax as termination_by', so that users start using termination_by is the deprecation strategy, and two years was enough” :-)?

No, there has never been any indication that this was on its way out. Primes in lean generally don't indicate deprecation, they indicate a less common variation on the operation for which we couldn't think of a better name.

Yeah, that is something I wonder as well: How fast can we still move? Do you have evidence that this is used anywhere? And moreover that any of these theses are not better served by termination_by (rather than WithWFRel)?

I do not doubt that uses are better served by termination_by in the vast majority of cases, but when upgrading the compiler you want to minimize the pain of fixing your broken proofs, and a simple migration that works but is not very elegant is much better than forcing a complex refactor.

And yes, I do have a current use of termination_by': it is currently used by mathport for translating termination arguments from lean 3. I'll retarget it to use WithWFRel if you add it.

Also, would you argue we need a migration strategy for #2921 as well?

Yes, of course. Any change which breaks proofs needs to have a migration strategy, even if it is only expressed in prose in the release notes.

nomeata · 2023-12-06T10:38:51Z

That’s what I thought :-)

I’ll escalate this to @leodemoura.

Personally I hope we are still in a phase of lean development where we can still clean up things, even if it breaks hypothetical code, and where we can use std and mathlib (and soon more stuff on reservior) to distinguish actual breakage from hypothetical breakage.

digama0 · 2023-12-06T10:42:22Z

Personally I hope we are still in a phase of lean development where we can still clean up things,

I think you misunderstand. Having a deprecation period doesn't mean you can't clean up, and even if you don't do a deprecation period a migration guide for breakage is essential to keep users happy. Lean is moving fast and breaking my code all the time, and this is off-putting to many users we want to attract.

nomeata · 2023-12-06T10:46:22Z

if you don't do a deprecation period a migration guide for breakage is essential to keep users happy.

Oh, that I am absolutely on board with; this change should be well documented in the release notes.

nomeata · 2023-12-06T10:49:10Z

this is not used anywhere in the lean, std

I stand corrected, my std checkout was a tad old, and just there weeks ago a use of termination_by' was introduced there. That's a bit embarrasing.

digama0 · 2023-12-06T10:50:54Z

if you don't do a deprecation period a migration guide for breakage is essential to keep users happy.

Oh, that I am absolutely on board with; this change should be well documented in the release notes.

I didn't say document the change, I said a migration guide. That means to explain not just that X was removed but what to replace it with. A trivial syntactic change would be best for this, followed by an explanation of how to make the more involved change to the new syntax (and potentially new proof goals).

To be clear, I'm not opposed to this change. But removals especially need to come with assistance for users on how to fix their stuff.

nomeata · 2023-12-06T11:02:26Z

I agree!

I’d like to remove support for the `termination_by'` annotation. Until leanprover-community#371 it wasn't used anywhere in lean, std, mathlib, so this PR removes the single use of it. It does so using the pattern that can be used to replace uses of `termination_by'`, should there be more: Using the helper type `WellFounded.Wrap` one can indicate an explicit `WellFounded` relation to use. So this PR uses that pattern to avoid the use of `termination_by'` here, and at the same time provides the necessary definitions for others, so when Lean drops support for `termination_by'` (leanprover/lean4#3033), we can tell users how migrate.

nomeata · 2023-12-06T11:15:38Z

leanprover-community/batteries#420 adds the necessary definitions to std so that people can migrate, and dog-foods it right away there.

If the release note point out how to use that idiom when this change lands, would that be satisfactory?

digama0 · 2023-12-06T11:52:59Z

There are a few separate concerns here:

Usage in mathport: here we want something that can be applied fully automatically as a syntactic transformation
Grandfathered usage in user code: here we want something easy to explain, but not necessarily a pure syntactic transformation
Deliberate usage in user code: This is for cases where the old syntax is genuinely easier to use than the new syntax.

For (1) I'll do my best with whatever we end up with, but my quick take is that there is no simple replacement currently, because of the aforementioned packing process. For (2) I think your suggestion is sufficient. For (3) I think it might be worth considering a syntax similar to termination_by which lets you pass the instance instead of the value, or put an at-sign or optional argument somewhere. It's a bit awkward that the only way to pass that argument is via typeclass inference.

nomeata · 2023-12-06T14:33:32Z

Thanks for taking care of (1)!

For me, the big question is: does (3) even exist?

If I had seen more than the one use of termination_by' in std in the repos I could easily check, I wouldn’t even have proposed removing termination_by', but just kept it supported as I implement #2921 (probably with a better name, e.g. termination_relation, as it seemed to be a good opportunity to avoid the unhelpful '-suffix).

Using sourcegraph I can indeed find three more occurrences of termination_by' in the wild:

https://github.com/kovach/etch/blob/fa63a0bf500c9c9991012b84fea22000fbd29683/etch4/Etch/Verification/Semantics/SkipStream.lean#L327

This can be fixed using wrap:

@@ -324,7 +346,7 @@ noncomputable def Stream.eval [AddZeroClass α] (s : Stream ι α) [IsBounded s]
       have : s.WfRel (s.next q) q := s.next_wf _ h
       s.eval₀ q h + s.eval (s.next q)
     else 0
-termination_by' ⟨_, s.wf⟩
+termination_by _ q => s.wf.wrap q
 #align Stream.eval Etch.Verification.Stream.eval

 @[simp]

or using an explicit instance, like this

diff --git a/etch4/Etch/Verification/Semantics/SkipStream.lean b/etch4/Etch/Verification/Semantics/SkipStream.lean
index 5b07ed7..1b948e7 100644
--- a/etch4/Etch/Verification/Semantics/SkipStream.lean
+++ b/etch4/Etch/Verification/Semantics/SkipStream.lean
@@ -317,6 +317,9 @@ theorem Stream.no_backward (s : Stream ι α) [IsBounded s] (q hq i) :
   (s.wf_valid q hq i).imp_right And.right
 #align Stream.no_backward Etch.Verification.Stream.no_backward

+instance [AddZeroClass α] (s : Stream ι α) [IsBounded s] : WellFoundedRelation s.σ :=
+  ⟨_, s.wf⟩
+
 /-- Evaluates `∑_{q →* r} eval₀ r`, which is well-defined for bounded streams. -/
 noncomputable def Stream.eval [AddZeroClass α] (s : Stream ι α) [IsBounded s] : s.σ → ι →₀ α
   | q =>
@@ -324,7 +327,7 @@ noncomputable def Stream.eval [AddZeroClass α] (s : Stream ι α) [IsBounded s]
       have : s.WfRel (s.next q) q := s.next_wf _ h
       s.eval₀ q h + s.eval (s.next q)
     else 0
-termination_by' ⟨_, s.wf⟩
+termination_by _ q => q
 #align Stream.eval Etch.Verification.Stream.eval

 @[simp]

https://github.com/leanprover-community/con-nf/blob/688a8ab014bafbef47553e81e50de7db3f1d080e/ConNF/Foa/Complete/HypAction.lean#L52

Not entirely trivial, but also doable, and arguably also an improvement:

diff --git a/ConNF/Foa/Complete/HypAction.lean b/ConNF/Foa/Complete/HypAction.lean
index 532dacc..8f010f2 100644
--- a/ConNF/Foa/Complete/HypAction.lean
+++ b/ConNF/Foa/Complete/HypAction.lean
@@ -24,16 +24,8 @@ namespace HypAction

 variable {β : Iic α}

-def fixMap :
-    PSum (Σ' _ : ExtendedIndex β, Atom) (Σ' _ : ExtendedIndex β, NearLitter) → SupportCondition β
-  | PSum.inl ⟨A, a⟩ => ⟨A, inl a⟩
-  | PSum.inr ⟨A, N⟩ => ⟨A, inr N⟩
-
-def fixWf :
-    WellFoundedRelation
-      (PSum (Σ' _ : ExtendedIndex β, Atom) (Σ' _ : ExtendedIndex β, NearLitter)) :=
-  ⟨InvImage (Relation.TransGen (Constrains α β)) fixMap,
-    InvImage.wf _ (WellFounded.transGen <| constrains_wf α β)⟩
+instance : WellFoundedRelation (SupportCondition β) :=
+  ⟨_, WellFounded.transGen <| constrains_wf α β⟩

 mutual
   /-- Construct the fixed-point functions `fix_atom` and `fix_near_litter`.
@@ -49,7 +41,9 @@ mutual
       ExtendedIndex β → NearLitter → NearLitter
     | A, N => FN A N ⟨fun B b _ => fixAtom Fa FN B b, fun B N _ => fixNearLitter Fa FN B N⟩
 end
-termination_by' fixWf
+termination_by
+  fixAtom A n => SupportCondition.mk A (inl n)
+  fixNearLitter A N => SupportCondition.mk A (inr N)

 theorem fixAtom_eq (Fa FN) (A : ExtendedIndex β) (a : Atom) :
     fixAtom Fa FN A a =

https://sourcegraph.com/github.com/YaelDillies/LeanCamCombi@1f1eaf355cfc5b62ccd08a0405d266e42bb43614/-/blob/LeanCamCombi/Incidence.lean?L409:1

This looks like it is obviously better served using termination_by, such as

After this research I am not entirely sure that (3) doesn’t exist. With the current facts I’d say removal is still the better option. But nothing stops us from adding termination_relation later again, if we find this removal was misguided after all.

digama0 · 2023-12-06T15:02:17Z

One thing which I don't like about the current system which seems vaguely (3)-like is that you have to declare an instance in order to make the definition, even though it may just be something private to the definition. This pollutes the namespace with additional declarations (sometimes with long names), and unlike most cases you can't use a local have to introduce the instance, because termination_by lives "outside" the definition and there is nothing "outside" the termination_by where you would otherwise be able to put the have declaration. That's how you end up with private local instance like in the std example.

nomeata · 2023-12-06T15:15:16Z

Right, but you can work around that using WellFounded.wrap, where you do not have to define new instances.

So a work-around exists, the question is whether the work-around is ok enough, or bad enough to warrant supporting (and documenting, explaining, including the internals of bundling paramters etc.) a separate termination_relation, isn't it?

digama0 · 2023-12-06T15:48:06Z

True, I think under the circumstances it's better not to pursue termination_relation at this time. (I would not include the internals of bundling parameters, I would prefer a way to specify the bundling pattern. But I can't think of a nice syntax for this which isn't suspiciously similar to termination_by.)

This removes support for the `termination_by'` annotation. Until #371 it wasn't used anywhere in lean, std, mathlib, so this PR removes the single use of it. It does so using the pattern that can be used to replace uses of `termination_by'`, should there be more: Using the helper type `WellFounded.Wrap` one can indicate an explicit `WellFounded` relation to use. So this PR uses that pattern to avoid the use of `termination_by'` here, and at the same time provides the necessary definitions for others, so when Lean drops support for `termination_by'` (leanprover/lean4#3033), we can tell users how migrate. * Use wfRel instead

nomeata · 2023-12-08T08:42:54Z

Added a (short) migration guide to the release notes.

Will probably merge next week, maybe around monday afternoon my time.

nomeata · 2023-12-08T08:50:28Z

(I would not include the internals of bundling parameters, I would prefer a way to specify the bundling pattern. But I can't think of a nice syntax for this which isn't suspiciously similar to termination_by.)

Right. I guess you’d end up with something like “termination_by + explicitly specified relation”, which may be a bit more convenient than wf.wrap … inside termination_by, but target audience that benefits from this small DX delta might not be worth the effort on the lean side. When evidence refutes that, we can still do it.

I plan to remove support for `termination_by' (leanprover/lean4#3033), and investigated uses in the wild. Your case case be replaced with `termination_by` rather easily.

…termination_by_core

nomeata requested review from Kha and leodemoura as code owners December 6, 2023 09:46

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 6, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 6, 2023

Update lean-toolchain for testing leanprover/lean4#3033

1470b3e

leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 6, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 6, 2023

Trigger CI for leanprover/lean4#3033

a4d3c1d

nomeata marked this pull request as draft December 6, 2023 10:50

nomeata mentioned this pull request Dec 6, 2023

feat: avoid termination_by', introduce WellFounded.wrap leanprover-community/batteries#420

Merged

nomeata force-pushed the joachim/no-termination_by_core branch from af3d4e0 to f6f6edd Compare December 6, 2023 14:34

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 6, 2023

Trigger CI for leanprover/lean4#3033

4d6342e

nomeata marked this pull request as ready for review December 6, 2023 16:20

leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 6, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 6, 2023

Trigger CI for leanprover/lean4#3033

789a45d

Add Migration guide to RELEASES.md

e2f26d9

nomeata requested a review from kim-em as a code owner December 8, 2023 08:39

Merge branch 'master' into joachim/no-termination_by_core

3f97f77

nomeata added the will-merge-soon …unless someone speaks up label Dec 8, 2023

leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Dec 8, 2023

Fix merge fallout

401ebed

YaelDillies mentioned this pull request Dec 8, 2023

Avoid termination_by', use termination_by leanprover-community/con-nf#42

Merged

nomeata mentioned this pull request Dec 8, 2023

feat: per-function termination hints #3040

Merged

nomeata added 3 commits December 8, 2023 19:13

Merge branch 'master' of github.com:leanprover/lean4 into joachim/no-…

1a59dc9

…termination_by_core

Use current stage quotation

dcb923a

Trigger CI

1a6a902

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 9, 2023

Trigger CI for leanprover/lean4#3033

7714fe8

leanprover-community-mathlib4-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 9, 2023

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 9, 2023

Trigger CI for leanprover/lean4#3033

26712ca

nomeata added this pull request to the merge queue Dec 11, 2023

Merged via the queue into master with commit 5cd90f5 Dec 11, 2023
13 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: drop support for termination_by' #3033

feat: drop support for termination_by' #3033

nomeata commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 6, 2023 •

edited

Loading

digama0 commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023 •

edited

Loading

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 8, 2023 •

edited

Loading

nomeata commented Dec 8, 2023 •

edited

Loading

feat: drop support for termination_by' #3033

feat: drop support for termination_by' #3033

Conversation

nomeata commented Dec 6, 2023 • edited Loading

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Dec 6, 2023 • edited Loading

digama0 commented Dec 6, 2023 • edited Loading

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023 • edited Loading

nomeata commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023 • edited Loading

digama0 commented Dec 6, 2023

nomeata commented Dec 6, 2023

digama0 commented Dec 6, 2023

nomeata commented Dec 8, 2023 • edited Loading

nomeata commented Dec 8, 2023 • edited Loading

nomeata commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 6, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Dec 6, 2023 •

edited

Loading

digama0 commented Dec 6, 2023 •

edited

Loading

digama0 commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 6, 2023 •

edited

Loading

nomeata commented Dec 8, 2023 •

edited

Loading

nomeata commented Dec 8, 2023 •

edited

Loading