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: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
- To: "coq-club AT inria.fr" <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 04:50:47 +0000
- Accept-language: en-CA, en-US
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
- Ironport-phdr: 9a23:3J46GBCdszb/JY0PnsLAUyQJP3N1i/DPJgcQr6AfoPdwSPT8p8bcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJNyA3/nzLisJ+j6xbrhCuqABwzIPPeo6ZKOZyc7nBcd8GW2ZMWNtaWSxbAoO7aosCF+4PMvxDr4n6oVsFsAKyCgqsBOPozD9IiWL907A60+s/FwHG0xUsFM8MvnTJsd74M6kSXv21zKjJ1jXPce9a1Srh5IXTchAhpu2MXbdqfsrQzUkjDR/KjlKVqYH8OT6ey+oDs2+e7+V6VOKvjXYqqwB3oji1x8cjkJPFhowPyl3C6C53w541KMW3RUJne9KpFIVcuzuGO4dsTM4vTHlkuCgkxbAFpZK2eS0HyJo7yxPdaPGKdoyF7xHjWeuQJDp3mXBoeLy8ihu370Ss1/PwWdKy3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DiXyw3d7f1ILV0tmafGM5AszKc8lp0IvkvdBCP2n1j2jLONeUUj5+io7fnobq/+pp+GMI90lh/xPbgymsy+BuQ4NBICX2+G+eSg0L3j+kr5QLZQgvIqlanZtYjWJcUdpqGnHw9Yyoku5wqlAzqiztgUh2ULIEhLdR+Il4TpPkvBIPH8DfexmVSslzJryujIPrL8ApXML2PDnKn9cbpg90JR0wozzddD55JREL4BIfbzVlXtu9zfCx81Kxa0zPr/CNVhyoMeXnqCDbOeMKPLqFOH+uYvI/SXa4IOozb8K/0l5+b0gnMjmF8de7Op3ZoNZ3yiEPRmORbRXX25yNwGCCIBuhc0ZO3sklyLFzBJLT7mVKUlozo/FYiODIHZR4nrjqbXjwmhGZgDRGldDVbEVEXocIOLE8wMZSSdZ4dBj3RQW7ShWZR7jUj2nA/9179uL+6S8Sod48GwnONp7vHewElhvQd/CN6QhjnUHjNE21gQTjpz55hR5El0y1ONy6992qcKFdtP4vpIVkExMpuOlrUmWeC3YRrIe5KycHjjWs+vWGpjTtUtxtYPZwB2HNDw1kmejRrvOKcckvmwPLJx8q/Y2CSudeBU7i6fkYMH1BwhSMYJMnC6jKli8QSVH5TOj0iSi6etc+IbwTLJ82CAi2GJuRMBXQ==
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; 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:
idtac tac.
Goal True.
bar_tac TA2.
(* <tactic> *)
Inductive TA2 : Set :=.
bar_tac TA2.
(* TA2 *)
Abort.
Also,
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).
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.)
- [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.