Stream: Coq users

Topic: ✔ Tactic returning a proof witness and existential variables

Pierre Vial (Aug 24 2021 at 09:45):

Hi,
[EDIT (solved): apparently, it was just a matter of putting a clearat a wrong place]
I'm writing a Ltactactic tacsuch that:

• The first step of tac foo bar bar' is to produce a statement H
• The second step is asserting and proving H (namely with let t := fresh "t" in assert (t:H))
• the third (would-be) step is outputting the proof-witness tof H. I tried to do this with exact t

I'm pretty sure that step 1 and 2 are good.
When I try to do this on an example of the form:
assert (try1 := ltac:(tac foo bar bar' ) ).
I obtain the following error:
Cannot infer an existential variable of type "?T" in environment: H := forall (x : Set) (x0 x1 : x) (x2 x3 : list x), x0 :: x2 = x1 :: x3 -> x0 = x1 /\ x2 = x3 /\ True : Prop t : H
If I specify that the type of try1 is H, I get the error: The reference H was not found in the current environment.
Is there a direct workaround to solve this ?

Notification Bot (Aug 24 2021 at 15:01):

Christian Doczkal has marked this topic as resolved.

Last updated: Sep 28 2023 at 10:01 UTC