Modification intelligente de l'environnement Coq

Question

Ltac est utilisé pour automating proofs and modifying proof environment, outputting strings et defining complex notations. Peut-il également être utilisé pour des modifications «intelligentes» de l'environnement Coq? Voici deux tentatives ratées:

Variable Phy: Set. 

Fail Let pp (x:Type) := ltac: (match type of x with 
     | Set => constr: (Reset Phy) 
     | _ => idtac end). 
(*Cannot infer an internal placeholder of type "Type" in environment: x : Type*) 

Fail Ltac pp x := match type of x with 
     | Set => constr: (Reset Phy) 
     | _ => idtac end. 
(*The reference Reset was not found in the current environment.*) 

De plus, si ce n'est pas un emploi pour Ltac, peut-être il y a une autre façon?

Answer 1

Réponse courte: Non

Même si vous réaliseriez de le faire en utilisant un certain hack, il cessera de fonctionner dans la prochaine version Coq.

La raison en est que l'interprétation des commandes ltac se produit à un niveau inférieur à celui de l'interprétation de document. Ce choix pourrait être discutable, mais c'est comme ça. Les tactiques fonctionnent dans un environnement constant et n'ont accès qu'à la preuve. Ainsi, le plus que vous pouvez faire avec ltac est de modifier la preuve actuelle.

Votre erreur se produit car Reset est en effet analysé à un niveau supérieur auquel ltac n'a pas accès. Pour la manipulation programmatique de l'environnement et des documents eux-mêmes, vous devez vous appuyer sur le code ML ou peut-être essayer un script d'outil d'interfaçage tel que SerAPI pour obtenir ce que vous voulez.