The Coq mailing list

[Cao Qinxiang <caoqinxiang AT gmail.com>]

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? *)