Zulip Chat Archive

Stream: new members

Topic: equivalent of squeeze_simp for linarith, group, etc?


Chris M (Jul 02 2020 at 04:37):

I'm trying to find out how to prove example (a b c d e : ℝ) (h₀ : a ≤ b) (h₁ : b < c) (h₂ : c ≤ d) (h₃ : d < e) : a < e := by linarith without using linarith. It would be useful to have something like squeeze_linarith. Does it exist?

Kenny Lau (Jul 02 2020 at 04:38):

what's the statement?

Scott Morrison (Jul 02 2020 at 04:38):

by kenny

Scott Morrison (Jul 02 2020 at 04:39):

linarith uses Fourier-Motzkin elimination, which does not tend to give human readable proofs.

Scott Morrison (Jul 02 2020 at 04:39):

hence there's no linarith?

Chris M (Jul 02 2020 at 04:40):

sorry I failed to copy the entire statement. edited

Scott Morrison (Jul 02 2020 at 04:40):

the lemmas you want are lt_of_lt_of_le and friends

Scott Morrison (Jul 02 2020 at 04:40):

find them by making a simpler example and using library_search

Kenny Lau (Jul 02 2020 at 04:41):

just use calc

Chris M (Jul 02 2020 at 04:42):

It seems pretty annoying to get this to work with a tactic proof using apply.

Chris M (Jul 02 2020 at 04:42):

library_search gives me unkown identifier 'library_search'

Kenny Lau (Jul 02 2020 at 04:43):

import data.real.basic

example (a b c d e : ) (h₀ : a  b) (h₁ : b < c) (h₂ : c  d) (h₃ : d < e) :  a < e :=
calc  a
     b : h₀
... < c : h₁
...  d : h₂
... < e : h₃

Scott Morrison (Jul 02 2020 at 04:43):

oh dear. import tactic :-)

Scott Morrison (Jul 02 2020 at 04:43):

you really should get used to using library_search!

Chris M (Jul 02 2020 at 04:44):

Oh sorry, I didn't interpret it as a tactic. Ok. IN this case it gives me failed though.

Scott Morrison (Jul 02 2020 at 04:45):

Yes -- I really need to fix that error message :-)

Scott Morrison (Jul 02 2020 at 04:45):

library_search will only use a single lemma from the library

Scott Morrison (Jul 02 2020 at 04:45):

hence my suggestion that you do a smaller example (where you are chaining a single < and ≤ together)

Scott Morrison (Jul 02 2020 at 04:45):

to identify the lemma that you want to use

Chris M (Jul 02 2020 at 04:45):

oh I see.

Chris M (Jul 02 2020 at 04:45):

nice

Scott Morrison (Jul 02 2020 at 04:45):

once you know the lemma name, you build the proof yourself

Scott Morrison (Jul 02 2020 at 04:46):

