Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Jul 02 2020 at 04:38):

what's the statement?

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:38):

by kenny

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:39):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:39):

hence there's no linarith?

view this post on Zulip Chris M (Jul 02 2020 at 04:40):

sorry I failed to copy the entire statement. edited

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:40):

the lemmas you want are lt_of_lt_of_le and friends

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:40):

find them by making a simpler example and using library_search

view this post on Zulip Kenny Lau (Jul 02 2020 at 04:41):

just use calc

view this post on Zulip Chris M (Jul 02 2020 at 04:42):

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

view this post on Zulip Chris M (Jul 02 2020 at 04:42):

library_search gives me unkown identifier 'library_search'

view this post on Zulip 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₃

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:43):

oh dear. import tactic :-)

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:43):

you really should get used to using library_search!

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:45):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:45):

library_search will only use a single lemma from the library

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:45):

to identify the lemma that you want to use

view this post on Zulip Chris M (Jul 02 2020 at 04:45):

oh I see.

view this post on Zulip Chris M (Jul 02 2020 at 04:45):

nice

view this post on Zulip Scott Morrison (Jul 02 2020 at 04:45):

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

view this post on Zulip 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 :-)

view this post on Zulip Chris M (Jul 02 2020 at 04:48):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 02 2020 at 05:22):

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

view this post on Zulip Scott Morrison (Jul 02 2020 at 05:22):

that's how it should work

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jul 02 2020 at 05:29):

mono?

view this post on Zulip Scott Morrison (Jul 02 2020 at 05:35):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 02 2020 at 05:36):

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

view this post on Zulip 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*

view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 02 2020 at 05:39):

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

view this post on Zulip 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 :)

view this post on Zulip Scott Morrison (Jul 02 2020 at 06:18):

The library_search bug is fixed in #3270

view this post on Zulip 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.

view this post on Zulip 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? :)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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? :-)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 03 2020 at 01:56):

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

view this post on Zulip Scott Morrison (Jul 03 2020 at 01:56):

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

view this post on Zulip 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.

view this post on Zulip 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! :-)

view this post on Zulip Chris M (Jul 03 2020 at 02:00):

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

view this post on Zulip Chris M (Jul 03 2020 at 02:01):

could that mean that I followed the installation instructions incorrectly?

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 03 2020 at 02:03):

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

view this post on Zulip Scott Morrison (Jul 03 2020 at 02:04):

There's also advice at #contrib about making PRs

view this post on Zulip Scott Morrison (Jul 03 2020 at 02:04):

leanproject up perhaps

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Chris M (Jul 03 2020 at 02:06):

ah it's leanproject update-mathlib

view this post on Zulip 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)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 ?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.)

view this post on Zulip 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!)

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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?

view this post on Zulip Jalex Stark (Jul 08 2020 at 04:31):

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

view this post on Zulip 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'

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 04:39):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 04:45):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 04:45):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 04:49):

Invite sent.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jul 08 2020 at 04:52):

Yup, that will start the PR

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:00):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:00):

Oops, Bryan was a little bit faster

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 05:03):

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

view this post on Zulip 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)

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 05:04):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 05:04):

well, escape and then :x

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:05):

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

view this post on Zulip Chris M (Jul 08 2020 at 05:05):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:05):

Is that commit message appearing in VScode?

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:05):

I thought you wrote git commit -a in a terminal

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:06):

Did you configure git to use VScode as the editer?

view this post on Zulip Chris M (Jul 08 2020 at 05:06):

yes, actually it seems :x also worked.

view this post on Zulip Chris M (Jul 08 2020 at 05:06):

Yes I wrote it in the VSCode terminal

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:06):

Aah, so it was vim inside that terminal

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:07):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:07):

What happens on Windows?

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:07):

They don't default to vim, I guess.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:09):

@Chris M I don't see the PR yet

view this post on Zulip Chris M (Jul 08 2020 at 05:09):

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

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 05:09):

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

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:09):

You're almost done!

view this post on Zulip Chris M (Jul 08 2020 at 05:10):

How about now?

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:10):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 08 2020 at 05:10):

Yep! #3318

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:10):

There you go. Top of the list.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Jul 08 2020 at 05:13):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Jul 10 2020 at 07:52):

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

view this post on Zulip Johan Commelin (Jul 10 2020 at 07:52):

The dot notation gives a shorthand for that.

view this post on Zulip Johan Commelin (Jul 10 2020 at 07:53):

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

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Jul 10 2020 at 08:03):

No, for iff.mpr

view this post on Zulip Chris M (Jul 10 2020 at 08:03):

right. ok cool

view this post on Zulip Johan Commelin (Jul 10 2020 at 08:03):

Because \iff is notation for iff

view this post on Zulip 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: May 08 2021 at 05:14 UTC