Coq定义STLC step规则时如何将nat类型S n表示为tm项？

开发者阿泽

2026-8-28

问题说明

在完成《Software Foundations 第二卷》StlcProp章节最后一道练习时，定义step归约关系的ST_SuccNat规则时出现类型错误，相关代码如下：

Inductive step : tm -> tm -> Prop :=
  | ST_AppAbs : forall x T2 t1 v2,
      value v2 ->
      <{(\x:T2, t1) v2}> --> <{ [x:=v2]t1 }>
  | ST_App1 : forall t1 t1' t2,
      t1 --> t1' ->
      <{t1 t2}> --> <{t1' t2}>
  | ST_App2 : forall v1 t2 t2',
      value v1 ->
      t2 --> t2' ->
      <{v1 t2}> --> <{v1  t2'}>
  | ST_SuccNat: forall n:nat,
      <{succ n}> --> <{ S n }> (* <----- 报错位置 *)

报错信息

In environment
step : tm -> tm -> Prop
n : nat
The term "S" has type "nat -> nat" while it is expected to have type "tm".

错误含义：当前环境中S的类型为nat -> nat，但规则上下文需要的是tm类型的项。

错误原因

核心问题是元语言与对象语言的构造子混淆：

S是Coq元语言中nat类型的后继构造子，类型为nat -> nat，只能生成Coq层面的自然数，无法直接生成STLC对象语言定义的tm类型语法项。
代码中使用的<{ ... }>是SF封装的自定义语法记号，会自动将Coq的nat类型值包装为STLC中对应的自然数常量项（即tm类型的常量构造器，通常为const n），但S不在该记号的默认解析范围内，直接写<{ S n }>时，Coq会尝试将S识别为tm类型的语法构造，最终触发类型不匹配错误。

解决方案

两种写法均可通过类型检查：

直接操作AST构造子，完全绕开记号解析的歧义，最稳妥：
首先确认tm类型的定义中，succ对应的AST构造子为tsucc : tm -> tm，自然数常量嵌入构造子为const : nat -> tm，将规则改写为：
```
| ST_SuccNat : forall n : nat,
    tsucc (const n) --> const (S n)
```
继续使用<{ ... }>记号，将S n替换为等价的Coq自然数算术表达式n + 1，记号可正确识别该表达式为Coq自然数，自动包装为合法的tm项：
```
| ST_SuccNat: forall n:nat,
    <{succ n}> --> <{ n + 1 }>
```