How to apply at a hypothesis/assumtption?

Stream: general

[Viliam Vadocz]

Hi, beginner question:

I have hypothesis h: p and I want to apply not_not.mpr to get \not \not p. When I true by apply not_not.mpr at h, I get unexpected token 'at'. How do I use the apply tactic at a hypothesis?

[Ruben Van de Velde]

Please provide a #mwe

[Viliam Vadocz]

@Ruben Van de Velde

open Classical

example (p : Prop) : ¬p :=
  by
  intro h
  apply not_not.mpr at h
  sorry

Obviously, this is impossible to prove, but it shows the error.

[Henrik Böving]

What you are trying to do here is called forward reasoning, this is not what apply is for, apply is for backwards reasoning. What this means is that if you have a goal Q and a lemma P -> Q then applying that lemma changes your goal to P. What you can do for example is use have h2 := not_not.mpr h or if you wish to get rid of h: replace h := not_not.mpr h Note that you can optionally specifiy a type annotation like so: have name : type := proof

[Ruben Van de Velde]

It works if you add import Mathlib, though

[Viliam Vadocz]

Thanks, that answers my question.

[Shreyas Srinivas]

Henrik: I recall a few months ago Kevin asked for forward reasoning with apply on hypothesis and this was added

[Henrik Böving]

Added to Mathlib it seems yeah, I don't keep up with the tactics that are developed there as much.

[Shreyas Srinivas]

But I really dislike the way it works because it intuitively renames the wrong hypothesis

[Shreyas Srinivas]

I just use replace or specialize

[Shreyas Srinivas]

specialize is way more intuitive than apply at because I am clearly just instantiating a general hypothesis with specific parameters

[Kevin Buzzard]

Hoards of mathematicians disagree with you. In fact I'm surprised you don't find it intuitive -- mathematicians find apply at very intuitive, this is a standard step for them. In contrast they find apply extremely unintuitive. I know this from lots of NNG feedback.

[Shreyas Srinivas]

Kevin I don't find the normal apply on a goal unintuitive. But if I have a hypothesis ha : a and hab : a -> b then apply hab at ha leaves me with ha : b.

[Shreyas Srinivas]

This messes with my naming scheme

[Shreyas Srinivas]

whereas if it was hab : b I would be less confused because now I have applied the specific argument ha and now I have the specialized hypothesis

[Shreyas Srinivas]

See the states below:

import Mathlib

example (a b : Prop) (ha : a) (hab : a → b) : b := by
  apply hab at ha -- see state here

example (a b : Prop) (ha : a) (hab : a → b) : b := by
  specialize hab ha  -- see state here

[Shreyas Srinivas]

I assure you I am a novice at this type theory business.

[Shreyas Srinivas]

specialize is just applying a function to its arguments. That's easy.

[Kevin Buzzard]

I see your point!

[Shreyas Srinivas]

I would find it more intuitive if the syntax was apply ha at hab and this changed
hab : a -> b to hab : b

[Kevin Buzzard]

Yes, this was the point I got from your messages.

[Shreyas Srinivas]

Is it really worth it to change this behaviour for all those NNG users and confuse them when I can use specialize and apply a full sequence of arguments at a hypothesis instead of using apply?

[Shreyas Srinivas]

I haven't heard anybody else complain about this

[Shreyas Srinivas]

Here's a quick and dirty version of this change with examples

import Mathlib

macro "apply " t:term " at " h:term :tactic => do
  `(tactic| specialize $h $t)

example (a b c : Prop) (ha : a) (hb : b) (hab : a → b → c) : c := by
  specialize hab ha hb -- see state here

example (a b c : Prop) (ha : a) (hb : b) (hab : a → b → c) : c := by
  apply ha at hab
  apply hb at hab

[Shreyas Srinivas]

specialize clearly has a brevity advantage

[Kevin Buzzard]

The issue I guess is that mathematicians don't tend to think of a proof as a function and in NNG4 we try to move away from that idea.

[Shreyas Srinivas]

If you like the behaviour of apply at that I show above, then I can make a PR to change it. Or we could do a poll. I am skeptical of making changes to tutorial relevant tactics when I don't see anybody else complaining about it or expressing opinions

[Kevin Buzzard]

Yeah I removed the suggestion to PR a change about 30 seconds after suggesting it but it seems you saw it anyway :-)

[Shreyas Srinivas]

I prefer my version of apply at even more for longer chains of implications or \foralls because I consistently retain one name for the hypothesis (in this case hab) that I am moving forward on.

[Shreyas Srinivas]

otherwise it is a confusing mess of names, which are both hard to find in the infoview when writing big proofs and look confusing in the proof script once the proof is done.

[Mario Carneiro]

I think it is better to keep them as they are. apply hab at ha renames ha to the result, specialize hab ha renames hab to the result, both might be useful depending on context

[Mario Carneiro]

I think the motivation for the apply at behavior is that hab may not be a variable in the context at all but rather a global theorem, in which case renaming it doesn't make sense

[Mario Carneiro]

also at h generally names a hypothesis in the context that may be rewritten

[Shreyas Srinivas]

That makes sense. I think I would find apply at less painful if the hypothesis didn't move around in the proof state. In a large proof it's like playing hide and seek with my hypotheses. Not moving the hypotheses around would still mess with my naming scheme but at least I won't lose track of the name change so easily. But again that could just be me and people might prefer seeing the latest hypothesis they are working on appear closer to the goal

[Shreyas Srinivas]

Anyway, I am happy with specialize so this is more or less a non-issue for me.

[Shreyas Srinivas]

Slightly related to what you mentioned @Mario Carneiro : Is there a tactic that just introduces a global theorem into the list of local hypothesis. Technically it's job is have lemma_name := lemma_name, but informally it is the equivalent of recall theorem <lemma_name> in mathematical english. It could be accompanied by a recall? <insert the shape of the theorem> which then calls something like loogle and says try this : recall <matching lemma name>

[Shreyas Srinivas]

It could just be a macro for have : <statement> := by exact? plus some code to add hypotheses

[Shreyas Srinivas]

The goal is not to invent a new tactic, just provide ergonomic options that match math english.

[Peter Nelson]

I think this recall would be really nice! Doing have := theorem_name usually fails because of metavariables, and have := @theorem_name and have’ := theorem_name can both give unreadable output. This is worse in lean 4 that is was in lean 3.

It would be good to have a quick way to see something like what #check shows, but as a hypothesis.

[Johan Commelin]

observe is almost that tactic

[Jon Eugster]

It's only today that I realised you can write #check theorem_name inside a tactic proof too, and not only outside a statement as a command.

import Mathlib

example : 5 = 5 := by
  #check Real.pi_div_four_le_arcsin
  rfl

[Shreyas Srinivas]

From a stylistic POV, a proof that that reads.

recall <lemma_name>
apply <assumption 1> at <lemma name>
apply <assumption 2> at <lemma name>
...
...

Is immediately legible to someone who wishes to understand the high level flow of the proof even before they get into the infoview. Note that I am using my version of apply at here so the hypothesis name remains <lemma_name> after each apply at.

PS (CW: idle speculation): Going further with the whole "math English" style, rw feels more English like if it said rewrite <hypothesis> with [eq1, eq2,....]