optionEquivLeft_apply simp

Stream: mathlib4

[Bolton Bailey]

I recently encountered this simp lemma MvPolynomial.optionEquivLeft_apply. This seems like something that shouldn't be a simp lemma - it expands an expression into something visually much larger with a match statement. Is there a good reason this is simp?

[Kevin Buzzard]

That'll be the power of @[simps!]

[Eric Wieser]

I'm surprised it's unfolding docs#Option.elim

[Eric Wieser]

Ugh, why is Option.elim simp? That looks like the issue here

[Kim Morrison]

Happy to merge a PR replacing that @[simp] annotation with appropriate simp lemmas.

[Eric Wieser]

I guess the equation lemmas RFC that @Joachim Breitner wrote will resolve this

[Eric Wieser]

And it seems that perhaps Option.elim is already de-simped somewhere in mathlib, as it doesn't show up as simp in the docs

[Ruben Van de Velde]

Might just be an issue with the docs, because we do have simp? says simp only [apply_ite, eval_ite_var, Option.elim, ite_eq_iff']

[Kevin Buzzard]

(FWIW I searched in mathlib and couldn't find it being un-simped)

[Kim Morrison]

Eric Wieser said:

I guess the equation lemmas RFC that Joachim Breitner wrote will resolve this

Probably better to clean this up in the meantime.

[Bolton Bailey]

Kim Morrison said:

Happy to merge a PR replacing that @[simp] annotation with appropriate simp lemmas.

This came up for me while making #11114 and seeing that the lemmas I was adding were already simp-proved, so maybe if we remove these, that PR should add simps to the lemmas it adds.

[Kim Morrison]

Sorry, I don't understand your message. I was talking about a PR to Lean to remove @[simp] from Option.elim.

[Bolton Bailey]

Kim Morrison said:

Sorry, I don't understand your message. I was talking about a PR to Lean to remove @[simp] from Option.elim.

Ah ok, I can put this on my to-do list.

[Bolton Bailey]

Note that this is also an issue for docs#MvPolynomial.finSuccEquiv_apply, as seen in this thread.

[Bolton Bailey]

Kim Morrison said:

Sorry, I don't understand your message. I was talking about a PR to Lean to remove @[simp] from Option.elim.

Is there something special I have to do to edit lean files in the src folder with the InfoView active? I am getting errors when I open these files:

/Users/boltonbailey/Desktop/mathlibcontribution/lean4/src> git --version
git version 2.39.2 (Apple Git-143)

/Users/boltonbailey/Desktop/mathlibcontribution/lean4/src> lean --version
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `lean4-stage0`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/expanded_assets/lean4-stage0' to '/Users/boltonbailey/.elan/tmp/n_pyewkm6glgurbq_file'
info: caused by: http request returned an unsuccessful status code: 404
=> Operation failed. Exit code: 1.
/Users/boltonbailey/Desktop/mathlibcontribution/lean4/src> curl --version
curl 8.6.0 (x86_64-apple-darwin23.0) libcurl/8.6.0 (SecureTransport) LibreSSL/3.3.6 zlib/1.2.12 nghttp2/1.61.0
Release-Date: 2024-01-31
Protocols: dict file ftp ftps gopher gophers http https imap imaps ipfs ipns ldap ldaps mqtt pop3 pop3s rtsp smb smbs smtp smtps telnet tftp
Features: alt-svc AsynchDNS GSS-API HSTS HTTP2 HTTPS-proxy IPv6 Kerberos Largefile libz MultiSSL NTLM NTLM_WB SPNEGO SSL threadsafe UnixSockets

/Users/boltonbailey/Desktop/mathlibcontribution/lean4/src> git --version
git version 2.39.2 (Apple Git-143)

/Users/boltonbailey/Desktop/mathlibcontribution/lean4/src> lean --version
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error:
could not download nonexistent lean version `lean4-stage0`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/expanded_assets/lean4-stage0' to '/Users/boltonbailey/.elan/tmp/pr_vdkwy20ra9g11_file'
info: caused by: http request returned an unsuccessful status code: 404
=> Operation failed. Exit code: 1.

[Matthew Ballard]

elan toolchain link lean4-stage0 build/release/stage0 after building the files

Similarly for stage1

[Bolton Bailey]

Eric Wieser said:

Ugh, why is Option.elim simp? That looks like the issue here

Even removing this, MvPolynomial.optionEquivLeft_apply becomes

MvPolynomial.optionEquivLeft_apply.{u, v} (R : Type u) (S₁ : Type v) [CommSemiring R] (a : MvPolynomial (Option S₁) R) :
  (optionEquivLeft R S₁) a = (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) a

Which again has more characters on the RHS of the equals sign.

[Bolton Bailey]

Matthew Ballard said:

elan toolchain link lean4-stage0 build/release/stage0 after building the files

Similarly for stage1

Ok, but the problem is that I don't know how to build this, I am getting

> lake build
info: downloading component 'lean'
Error(Download(HttpStatus(404)), State { next_error: None, backtrace: InternalBacktrace { backtrace: None } })
error: could not download nonexistent lean version `lean4-stage0`
info: caused by: could not download file from 'https://github.com/leanprover/lean/releases/expanded_assets/lean4-stage0' to '/Users/boltonbailey/.elan/tmp/46v_dlvxre2jxxew_file'
info: caused by: http request returned an unsuccessful status code: 404

[Matthew Ballard]

• mkdir -p build/release
• cd build/release
• cmake ../..
• make -jN for N = number of cores on your machine

[Matthew Ballard]

I am copying from memory from https://lean-lang.org/lean4/doc/dev/index.html#development-workflow

[Bolton Bailey]

Is it going to be a problem that I have not been able to upgrade my elan above version 1.4.2?

[Matthew Ballard]

Maybe? But you probably want to nuke your ~/.elan folder, uninstall it from homebrew and then reinstall using by piping the script from the repo

[Bolton Bailey]

Ok thanks @Matthew Ballard for all your help resolving my technical difficulties

@Kim Morrison , I have made a PR lean4#4504, currently very simple. Please let me know if there is something I should do in the way of making it better / making sure everyone is ok with it / making sure it doesn't break mathlib.

[Matthew Ballard]

Following the bot's suggestion: https://github.com/leanprover/lean4/pull/4504#issuecomment-2179478048

[Matthew Ballard]

Then you will be able to see the downstream breakage/lack of breakage

[Bolton Bailey]

That does not seem to have worked :frown:

[Bolton Bailey]

Are you sure that that is a good idea? This tutorial says "you should never rebase commits once they've been pushed to a public repository."

[Ruben Van de Velde]

PRs don't count

[Bolton Bailey]

Ok I am running the exact command it tells me to run, and nothing is happening

[Bolton Bailey]

> git rebase bc047b8530f76f75c4456192b3ca24ad28c85420 --onto 1cf71e54cf268e87cf5c43c830d953f5c88e6c39
Successfully rebased and updated refs/heads/desimp-option-elim.                        /0.7s

[Bolton Bailey]

But when I sync it doesn't show up on the PR

[Matthew Ballard]

Leo's suggestion in the comments should work

[Kim Morrison]

@Bolton Bailey, let us know if you need more help with the rebase.

[Bolton Bailey]

Thanks. I have tried your suggestion, and that does indeed seem to get me to a place where I can run

~/Desktop/mathlibcontribution/lean4 desimp-option-elim ........................ PIPE 11:07:02
> git remote -v
origin  https://github.com/BoltonBailey/lean4.git (fetch)
origin  https://github.com/BoltonBailey/lean4.git (push)
upstream        https://github.com/leanprover/lean4.git (fetch)
upstream        https://github.com/leanprover/lean4.git (push)                           /0.0s

~/Desktop/mathlibcontribution/lean4 desimp-option-elim ............................. 11:07:09
> git reset --hard upstream/nightly-with-mathlib

HEAD is now at 357b52928f fix: global definition shadowing a local one when using dot-notation (#4497)                                                                                 /0.7s

And this looks like it is working. VSCode now informs me that I have 35 commits to pull. I am not sure if I should pull those or not (I tried both ways, I don't think either worked, there weren't any instructions about that from Leo). If I proceed without pulling

~/Desktop/mathlibcontribution/lean4 desimp-option-elim <35 ......................... 11:07:23
> git cherry-pick 1c29870c1aa

[desimp-option-elim 0f1e343901] add changes
 Date: Wed Jun 19 17:04:00 2024 -0400
 1 file changed, 4 insertions(+), 1 deletion(-)                                          /0.2s

~/Desktop/mathlibcontribution/lean4 desimp-option-elim <35>1 ....................... 11:09:14
> git cherry-pick 4554124b873
[desimp-option-elim 6eece7c06e] remove duped lemmas, simp preexisting ones
 Date: Wed Jun 19 17:12:24 2024 -0400
 2 files changed, 2 insertions(+), 5 deletions(-)                                        /0.1s

After these commands the VSCode indicator says there are now 2 commands to push. But

~/Desktop/mathlibcontribution/lean4 desimp-option-elim <35>2 ....................... 11:09:18
> git push
To https://github.com/BoltonBailey/lean4.git
 ! [rejected]              desimp-option-elim -> desimp-option-elim (non-fast-forward)
error: failed to push some refs to 'https://github.com/BoltonBailey/lean4.git'
hint: Updates were rejected because the tip of your current branch is behind
hint: its remote counterpart. Integrate the remote changes (e.g.
hint: 'git pull ...') before pushing again.
hint: See the 'Note about fast-forwards' in 'git push --help' for details.               /0.6s

So it looks like I screwed up not pulling before

~/Desktop/mathlibcontribution/lean4 desimp-option-elim <35>2 ....................... 11:11:18
> git pull
warning: skipped previously applied commit 0f1e343901
warning: skipped previously applied commit 6eece7c06e
hint: use --reapply-cherry-picks to include skipped commits
hint: Disable this message with "git config advice.skippedCherryPicks false"
Successfully rebased and updated refs/heads/desimp-option-elim.                          /1.3s

But now it says I have nothing to push

~/Desktop/mathlibcontribution/lean4 desimp-option-elim ............................. 11:13:22
> git push
Everything up-to-date                                                                    /0.6s

[Bolton Bailey]

And git log, if I am reading it right, tells me I am still branching off of master (although a later master than the one I started with, I do not understand how that is possible given I explicitly referenced nightly-with-mathlib branch above, I would expect it to either be that branch or that the whole process somehow failed and left me with the same branching off point as before).

commit 023d76943c3b66e06918e2beb052445786468e4a (HEAD -> desimp-option-elim, origin/desimp-opt
ion-elim)
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date:   Wed Jun 19 17:12:24 2024 -0400

    remove duped lemmas, simp preexisting ones

commit 20ba9b0405337b4eb9c60505ea7a12a1b2dc7319
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date:   Wed Jun 19 17:04:00 2024 -0400

    add changes

commit 3d1d9c04938676f939a4d5f6233575b47cb6f2d6
Merge: 0ac79832a0 84e46162b5
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date:   Fri Jun 21 10:44:15 2024 -0400

    Merge branch 'leanprover:master' into desimp-option-elim

commit 84e46162b5d25581039cd575c40bc6bd347f0853 (upstream/master)
Author: David Thrane Christiansen <david@davidchristiansen.dk>
Date:   Fri Jun 21 14:49:30 2024 +0200

    feat: more infrastructure for tactic documentation (#4490)

    This is the groundwork for a tactic index in generated documentation, as
    there was in Lean 3. There are a few challenges to getting this to work
    well in Lean 4:
    * There's no natural notion of *tactic identity* - a tactic may be
    specified by multiple syntax rules (e.g. the pattern-matching version of
    `intro` is specified apart from the default version, but both are the
    same from a user perspective)
    * There's no natural notion of *tactic name* - here, we take the
    pragmatic choice of using the first keyword atom in the tactic's syntax
    specification, but this may need to be overridable someday.
    * Tactics are extensible, but we don't want to allow arbitrary imports
    to clobber existing tactic docstrings, which could become unpredictable
    in practice.

[Matthew Ballard]

You need to force push to the remote after cherry picking

[Bolton Bailey]

:octopus:

[Bolton Bailey]

Ok it seems like it worked, but the PR is still not showing a CI for checking mathlib. What has gone wrong now?

commit 7bc3fd366cca2df130c302584c1fa8fa5adc7ca5 (HEAD -> desimp-option-elim, origin/desimp-option-elim)
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date:   Wed Jun 19 17:12:24 2024 -0400

    remove duped lemmas, simp preexisting ones

commit 6dee7a13643ee971daf52f23b3fd23f64d076df1
Author: Bolton Bailey <bolton.bailey@gmail.com>
Date:   Wed Jun 19 17:04:00 2024 -0400

    add changes

commit 357b52928f905bfb85a3496e411cf12fa20e730c (upstream/nightly-with-mathlib)
Author: Leonardo de Moura <leomoura@amazon.com>
Date:   Wed Jun 19 07:52:45 2024 +0200

    fix: global definition shadowing a local one when using dot-notation (#4497)

    closes #3079

[Bolton Bailey]

The PR CI says "PR branched off: — nightly-2024-06-19", is that how it's supposed to be?

[Matthew Ballard]

You are good. You broke mathlib :)

[Matthew Ballard]

branch#lean-pr-testing-4504 should be made whole now

[Bolton Bailey]

Oh sweet, I just needed to wait. Thanks again!

[Matthew Ballard]

You got to 4659/4678 so not painful

[Bolton Bailey]

Getting the following error on branch#lean-pr-testing-4504

info: downloading component 'lean'
error: binary package was not provided for 'darwin_aarch64'

(Might be able to fix it even without lean running though)

[Matthew Ballard]

You need to ask a core maintainer to apply the full-CI tag

[Matthew Ballard]

Unless you want to drop into something running linux

[Matthew Ballard]

Or go blind

[Bolton Bailey]

I will try going blind for now

[Bolton Bailey]

Ok, I got mathlib building in branch#lean-pr-testing-4504. What's the next step? Do I have to make a mathlib PR (that doesn't seem right, since surely mathlib won't build without this low level change)?

[Matthew Ballard]

Now you wait on review.