Zulip Chat Archive

Stream: new members

Topic: naming convention for this?

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

Here is a lemma that I've been asked to add mathlib:

@[mono]
lemma exp_mono : ∀ {x y : ℝ}, x ≤ y → exp x ≤ exp y :=
exp_strict_mono.monotone

What would be the right name for @[mono] lemma exp_mono : ∀ {x y : ℝ}, exp x ≤ exp y \to x ≤ y?

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

@Chris M I think I would go for exp_le_exp.

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

And its buddy will be exp_lt_exp.

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

Or are those names already taken by the iff versions?

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

while keeping exp_mono for x\leq y \to exp x \leq exp y?

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

Johan Commelin said:

Or are those names already taken by the iff versions?

yes they are

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

I don't like exp_strict_mono for the lt version.

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

You mean the existing one? that one does exist: lemma exp_strict_mono : strict_mono exp :=

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

So I suggest that you do a global search-replace:

  • exp_le_exp → exp_le_exp_iff
  • exp_lt_exp → exp_lt_exp_iff

And then use exp_le_exp and exp_lt_exp for the lemmas you want to add.

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

Chris M said:

You mean the existing one? that one does exist: lemma exp_strict_mono : strict_mono exp :=

Yes, but the statement is not in a form that the mono tactic understands.

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

wow ok. So the tutorials will also have to be changed.

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

ooh

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

I didn't realise that.

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

@Chris M Another idea:

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

State the lemma as @[mono] lemma exp_monotone : monotone exp :=

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

And then someone (@Patrick Massot) can teach the monotone tactic about strict_monotone, and we can tag the exp_strict_mono lemma afterwards

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

I don't get it. Why doesn't mono understand lemma exp_strict_mono : strict_mono exp? because strict_mono exp is used instead of its expanded definition ∀ ⦃a b⦄, a < b → f a < f b?

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

Exactly

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

Then why do you want me to add @[mono] lemma exp_monotone : monotone exp :=?

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

It recently was taught to unfold monotone. But I don't think it was taught to do the same for strict_monos

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

I see.

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

If you are feeling courageous, you can mimic Patrick's PR, and teach it about strict_mono as well.

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

Oh by "teach" you mean teaching the tactic itself, I thought you meant "make a tutorial about" :P

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

to be clear, "teach" doesn't imply anything using machine learning? we're just talking about normal coding ... ? :P

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

In particular, once the mono tactic understands strict_mono, it might be enough to tag exp_strict_mono

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

Let me find the commit for you. It was this week, I think.

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

Ok I'll try this.

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

https://github.com/leanprover-community/mathlib/pull/3310

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

btw is there a reason you want to change from exp_mono to exp_monotone? Also, what to name the other direction?

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

I think that this is the relevant line: https://github.com/leanprover-community/mathlib/pull/3310/files#diff-54c5eab6d816f396b485233519d628acR356

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

The naming convention is to use f_monotone when you prove monotone f

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

The other direction doesn't deserve a lemma, I think. Because we already have the iff version with exp_le_exp.

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

And the mono tactic will never use the other direction

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

I see

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

Oh, also this line: https://github.com/leanprover-community/mathlib/pull/3310/files#diff-46d8fb7fe470316c30396976c88b30a9R99

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

However, if we want mono to automatically deduce the foo_le_foo version from strict_mono foo, then we need a bit more work.

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

I don't have enough tactic writing skills to do that.

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

It seems it was only merged with master yesterday, so I have to update first. Is leanproject upgrade-mathlib essentially a wrapper for merging the master with my current (github) branch?

Scott Morrison (Jul 10 2020 at 11:20):

I'm not actually sure. I just use git merge origin/master for this.

Kevin Buzzard (Jul 10 2020 at 11:34):

leanproject up will get updated oleans automatically. Scott's version won't

Johan Commelin (Jul 10 2020 at 11:37):

@Chris M 

git commit -am WIP
git checkout master
leanproject up
git checkout -
git merge master

Scott Morrison (Jul 10 2020 at 11:39):

but what oleans will it get if you're merging with a local branch?

Scott Morrison (Jul 10 2020 at 11:40):

what does git checkout - do?

Johan Commelin (Jul 10 2020 at 11:40):

Switch to previous branch

Johan Commelin (Jul 10 2020 at 11:41):

Scott Morrison said:

but what oleans will it get if you're merging with a local branch?

You'll get the oleans from master. Which is usually what you want, if your edits aren't too big.

Mario Carneiro (Jul 10 2020 at 19:41):

@Chris M I suggest using exp_le_exp for exp x ≤ exp y <-> x ≤ y and nothing at all for exp x ≤ exp y \to x ≤ y (use the biconditional instead)

Last updated: Dec 20 2023 at 11:08 UTC