0

Ltac is used for automating proofs and modifying proof environment, outputting strings and defining complex notations. Can it be also used for "smart" modifications of Coq environment? Here are two failed attempts:

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.*)

Also, if this isn't a job for Ltac, maybe there's another way?

Community
  • 1
  • 1
jaam
  • 900
  • 4
  • 23

1 Answers1

2

Short answer: No.

Even if you would achieve to do that using some hack, it will stop working in the next Coq version.

The reason is because the interpretation of ltac commands happens at a lower level than document interpretation. This choice could be debatable, but it is the way it is. Tactics run in a constant environment and have only access to the proof. Thus, the most you can do from ltac is to modify the current proof.

Your error happens because Reset is indeed parsed at a higher level which ltac doesn't have access to.

For programmatic manipulation of the environment and documents themselves, the you need to rely in ML code or maybe you could try to script some interfacing tool such as SerAPI to achieve what you want.

ejgallego
  • 6,709
  • 1
  • 14
  • 29
  • "Tactics run in a constant environment and have only access to the proof" this is not totally true as currently there is a hack to be able to add definitions inside proofs, but it is very likely that it goes away as it greatly difficults parallel proof processing. – ejgallego Mar 18 '17 at 09:56
  • For completeness, could you please add a reference to the hack – jaam Mar 18 '17 at 18:51
  • Just do `Definition a := 3` inside a proof. This will alter the environment from the proof. This is itself is implemented as several thousand lines of codes spread over all Coq's source. – ejgallego Mar 18 '17 at 22:38
  • Look for the `side_effects` type as an entry point to that part of the code, but it is fairly complex. – ejgallego Mar 19 '17 at 07:11