The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 06/23/2015 10:32 AM, Armaël Guéneau wrote:
> On 06/19/2015 07:49 PM, Jonathan Leivent wrote:
> > Do you have a test case?  I tried a few simple cases, and couldn't 
> > replicate the behavior.
>
> Sure. Actually, I didn't have a simple one at first; now I have
> something.  Minimizing the thing was not as simple as I expected, as I
> couldn't understand clearly when some subgoal was going to be shelved.
>
> The behavior I observed seems to appear on implicit parameters
> specified using Context in a section. So, anyway, here's a test case
> (maybe not minimal).
>
>     Definition filter (A: Type) := (A -> Prop) -> Prop.
>
>     Class Filter {A: Type} (f: filter A) := {
>       filter_foo : False
>     }.
>
>     Section S.
>       Context {A: Type} {f: filter A} `{@Filter A f}.
>
>       Lemma filter_universe:
>         forall P : A -> Prop,
>         (forall a, P a) ->
>         f P.
>       Proof. admit. Admitted.
>     End S.
>
>     Axiom f : filter unit.
>     Axiom P : Prop.
>     Axiom p : P.
>
>     Goal f (fun _ => P).
>       (* Succeeds. *)
>       eapply filter_universe; intros. apply p.
>       (* Fails. *)
>       eapply filter_universe; intros; apply p.
>
>
> (Of course here, the goal is not solved by the first line, but the
> application of tactics succeeds, leaving a shelved goal to be proved;
> using the second line instead of the first fails.)

This is indeed quite strange.  I tried inserting an "instantiate" in 
that failing sequence, but that didn't help.  Also, if the failing 
sequence is modified to be "eapply filter_universe; [|intros; apply p]", 
it fails saying that it expects just 1 tactic (meaning it has just one 
subgoal) - so, the failure is not due to "apply p" being applied to two 
subgoals.  I also printed out the goal using a debugging tactic just 
prior to the final failing "apply p", and it is "a : unit |- P" just as 
expected.

Furthermore, replacing that final "apply p" with "exact p", "eapply p" 
or "refine p" makes the sequence work.  It also works to first pose p, 
then use "assumption" in place of that final "apply p".

Also, adding "Axiom g : Filter f" to the list of axioms makes the final 
"apply p" work - evidently because then the "eapply filter_universe" 
doesn't need to shelve the typeclass constriant "|- Filter f".

I think this is probably a bug about something specific to apply vs. 
typeclass constraints.  It is as if apply alone among the tactics 
believes it must solve typeclass constraints shelved earlier in the 
sequence.

-- Jonathan