Search code examples
coqdependent-typetheorem-provingcoq-tacticltac

Ltac: Matching goal with type that depends on name of previous goal

I'm trying to write Ltac code that looks like this:

match goal with
    | [ e : expr, H : (is_v_of_expr e = true) |- _ ] => idtac
end.
(* The reference e was not found in the current environment *)

The problem is, trying to match a case where there's a value in the context, and some fact about that value. So I'm mixing the namespaces of the hypothesis names, and the hypothesis types. The end goal is to have a loop that destructs (is_v_of_expr e) for each expr in the context, but to make sure that it doesn't loop by continuously destructing the same expression.

Is it possible to write an Ltac match expression for something like this?

Solution

  • You need to use a nested match. The following should work.

    match goal with
| e : expr |- _ =>
  match goal with
  | H : is_v_of_expr e = true |- _ => idtac
  end
end.