The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

I see, then that sounds like that it's more or less an expected behavior from Ltac's perspective as a programming language using call-by-value, for the sake of possessing dual status, and in the situation where users expect a thunk to be passed in, they in fact want call-by-name for that portion. Then I'd imagine that can be addressed by adding some sort of syntax to distinguish both cases?

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jason Gross <jasongross9 AT gmail.com>
Sent: April 16, 2018 1:46:48 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)

 

Er, where I said "As for the failure", I meant "As for the success"

On Mon, Apr 16, 2018, 1:45 PM Jason Gross <jasongross9 AT gmail.com> wrote:

> I am not sure why it's like that. Maybe someone else can give you more insight.

Historical fact: in Coq <= 8.4, it gave an error message.  "Immediate match producing tactics not allowed in this location" or something.  This error message was removed in Coq 8.5, when Ltac switched to the new proof engine.

My hypothesis is that the original author of Ltac wanted a language that could both run tactics and produce terms, implemented it in the first way they thought of, noticed that this sort of thing was weird and unintuitive, and added an error message forbidding it.  This quirk of implementation, that `match` runs its branches doing tactic _expression_ evaluation, was nearly unobservable (you could only notice it by nesting match in lazymatch and noticing that you could get an unexpected failure level).

Many years later, when the devs rewrote the tactic engine to be saner, they had no collective recollection of why Ltac was the way it was (and, after all, this is all merely my guessing based on the feel of Ltac as a language), and saw no reason to keep the error message, so they permitted this behavior.  They could not change the fact that match runs early, though, because that would break almost every tactic that constructs a term.

As for the failure of too_tac destruct_one_ex before destruct_one_ex is defined, my guess is that destruct_one_ex gets interpreted as an identifier ( like what you might pass to intro), and that try catches the error message that comes from trying to execute an undefined identifier as a tactic.

On Mon, Apr 16, 2018, 1:03 AM Cao Qinxiang <caoqinxiang AT gmail.com> wrote:

Thank you very much! This is very helpful.

Qinxiang

On Mon, Apr 16, 2018 at 12:50 AM, Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

It's due to a quirk in how [match] interactive with closure that does not take argument(I call that a thunk). Whenever a Ltac [match] appear in the first position of any argument, instead of being wrapped into a thunk, [match] will be run, that's why it escaped from the [try]. The workaround is to prepend the sequence with some other tactic that is not [match], in which case [idtac] is frequently used. In short, following code would work:

  foo_tac ltac:(idtac; TA1).
  foo_tac ltac:(idtac; TA2).

I am not sure why it's like that. Maybe someone else can give you more insight. In general, you will want to distinguish Ltac term and Gallina term by spelling out ltac:() in arguments. FYI, when in argument position, Ltac prioritizes Gallina terms, so if TA2 was one, then it will give a different output. Following program illustrates that:

Ltac bar_tac tac :=
  idtac tac.

Goal True.
  bar_tac TA2.
  (* <tactic> *)
 
  Inductive TA2 : Set :=.
  bar_tac TA2.
  (* TA2 *)
Abort.
 

Also,

foo_tac destruct_one_ex.  (* This succeed. *)

This one did not work for me, and it also failed for the same reason. Following code works for me:

foo_tac ltac:(idtac; destruct_one_ex).

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Cao Qinxiang <caoqinxiang AT gmail.com>
Sent: April 16, 2018 12:27:28 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)

 

Hello,

Do you have any idea why the following tactics fail?

Best,

Qinxiang

Ltac foo_tac tac :=

try tac.

Ltac TA1 :=

match goal with

| |- _ _  => idtac

end.

Ltac TA2 :=

match goal with

| |- _ _  => idtac

| |- _ => idtac

end.

Goal True.

foo_tac TA2. (* This succeed. *)

foo_tac TA1. (* WHY fail? *)

foo_tac destruct_one_ex.  (* This succeed. *)

Ltac destruct_one_ex := (* copied from https://coq.inria.fr/library/Coq.Program.Tactics.html *)

  let tac H := let ph := fresh "H" in (destruct H as [H ph]) in

  let tac2 H := let ph := fresh "H" in let ph' := fresh "H" in 

    (destruct H as [H ph ph']) 

  in

  let tacT H := let ph := fresh "X" in (destruct H as [H ph]) in

  let tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in 

    (destruct H as [H ph ph']) 

  in

    match goal with

      | [H : (ex _) |- _] => tac H

      | [H : (sig ?P) |- _ ] => tac H

      | [H : (sigT ?P) |- _ ] => tacT H

      | [H : (ex2 _ _) |- _] => tac2 H

      | [H : (sig2 ?P _) |- _ ] => tac2 H

      | [H : (sigT2 ?P _) |- _ ] => tacT2 H

    end.

foo_tac destruct_one_ex. (* WHY fail? *)