The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 04/03/2016 05:17 PM, scott constable wrote:
> In the following, why does attempt1 succeed, whereas attempt2 fails? I 
> followed
> through with the Ltac debugger, and found that extractor' is never executed
> after intros, but I cannot come up with an explanation as to why.

Try rewriting exactor' as:

Ltac exactor' := idtac;
   match goal with
   | [ H : ?P |- ?P ] => exact H
   | _ => idtac
   end.

What's happening with the original exactor' is that because it's body a 
raw match tactical, it can be evaluated in the arg position of my_solve 
prior to calling my_solve - and it evaluates to the tactic idtac there 
(because the intros haven't happened yet).  In exactor, the try tactical 
prevents this early evaluation.  In the above rewrite of exactor', the 
sequence tactical ";" prevents the early evaluation.

-- Jonathan

> Ltac my_solve m :=
>     intros; m.
>
> Ltac exactor := try
>     match goal with
>     | [ H : ?P |- ?P ] => exact H
>     end.
>
> Ltac exactor' :=
>     match goal with
>     | [ H : ?P |- ?P ] => exact H
>     | _ => idtac
>     end.
>
> Theorem attempt1 : forall (A : Type) (x y : A),
>       x = y -> x = y.
> Proof. my_solve exactor. Qed.
>
> Theorem attempt2 : forall (A : Type) (x y : A),
>       x = y -> x = y.
> Proof. my_solve exactor'. Qed.
>
> Thanks in advance,
>
> ~Scott Constable