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.
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
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.
Evgenii Petrov has marked this topic as resolved.
Last updated: Oct 04 2023 at 20:01 UTC