Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Float RecApp out of applications #2818

Merged
merged 5 commits into from
Nov 22, 2023
Merged

fix: Float RecApp out of applications #2818

merged 5 commits into from
Nov 22, 2023

Conversation

nomeata
Copy link
Contributor

@nomeata nomeata commented Nov 4, 2023

This didn't work before

def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => (f) n

because the RecApp metadata marker gets in the way. More practically
relevant, such code is to be produced when using rw or simp in
recursive theorems (see included test case).

We can fix this by preprocessing the definitions and floating the
.mdata marker out of applications.

For structural recursion, there already exists a preprocess function;
this now also floats out .mdata markers.

For well-founded recursion, this introduces an analogous preprocess
function.

Fixes #2810.

One test case output changes: With the .mdata out of the way, we get a
different error message. Seems fine.

Alternative approaches are:

@nomeata
Copy link
Contributor Author

nomeata commented Nov 4, 2023

Open question: Should there be one preprocess function invoked by addPreDefinitions for both strategies? Would the well-founded recursion code benefit or be hurt by the beta-reductions done for structural recursion?

@nomeata nomeata added the awaiting-review Waiting for someone to review the PR label Nov 4, 2023
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 4, 2023
semorrison added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 5, 2023
@leodemoura
Copy link
Member

Open question: Should there be one preprocess function invoked by addPreDefinitions for both strategies? Would the well-founded recursion code benefit or be hurt by the beta-reductions done for structural recursion?

Great question. I don't see any reason why it would hurt well-founded recursion.
Let's try a single preprocess function for both of them.
Note that the current preprocess assumes there is only one function on the recursive block. This is not sufficient for well-founded recursion since it already supports mutual recursion. We need support for this too.

@nomeata
Copy link
Contributor Author

nomeata commented Nov 5, 2023

Let's try a single preprocess function for both of them.

Will do (tomorrow)

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 5, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 5, 2023
@leanprover leanprover deleted a comment from github-actions bot Nov 6, 2023
@semorrison
Copy link
Collaborator

(Apologies for force pushing to your branch, I am still diagnosing some CI weirdnesses!)

@leanprover-community-mathlib4-bot
Copy link
Collaborator

leanprover-community-mathlib4-bot commented Nov 6, 2023

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-06 03:23:43)
  • ❗ Mathlib CI can not be attempted yet, as the 'nightly-testing-2023-11-06' branch does not exist there yet. We will retry when you push more commits. It may be necessary to rebase onto 'nightly' tomorrow. (2023-11-06 10:52:58)
  • ✅ Mathlib branch lean-pr-testing-2818 has successfully built against this PR. (2023-11-06 12:09:47) View Log

This didn't work before
```
def f (n : Nat) : Nat :=
  match n with
  | 0 => 0
  | n + 1 => (f) n
```
because the `RecApp` metadata marker gets in the way. More practically
relevant, such code is to be produced when using `rw` or `simp` in
recursive theorems (see included test case).

We can fix this by preprocessing the definitions and floating the
`.mdata` marker out of applications.

For structural recursion, there already exists a `preprocess` function;
this now also floats out `.mdata` markers.

For well-founded recursion, this introduces an analogous `preprocess`
function.

Fixes #2810.

One test case output changes: With the `.mdata` out of the way, we get a
different error message. Seems fine.

Alternative approaches are:

* Leaving the `.mdata` marker where it is, and looking around it.
  Tried in #2813, but not nice (many many places where `withApp` etc.
  need to be adjusted).
* Moving the `.mdata` _inside_ the application, so that `withApp` still
  works. Tried in #2814. Also not nice, the invariant that the `.mdata`
  is around the `.const` is tedious to maintain.
@nomeata
Copy link
Contributor Author

nomeata commented Nov 6, 2023

Great question. I don't see any reason why it would hurt well-founded recursion.
Let's try a single preprocess function for both of them.

