The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Unfortunately there is currently no equivalent of ltac for commands.
The only way of defining new commands is via ocaml plugins AFAIK.

Best Regards,
Pierre

2017-12-14 14:42 GMT+01:00 Dominique Larchey-Wendling
<dominique.larchey-wendling AT loria.fr>:
> Thank you Pierre for your time.
>
> Actually, what I though about was textual manipulation of
> Coq code, not only terms or tactics ...
>
> For instance, consider a lemma foo such as for instance
>
> Lemma foo f x : f (f^n x) = f^(1+n) x.
>
> That I would like to incorporate into an autorewrite
> tactic.
>
> Ltac myauto := autorewrite with mydb.
>
> Hint Rewrite foo : mydb.
>
> The point is for instance that I do not want myauto to
> use foo for any f, but only for a specific f, which
> might change depending on the context.
>
> So
>
> Hint Rewrite (foo f) : mydb.
>
> But then, I would like a macro like :
>
> Marco myauto arg(f) :=
>    Hint Rewrite (foo f) : mydb; autorewrite with mydb.
>
> So a macro is something that expands into Coq code.
> I agree it might lead to unreadable code before
> expansion. You can write unreadable (La)TeX code as
> well. But used wisely, it might help shrink code.
>
> Best,
>
> Dominique
>
> ---------------
>
> Le 14/12/2017 à 13:46, Pierre Courtieu a écrit :
>> I come back to this question after some thinking about it.
>>
>> Indeed uconstr does not fit in the suggestion I made. Something you
>> may be able to do in some cases (but not in your case I guess, see
>> below) is to use the String type where you need some specific non
>> typable format.
>>
>> Inductive args :=
>>   Step: args
>> | Iter: nat -> args
>> | Hyp: forall (A:Type) (t:A), args
>> | Trans: String -> args.   (* <--- here *)
>>
>> and hopefully you can analyse the string character by character to
>> implement the behaviour you want.
>>
>> BUT it seems your uconstr has subparts that you want to consider as
>> real coq terms, and I am not aware of a way to take a String and
>> transform it into a constr by giving it to the  coq parser.
>>
>> What are the possible forms of your uconstr arguments? Maybe you can
>> describe them in a inductive type.
>>
>> Best,
>> Pierre
>>
>>
>>
>>
>> 2017-10-30 14:25 GMT+01:00 Dominique Larchey-Wendling
>> <dominique.larchey-wendling AT loria.fr>:
>>> Dear Pierre,
>>>
>>> Thx for the suggestion but there is a problem with
>>> the untyped argument <uconstr> which cannot be represented
>>> as a Coq typed term.
>>>
>>> Is there no way or extension for Tactic to manipulate
>>> text ?
>>>
>>> Dominique
>>>
>>> Le 30/10/2017 à 12:03, Pierre Courtieu a écrit :
>>>> Hi,
>>>> I guess you should define a tactic taking a list (coq lists) over some
>>>> inductive type describing the steps. Then some Tactic notation could get
>>>> you close to the syntax you want.
>>>>
>>>> Pierre
>>>>
>>>> Le lun. 30 oct. 2017 à 10:26, Dominique Larchey-Wendling
>>>> <dominique.larchey-wendling AT loria.fr
>>>> <mailto:dominique.larchey-wendling AT loria.fr>>
>>>>  a écrit :
>>>>
>>>>     Dear all,
>>>>
>>>>     I am wondering if there is a way to define macros within the
>>>>     tactic language.
>>>>
>>>>     For instance, consider that I have already defined
>>>>     tactic notations such as:
>>>>
>>>>     wcbv step
>>>>     wcbv iter <integer>
>>>>     wcbv hyp
>>>>     wcbv trans <uconstr>
>>>>
>>>>     Then I would like to be able to write
>>>>
>>>>     wcbv step, hyp, hyp, trans (t @ a), iter 2.
>>>>
>>>>     instead of
>>>>
>>>>     wcbv step; do 2 wcbv hyp; wcbv trans (t @ a); wcbv iter 2.
>>>>
>>>>     Can I do this using Ltac and Tactic Notation ?
>>>>     Because it seems neither can input <text> as an
>>>>     argument (like latex or metapost macros would do)
>>>>
>>>>     Thanks very much in advance for any hint
>>>>
>>>>     Dominique
>>>>
>>>
>