equivalent of squeeze_simp for linarith, group, etc?

Stream: new members

[Chris M]

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]

what's the statement?

[Scott Morrison]

by kenny

[Scott Morrison]

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

[Scott Morrison]

hence there's no linarith?

[Chris M]

sorry I failed to copy the entire statement. edited

[Scott Morrison]

the lemmas you want are lt_of_lt_of_le and friends

[Scott Morrison]

find them by making a simpler example and using library_search

[Kenny Lau]

just use calc

[Chris M]

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

[Chris M]

library_search gives me unkown identifier 'library_search'

[Kenny Lau]

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]

oh dear. import tactic :-)

[Scott Morrison]

you really should get used to using library_search!

[Chris M]

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

[Scott Morrison]

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

[Scott Morrison]

library_search will only use a single lemma from the library

[Scott Morrison]

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

[Scott Morrison]

to identify the lemma that you want to use

[Chris M]

oh I see.

[Chris M]

nice

[Scott Morrison]

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

[Scott Morrison]

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

[Chris M]

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

[Chris M]

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]

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]

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

[Scott Morrison]

that's how it should work

[Chris M]

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]

mono?

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Mario Carneiro]

@[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]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

The library_search bug is fixed in #3270

[Scott Morrison]

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]

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]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Chris M]

could that mean that I followed the installation instructions incorrectly?

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

There's also advice at #contrib about making PRs

[Scott Morrison]

leanproject up perhaps

[Scott Morrison]

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]

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]

ah it's leanproject update-mathlib

[Chris M]

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]

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]

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

[Chris M]

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

[Alena Gusakov]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Jalex Stark]

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

[Chris M]

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]

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

[Chris M]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Chris M]

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]

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

[Chris M]

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]

Invite sent.

[Chris M]

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]

Yup, that will start the PR

[Bryan Gin-ge Chen]

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]

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

[Johan Commelin]

Oops, Bryan was a little bit faster

[Bryan Gin-ge Chen]

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

[Chris M]

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]

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

[Bryan Gin-ge Chen]

well, escape and then :x

[Johan Commelin]

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

[Chris M]

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

[Johan Commelin]

Is that commit message appearing in VScode?

[Johan Commelin]

I thought you wrote git commit -a in a terminal

[Johan Commelin]

Did you configure git to use VScode as the editer?

[Chris M]

yes, actually it seems :x also worked.

[Chris M]

Yes I wrote it in the VSCode terminal

[Johan Commelin]

Aah, so it was vim inside that terminal

[Johan Commelin]

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

[Johan Commelin]

What happens on Windows?

[Johan Commelin]

They don't default to vim, I guess.

[Bryan Gin-ge Chen]

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

[Chris M]

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]

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

[Johan Commelin]

@Chris M I don't see the PR yet

[Chris M]

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

[Bryan Gin-ge Chen]

@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]

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

[Johan Commelin]

You're almost done!

[Chris M]

How about now?

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Yep! #3318

[Johan Commelin]

There you go. Top of the list.

[Chris M]

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]

@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]

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

[Patrick Stevens]

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]

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

[Johan Commelin]

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]

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]

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]

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

[Johan Commelin]

The dot notation gives a shorthand for that.

[Johan Commelin]

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

[Chris M]

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

[Johan Commelin]

No, for iff.mpr

[Chris M]

right. ok cool

[Johan Commelin]

Because \iff is notation for iff

[Chris M]

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