The Coq mailing list

[scott constable <sdconsta AT syr.edu>]

Jonathan,

Thanks for the quick response. I have two follow-up questions:

1. Based on your description, it seems as though arguments to Ltac sometimes are call-by-value (i.e. the first exactor') and at other times are call-by-name (i.e. the second exactor'). Is this statement correct?
   
2. If the answer to (1) was "Yes," then is there a general rule to determine whether an argument will be evaluated by call-by-value or call-by-name?

Thanks again,

~Scott

On Sun, Apr 3, 2016 at 5:29 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

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