Zulip Chat Archive

Stream: new members

Topic: Apply in an assumption?


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, ....

Alex J. Best (May 17 2020 at 00:06):

specialize f h\_1

Bryan Gin-ge Chen (May 17 2020 at 00:11):

replace is also sometimes useful.

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.

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!

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?

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?

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.

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".

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

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.

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.

Kevin Buzzard (May 17 2020 at 00:38):

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

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.

Mario Carneiro (May 17 2020 at 00:55):

I think we should add apply at though

Mario Carneiro (May 17 2020 at 00:55):

apply_fun at is not the same

Mario Carneiro (May 17 2020 at 00:55):

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

Scott Morrison (May 17 2020 at 04:28):

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

Scott Morrison (May 17 2020 at 04:28):

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

Alex J. Best (May 17 2020 at 04:31):

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

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.

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

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

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.

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?

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

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

Mario Carneiro (May 18 2020 at 02:53):

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

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

Mario Carneiro (May 18 2020 at 02:54):

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

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.

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 .

Jalex Stark (May 18 2020 at 03:22):

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

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 {}

Mario Carneiro (May 18 2020 at 03:24):

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

Mario Carneiro (May 18 2020 at 03:24):

or did you mean something else?

Jalex Stark (May 18 2020 at 03:24):

oh okay, thanks

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?

Jalex Stark (May 18 2020 at 03:25):

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

Mario Carneiro (May 18 2020 at 03:26):

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

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

Mario Carneiro (May 18 2020 at 03:26):

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

Mario Carneiro (May 18 2020 at 03:27):

_* is not lean code

Jalex Stark (May 18 2020 at 03:27):

okay, thanks, I think I am de-confused

Eric Wieser (Oct 31 2022 at 23:31):

Should the semantics instead be replace h := f _* h? That way apply f _ _ at h is similar to apply f at h in the same way that apply f _ _ is similar to apply f.


Last updated: Dec 20 2023 at 11:08 UTC