Matching on unary data constructors in Ltac

Question

I am doing some exercises about formalizing simply-typed lambda calculus in Coq and would like to automate my proofs using Ltac. While proving progress theorem:

Theorem progress : forall t T,
   empty |-- t \in T -> value t \/ exists t', t ==> t'.

I came up with this piece of Ltac code:

Ltac progress_when_stepping :=
  (* right, because progress statement places stepping on the right of \/ *)
  right;
  (* use induction hypotheses *)
  repeat
    match goal with
    | [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 _ ==> _ ] =>
      induction H; auto
    | [ H : _ -> value _ \/ exists _, ?t2 ==> _, H0 : value ?t1 |-
        exists _, ?C ?t1 ?t2 ==> _ ] =>
      induction H; auto
    | [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] =>
      induction H; auto
    end.

==> denotes a single step of evaluation (via small-step semantics). The intention for each of the match cases is:

1. Match any binary constructor when we have a hypothesis which says that the first term in the constructor steps.
2. Match any binary constructor when we have a hypothesis which says that the second term in the constructor steps and first term in the constructor is already a value
3. Match any unary constructor when we have a hypothesis which says that the term in the constructor steps.

However, looking at the behaviour of this code it looks that the third case also matches binary constructors. How do I restrict it to actually match unary constructors only?

Answer 1

The problem is that ?C matches a term of the form ?C0 ?t0. You can do some secondary matching to rule out this case.

match goal with
  …
| [ H : _ -> value _ \/ exists _, ?t1 ==> _ |- exists _, ?C ?t1 ==> _ ] =>
  match C with
    | ?C0 ?t0 => fail
    | _ => induction H; auto
  end
end.

Answer 2

It seems like the context ident [ term ] construction would work:

There is a special form of patterns to match a subterm against the pattern: context ident [cpattern]. It matches any term with a subterm matching cpattern. If there is a match, the optional ident is assigned the “matched context”, i.e. the initial term where the matched subterm is replaced by a hole. ...

For historical reasons, context used to consider n-ary applications such as (f 1 2) as a whole, and not as a sequence of unary applications ((f 1) 2). Hence context [f ?x] would fail to find a matching subterm in (f 1 2): if the pattern was a partial application, the matched subterms would have necessarily been applications with exactly the same number of arguments.

So, I guess this would work (at least it works on a minimal artificial example I've concocted):

...
  | [ H : _ -> value _ \/ exists _, ?t1 ==> _
    |- context [exists _, ?C ?t1 ==> _ ]] => induction H; auto
...