在 Ltac 中匹配一元数据构造函数

Question

我正在做一些关于在 Coq 中形式化简单类型的 lambda 演算的练习，并且想使用 Ltac 自动化我的证明。在证明进步定理时：

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

我想出了这段 Ltac 代码：

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.

==> 表示单步求值（通过小步语义）。每个匹配案例的意图是：

匹配任何 binary 构造函数，当我们有一个假设表明构造函数步骤中的第一项时。
当我们假设构造函数步骤中的第二项和构造函数中的第一项已经是一个值

二进制

匹配任何一元构造函数，当我们有一个假设表明构造函数步骤中的术语时。

但是，从这段代码的行为来看，第三种情况似乎也匹配 binary 构造函数。如何将其限制为仅实际匹配一元构造函数？

Answer 1

context ident [ term ] 构造似乎可行：

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.

所以，我想这会起作用（至少它适用于我编造的最小人工示例）：

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

Answer 2

问题是 ?C 匹配 ?C0 ?t0 形式的术语。你可以做一些二次匹配来排除这种情况。

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

在 Ltac 中匹配一元数据构造函数

Matching on unary data constructors in Ltac

coq

ltac