## Stream: Coq users

### Topic: ✔ How to get rid of unnecessary existential variables?

#### Evgenii Petrov (Dec 18 2022 at 09:59):

Hi all,

I'm trying to understand how proofs in https://github.com/GeoCoq/GeoCoq work by re-writing them without using custom tactics or notation (or at least using fewer of them).

I got to a point where I've resolved all goals in the "first" lemma - `lemma_localextension`, but I can't close the proof because "some unresolved existential variables remain".

At some point in the proof I have a goal of the following form:

``````exists X Y U V W, CI J U V W /\ (eq P U \/ (BetS U Y X /\ Cong U X V W /\ Cong U P U Y));
``````

I can only provide witnesses for U V W, but that is also sufficient, so I use the following, which resolves the goal:

``````  eexists.
eexists.
exists B.
exists B.
exists Q.
split.
exact h_postulate_Euclid3.
left.
reflexivity.
``````

This leaves two existential variables introduced by eexists, how do I get rid of them?

Just in case, here is the full proof with all dependencies in a single file: https://gist.github.com/blin/d2bca64d034ac70905b933952cc3b23c . Comments on doing things differently/better would be appreciated.

#### Gaëtan Gilbert (Dec 18 2022 at 10:10):

that is also sufficient

the system is telling you that it's not
you can do `Unshelve` to get the remaining goals, then solve them
or you can provide the value to `exists` instead of using `eexists`

#### Evgenii Petrov (Dec 18 2022 at 10:23):

Thanks Gaëtan, doing Unshelve showed that supplying any two points is sufficient by the end of the proof so the following works

``````Unshelve.

auto.
auto.
``````

But also supplying unrelated points instead of eexists works:

``````  exists B.
exists B.
exists B.
exists B.
exists Q.
``````

#### Notification Bot (Dec 18 2022 at 10:26):

Evgenii Petrov has marked this topic as resolved.

Last updated: Jun 18 2024 at 08:01 UTC