coqltac

Why does Ltac not match the clause?

In the following Coq proof:

Ltac easy_ltac t  := match goal with
  | [Z: @eq nat t ?Y |- _ ] => pose ?Y as N 
  end.

Lemma easy: forall (n: nat), (n >= O)%nat.
Proof.
intros n. destruct n eqn: M.  easy_ltac n.

I get the error message: "No matching clauses for match.", while I have the hypothesis

M : @eq nat n O

I do not understand why.

Solution

  • The culprit is the extraneous ? before the 2nd occurrence of Y.

    Also just to recall, you might want to use the fresh tactic rather than hard-coded N as an hypothesis name.

    So, it should work if you just write:

    Ltac easy_ltac t := match goal with
  | [Z: @eq nat t ?Y |- _ ] => let N := fresh "N" in pose Y as N
  end.

Lemma easy: forall (n: nat), (n >= O)%nat.
Proof.
intros n. destruct n eqn: M. easy_ltac n. easy_ltac n.