search

coq / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
https://coq.inria.fr/
GNU Lesser General Public License v2.1
4.86k stars 650 forks source link

Show Existentials changes the behaviour of shelved goals #18689

Open louiseddp opened 9 months ago

louiseddp commented 9 months ago

I am using coq v.8.19.0, and OCaml 4.10.0

I was experimenting with the Unshelve command and realized that, in the following example, the given up goal is not the expected one:

Goal (True /\ (True -> True)).
split. 
2: shelve. 
{ exact I.  Unshelve. } 
Show Existentials.
(* Existential 1 = ?Goal : [ |- True] (given up)
Existential 2 = ?Goal0 : [ |- True -> True] (shelved) *)
Unshelve. intros. exact I. Fail Qed.

The expected behaviour is probably the following one, but for some reason it is triggered only when we use the vernacular command Show Existentials:

Goal (True /\ (True -> True)).
split. 
2: shelve. 
{  Show Existentials. exact I.  Unshelve. } (* This proof is focused, but cannot be unfocused this way *)
SkySkimmer commented 9 months ago

I get This proof is focused, but cannot be unfocused this way regardless of Show Existentials. Are you using some IDE?

louiseddp commented 9 months ago

I was using CoqIDE

SkySkimmer commented 9 months ago

Looks like coqide implicitly gives up (admits) the remaining goals on }. Not sure why it doesn't when using Show Existentials, probably demons coming from the stm.

ckeller commented 9 months ago

Looks like coqide implicitly gives up (admits) the remaining goals on }. Not sure why it doesn't when using Show Existentials, probably demons coming from the stm.

If I may, there is one more strange thing happening here: in the first example, it does not admit the correct goal.

SkySkimmer commented 9 months ago

Oh it's not admitting the remaining goal, instead it seems like it's resetting to before the { and admitting the goal that was focused.