What is the remaining goals on the shelf?

Question

When I prove a theorem in Coq, I made a hypothesis that is 'False', and by using 'contradiction' tactics, I finish my proof.

However, the coq program show some words for me.

All the remaining goals are on the shelf:

positive

What is this, and how can I deal with it?

---

Edit : I wrote my code here. The last lemma has a problem.

Edit2 : With Jason Rute's advice, my proble is solved.

From mathcomp Require Import all_ssreflect.

Require Import QArith.

Axiom excluded_middle :
forall P : Prop, P \/ not P.

Lemma all_prop (S : Set) (P : S -> Prop) :
(forall x : S, (P x)) <-> not (exists x : S, not (P x)).
Proof.
split.
{ unfold not. intros. destruct H0 as [x Hx].
  apply Hx. apply H. }
{ unfold not. intros.
  specialize (excluded_middle (P x)) as Hx.
  destruct Hx. { exact H0. }
  { destruct H. exists x. exact H0. } }
Qed.

Lemma not_not_equiv (P : Prop) :
P <-> (not (not P)).
Proof.
split.
{ unfold not. intros. apply H0 in H. exact H. }
{ unfold not. intros.
  specialize (excluded_middle P) as HP. destruct HP.
  { exact H0. } { apply H in H0. contradiction. } }
Qed.

Lemma not_all_prop (S : Set) (P : S -> Prop) :
not (forall x : S, (P x)) <-> exists x : S, not (P x).
Proof.
rewrite all_prop. symmetry. apply not_not_equiv.
Qed.

Lemma not_exists_prop (S : Set) (P : S -> Prop) :
not (exists x : S, (P x)) <-> forall x : S, not (P x).
Proof.
symmetry. rewrite all_prop.
setoid_rewrite <- not_not_equiv. reflexivity.
Qed.



