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=
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).
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| |- _ _ => idtacend.
Ltac TA2 :=match goal with| |- _ _ => idtac| |- _ => idtacend.
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]) inlet tac2 H := let ph := fresh "H" in let ph' := fresh "H" in(destruct H as [H ph ph'])inlet tacT H := let ph := fresh "X" in (destruct H as [H ph]) inlet tacT2 H := let ph := fresh "X" in let ph' := fresh "X" in(destruct H as [H ph ph'])inmatch 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 Hend.
foo_tac destruct_one_ex. (* WHY fail? *)
- [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Cao Qinxiang, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason -Zhong Sheng- Hu, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Cao Qinxiang, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason Gross, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason Gross, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason -Zhong Sheng- Hu, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason Gross, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason Gross, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Cao Qinxiang, 04/16/2018
- Re: [Coq-Club] Why this Ltac program fail? (Ltac program use another Ltac program as an argument.), Jason -Zhong Sheng- Hu, 04/16/2018
Archive powered by MHonArc 2.6.18.