feat: encode let_fun using a letFun function
#2973
Conversation
|
@leodemoura I carried out your suggestion to re-encode 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 |
github-actions
bot
added
the
toolchain-available
|
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
leanprover-community-mathlib4-bot
added
builds-mathlib
It is for non-dependent lets.
I can encode all 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] |
|
@leodemoura I've used the wrong terminology -- using |
@kmill 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 #check id (α := { as : List Bool // as.length ≤ 5 }) $
let_fun n := 5
⟨[], Nat.zero_le n⟩ -- Error hereEven 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 })) 5We usually use def letFun {α : Sort u} {β : Sort v} (v : α) (f : α → β) : β := f v |
|
@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 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 |
|
@kmill Let's move forward and merge. |
|
@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?) |
Yes please. |
|
@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 |
src/Init/Prelude.lean
Outdated
| 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 |
There was a problem hiding this comment.
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]?
There was a problem hiding this comment.
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.)
There was a problem hiding this comment.
@leodemoura I'll wait for your final confirmation on this point before merging
There was a problem hiding this comment.
Agreed. We don't want to reduce let_funs when config.zeta = false and using the default reducibility.
There was a problem hiding this comment.
Agreed. We don't want to reduce let_funs when config.zeta = false and using the default reducibility.
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
leanprover-community-mathlib4-bot
removed
the
builds-mathlib
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
@Kha, @kmill, I don't think we should have merged this while it had a It has indeed broken both Std and Mathlib's (The discussion on zulip might be a better place for follow-up than here.) |
|
@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`.)
…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).
Switches from encoding
let_funusing an annotated(fun x : t => b) vexpression to a function applicationletFun v (fun x : t => b).