Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Maintaining a list of tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Maintaining a list of tactics


Chronological Thread 
  • From: Qinshi Wang <qinshiw AT cs.princeton.edu>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Maintaining a list of tactics
  • Date: Tue, 28 Apr 2020 00:51:45 +0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=qinshiw AT cs.princeton.edu; spf=Pass smtp.mailfrom=qinshiw AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT yellowcard.cs.princeton.edu
  • Ironport-phdr: 9a23:Lhrdrhx/1bmsjWLXCy+O+j09IxM/srCxBDY+r6Qd1O8eIJqq85mqBkHD//Il1AaPAdyGra8VwLOO6ejJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglVhDexe7N/IRG5oQnMqsUan5ZpJ7osxBfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQrNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4qF2QxLulSwJNSM28HvPh8N/jKxVrhGvqQFhzYHIe4yaLuZyc7nHcN8GWWZMXMBcXDFBDIOmaIsPCvIMM/1Zr4n7vFsOrRq+DhSsC+z1zD9IiWL90Koj0+QgFwHGxwwgH9MAsXnPsNr1L70eUfivzKnJyzXMc+1Z2Sv66IjOaBwuv+yDXa9pfMfX1EIhFBvFg02NpYD7PD6ZzPkBv3WF4+Z6SO6ihW8qpxtwrzWu3ssglJXFi4YPxl3H9Sh12ps5KcO7RUJhbtOpH51dvDyAOYRsWMMtWWRotT46yrIYvZ67ezAHyZQ5yB7bb/yHdIaJ7Q75W+aLPDh0nm5qeKmlixaq60igy+v8WdWq31ZWqSpFlMPAuW4Q2BzO8sSHS/198Vm92TuXygzf9OJJLVopmabGNZIt2KM8m5QSvEjZHyL7mV36jKqMeUUl/uio5f7nYrLjppKELo90iwf+Mr8umsy+D+U1KRQBX3OB9eSkzr3j/Ev5T6lUgf0qlanZtorWKtoGqa6kGwNVyJos6w6jDze619QVhWUILFVceB6ek4fpP0zOL+vjAPekg1WslS9ryOrcMr3gBJXNNHnDn637cbZz8U4PgDY0mNtY/tdfDqwLCPP1QE748tLCXTEjNAnh+ufhE9V8nrwXX23HVraYNrjSsECg7flpO/ONYoQYpDH7bfUp+qi93jcChVYBcPzxjtMsY3eiE6E+ehjLUT/Xmt4EVFwykE8+Qejt0gzQQDNXY3GtVKsm6ncwE8S+F4bFTY2xh7rH0SumTMQPNzJ2T2uUGHKtTL2qHvIFaSacOMhky2xWXqPnU5Ug0xqjqAj8jbdrM7iNo3FKhdfYzNFwotbru1Qq7zUtX5aWyCeVVWBylW4UQDlw0axi8xRw

Dear Coq community,

This is what I need in my project. I think it could be a problem for many people, not just me.

I have a tactic
Ltac my_tac := first [tac1 | tac2 ... ].
I would like to add tactics to this list, like adding hints to a hint database, like
Hint Extern tac : ...
But auto only succeed when it can solve the goal, while I want it to try the tactics in the list and do not need to solve the goal. It is possible to add tactics by redefine my_tac, as
Ltac my_tac ::= first [tac1 | tac2 | ... | new_tac1].
But it becomes troublesome, if two separated modules M1 and M2 adds their tactics to my_tac and another module M3 requires M1 and M2.

I tried Ltac2, and I find I can create a list of tactic and do first [tac_list]. But when I try to add another tactic to the list by
Ltac2 Set tac_list := new_tac :: tac_list.
it does not work, maybe because Ltac2 does not allow top level side effect. I cannot redefine a top level definition by reading its old value. I am wondering if it is possible to allow top level side effect for Ltac2.

There is another application of maintaining a list of tactics. Before starting the core part of a tactic, it calls a preprocess procedure which is a list of tactics called in sequence, as
Ltac preprocess := tac1; tac2 ...
It is also useful to add tactics to this list.

Thanks,
Qinshi Wang
Princeton University



Archive powered by MHonArc 2.6.18.

Top of Page