The Coq mailing list

[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
>>>
>>