Forward Reasoning

Stream: new members

[Josh Cohen]

Is there a way to easily apply implications in hypotheses? e.g. I have hypotheses H: P -> Q and H1: P and I want a hypothesis Q. In Rocq, this would be apply H in H1 but something similar does not appear to exist in Lean. I know I can do have H2 := H H1 but this gets very verbose with long definition names and many arguments. Is there some tactic that does this that I am missing? Thanks

[Kenny Lau]

• specialize H H1
• apply H at H1
• replace H := H H1

[Josh Cohen]

The second option (apply...at...) gives me an error, Lean seems to ignore the at entirely and attempt to apply H to the goal

[Riccardo Brasca]

It's a mathlib tactic, you probably need to import it.

[Kenny Lau]

import Mathlib.Tactic.ApplyAt

example (P Q : Prop) (H : P → Q) (H1 : P) : Q := by
  apply H at H1
  exact H1

@Josh Cohen you need to import Mathlib.Tactic.ApplyAt

[Josh Cohen]

Is it possible to put this tactic in vanilla Lean? It seems useful enough to be used in non-mathlib contexts

[Kenny Lau]

(also for future purposes, it would be more helpful to include #mwe like I just did)

[Josh Cohen]

For context, I am working on a project where I cannot add a mathlib dependency, so it is somewhat frustrating when useful Lean capabilities are found only in mathlib.

[Kenny Lau]

but you can still use specialize

[Kenny Lau]

and also you can just copy the code of apply_at to your project

[Riccardo Brasca]

You can open an issue, but honestly it seems unlikely, there is already specialize.

[Kenny Lau]

@Josh Cohen is there any reason why you prefer apply_at over specialize?

[Riccardo Brasca]

In fact most of the time one can write H H1 directly, without even using specialize.

[Kenny Lau]

presumably they want it to be reusable

but this gets very verbose with long definition names and many arguments

[Josh Cohen]

Kenny Lau said:

Josh Cohen is there any reason why you prefer apply_at over specialize?

Experimenting a bit more, I think specialize should suffice, thank you both for your help. However, I am now wondering what apply...at does that is different than specialize (as in, why was it created separately?)

[Kenny Lau]

@Josh Cohen they change different things

[Kenny Lau]

specialize H H1 modifies H, while apply H at H1 modifies H1

[Kenny Lau]

@Josh Cohen in general you will find it useful to read the docstrings of tactics, which you can access by hovering your mouse over said tactics in a working code

[Josh Cohen]

In Rocq, if I had a quantified hypothesis H: \forall (x: A) (y: B), P x y -> Q x y and hypothesis H1: P a b, apply H in H1 would produce H1: Q a b, whereas I would need to use specialize (H _ _ H1) (or else instantiate x and y explicitly). In other words, apply will infer parameters. This was my original motivation for preferring apply. But maybe this is not similar in Lean.

[Josh Cohen]

Kenny Lau said:

Josh Cohen in general you will find it useful to read the docstrings of tactics, which you can access by hovering your mouse over said tactics in a working code

Yes, I have found that useful. I think my primary problem has been discovering tactics; the Lean Tactic Reference is useful but it is sometimes difficult to know what to look for.

[Kenny Lau]

that's why #new members exists!

[Kenny Lau]

Josh Cohen said:

In Rocq, if I had a quantified hypothesis H: \forall (x: A) (y: B), P x y -> Q x y and hypothesis H1: P a b, apply H in H1 would produce H1: Q a b, whereas I would need to use specialize (H _ _ H1) (or else instantiate x and y explicitly). In other words, apply will infer parameters. This was my original motivation for preferring apply. But maybe this is not similar in Lean.

according to the docstrings, apply_at does exactly that

[Josh Cohen]

The other advantage of apply is that it works even if I do not have the implication in the context. Given a separate theorem foo: P -> Q and hypothesis H: P, I would like to be able to say apply foo in H. Unless I am mistaken, with specialize, I would need to first add foo to the context (which is annoying if foo has a long name or lots of implicit arguments). Is this correct?

[Aaron Liu]

You could also just have := foo H