Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
(Part of the Coq FAQ)
What is Ltac?
Ltac is the tactic language for Coq. It provides the user with a high-level “toolbox” for tactic creation.
Is there any printing command in Ltac?
You can use the
idtac tactic with a string argument. This string will be printed out. The same applies
What is the syntax for
let in Ltac?
If xi are identifiers and ei and expr are tactic expressions, then
let x1 := e1 with x2 := e2 ... with xn := en 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).
What is the syntax for pattern matching in Ltac?
Pattern matching on a term expr (non-linear first order unification) with patterns _pi and tactic expressions ei reads:
match expr with p1 => e1 | p2 => e2 ... | pn => en | _ => en+1 end.
Underscore matches all terms.
What are the semantics for
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: hyp1 ...hypn |- 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 _hypi before dropping the branch and moving to the next one. Underscore matches all terms.
Why can’t I use a
match goal returning a tactic in a non tail-recursive position?
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.
How can I generate a new name?
You can use the following syntax:
let id:=fresh in ... For example:
Ltac introIdGen := let id:=fresh in intro id.