The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

For 1) and 3) I think you would use Tactic Notation 
https://coq.inria.fr/distrib/current/refman/Reference-Manual014.html#hevea_command230

eg

    Tactic Notation "tactic_example" whatever(H) "in" hyp(H') := code 
of tactic_example_in.

According to the manual it can be used to get argument lists but I don't 
know how that part works.

Gaëtan Gilbert

On 12/09/2016 14:00, Sebastian Böhne wrote:
> Dear Coq-community!
>
> I've accumulated some questions about tactics in Coq. It would be very 
> nice if you could help me with some of these. (I'm using CoqIDE 
> (8.4pl3)):
>
> 1) Tactics like simpl can be used in hypotheses as well by adding 'in 
> Hyp' at the end. Is it possible to define my own tactics in that 
> style, too? So far in such cases I defined tactics like tactic_example 
> H and a second one called tactic_example_in H H' for use in the 
> hypotheses, but I would prefer to be able to write tactic_example H in 
> H' in the latter case.
>
> 2) When I want to unfold a notation I can first locate it ('locate 
> "operator-sign"') and then do an unfold with the real non-abbreviated 
> name. However, I would appreciate a direct way. Is there a tactic to 
> do so?
>
> 3) Is it possible to define tactics like intros which get a list as 
> input? Up to now I made different tactics like my_tactic_n for n up to 
> 5 or so for the different numbers of arguments, but this is not really 
> satisfying.
>
> 4) I would like to build an induction-tactic which behaves a little 
> bit different than the original one: It should only match with the 
> current goal and should not be the induction of one of the hypotheses. 
> So far I know how to do it. Another thing is, however, that when 
> applied the original induction tactic makes some intros automatically. 
> For instance when using induction for nat, one subgoal is P(0) (which 
> is ok), while the other is P(Suc n) where n : nat and P(n) are already 
> assumed. I would prefer if it would be simply ∀ n : nat, P n → P (Suc 
> n) as goal instead.
>
> It is no problem to create such a tactic for special cases (like nat), 
> but I would like a tactic as general as the orginal one. The problem 
> seems to me to be that I somehow had to use A_ind for the different 
> inductive types A. Yet ind A or something like that does not work 
> since ind is not a total function and I don't know how to refer to 
> A_ind otherwise.
>
> Another attempt would be to use induction and to regeneralise the 
> hypotheses, but then I need the names and the number of the hypotheses 
> for reconstruction. This in turn seems to me to amount to the same 
> problem of having to know A_ind.
>
> Thank you very much and best regards
>
> Sebastian Böhne