The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

Hi Bas,

> I am trying to use Declare Implicit Tactic.
> 
> It does not seem to work in my example, the corn division for real numbers.
> So, I tried the example from the reference manual.
> 
> Parameter quo : nat -> forall n:nat, n<>O -> nat.
> Notation "x // y" := (quo x y _) (at level 40).
> (* Declare Implicit Tactic assumption.*)
> Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
> intros. exists (n//m).
> 
> As you can see the "Declare Implicit Tactic assumption" does not even seem 
> to 
> be needed. Can someone provide me with a real example?

The use of "Declare Implicit Tactic" in the "exists" tactic is indeed
broken in Coq 8.2: a collision happened with the extended support for
resolution of implicit arguments using informations of the goal (as in
"exists (@nil _)" for proving "exists l:list nat, l=l").

In addition, there is a bug in this extended support for resolution of
implicit arguments: since you said "exists" and not "eexists",
"exists" should have failed due to the unresolved implicit argument.

In your case, the implicit argument has in fact not been proved but as
a further call to "Show Existentials" shows:

  Existential 1 = ?8 : [n : nat  m : nat  H : m <> 0 |- m <> 0] 

Then, so as to take benefit of "Declare Implicit Tactic" in 8.2, I can
(only) recommend a workaround:

Ltac myexists c := exists c.
Parameter quo : nat -> forall n:nat, n<>O -> nat.
Notation "x // y" := (quo x y _) (at level 40).
Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }.
intros. 
myexists (n//m). (* fails *)
Declare Implicit Tactic assumption.
myexists (n//m). (* succeeds *)

Alternatively, "apply (existT _ (n//m))" works also (but unfortunately
"apply with (n//m)" has the same problem as "exists").

Hugo