coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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,
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
- [Coq-Club] Maintaining a list of tactics, Qinshi Wang, 04/27/2020
- Re: [Coq-Club] Maintaining a list of tactics, Yannick Forster, 04/27/2020
Archive powered by MHonArc 2.6.18.