As a basic example, if I have a lemma which looks like

```
Lemma test2 (x : Type) (f : 1 = 1 -> x) : x.
```

how can I, in my proof, obtain an explicit hypothesis of type `x`

from `f`

? Obviously, this example can be solved easily with `apply f`

, but it's meant as an idea for a situation I'm in with a larger proof, where I can't just `apply`

it, and I want to get the conclusion of an implication like this.

Is there a tactic for this?

Well, `f`

is a function which to any proof that `1 = 1`

associates `x`

; so if you have a proof `foo: 1 = 1`

, then `f foo`

will be what you want:

```
Lemma test2 (x : Type) (foo: 1 = 1) (f : 1 = 1 -> x) : x.
Proof.
exact (f foo).
Qed.
```

`assert (H:x). { apply f;reflexivity. }`

or `pose proof (f eq_refl)`

when the argument is small enough

Julien Puydt This requires me to pass an extra value to the lemma, which I don't want

Gaëtan Gilbert zei:

`assert (H:x). { apply f;reflexivity. }`

or`pose proof (f eq_refl)`

when the argument is small enough

The first one is a good solution, but the type of `x`

is sadly much more complex in the actual scenario I want to use this, so it's a bit cumbersome to type out. The second one works perfectly, thanks!

In general you could also do an `unshelve epose proof (f _).`

if the argument of `f`

is not necessarily an identity proof (and add as many underscore as arguments you want to pop).

You may find the LibHyps library useful (`opam install coq-libhyps`

). It gives you `especialize H at 1`

and its variants.

```
Require Import LibHyps.LibHyps.
Lemma test2 (x : Type) (f : 1 = 1 -> x) : x.
Proof.
especialize f at 1 as h.
2 goals
x : Type
f : 1 = 1 -> x
============================
1 = 1
goal 2 is:
x : Type
h : x
============================
x
```

Last updated: Jun 24 2024 at 12:02 UTC