3

我正在做一些关于在 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. 当我们有一个假设说构造函数中的术语是步骤时，匹配任何一元构造函数。

然而，看看这段代码的行为，它看起来第三种情况也匹配二进制构造函数。如何将其限制为仅实际匹配一元构造函数？

4

2 回答 2

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.
于 2016-05-06T10:13:52.830 回答
0

看起来context ident [ term ]建筑会起作用：

有一种特殊形式的模式可以将子项与模式匹配： context ident [cpattern]. 它匹配具有匹配 cpattern 的子术语的任何术语。如果存在匹配，则为可选的 ident 分配“匹配上下文”，即匹配的子项被替换为空洞的初始项。 ...

由于历史原因，context曾经将 n-ary 应用程序(f 1 2)视为一个整体，而不是作为一元应用程序的序列((f 1) 2)。因此context [f ?x]将无法在(f 1 2): 中找到匹配的子项，如果模式是部分应用程序，则匹配的子项必然是具有完全相同数量参数的应用程序。

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

...
  | [ H : _ -> value _ \/ exists _, ?t1 ==> _
    |- context [exists _, ?C ?t1 ==> _ ]] => induction H; auto
...
于 2016-05-06T10:08:39.323 回答