Zulip Chat Archive

Stream: general

Topic: apply_fun

Patrick Massot (Jul 04 2019 at 12:41):

I'm trying to get rid of all the small lemmas and tactic I wrote during my undergrad course using Lean. The next thing is https://gist.github.com/PatrickMassot/a54fb57815ce748ebc907d66f491bb0d which is a small tactic wrapping congr_arg. I know it's kind of stupid, but I didn't feel like explaining to students that going from h : a = b to h : f(a) = f(b) required applying a lemma (especially with a weird name). In real world we say "apply f" to the assumption h, so I wrote apply_fun f at h. Then I generalized to the case of inequalities, but didn't actually use that version in the end. The question is: can I prepare a mathlib PR? I don't expect this tactic to be used much in mathlib itself, but since I managed to get push_neg and contraposein then maybe teaching tactics are fine.

Simon Hudon (Jul 04 2019 at 12:49):

I think we could merge that. For inequalities, how do you feed in a proof that f is monotonic?

Patrick Massot (Jul 04 2019 at 12:54):

I don't understand the question

Patrick Massot (Jul 04 2019 at 12:55):

Is something unclear in the docstring or examples?

Patrick Massot (Jul 04 2019 at 12:55):

Or maybe you read the Zulip post but not the gist?

Simon Hudon (Jul 04 2019 at 13:01):

I didn't read the gist. Sorry. Let me do that now

Simon Hudon (Jul 04 2019 at 13:02):

There's a mono attribute that the tactic mono uses. You could use it to discharge side goals sometimes

Patrick Massot (Jul 04 2019 at 13:04):

How would that work?

Patrick Massot (Jul 04 2019 at 13:05):

Should I try running the mono tactic?

Simon Hudon (Jul 04 2019 at 13:14):

I think that would be the simplest way to do it

Patrick Massot (Jul 04 2019 at 13:25):

I struggle to find any example that would work for tests. There are almost no mono lemma in mathlib :sad:

Simon Hudon (Jul 04 2019 at 14:27):

Really? What are you looking for?

Patrick Massot (Jul 04 2019 at 14:28):

I found something

Patrick Massot (Jul 04 2019 at 14:28):

I'll open a PR

Patrick Massot (Jul 04 2019 at 14:34):

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

Simon Hudon (Jul 04 2019 at 15:48):

It looks good

Simon Hudon (Jul 04 2019 at 15:48):

The name might not be the best

Simon Hudon (Jul 04 2019 at 15:50):

I could expect people to understand apply_fun as the same as apply ... in ... in Coq. Against your early intuition, I'd be tempted to mention congr in the name. The tactic might even be unified with congr'

Patrick Massot (Jul 04 2019 at 16:19):

This is a tactic for students, not Coq users...

Simon Hudon (Jul 04 2019 at 16:24):

That is true but if we want to put it in mathlib, it has to make sense to more than just your students. And comparing to Coq is useful because they have solved similar problems before so making the same choices that they made at least brings in the thought that they put in their choices. Plus, it's good to not be different when we don't need to

Johan Commelin (Jul 04 2019 at 16:26):

We'll also want the version where you evaluate f = g on the inputs x = y. Is that supported?

Patrick Massot (Jul 04 2019 at 16:56):

Simon, what name would make you happy?

Patrick Massot (Jul 04 2019 at 16:57):

Johan, your version can be obtained by apply_fun followed by rw. I don't see how to make something simpler.

Jeremy Avigad (Jul 05 2019 at 20:43):

Patrick, do you think students really prefer apply_fun f at h to rw h? I know they are not the same, but for purposes like this rw is intuitive, and it is the right idiom.

Patrick Massot (Jul 05 2019 at 21:31):

I don't understand this question. Those two tactics don't do the same thing

Patrick Massot (Jul 05 2019 at 21:36):

How do you want to do the example in tactics.md https://github.com/leanprover-community/mathlib/pull/1184/files with rw?

Chris Hughes (Jul 05 2019 at 21:43):

have : f x = f y, by rw h,

Chris Hughes (Jul 05 2019 at 21:45):

40 billion tactics to remember to slightly shorten things isn't necessarily easier than just knowing have and rw, which are more powerful, if more verbose.

Reid Barton (Jul 05 2019 at 22:11):

When I want to do this I usually also want to replace the old hypothesis, too, though. So I write something like replace h := congr_arg f h. That is already a bit outside the most commonly used tactics, so I wouldn't mind having a specialized way to write it.

Yury G. Kudryashov (Jul 05 2019 at 22:58):

With just replace and rw: replace h : f x = f y := by rw h

Yury G. Kudryashov (Jul 05 2019 at 22:59):

Though this way one has to write f x = f y explicitly. This might be inconvenient for long x and y

Patrick Massot (Jul 06 2019 at 13:47):

I think none of these alternative capture the fact that we have an atomic operation "apply f to h".

Patrick Massot (Jul 08 2019 at 16:05):

Shall we merge #1184 then?

Simon Hudon (Jul 09 2019 at 00:24):

Yes go ahead

Last updated: Dec 20 2023 at 11:08 UTC