Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)


Chronological Thread 
  • From: Cao Qinxiang <caoqinxiang AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.)
  • Date: Mon, 16 Apr 2018 01:02:45 -0400
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f44.google.com
  • Ironport-phdr: 9a23:ruqRexPVtxDo/loQUb4l6mtUPXoX/o7sNwtQ0KIMzox0Lf/7rarrMEGX3/hxlliBBdydt6ofzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlGiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgFOT438G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5uiYoQVCOoKIP1Wr4j7p1oBrBuxHw+sBOzywTJPmnD5x6o60/0gEQHA0w0gHsgBsHLbrNjuO6cSVPq6zKjMzTnZc/xW3jL95ZHOfxs8r/+MWrdwftDQyUkpDw7Fj1OQqZbkPzyPzOgNvXKb4ux9Xuysk24qsx99riSry8s2iYTEhpgZxk7Z+Sh52oo4KtK1RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UDuZGhfSgKzI0rxxrRa/CbaoSI7B3uWemLLTd3g3Jlf72/hxKs/kS61uL8Ucy03E5LripDjNbMqmgA2wLP5sWDUPdw/Ues1SyR2wzO6uxIO085mKXDJ54k2LEwl54TsUrZHi/xnUX7lLOZeV8j+uix6uTnZLrnpp6GOI9yhQHzKasumsmlDuQ5NggCRXSU+eO51LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mPtW4NptC7cRIfv1VQelv9XfFx4/Iw29xenPB9B014dYUmWKVPzKeJjOuEOFs7p8a9KHY5UY7W6keqoVosX2hHp8omczOKyg3J8Zcne9R600LECQYH6qidAEQz5T4lgOCdfygVjHagZ9Im6oVvtltD4+AYOiS4zEQ9L12eHT7GKABpRTI1t+JBWMHHPvLdjWXv4NbGeWLJcknGBYE7emTIAl2Felswqok7c=

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




Archive powered by MHonArc 2.6.18.

Top of Page