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.

==>表示计算的单个步骤(通过小步骤语义)。每一场比赛的意图是：

1. 当我们有一个假设时，匹配任何二进制构造函数，假设构造函数中的第一个项是步骤。
2. 如果我们有一个假设，即构造函数步骤中的第二个项和构造函数中的第一个项已经是值，则可以匹配任何二进制构造函数。
3. 当我们有一个假设时，匹配任何一元构造函数，假设构造函数中的术语是步骤。

但是，从这段代码的行为来看，第三种情况也与二进制构造函数相匹配。如何将其限制为只匹配一元构造函数？

Answer 1

问题是?C与表单?C0 ?t0的一个术语相匹配。你可以做一些次要的匹配来排除这种情况。

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

Answer 2

看起来，context ident [ term ]的构造是可行的：

有一种特殊形式的模式可以将子项与模式相匹配：context ident [cpattern]。它将任何项与匹配的子项cpattern匹配。如果匹配，则可选标识符被指定为“匹配上下文”，即将匹配子项替换为空洞的初始项。… 由于历史原因，context过去通常将n进制应用程序(如(f 1 2) )作为一个整体来考虑，而不是将其作为一元应用程序的序列( ((f 1) 2) )。因此，context [f ?x]将无法在(f 1 2)中找到匹配的子项:如果模式是一个部分应用程序，那么匹配的子项必然是具有完全相同数量的参数的应用程序。

所以，我想这是可行的(至少在我编造的一个最小的人工例子中是可行的)：

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