(or use Kenny's suggestion, which is secretly using that calc knows the name of this lemma :-)

Chris M (Jul 02 2020 at 04:48):

So calc basically turns what you write into a proof using all the appropriate lemma names?

Chris M (Jul 02 2020 at 04:54):

So if I want to prove a theorem, library search will basically search the entire library for a lemma, and if it is possible to prove the theorem by just one direct application of a lemma in the library, applied to some sequence of the theorem's assumptions, then it will find it?

Chris M (Jul 02 2020 at 05:13):

maybe not because example (h: a ≤ b) : exp a ≤ exp b := by library_search gives me failed, even though it can be proved by exp_le_exp.mpr h

Scott Morrison (Jul 02 2020 at 05:22):

no, I'd say that's a library_search bug!

Scott Morrison (Jul 02 2020 at 05:22):

that's how it should work

Chris M (Jul 02 2020 at 05:27):

And what about this:
I have the following proof which type checks:

example (h₀ : d  e) : c + exp (a + d)  c + exp (a + e) :=
begin
  suffices h: exp (a + d)  exp (a + e), {linarith},
  apply exp_le_exp.mpr,
  linarith
end

but the following doesn't:

example (h₀ : d  e) : c + exp (a + d)  c + exp (a + e) :=
begin
  linarith [exp_le_exp.mpr]
end

Is there a way to make this work?

Mario Carneiro (Jul 02 2020 at 05:29):

mono?

Scott Morrison (Jul 02 2020 at 05:35):

Indeed, it's a bug in library_search involving stuck metavariables.

Scott Morrison (Jul 02 2020 at 05:35):

The problem is that the .mp direction of exp_le_exp matches, giving a new goal exp (exp a) <= exp (exp b), which can't be discharged

Scott Morrison (Jul 02 2020 at 05:36):

this then seems to prevent the .mpr direction from being tried.

Mario Carneiro (Jul 02 2020 at 05:37):

@[mono] lemma exp_le_exp' {x y : } : x  y  exp x  exp y := exp_le_exp.2

example (h₀ : d  e) : c + exp (a + d)  c + exp (a + e) :=
by mono*

Mario Carneiro (Jul 02 2020 at 05:39):

linarith [exp_le_exp.mpr] isn't going to work because linarith doesn't do heuristic instantiation, it's not an SMT solver

Scott Morrison (Jul 02 2020 at 05:39):

@Chris M, want to make a PR adding that @[mono] tag? :-)

Mario Carneiro (Jul 02 2020 at 05:43):

Hi @Rob Lewis , how's the polya tactic going? I recall this example being on the recommended list :)

Scott Morrison (Jul 02 2020 at 06:18):

The library_search bug is fixed in #3270

Scott Morrison (Jul 02 2020 at 06:18):

import analysis.special_functions.exp_log

open real

example {a b : } (h: a  b) : exp a  exp b := by library_search

now works, finding exp_le_exp.

Rob Lewis (Jul 02 2020 at 10:26):

Mario Carneiro said:

Hi Rob Lewis , how's the polya tactic going? I recall this example being on the recommended list :)

Coming 202? :)

Rob Lewis (Jul 02 2020 at 10:28):

As for the original question in this thread, there are complications with squeeze_linarith. linarith makes no guarantees to find a minimal proof, and often finds non-minimal ones -- twice now, I've made changes that caused the linter to start complaining about unused arguments in theorems, because before it was using unnecessary hypotheses just because they were there.

Rob Lewis (Jul 02 2020 at 10:30):

There are a number of steps between the input list of hypotheses and what linarith actually runs on. Tracking the original source of each hypothesis would take some overhead.

Kevin Buzzard (Jul 02 2020 at 10:33):

Rob Lewis said:

Mario Carneiro said:

Hi Rob Lewis , how's the polya tactic going? I recall this example being on the recommended list :)

Coming 202? :)

Aah, so is this a promise that it will be finished within a decade? :-)

Rob Lewis (Jul 02 2020 at 10:34):

Unlike simp vs simp only, linarith is not necessarily so much slower than linarith only. Depending on what else is in the context, what variables are present, the order it finds things, etc., there can be very little overhead to just using linarith. nlinarith only gains a bit more over nlinarith though.

Rob Lewis (Jul 02 2020 at 10:35):

And one of the main uses of squeeze_simp is to allow nonterminal simps; there's no notion of a nonterminal linarith.

Mario Carneiro (Jul 02 2020 at 10:36):

Kevin Buzzard said:

Rob Lewis said:

Mario Carneiro said:

Hi Rob Lewis , how's the polya tactic going? I recall this example being on the recommended list :)

Coming 202? :)

Aah, so is this a promise that it will be finished within a decade? :-)

or in about 18000 years...

Rob Lewis (Jul 02 2020 at 10:38):

Scott Morrison said:

linarith uses Fourier-Motzkin elimination, which does not tend to give human readable proofs.

Note that the FM elimination isn't verified. linarith uses an oracle to find a linear combination of the input hypotheses that simplifies to a proof of 0 < 0. The "readable" output of linarith is something like 5*h1 + 3*h2 + 10*h3 = 0 < 0.

