feat: encode `let_fun` using a `letFun` function #2973

kmill · 2023-11-28T06:30:52Z

Switches from encoding let_fun using an annotated (fun x : t => b) v expression to a function application letFun v (fun x : t => b).

kmill · 2023-11-28T06:35:06Z

@leodemoura I carried out your suggestion to re-encode let_fun as a function application.

I'm not sure if you were expecting it to be for dependent or non-dependent lets. I investigated making it be only for non-dependent lets, but I found that the first example in tests/lean/letFun.lean was dependent until metavariables were finally solved for when synthesizing default instances.

leanprover-community-mathlib4-bot · 2023-11-28T07:17:31Z

❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-11-28 07:17:31)
💥 Mathlib branch lean-pr-testing-2973 build failed against this PR. (2023-11-28 19:29:24) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-11-28 20:10:38) View Log
💥 Mathlib branch lean-pr-testing-2973 build failed against this PR. (2023-11-28 20:25:36) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-11-29 00:36:08) View Log
🟡 Mathlib branch lean-pr-testing-2973 build against this PR was cancelled. (2023-11-29 00:36:11) View Log
❌ Mathlib branch lean-pr-testing-2973 built against this PR, but linting failed. (2023-11-29 01:39:02) View Log
✅ Mathlib branch lean-pr-testing-2973 has successfully built against this PR. (2023-11-29 03:14:34) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-12-14 20:19:19) View Log
💥 Mathlib branch lean-pr-testing-2973 build failed against this PR. (2023-12-14 21:11:06) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-12-20 09:37:14) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-12-20 09:37:50) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-12-20 09:39:43) View Log
🟡 Mathlib branch lean-pr-testing-2973 build this PR didn't complete normally. (2023-12-20 09:41:59) View Log
💥 Mathlib branch lean-pr-testing-2973 build failed against this PR. (2023-12-20 09:43:30) View Log

leodemoura · 2023-12-01T14:32:53Z

I'm not sure if you were expecting it to be for dependent or non-dependent lets.

It is for non-dependent lets.

I investigated making it be only for non-dependent lets, but I found that the first example in tests/lean/letFun.lean

I can encode all let_funs in this test file using the auxiliary letFun function. Could you please clarify the issue you are having?

def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v

#check
  letFun (fun x => x * 2) fun f =>
  letFun 1 fun x =>
  letFun (x + 1) fun y =>
  f (y + x)

example (a b : Nat) (h1 : a = 0) (h2 : b = 0) : (letFun (a + 1) fun x => x + x) > b := by
  simp (config := { beta := false }) [h1]
  trace_state
  simp (config := { decide := true }) [h2]

kmill · 2023-12-01T16:02:11Z

@leodemoura I've used the wrong terminology -- using SimpLetCase for clarification, I mean to say I wasn't sure if you were expecting the nondepDepVar or nondep encoding. I got the nondepDepVar encoding of letFun working in this PR, and it does exactly what you wrote in your code block.

leodemoura · 2023-12-06T14:09:35Z

I got the nondepDepVar encoding of letFun working in this PR, and it does exactly what you wrote in your code block.

@kmill
If I understood you correctly, you are saying that you can only handle cases where β is a constant function fun _ => β0, correct?

What is the obstacle for getting it working in the more general case?

