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: Oct 13 2024 at 01:02 UTC