Rob Lewis (Jul 02 2020 at 10:39):

There's not much it can produce for you to copy-paste, but if you're curious about what it finds, you can look toward the bottom of the output with set_option trace.linarith true.

Rob Lewis (Jul 02 2020 at 10:43):

Aah, so is this a promise that it will be finished within a decade? :-)

I have a strong suspicion that if I sit down and refactor the code, I'll spend a lot of time to conclude that it can't be done efficiently in Lean 3, and I can't afford that time right now. :four_leaf_clover:

Chris M (Jul 03 2020 at 01:48):

Scott Morrison said:

The library_search bug is fixed in #3270

:D, I tried installing the new version of lean wit hpip install --upgrade mathlibtools and also elan self update, but neither worked. How do I get the new version?

Chris M (Jul 03 2020 at 01:49):

Scott Morrison said:

Chris M, want to make a PR adding that @[mono] tag? :-)

What is a PR? Does it mean, edit to the library? If so, I want to do that yes :). I have no idea how though. (no real experience with github)

Scott Morrison (Jul 03 2020 at 01:56):

Ah -- so those are reasonable commands for upgrading Lean itself, but here you need to update mathlib.

Scott Morrison (Jul 03 2020 at 01:56):

(Lean changes about once a week, mathlib about every two hours. :-)

Scott Morrison (Jul 03 2020 at 01:56):

I think leanproject upgrade is the usual incantation, assuming you have previously followed the #install instructions.

Scott Morrison (Jul 03 2020 at 01:57):

A PR is a "pull request". It means you make a branch of mathlib, make the changes you'd like, and then push that branch to github, and ask that the community reviews it.

Scott Morrison (Jul 03 2020 at 01:58):

Often anyone's first PR will go through lots of comment and revision, as it takes a little while to learn all the ins and outs of mathlib style. But we try not to bite! :-)

Chris M (Jul 03 2020 at 02:00):

It gives me Error: No such command 'upgrade'. and similarly, Error: No such command 'update'.

Chris M (Jul 03 2020 at 02:01):

could that mean that I followed the installation instructions incorrectly?

Scott Morrison (Jul 03 2020 at 02:03):

No, it's just I'm the wrong person to ask, as apparently I don't use leanproject properly.

Scott Morrison (Jul 03 2020 at 02:03):

Just try leanproject and read the nice instructions? :-)

Scott Morrison (Jul 03 2020 at 02:04):

There's also advice at #contrib about making PRs

Scott Morrison (Jul 03 2020 at 02:04):

leanproject up perhaps

Scott Morrison (Jul 03 2020 at 02:05):

The first time you make a pull request to mathlib, you will need to fork mathlib on github, and push a new branch there, and make the PR from your fork.

Scott Morrison (Jul 03 2020 at 02:06):

Subsequent times you can ask for direct push access to non-master branches of mathlib, and then you don't need the fork.

Chris M (Jul 03 2020 at 02:06):

ah it's leanproject update-mathlib

Chris M (Jul 03 2020 at 02:14):

Ok. I assume that I can do pull requests and push requests within VSCode? Do I need some kind of extension for this? (I've looked online and there are extensions but I'm not sure if this is the appropriate way of doing it for mathlib)

Chris M (Jul 03 2020 at 02:28):

Ok, I tried to find out how to do github pull requests in VSCode but I'm not making progress. Do I need to do this in a command line terminal instead?

Alena Gusakov (Jul 03 2020 at 02:30):

Just jumping in - git is much easier to use in terminal, personally recommend doing it through the command line

Chris M (Jul 03 2020 at 02:31):

Do I just execute the steps in point 5 of https://leanprover-community.github.io/contribute/index.html ?

Alena Gusakov (Jul 03 2020 at 02:33):

Pretty much - though I've had trouble using the branch command in the first bullet point. My workaround was just doing leanproject get mathlib and then navigating into mathlib, and doing git checkout -b branch-name

