Ltac - coq/coq GitHub Wiki

(Part of the Coq FAQ)

Ltac is the tactic language for Coq. It provides the user with a high-level “toolbox” for tactic creation.

You can use the idtac tactic with a string argument. This string will be printed out. The same applies to the fail tactic.

If x_i are identifiers and e_i and expr are tactic expressions, then let reads:

let x₁ := e₁ with x₂ := e₂ ... with x_n := e_n in expr.

Beware that if expr is complex (i.e. features at least a sequence) parentheses should be added around it. For example:

Ltac twoIntro := let x:=intro in (x;x).

Pattern matching on a term expr (non-linear first order unification) with patterns _p_i and tactic expressions e_i reads:

match expr with p₁ => e₁ | p₂ => e₂ ... | p_n => e_n | _ => e_n+1 end.

Underscore matches all terms.

The semantics of match goal depend on whether it returns tactics or not. The match goal expression matches the current goal against a series of patterns: hyp₁ ...hyp_n |- ccl. It uses a first-order unification algorithm and in case of success, if the right-hand-side is an expression, it tries to type it while if the right-hand-side is a tactic, it tries to apply it. If the typing or the tactic application fails, the match goal tries all the possible combinations of _hyp_i before dropping the branch and moving to the next one. Underscore matches all terms.

This is precisely because the semantics of match goal is to apply the tactic on the right as soon as a pattern unifies what is meaningful only in tail-recursive uses.

The semantics in non tail-recursive call could have been the one used for terms (i.e. fail if the tactic expression is not typable, but don’t try to apply it). For uniformity of semantics though, this has been rejected.

You can use the following syntax: let id:=fresh in ... For example:

Ltac introIdGen := let id:=fresh in intro id.