Zulip Chat Archive

Stream: new members

Topic: Apply in an assumption?


view this post on Zulip Pedro Minicz (May 17 2020 at 00:03):

How can I apply a function to an assumption? Suppose I have h₁ : p and f : p → q, I want to end with a hypothesis of type q without using have h₂ : q, ....

view this post on Zulip Alex J. Best (May 17 2020 at 00:06):

specialize f h\_1

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 00:11):

replace is also sometimes useful.

view this post on Zulip Jeremy Avigad (May 17 2020 at 00:20):

Another tip: you can use h\1 instead of h\_1. It was a long time before I realized that.

view this post on Zulip Pedro Minicz (May 17 2020 at 00:22):

@Jeremy Avigad wow, thanks for the tip! I am sure I would go a long time without noticing that myself!

view this post on Zulip Pedro Minicz (May 17 2020 at 00:23):

In general I am having a very frustrating time trying to apply tactics to assumptions. Is the a "general" way of doing it? Or a cheat-sheet with many such instances?

view this post on Zulip Alex J. Best (May 17 2020 at 00:24):

Can you say a little more what you mean by this? Tactics like simp at h, rw at h, ring at h or something else?

view this post on Zulip Pedro Minicz (May 17 2020 at 00:33):

Not being able to apply at is particularly annoying. Other than that I guess most of my frustration is coming from now being familiar with simplification in Lean yet.

view this post on Zulip Kevin Buzzard (May 17 2020 at 00:36):

Computer scientists would rather you applied their tactics to the goal, which means you have to learn how to explain your proofs backwards. "It suffices to prove this, so it suffices to prove that, so...and so it suffices to prove something which is already an assumption".

view this post on Zulip Kevin Buzzard (May 17 2020 at 00:36):

If you think you want to argue forwards, they tell you that the forwards step should be split off as a separate lemma

view this post on Zulip Alex J. Best (May 17 2020 at 00:36):

I guess normally I use have := f h quite a bit which is pretty short (and then rw blah at this later) if I want to keep the old hypothesis (otherwise specialize or replace). Often I then notice that I only use f h once so giving it a name isn't needed, you can just do cases f h for example.

view this post on Zulip Kevin Buzzard (May 17 2020 at 00:38):

Yes sometimes the trick is not to make h at all. Beginner mathematicians are very good at generating lots and lots of intermediate hypotheses in their proofs, that is the sort of thing that happens if you argue forwards and go slowly and carefully.

view this post on Zulip Kevin Buzzard (May 17 2020 at 00:38):

Once you learn how to use lean a bit better then you start taking shortcuts

view this post on Zulip Bryan Gin-ge Chen (May 17 2020 at 00:40):

I think instead of apply at we have to write apply_fun at. Maybe this will be changed.

view this post on Zulip Mario Carneiro (May 17 2020 at 00:55):

I think we should add apply at though

view this post on Zulip Mario Carneiro (May 17 2020 at 00:55):

apply_fun at is not the same

view this post on Zulip Mario Carneiro (May 17 2020 at 00:55):

the equivalent of apply f at h is replace h := f h

view this post on Zulip Scott Morrison (May 17 2020 at 04:28):

I made an issue to track doing this: https://github.com/leanprover-community/lean/issues/247.

view this post on Zulip Scott Morrison (May 17 2020 at 04:28):

(This has to happen in community lean, not mathlib.)

view this post on Zulip Alex J. Best (May 17 2020 at 04:31):

Why does it need to be in lean? EDIT oh because you're redefining apply

view this post on Zulip Scott Morrison (May 17 2020 at 04:33):

If that sounds intimidating, it would be great for someone to write an apply' tactic that allowed the at syntax, and then someone who felt braver about community lean could migrate it once it had been tested/reviewed in mathlib.

view this post on Zulip Kevin Buzzard (May 17 2020 at 08:31):

This is a really nice way to do it. Beginner mathematician users who think forwards often want to apply functions to hypotheses

view this post on Zulip Kevin Buzzard (May 17 2020 at 08:32):

And stuff like rw works on hypotheses and goals even though in some sense it's doing different things in each case

view this post on Zulip Pedro Minicz (May 18 2020 at 00:49):

Yes, the difference in behavior would be more glaring on apply, but still a far cry from intimidating I would say.

view this post on Zulip Jalex Stark (May 18 2020 at 02:10):

so the behavior of apply f at h is supposed to be something like replace h := f _* h where by _* i mean "some nonnegative number of underscores"?

or is it already enough for it to be an alias for replace h := f h?

view this post on Zulip Mario Carneiro (May 18 2020 at 02:15):

I was wondering the same thing. I suppose it wouldn't be hard to support the described behavior - just revert h and then apply f

view this post on Zulip Mario Carneiro (May 18 2020 at 02:52):

Actually, I don't think my suggestion will work, because the expected type is not known. I think, in order to make it predictable, the h should go in as the first explicit argument. That way you can write apply @f _ _ _ at h if it gets the wrong argument

view this post on Zulip Mario Carneiro (May 18 2020 at 02:53):

in other words, replace h := f h _*

view this post on Zulip Mario Carneiro (May 18 2020 at 02:54):

but even here it seems like the _* could end up being problematic because you have no control

view this post on Zulip Mario Carneiro (May 18 2020 at 02:54):

maybe it should just literally be replace h := f h

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 02:59):

Once you have f h : ∀ ..., ... you can't guess how many arguments the user wants to be gone, so I think that replace h := f h is the only "predictable" option.

view this post on Zulip Yury G. Kudryashov (May 18 2020 at 03:01):

I mean, if after apply f at h one gets h : ∀ ..., ..., then specialize can help with getting rid of .

view this post on Zulip Jalex Stark (May 18 2020 at 03:22):

how is apply f h _* different from apply f h?

view this post on Zulip Jalex Stark (May 18 2020 at 03:24):

i guess the first one will infer whatever arguments it can, and the second one will infer exactly the arguments marked as optional with {}

view this post on Zulip Mario Carneiro (May 18 2020 at 03:24):

it's not, apply f h is the same as refine f h _*

view this post on Zulip Mario Carneiro (May 18 2020 at 03:24):

or did you mean something else?

view this post on Zulip Jalex Stark (May 18 2020 at 03:24):

oh okay, thanks

view this post on Zulip Jalex Stark (May 18 2020 at 03:25):

Mario Carneiro said:

in other words, replace h := f h _*

oh, right, the question was here, how is f h _* different from f h?

view this post on Zulip Jalex Stark (May 18 2020 at 03:25):

(also, just to check, _* is not literally Lean code, right?)

view this post on Zulip Mario Carneiro (May 18 2020 at 03:26):

in apply (no at), the goal type is known so you can match pis

view this post on Zulip Mario Carneiro (May 18 2020 at 03:26):

with apply at you don't know what the target type is, so there isn't anything to determine how many _ to put

view this post on Zulip Mario Carneiro (May 18 2020 at 03:26):

so the only reasonable option is to be conservative and not introduce any _ as Yury says

view this post on Zulip Mario Carneiro (May 18 2020 at 03:27):

_* is not lean code

view this post on Zulip Jalex Stark (May 18 2020 at 03:27):

okay, thanks, I think I am de-confused


Last updated: May 10 2021 at 16:20 UTC