Dennis H (Mar 16 2023 at 14:13): 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.
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. }
orpose 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: Sep 23 2023 at 07:01 UTC