If I understood you correctly, you currently cannot elaborate an example that would produce:

  letFun (α := Nat) (β := fun n => { as : List Bool // as.length ≤ n } ) 5 fun n =>
    ⟨[], Nat.zero_le n⟩

As far as I remember, the old let_fun elaborator does not support this kind of example. Example:

#check id (α := { as : List Bool // as.length ≤ 5 }) $ 
  let_fun n := 5
  ⟨[], Nat.zero_le n⟩ -- Error here

Even using lambda directly, we need to include a helper type ascription.

#check id (α := { as : List Bool // as.length ≤ 5 }) $ 
  (fun n => (⟨[], Nat.zero_le n⟩ : { as : List Bool // as.length ≤ n })) 5

We usually use kabstract in this kind of situation. Not sure whether it is worth the trouble if your current implementation works for every example where the old one works.
Moreover, if we will never support the more general case, should we simplify letFun?

def letFun {α : Sort u} {β : Sort v} (v : α) (f : α → β) : β := f v

kmill · 2023-12-06T17:02:04Z

@leodemoura I don't have any obstruction here, and I can handle non-constant type families. I just wanted to be sure that you weren't expecting this simplified letFun encoding that you had proposed in your original message since I instead used this "nonDepDepVar" encoding, which I switched to at the first sign of trouble. The latter was more obvious how to implement. In particular mkLetFun, to produce the simple encoding, would need to force β to not depend on the fvar x, even in the presence of metavariables.

Examples like this one definitely work with this PR's implementation:

#check let_fun n := 5
  (⟨[], Nat.zero_le n⟩ : { as : List Bool // as.length ≤ n })

I haven't evaluated whether these sorts of examples appear in the wild, but I would not be surprised if they do.

You are correct that it does not generalize the value in the expected type, so your examples with { as : List Bool // as.length ≤ 5 } do not work. I personally believe generalization would be a surprising feature for let_fun, and if that is at some point a requested feature, that it should be either an option (like let_fun (generalizing := true) n := 5; ...) or be a new binding syntax.

leodemoura · 2023-12-11T03:32:23Z

@kmill Let's move forward and merge.

kmill · 2023-12-12T18:30:58Z

@leodemoura Sounds good. Let me know if you need me to do anything. (Maybe I should rebase this onto the newest nightly and regenerate the stage0?)

kim-em · 2023-12-12T23:16:25Z

(Maybe I should rebase this onto the newest nightly and regenerate the stage0?)

Yes please.

kmill · 2023-12-13T00:16:41Z

@semorrison Done.

By the way, this will take a small change to std. I don't have push access to that project, so didn't update the testing branch. Instead, I made my own branch and modified the mathlib testing branch to use that. It was an easy fix: kmill/std4@7ca1c2c

Kha · 2023-12-13T09:05:10Z

src/Init/Prelude.lean

+This is an abbreviation for `(fun x => b) v`, so the value of `x` is not accessible to `b`,
+unlike with `let x := v; b`.
+-/
+def letFun {α : Sort u} {β : α → Sort v} (v : α) (f : (x : α) → β x) : β v := f v


This encoding means that even with config.zeta false, we reduce let_funs when at default reducibility, correct? Is that intentional or should it be [irreducible]?

Good point, that is something I did not think enough about. I made it be irreducible and added more tests. (I also extended the optimization for ignoring unnecessary lets in isDefEqQuick to also consider let_fun.)

@leodemoura I'll wait for your final confirmation on this point before merging

Agreed. We don't want to reduce let_funs when config.zeta = false and using the default reducibility.

…tation

src/Init/Prelude.lean

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

kim-em · 2023-12-20T00:47:54Z

@Kha, @kmill, I don't think we should have merged this while it had a breaks-mathlib label!

It has indeed broken both Std and Mathlib's nightly-testing branches, and without understanding this PR in detail I don't immediately know how to fix them.

(The discussion on zulip might be a better place for follow-up than here.)

kmill · 2023-12-20T01:19:08Z

@semorrison Did you see my message earlier, #2973 (comment) ?

I'll follow up on zulip too.

This is a PR to Mathlib's `bump/v4.5.0` branch, containing adaptations required for leanprover/lean4#2973, which landed in `leanprover/lean4:nightly-2023-12-19` and will become part of `v4.5.0-rc1` soon. Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

…h. (#9188) This PR: * bumps to lean-toolchain to `v4.5.0-rc1` * bumps the Std and Aesop dependencies to their versions using `v4.5.0-rc1` * merge the already reviewed changes from the `bump/v4.5.0` branch * adaptations for leanprover/lean4#2923 in #9011 * adaptations for leanprover/lean4#2973 in #9161 * adaptations for leanprover/lean4#2964 in #9176 Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

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`.)

@david-christiansen

…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).

kmill requested review from Kha and leodemoura as code owners November 28, 2023 06:30

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

kmill force-pushed the let_fun branch from e65dafc to 6f08b85 Compare November 28, 2023 18:33

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

Update lean-toolchain for testing leanprover/lean4#2973

84f37b6

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 28, 2023

kmill mentioned this pull request Nov 29, 2023

Fix: use exprToSyntax in comefrom elaborator leanprover-community/quote4#28

Merged

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

Trigger CI for leanprover/lean4#2973

f1f7751

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 Nov 29, 2023

kmill added 3 commits December 12, 2023 15:27

feat: use letFun function for let_fun instead of annotation

d880045

chore: update stage0

d0461d9

Tweak comment style

716bdbb

kmill force-pushed the let_fun branch from eecb110 to 716bdbb Compare December 12, 2023 23:44

Kha reviewed Dec 13, 2023

View reviewed changes

kmill added 2 commits December 13, 2023 13:43

make letFun irreducible, make isDefEqQuick let_fun-aware, add documen…

2263065

…tation

more tests

fbf746d

Kha approved these changes Dec 14, 2023

View reviewed changes

src/Init/Prelude.lean Outdated Show resolved Hide resolved

fix typo in docstring

146d2e1

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

leanprover-community-mathlib4-bot removed the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 14, 2023

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 14, 2023

Kha added this pull request to the merge queue Dec 18, 2023

Merged via the queue into leanprover:master with commit a2226a4 Dec 18, 2023

This was referenced Dec 20, 2023

chore: adaptations for leanprover/lean4#2973 leanprover-community/mathlib4#9160

Closed

[Merged by Bors] - chore: adaptations for leanprover/lean4#2973 leanprover-community/mathlib4#9161

Closed

kim-em mentioned this pull request Dec 21, 2023

[Merged by Bors] - chore: move to v4.5.0-rc1, and merge changes from bump/v4.5.0 branch. leanprover-community/mathlib4#9188

Closed

This was referenced Jan 4, 2024

chore: fix nightly testing to work with 2024-01-03 leanprover-community/mathlib4#9438

Merged

[Merged by Bors] - chore: CI: improve comment created on lean PRs leanprover-community/mathlib4#9585

Closed

nomeata mentioned this pull request Jan 22, 2024

fix: predefinition preprocessing: float .mdata out of non-unary applications #3204

Merged

leodemoura mentioned this pull request Feb 20, 2024

let_fun elaboration #2289

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: encode `let_fun` using a `letFun` function #2973

feat: encode `let_fun` using a `letFun` function #2973

kmill commented Nov 28, 2023

kmill commented Nov 28, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Nov 28, 2023 •

edited

Loading

leodemoura commented Dec 1, 2023

kmill commented Dec 1, 2023

leodemoura commented Dec 6, 2023 •

edited

Loading

kmill commented Dec 6, 2023

leodemoura commented Dec 11, 2023

kmill commented Dec 12, 2023

kim-em commented Dec 12, 2023

kmill commented Dec 13, 2023

Kha Dec 13, 2023

kmill Dec 13, 2023

Kha Dec 14, 2023

leodemoura Dec 17, 2023

leodemoura Dec 17, 2023

kim-em commented Dec 20, 2023

kmill commented Dec 20, 2023

feat: encode let_fun using a letFun function #2973

feat: encode let_fun using a letFun function #2973

Conversation

kmill commented Nov 28, 2023

kmill commented Nov 28, 2023 • edited Loading

leanprover-community-mathlib4-bot commented Nov 28, 2023 • edited Loading

leodemoura commented Dec 1, 2023

kmill commented Dec 1, 2023

leodemoura commented Dec 6, 2023 • edited Loading

kmill commented Dec 6, 2023

leodemoura commented Dec 11, 2023

kmill commented Dec 12, 2023

kim-em commented Dec 12, 2023

kmill commented Dec 13, 2023

Kha Dec 13, 2023

Choose a reason for hiding this comment

kmill Dec 13, 2023

Choose a reason for hiding this comment

Kha Dec 14, 2023

Choose a reason for hiding this comment

leodemoura Dec 17, 2023

Choose a reason for hiding this comment

leodemoura Dec 17, 2023

Choose a reason for hiding this comment

kim-em commented Dec 20, 2023

kmill commented Dec 20, 2023

feat: encode `let_fun` using a `letFun` function #2973

feat: encode `let_fun` using a `letFun` function #2973

kmill commented Nov 28, 2023 •

edited

Loading

leanprover-community-mathlib4-bot commented Nov 28, 2023 •

edited

Loading

leodemoura commented Dec 6, 2023 •

edited

Loading