Apply in an assumption?

Stream: new members

[Pedro Minicz]

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]

specialize f h\_1

[Bryan Gin-ge Chen]

replace is also sometimes useful.

[Jeremy Avigad]

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

[Pedro Minicz]

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

[Pedro Minicz]

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]

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]

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]

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]

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]

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]

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]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

I think we should add apply at though

[Mario Carneiro]

apply_fun at is not the same

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Alex J. Best]

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

[Scott Morrison]

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]

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

[Kevin Buzzard]

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

[Pedro Minicz]

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

[Jalex Stark]

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]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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]

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

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Mario Carneiro]

or did you mean something else?

[Jalex Stark]

oh okay, thanks

[Jalex Stark]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

_* is not lean code

[Jalex Stark]

okay, thanks, I think I am de-confused

[Eric Wieser]

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.