Stream: Coq users

Topic: Get conclusion of implication with trivial hypothesis


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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).

view this post on Zulip 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