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: 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; 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