HOL Theorem Prover：向已有理论添加定理时遇设目标错误

看起来你在尝试证明列表拼接的长度定理时，卡在了目标设置这一步。我帮你拆解下问题所在，再给出完整的解决步骤：

首先定位错误根源 #

你给出的待证明定理和目标语句里有两个关键问题：

1. 类型不匹配错误：待证定理里的LENGTH l1 + l2明显有问题——LENGTH l1是自然数类型（num），而l2是列表类型（'a list），HOL不允许不同类型的对象相加，这是最核心的错误。正确的表述应该是LENGTH l1 + LENGTH l2。
2. 语法细节问题：HOL对标识符和符号之间的空格有一定要求（比如LENGTH(最好写成LENGTH (），虽然部分版本有容错，但规范写法能避免不必要的语法报错。另外，部分HOL版本（比如HOL4）更常用Goal而非set_goal来设置证明目标。

正确的目标设置与证明步骤 #

1. 修正后的目标语句 #

如果是HOL4环境，用以下语句设置目标（兼容大部分HOL版本）：

Goal `! (l1:'a list) (l2:'a list). LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2`;

如果你的环境必须用set_goal，则写成：

set_goal ([], `! (l1:'a list) (l2:'a list). LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2`);

2. 完整的证明脚本 #

设置好目标后，我们可以用列表归纳法来完成证明，这是处理列表性质定理的标准方法：

# 设置目标
Goal `! (l1:'a list) (l2:'a list). LENGTH (APP l1 l2) = LENGTH l1 + LENGTH l2`;

# 对列表l1进行归纳
Induct_on `l1`;

# 处理基例（l1 = []）：直接用重写规则自动验证
REWRITE_TAC [];

# 处理归纳步骤：用归纳假设结合算术规则重写
ASM_REWRITE_TAC [ARITH_RULE `1 + (x + y) = (1 + x) + y`];

# 完成证明并保存定理
QED;

证明思路解释 #

• 基例：当l1是空列表时，APP [] l2就是l2，左边长度是LENGTH l2；右边LENGTH [] + LENGTH l2等于0 + LENGTH l2，两者相等，REWRITE_TAC会自动调用已有的定义（比如APP的基例、LENGTH的基例）完成验证。
• 归纳步骤：假设对于任意列表l1定理成立，我们要证明h::l1的情况。左边LENGTH (APP (h::l1) l2)展开后是1 + LENGTH (APP l1 l2)，右边LENGTH (h::l1) + LENGTH l2展开是1 + LENGTH l1 + LENGTH l2。用归纳假设把左边的LENGTH (APP l1 l2)替换成LENGTH l1 + LENGTH l2，再用算术结合律调整顺序，就能得到两边相等的结论。

内容的提问来源于stack exchange，提问作者Tuffie