The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

Ltac has no built-in way of getting information out of a failed tactic that can then be used in the proof.  It can print a message to the user, but that's all.  There's no analog in Ltac to a try/raise construct common to many programming languages.

However, in 8.5, one can do the following:

Inductive maybeException {T:Type} : Type :=
| Exception(val:T)
| NoException(val:T).

Axiom raised : forall T (val:T) X, X.

Ltac raise val := apply (raised _ val).

Ltac catch tac type :=
  let X:=constr:($(tac)$ : type) in
  lazymatch X with
  | context [raised] =>
    multimatch X with
    | context [raised _ ?V _] => constr:(Exception V)
    end
  | _ => constr:(NoException X)
  end.

One uses this as:

match catch tac type with
| NoException ?Result => ... normal case ...
| Exception ?Value => ... handler ...
end.

where tac does some processing and either calls "raise V" for some value V, or just completely solves its goal.  It can do multiple raises if tac produces multiple subgoals - which is the reason for that "multimatch" in catch.  It's possible to define a variant of catch that collects all raised values into a single exception instead of offering them as backtrackable alternatives.

Note that the raise tactic is a variant of admit - using a prove-anything axiom (raised) instead of actually failing.  However, because of the way catch works - using "$(...)$" to run tac, and then filtering out results that contain "raised" - the result of catch is never dependent on that axiom.

If tac might fail, and if one wants to view that failure as an exception in addition to any others that tac might raise, then do something like:

Inductive itFailed : Prop :=.
match catch ltac:(first [tac | raise itFailed]) type with...

An important flaw is that if raise is used when there is no surrounding catch, then the result will depend on the raised axiom instead of failing.  I'm hoping that Coq eventually has a way to assert assumptions - like Print Assumptions, but producing an error if the proof depends on different assumptions (such as raised) than those specified.

Another caveat: any evar instantiations that tac does will not get undone if it calls raise, unlike when it fails.

One more: if a raised value would be trapped under binders - then catch will not see it.  Another possible variant of catch could dig such values out from under binders and properly rebind them when constructing the Exception.

-- Jonathan