Tried in #2823. Beta-reduction (if done as it is defined now) can remove let_fun redexes that we want to keep because of the termination argument they bring into scope; example for a test case now failing:

def f (p : Pos) : Pos :=
  match h : p.view with -- It would also be nice to have a feature to force Lean to applies "views" automatically for us.
  | 1 => 1
  | .succ x =>
    have : sizeOf x < sizeOf p := sizeof_lt_of_view_eq h -- See comment at `sizeof_lt_of_view_eq`
    f x + x + 1

Maybe one could use a more careful form of beta-reduction that works for both, but I’d say it’s not worth for the gain, and who knows, maybe the next derecursifier that comes along may need some other set of preprocessors again.

I left a note in the code that the difference between the two functions is deliberate.

@digama0
Copy link
Collaborator

digama0 commented Nov 6, 2023

Note: the fact that the WF preprocessor does not remove beta redexes during preprocessing is a bug, which causes unusedHavesSuffices linter failures on the generated equation lemmas. Of course it is understandable due to the way WF receives hypotheses, but it should remove betas after doing the termination proofs.

It may or may not be possible to remove betas without breaking the WF termination prover with the current preprocessor design, I have not looked in detail. Perhaps we need a postprocessor too.

@nomeata
Copy link
Contributor Author

nomeata commented Nov 6, 2023

Thanks! That sounds indeed like you want to post-process them. Separate issue, I’d say?

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Nov 6, 2023
@semorrison semorrison removed the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 6, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 6, 2023
@nomeata
Copy link
Contributor Author

nomeata commented Nov 20, 2023

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 47d1e07.
There were no significant changes against commit 8b86bee.

@nomeata
Copy link
Contributor Author

nomeata commented Nov 20, 2023

Will merge this on Wednesday.

@nomeata nomeata added will-merge-soon …unless someone speaks up and removed awaiting-review Waiting for someone to review the PR labels Nov 21, 2023
@nomeata nomeata added this pull request to the merge queue Nov 22, 2023
Merged via the queue into master with commit dede354 Nov 22, 2023
17 checks passed
@nomeata nomeata deleted the joachim/float-recapp branch November 22, 2023 15:36
nomeata added a commit that referenced this pull request Jan 22, 2024
both Structural and WF recursion have a preprocess module (since #2818
at least). Back then I found that betareducing in WF, like it happens
for structural, bytes because it would drop `let_fun` annotations, which
are of course worth preserving.

Now that #2973 is landed let's see if we can do it now.

I hope that this fixes an issue where code like
```
theorem size_rev {α} (arr : Array α) (i : Nat) : (rev arr i).size = arr.size := by
  unfold rev
  split
  · rw [size_rev]
    rw [Array.size_swap]
  · rfl
termination_by arr.size - i
decreasing_by simp_wf; omega
```
fails but works with `size_rev _ _`.

It fails due to some lambda-redexes that maybe go away.

(Maybe we can also/additinally/alternatively track down where that redex
is created and use `.beta` instead of `.app`.)
github-merge-queue bot pushed a commit that referenced this pull request Jan 24, 2024
…cations (#3204)

Recursive predefinitions contains “rec app” markers as mdata in the
predefinitions,
but sometimes these get in the way of termination checking, when you
have
```
  [mdata (fun x => f)] arg
```

Therefore, the `preprocess` pass floats them out of applications
(originally
only for structural recursion, since #2818 also for well-founded
recursion).

But the code was incomplete: Because `Meta.transform` calls `post` on `f
x y` only
once (and not also on `f x`) one has to float out of nested applications
as well.

A consequence of this can be that in a recursive proof, `rw [foo]` does
not work
although `rw [foo _ _]` does.

Also adding the testcase where @david-christiansen and I stumbled over
this


(Maybe the two preprocess modules can be combined, now that #2973 is
landed, will try that
in a follow-up).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Superfluous parentheses can inhibit structural recursion
6 participants