Alena Gusakov (Jul 03 2020 at 02:36):

Oh wait hold up - I misunderstood the question. Those steps are for making changes to mathlib ignore that, I skimmed through the thread and misread

Scott Morrison (Jul 03 2020 at 02:40):

There are some nice VSCode extensions for using Git, but as Alena says it's worth learning to use the command line for git. (Note you can open a terminal right inside VSCode, so it's pretty smooth.)

Scott Morrison (Jul 03 2020 at 02:43):

Neither of these replace using git on the command line for branching/merging operations, but I also use the extensions

  • GitLens (mostly it adds the "blame" lines everywhere unobtrusively, which is nice for understanding who wrote what in mathlib)
  • Github Pull Requests (perhaps only useful once you regularly have multiple PRs open concurrently!)

Bryan Gin-ge Chen (Jul 03 2020 at 03:09):

I highly recommend reading a bit of the git book if you're not comfortable with git. It's easy to get confused later on if you don't have a good mental model of what the various git commands are doing (or at least a place to look to figure it out).

Bryan Gin-ge Chen (Jul 03 2020 at 03:10):

I also frequently forget the commands for leanproject. Fortunately, just typing leanproject will return a help string with brief descriptions of all the commands.

Chris M (Jul 08 2020 at 04:26):

I've tried to push my branch to github with$ git push origin, but I'm getting the following error message:

fatal: The current branch master has no upstream branch.
To push the current branch and set the remote as upstream, use

    git push --set-upstream origin master

Chris M (Jul 08 2020 at 04:27):

Before that, I used: $ git commit -a and got the following:

On branch master

Initial commit

Untracked files:
  (use "git add <file>..." to include in what will be committed)
        .gitignore
        Chris_styleguide.lean
        leanpkg.toml
        mathlib_exp_le_exp-mono-tag/
        src/

nothing added to commit but untracked files present (use "git add" to track)

(all of this is in the terminal of vscode).

Chris M (Jul 08 2020 at 04:28):

Does this mean I did something wrong earlier, or is this fine? should I just use git push --set-upstream origin master?

Jalex Stark (Jul 08 2020 at 04:31):

yes, in this case you want to follow the advice git gives you

Chris M (Jul 08 2020 at 04:35):

This gives me the following error:

$ git push --set-upstream origin master
error: src refspec master does not match any
error: failed to push some refs to 'origin'

Bryan Gin-ge Chen (Jul 08 2020 at 04:39):

Did you create a repo on github? What does git remote -v say?

Chris M (Jul 08 2020 at 04:41):

git remote -v produces no text at all.

What I did is follow the guidelines at https://leanprover-community.github.io/contribute/index.html without any adjustments. I am not sure whether this created a repo on github or how to know.

Bryan Gin-ge Chen (Jul 08 2020 at 04:44):

That doesn't seem right. If I run (following the very first step in "Making a Pull Request"):

leanproject get -b mathlib:shiny_lemma
cd mathlib_shiny_lemma
git remote -v

I see:

origin  git@github.com:leanprover-community/mathlib.git (fetch)
origin  git@github.com:leanprover-community/mathlib.git (push)

Bryan Gin-ge Chen (Jul 08 2020 at 04:45):

Also, did we already give you write access to mathlib?

Bryan Gin-ge Chen (Jul 08 2020 at 04:45):

If not, please let us know what your github username is.

Chris M (Jul 08 2020 at 04:46):

Ok, I didn't do cd mathlib_shiny_lemma (note that this isn't on that webpage). Now that I did that, I'm getting

origin  https://github.com/leanprover-community/mathlib.git (fetch)
origin  https://github.com/leanprover-community/mathlib.git (push)

Bryan Gin-ge Chen (Jul 08 2020 at 04:47):

OK, good point. All the git commands need to be run inside mathlib_shiny_lemma.

Chris M (Jul 08 2020 at 04:48):

Bryan Gin-ge Chen said:

Also, did we already give you write access to mathlib?