(* 1 # n is equal to 1/n *)
Lemma Archimedean :
forall q : Q, 0 < q ->
exists n : positive, 1 # n < q.
Proof.
intros. destruct q. exists (Qden + 1)%positive. unfold Qlt. simpl.
specialize (Zgt_succ (Z.pos Qden)) as H0. simpl in H0.
apply Z.gt_lt in H0. setoid_rewrite <- Zmult_1_l at 1.
apply Zmult_lt_compat2.
{ assert (H1 : (0 < Qnum)%Z).
  { unfold Qlt in H. simpl in H. rewrite Zmult_1_r in H. exact H. }
  specialize (Zlt_le_succ _ _ H1) as H2. simpl in H2.
  split. by []. exact H2. }
{ split. by []. exact H0. }
Qed.

Lemma Pos_max_four (a b c d : positive) :
exists x : positive, (a <= x /\ b <= x /\ c <= x /\ d <= x)%positive.
Proof.
exists (Pos.max (Pos.max a b) (Pos.max c d)). repeat split.
{ apply Pos.le_trans with (Pos.max a b)%positive.
  apply Pos.le_max_l. apply Pos.le_max_l. }
{ apply Pos.le_trans with (Pos.max a b)%positive.
  apply Pos.le_max_r. apply Pos.le_max_l. }
{ apply Pos.le_trans with (Pos.max c d)%positive.
  apply Pos.le_max_l. apply Pos.le_max_r. }
{ apply Pos.le_trans with (Pos.max c d)%positive.
  apply Pos.le_max_r. apply Pos.le_max_r. }
Qed.

Lemma Pos_max_le_l (a b c : positive) :
(Pos.max a b <= c -> a <= c)%positive.
Proof.
intros.
apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_l. exact H.
Qed.

Lemma Pos_max_le_r (a b c : positive) :
(Pos.max a b <= c -> b <= c)%positive.
Proof.
intros.
apply Pos.le_trans with (Pos.max a b)%positive.
apply Pos.le_max_r. exact H.
Qed.





Definition compare (f g : positive -> Q) :=
exists s : positive, (forall n m : positive,
(s <= n)%positive -> (s <= m)%positive -> f n <= g m).

Definition get_closer (f g : positive -> Q) :=
forall n : positive, (exists m : positive,
(forall p : positive, (m <= p)%positive -> g p - f p < 1 # n) ).

Record P := mkP {
  l : positive -> Q;
  r : positive -> Q;
  Cond1 : compare l r;
  Cond2 : get_closer l r;
}.

Definition Plt (X Y : P) :=
forall s : positive, (exists n m : positive,
(s <= n)%positive /\ (s <= m)%positive /\
(r X) n < (l Y) m).






Lemma Plt_equiv (X Y : P) :
compare (l Y) (r X) <-> not (Plt X Y).
Proof.
unfold compare, Plt. split.
{ unfold not. intros. destruct H as [s Hs].
  destruct (H0 s) as [n [m [H1 [H2 H3]]]].
  specialize (Hs m n H2 H1) as H4.
  specialize (Qlt_le_trans _ _ _ H3 H4) as H5.
  apply Qlt_irrefl in H5. exact H5. }
{ rewrite not_all_prop. intros [x Hx]. rewrite not_exists_prop in Hx.
  exists x. intros. specialize (Hx m) as H1.
  rewrite not_exists_prop in H1. specialize (H1 n) as H2.
  destruct (Qlt_le_dec (r X m) (l Y n)) as [Hdec|Hdec]; first last.
  { exact Hdec. } { unfold not in H2.
  assert (H3 : (x <= m)%positive /\ (x <= n)%positive /\ r X m < l Y n).
  { repeat split. exact H0. exact H. exact Hdec. } 
  apply H2 in H3. contradiction. } }
Qed.

Lemma Peq_trans_half (a b c : P) :
not (Plt a b) -> not (Plt b c) -> not (Plt a c).
Proof.
rewrite -Plt_equiv. rewrite -Plt_equiv. 
unfold compare, not, Plt. intros.
destruct H as [s Hs], H0 as [t Ht].
destruct (H1 (Pos.max s t)) as [n [m [H2 [H3 H4]]]].
rewrite Qlt_minus_iff in H4.
destruct (Archimedean _ H4) as [u Hu].
destruct ((Cond2 b) u) as [v Hv].
specialize (Pos_max_four s t v) as [x [H5 [H6 [H7 _]]]].
specialize (Hv _ H7) as H8.
specialize (Hs x n H5 (Pos_max_le_l _ _ _ H2)) as H9.
specialize (Ht m x (Pos_max_le_r _ _ _ H3) H6) as H10.
apply Qopp_le_compat in H9.
specialize (Qlt_trans _ _ _ H8 Hu) as H11.
specialize (Qplus_le_compat _ _ _ _ H10 H9) as H12.
specialize (Qlt_le_trans _ _ _ H11 H12) as H13.
apply Qlt_irrefl in H13. exact H13. Unshelve.
Admitted.

Answer 1

The root of your issue comes from the line

specialize (Pos_max_four s t v) as [x [H5 [H6 [H7 _]]]].

What happens here is that Pos_max_four requires four arguments, to create a value greater than all four arguments. But here you supply it only with three such values, so that Pos_max_four s t v is of type

forall (d : positive),
  exists x : positive, (a <= x /\ b <= x /\ c <= x /\ d <= x)%positive

Since you immediately destruct it, Coq understands you want to destruct the existential exists x : positive ..., but you still need to provide some d : positive in order to be able to do that. So a new existential variable gets created for d and shelved, with the hope that the way you use the hypothesis of type d <= x will tell what its value should be. But since you immediately discard that hypothesis and never use it, this does not happen, and so you reach the end of the script with the value of d still unknown, which is what Coq complains about.

As far as I know, unshelving like you do at the end of the script is considered a bad style, as it is quite fragile, because it loses the link between the existential variable and the tactic that introduces it. If you end up changing that tactic, the unshelving part will break, in a quite impredictable manner. More robust solutions are either to avoid introducing an existential variable, for instance by proving a lemma Pos_max_three, or directly use something like

pose x := (Pos.max (Pos.max s t) u)%positive.
assert (s <= x).
{ 
 (* proof goes here, using lemmas on Pos.max *)
}
assert (t <= x).
{ (* same *) }
assert (u <= x).
{ (* one last time *) }

An alternative solution, rather than unshelving at the very end of the script, is to clearly "mark" the tactic which introduces the shelved variable, with something like

unshelve specialize (Pos_max_four s t v) as [x [H5 [H6 [H7 _]]]].

Answer 2

I'm not a Coq expert, but I think I see what is going on:

Coq gives you the power to remove goals temporarily and place them on a "shelf". This is called shelving the goal. Sometimes the shelved goal will resolve itself---since it is linked to a current goal, and when you apply a tactic to the current goal, it will unify with the shelved goal and solve it. Other times, you have to later bring back the shelved goal with Unshelved. and solve it manually.

In your case, you have a shelved goal whose goal is positive. This is weird looking since positive is a Set, not a Prop, but it is also easy to solve. Just unshelve the goal with Unshelve. and complete the "proof" of positive by giving it any element of positive, e.g. exact xH..

---

Now, why can one end up in this situation? After some Googling, I found this issue. I don't know if your situation is related, but nonetheless, their MWE shows what could happen:

Hint Extern 1000 => exfalso : core.

Lemma foo (H : False) : exists x : nat, None = Some x.
eauto.
(*
All the remaining goals are on the shelf:
nat
*)

Clearly, the hypothesis H could solve any goal, but the automation, instead of directly applying H to the outer goal does something like this proof:

Lemma foo2 (H : False) : exists x : nat, None = Some x.
eexists.
exfalso.
exact H.

To prove an exists x : nat, ... we normally have to directly supply x. The tactic eexists delays that decision by making two linked goals: nat and H : False |- None = Some ?x. The "proof" of the first goal is that x, and the ?x in the second goal is linked to be whatever the "proof" of the first goal comes out to. Normally, one doesn't touch this first goal nat. Instead, the proof of the second goal will tell you what ?x is and then this will unify with the nat goal, filling the value in and solving the goal. Because of this, eexists shelves the first goal nat to get it out of the way.

The rest of this proof exfalso. exact H. just finishes the proof of H : False |- None = Some ?x, but since we used exfalso, we never actually supplied a value of ?x in the proof, so we have to manually fill in some value (any value) of nat as follows:

Lemma foo2 (H : False) : exists x : nat, None = Some x.
eexists.
exfalso.
exact H.
Unshelve.
exact 0.
Qed.

or in the first case:

Lemma foo (H : False) : exists x : nat, None = Some x.
eauto.
Unshelve.
exact 0.
Qed.