The Coq mailing list

[Matthias Puech <puech AT cs.unibo.it>]

Le 11/02/2011 01:49 PM, Victor Porton a écrit :
> Probably a stupid question:

It's actually a pretty good one (i.e. it was already thought about a lot).

> Can't programs generated from existence proof be use instead of tactic 
> scripts?

They can! A tactic programmed in Gallina is called a *reflexive* tactic. 
It involves:
- turning your goal (written in Gallina) into an AST (belonging to an 
inductive type) -> reification step
- applying your theorem, resulting in a modified AST preserving the 
meaning -> adequacy lemma
- apply a [semantics] function which maps back the AST into Coq's world 
-> interpretation step

> Why Coq has special language for writing new tactics, while Coq proofs can be 
> turn into programs?

Because it is very hard and time consuming to build a full-blown tactic 
reflexively, and in some cases not possible: you have to prove 
correctness and termination (as part of adequacy), and be able to 
reflect a large part of the language, which in many cases is not 
obvious. As a quick-and-dirty way to build compound tactics, we have Ltac.
    -m