I don't think so. My username is xxxxxxx

Bryan Gin-ge Chen (Jul 08 2020 at 04:49):

Invite sent.

Chris M (Jul 08 2020 at 04:51):

Accepted. After trying things again now, I'm getting:

$ git push --set-upstream origin exp_le_exp-mono-tag
Total 0 (delta 0), reused 0 (delta 0), pack-reused 0
remote:
remote: Create a pull request for 'exp_le_exp-mono-tag' on GitHub by visiting:
remote:      https://github.com/leanprover-community/mathlib/pull/new/exp_le_exp-mono-tag
remote:
To https://github.com/leanprover-community/mathlib.git
 * [new branch]        exp_le_exp-mono-tag -> exp_le_exp-mono-tag
Branch 'exp_le_exp-mono-tag' set up to track remote branch 'exp_le_exp-mono-tag' from 'origin'.

I'm assuming this is how things should go and I should follow the link https://github.com/leanprover-community/mathlib/pull/new/exp_le_exp-mono-tag

Johan Commelin (Jul 08 2020 at 04:52):

Yup, that will start the PR

Bryan Gin-ge Chen (Jul 08 2020 at 04:58):

I made a PR to tell users to run git commands inside the mathlib repo: https://github.com/leanprover-community/leanprover-community.github.io/pull/79

Feel free to suggest better wording.

Johan Commelin (Jul 08 2020 at 05:00):

https://github.com/leanprover-community/leanprover-community.github.io/pull/80

Johan Commelin (Jul 08 2020 at 05:00):

Oops, Bryan was a little bit faster

Bryan Gin-ge Chen (Jul 08 2020 at 05:03):

Yours edits are a little more detailed, so I closed my PR.

Chris M (Jul 08 2020 at 05:03):

It turned out that I didn't commit the right repository earlier, so didn't even get to write a commit message. Now that I can write a commit message I'm not sure what to do:
I'm getting this:

# Please enter the commit message for your changes. Lines starting
# with '#' will be ignored, and an empty message aborts the commit.
#
# On branch exp_le_exp-mono-tag
# Your branch is up to date with 'origin/exp_le_exp-mono-tag'.
#
# Changes to be committed:
#       modified:   src/data/complex/exponential.lean
#
~
~
~

I wrote

feat(src/data/complex/exponential)
added @[mono] tag to exp_le_exp and exp_lt_exp.

but it appeared ABOVE that long message, and I'm not sure how to actually send it. (enter doesn't work)

Bryan Gin-ge Chen (Jul 08 2020 at 05:04):

I guess you're probably in vim, so you have to type :x.

Bryan Gin-ge Chen (Jul 08 2020 at 05:04):

well, escape and then :x

Johan Commelin (Jul 08 2020 at 05:05):

Or nano? In which case it is Ctrl-X Ctrl-O or something like that.

Chris M (Jul 08 2020 at 05:05):

if you mean the text editor vim, no I'm in VSCode

Johan Commelin (Jul 08 2020 at 05:05):

Is that commit message appearing in VScode?

Johan Commelin (Jul 08 2020 at 05:05):

I thought you wrote git commit -a in a terminal

Johan Commelin (Jul 08 2020 at 05:06):

Did you configure git to use VScode as the editer?

Chris M (Jul 08 2020 at 05:06):

yes, actually it seems :x also worked.

Chris M (Jul 08 2020 at 05:06):

Yes I wrote it in the VSCode terminal

Johan Commelin (Jul 08 2020 at 05:06):

Aah, so it was vim inside that terminal

Johan Commelin (Jul 08 2020 at 05:07):

@Bryan Gin-ge Chen I guess we need instructions for that as well...

Johan Commelin (Jul 08 2020 at 05:07):

What happens on Windows?

Johan Commelin (Jul 08 2020 at 05:07):

They don't default to vim, I guess.

Bryan Gin-ge Chen (Jul 08 2020 at 05:07):

Hmm, maybe we can suggest writing the commit message together with git commit to avoid getting people stuck in vim?

