rocq prover - How to destruct evars in Coq? - Stack Overflow

In the following proof script:

Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.

we end up with the goal:

  n, n0 : nat
  ============================
  (n, n0) = (1, 1)

Is there a way to destruct ?p such that we end up with the same goal we would get if we did eexists (?[p1], ?[p2]). instead of eexists ?[p].? I.e.:

(?p1, ?p2) = (1, 1)

In the following proof script:

Theorem foo : exists p, p = (1, 1).
Proof. eexists ?[p]. destruct ?p.

we end up with the goal:

  n, n0 : nat
  ============================
  (n, n0) = (1, 1)

Is there a way to destruct ?p such that we end up with the same goal we would get if we did eexists (?[p1], ?[p2]). instead of eexists ?[p].? I.e.:

(?p1, ?p2) = (1, 1)

• rocq-prover

Share Improve this question Follow asked Dec 31, 2024 at 10:58 andreasandreas 7,42533 gold badges2525 silver badges3737 bronze badges

Add a comment  | 

1 Answer 1

Sorted by: Reset to default 1

destruct <term> replaces all occurrences of <term> with a constructor applied to its arguments (which are generated as variables in the context), with one goal per constructor. With an evar, you can choose which constructor should be applied by doing the instantiation yourself, e.g. with instantiate (p := (?[p1], ?[p2])).