Stream: Coq users

Topic: Get conclusion of implication with trivial hypothesis

Dennis H (Mar 16 2023 at 14:13):

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?

Julien Puydt (Mar 16 2023 at 14:24):

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

Gaëtan Gilbert (Mar 16 2023 at 14:26):

`assert (H:x). { apply f;reflexivity. }`
or `pose proof (f eq_refl)` when the argument is small enough

Dennis H (Mar 16 2023 at 14:38):

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

Dennis H (Mar 16 2023 at 14:40):

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!

Kenji Maillard (Mar 16 2023 at 15:18):

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

Pierre Courtieu (Mar 16 2023 at 22:04):

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