Chris M (Jul 08 2020 at 05:08):

I THINK I did a pull request? If I open the link that the terminal in vscode gives me it says exp_le_exp-mono-tag had recent pushes 1 minute ago

Bryan Gin-ge Chen (Jul 08 2020 at 05:08):

I can't check right this moment, but I think git bash probably has vim?

Johan Commelin (Jul 08 2020 at 05:09):

@Chris M I don't see the PR yet

Chris M (Jul 08 2020 at 05:09):

That's on the github website I mean: https://gyazo.com/102bd44ed1630dedb48180bc76ee1ee0

Bryan Gin-ge Chen (Jul 08 2020 at 05:09):

@Chris M Nope, not yet. You have to visit https://github.com/leanprover-community/mathlib/compare/exp_le_exp-mono-tag and click the "Create Pull Request" button.

Bryan Gin-ge Chen (Jul 08 2020 at 05:09):

Or you can click the "Compare & pull request" button in your screenshot.

Johan Commelin (Jul 08 2020 at 05:09):

You're almost done!

Chris M (Jul 08 2020 at 05:10):

How about now?

Johan Commelin (Jul 08 2020 at 05:10):

https://github.com/leanprover-community/mathlib/pulls

Bryan Gin-ge Chen (Jul 08 2020 at 05:10):

Yep! #3318

Johan Commelin (Jul 08 2020 at 05:10):

There you go. Top of the list.

Chris M (Jul 08 2020 at 05:12):

great. So what happens now? I'm guessing others will review it and I would get a message somehow if it needs to be changed?

Johan Commelin (Jul 08 2020 at 05:12):

@Chris M I edited the PR title a bit. (We don't put src/ in the path, because it would be in almost every PR title, so we save 4 characters.)

Johan Commelin (Jul 08 2020 at 05:13):

Yup, see the "PR lifecycle" on the contribution page

Patrick Stevens (Jul 08 2020 at 06:29):

I'd suggest git config --global core.editor code as part of the standard initial setup workflow - anyone for whom VS Code is not a suitable Git editor will already know enough to not follow that command

Johan Commelin (Jul 08 2020 at 06:31):

Yup, that sounds like a good idea. But it shouldn't be part of the one-line-install-sh

Johan Commelin (Jul 08 2020 at 06:32):

I suggest:

Please execute git config --global core.editor code in a terminal if and only if you don't know what it means.

Chris M (Jul 10 2020 at 07:38):

Why is the following a well-formed term?
@[mono] lemma exp_mono : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y := exp_strict_mono.monotone
In particular, exp_strict_mono has type strict_mono exp, which is defined as

def strict_mono [has_lt α] [has_lt β] (f : α  β) : Prop :=
 a b⦄, a < b  f a < f b

I don't see why .monotone is well-formed here.

Johan Commelin (Jul 10 2020 at 07:51):

exp_strict_mono has type strict_mono exp. So when lean sees the . after exp_strict_mono it will start looking in the strict_mono namespace.

Johan Commelin (Jul 10 2020 at 07:52):

It finds strict_mono.monotone, and thus we get strict_mono.monotone exp_strict_mono

Johan Commelin (Jul 10 2020 at 07:52):

The dot notation gives a shorthand for that.

Johan Commelin (Jul 10 2020 at 07:53):

It's quite powerful when you chain these things together.

Chris M (Jul 10 2020 at 08:03):

Lets say I have an \iff lemma foo. Is foo.mpr actually shorthand for something like logic.mpr foo?

Johan Commelin (Jul 10 2020 at 08:03):

No, for iff.mpr

Chris M (Jul 10 2020 at 08:03):

right. ok cool

Johan Commelin (Jul 10 2020 at 08:03):

Because \iff is notation for iff

Chris M (Jul 19 2020 at 04:22):

This PR is merged now. Sorry for the delay, I had been reading about how git & github works.


Last updated: Dec 20 2023 at 11:08 UTC