用 Isabelle 重写证明一个简单的算术语句
Proving a simple arithmetic statement with rewriting in Isabelle
我试图证明 Isabelle 中一些（概念上的）简单算术语句的大写区别。在证明过程中，我偶然发现了以下子目标。
⋀d l k. 0 < d ⟹
¬ 2 * k + 1 ≤ 2 * l ⟹
2 * l ≠ 1 ⟹ - (2 * l) < 2 * k - 1 ⟹ k ≤ l ⟹ d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)
从数学上讲，它相当简单：¬ 2 * k + 1 ≤ 2 * l 和 k ≤ l 这两个陈述意味着 k=l，因此最后一个公式成立。
然而，我无法在伊莎贝尔身上证明这一点。我认为应该可以使用我在 Isar 中的上述推理来构建一个证明，但我仍然是一个初学者，我很难找到正确的关键字。我收到各种令人沮丧的错误。这是我的（其中之一）尝试：
lemma [simp]: "⋀ d k l :: int. 0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶ - (2 * l) < 2 * k - 1 ⟶ k ≤ l ⟶ d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l :: int
assume "¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this show ?thesis
qed
我收到一个奇怪的 "Type unification failed" 错误。
Operator: Trueprop :: bool ⇒ prop
Operand: ?thesis :: int ⇒ int ⇒ int ⇒ bool
有人知道吗？也许如何才能更简单地整体证明这一说法？
(更新：我从这些开始，然后在我努力了很多之后其他人给出了答案，所以我继续把我所做的放在一起。
我想知道的是另一个答案，即在证明中使用 term ?thesis，以帮助将错误消息与问题所在相匹配。
也许我在这里的回答为其他答案增加了一点背景。）
下面，我使用 !! 作为元逻辑 all，而不是 \<And>。
您已进入神秘的元逻辑与对象逻辑区域。稍微了解一下，事情就没那么神秘了。
下面给大家展示一下隐藏Trueprop函数的使用方法，解开一些谜底。
- 稍微解释一下 3 个纯元逻辑运算符，以及它们与 HOL 对象逻辑的关系，
- 给出 3 种不同形式的
lemma，从你的开始，
- 其中第三种形式的
show ?thesis最终被证明引擎接受。
我没有完全解决这里的问题。对我自己来说，很多时候我完全理解一切并不重要，但重要的是我不完全不知道正在使用的元逻辑和对象逻辑函数的类型，这是核心所有这些。
HOL bool、Pure prop 和 Trueprop :: (bool => prop)，将 HOL 绑定到 Pure
Trueprop 函数的符号通常是隐藏的。您可以定义符号以查看它在输出面板中的应用位置。我在这里用一些声明定义 notation：
notation (output) Trueprop ("_:@T" [1000] 999)
declare[[show_brackets=false, show_types, show_sorts=false, show_consts]]
这是Trueprop的类型：
term "Trueprop :: bool => prop"
在您下面的 lemma 中，因为您使用的是 --> 而不是 ==>，所以输出显示系列的含义是 bool 类型，并且它被 Trueprop 强制为 prop，如符号 :@T.
所示
HOL 逻辑连接词的类型为 bool。例如，
term "op --> :: (bool => bool => bool)"
term "A --> B :: bool"
Pure 的 3 个主要运算符：eq (==)、imp (==>) 和 all (!!)
在这里，我确认一下它们的类型。 CNTL-单击它们将您带到它们那里。稍微了解所涉及的类型，可以使错误消息不那么神秘。
term "Pure.eq :: 'a => 'a => prop"
term "Pure.imp :: prop => prop => prop"
term "Pure.all :: ('a => prop) => prop"
关于这一切，有太多要说的了。有人需要写一本教科书，针对像我这样的逻辑新手，解释Isabelle/HOL的逻辑，从Pure.
开始
prop 与 bool
自由变量是隐式的、普遍量化的，所以我可以摆脱对!!的使用。结果是术语的类型从 prop 变为 bool。打开类型信息有助于理解类型错误消息。
term "(!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: prop"
term "(0 < (d::int) --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: bool"
你的原创
您从 ?thesis ::int => int => int => bool` 开始。
declare[[show_types=false]]
lemma "!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" (*
1. !!d k l. (0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 -->
- (2 * l) < 2 * k - 1 --> k ≤ l -->
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"λd k l. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int => int => int => bool" *)
show ?thesis (*
Type unification failed: Clash of types "_ => _" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool => prop
Operand: ?thesis∷int => int => int => bool ::
int => int => int => bool
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "bool" *)
oops
摆脱 !!
的显式使用
我摆脱了 !!，现在我得到了 ?thesis :: bool，并且错误消息变成了一个非常常见的令人沮丧的错误，"fails to refine any pending goal"。这意味着某种程度上，我没有将我将要做的事情 show 与证明引擎认为的目标（我猜）相匹配。
lemma "0 < (d::int)
--> ¬ 2 * k + 1 ≤ 2 * l
--> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "bool"
*)
show ?thesis (*
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
((¬ 2 * ?ka2 + 1 ≤ 2 * ?la2):@T) ==>
((?ka2 ≤ ?la2):@T) ==>
(0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
oops
现在 ==> 代替 -->，show ?thesis 被接受
现在我将 --> 替换为 ==>。 ?thesis 的类型仍然是 bool，它现在接受 show ?thesis.
lemma "0 < (d::int)
==> ¬ 2 * k + 1 ≤ 2 * l
==> 2 * l ≠ 1
==> - (2 * l) < 2 * k - 1 ==> k ≤ l
==> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" :: "bool"*)
show ?thesis (*
goal (1 subgoal):
1. (d * ((2::int) * k - (2::int)) + d * ((2::int) * l) + d =
d * ((4::int) * k - (1::int))):@T *)
oops
今天不用再费脑筋了。我们必须做的事情有一些微妙之处，即以引擎想要的方式向引擎提供它想要的事实证明。我可以查看其他答案并进一步解决问题。
这个错误一点也不奇怪。看看 ?thesis（通过 term "?thesis"）
表示的术语
"λd k l.
0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶
- (2 * l) < 2 * k - 1 ⟶
k ≤ l ⟶
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int ⇒ int ⇒ int ⇒ bool"
您可以看到 ⋀ 绑定变量已变成 ?thesis 的参数（因此具有函数类型）。
此外，您在证明中使用了 assume，而没有先从 HOL 蕴涵 --> 到纯蕴涵 ==>。你的引理可以证明如下：
lemma [simp]:
"⋀ d k l ::int. 0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶
- (2 * l) < 2 * k - 1 ⟶
k ≤ l ⟶
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l :: int
{ assume "¬ 2 * k + 1 ≤ 2 * l" and "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto }
then show "?thesis d k l" by simp
qed
这里我使用原始证明块（在花括号内）在本地证明一个语句，然后用于获得最终结果。
更抽象的是块
{ fix x assume "A x" ... have "B x" ... }
事实结果
!!x. A x ==> B x
这在第 2.2 节中有更详细的描述
Isabelle/Isar Reference Manual.
我试图证明 Isabelle 中一些（概念上的）简单算术语句的大写区别。在证明过程中，我偶然发现了以下子目标。
⋀d l k. 0 < d ⟹
¬ 2 * k + 1 ≤ 2 * l ⟹
2 * l ≠ 1 ⟹ - (2 * l) < 2 * k - 1 ⟹ k ≤ l ⟹ d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)
从数学上讲，它相当简单：¬ 2 * k + 1 ≤ 2 * l 和 k ≤ l 这两个陈述意味着 k=l，因此最后一个公式成立。
然而，我无法在伊莎贝尔身上证明这一点。我认为应该可以使用我在 Isar 中的上述推理来构建一个证明，但我仍然是一个初学者，我很难找到正确的关键字。我收到各种令人沮丧的错误。这是我的（其中之一）尝试：
lemma [simp]: "⋀ d k l :: int. 0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶ - (2 * l) < 2 * k - 1 ⟶ k ≤ l ⟶ d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l :: int
assume "¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this show ?thesis
qed
我收到一个奇怪的 "Type unification failed" 错误。
Operator: Trueprop :: bool ⇒ prop
Operand: ?thesis :: int ⇒ int ⇒ int ⇒ bool
有人知道吗？也许如何才能更简单地整体证明这一说法？
(更新：我从这些开始，然后在我努力了很多之后其他人给出了答案，所以我继续把我所做的放在一起。
我想知道的是另一个答案，即在证明中使用 term ?thesis，以帮助将错误消息与问题所在相匹配。
也许我在这里的回答为其他答案增加了一点背景。）
下面，我使用 !! 作为元逻辑 all，而不是 \<And>。
您已进入神秘的元逻辑与对象逻辑区域。稍微了解一下，事情就没那么神秘了。
下面给大家展示一下隐藏Trueprop函数的使用方法，解开一些谜底。
- 稍微解释一下 3 个纯元逻辑运算符，以及它们与 HOL 对象逻辑的关系，
- 给出 3 种不同形式的
lemma，从你的开始， - 其中第三种形式的
show ?thesis最终被证明引擎接受。
我没有完全解决这里的问题。对我自己来说，很多时候我完全理解一切并不重要，但重要的是我不完全不知道正在使用的元逻辑和对象逻辑函数的类型，这是核心所有这些。
HOL bool、Pure prop 和 Trueprop :: (bool => prop)，将 HOL 绑定到 Pure
Trueprop 函数的符号通常是隐藏的。您可以定义符号以查看它在输出面板中的应用位置。我在这里用一些声明定义 notation：
notation (output) Trueprop ("_:@T" [1000] 999)
declare[[show_brackets=false, show_types, show_sorts=false, show_consts]]
这是Trueprop的类型：
term "Trueprop :: bool => prop"
在您下面的 lemma 中，因为您使用的是 --> 而不是 ==>，所以输出显示系列的含义是 bool 类型，并且它被 Trueprop 强制为 prop，如符号 :@T.
HOL 逻辑连接词的类型为 bool。例如，
term "op --> :: (bool => bool => bool)"
term "A --> B :: bool"
Pure 的 3 个主要运算符：eq (==)、imp (==>) 和 all (!!)
在这里，我确认一下它们的类型。 CNTL-单击它们将您带到它们那里。稍微了解所涉及的类型，可以使错误消息不那么神秘。
term "Pure.eq :: 'a => 'a => prop"
term "Pure.imp :: prop => prop => prop"
term "Pure.all :: ('a => prop) => prop"
关于这一切，有太多要说的了。有人需要写一本教科书，针对像我这样的逻辑新手，解释Isabelle/HOL的逻辑，从Pure.
开始prop 与 bool
自由变量是隐式的、普遍量化的，所以我可以摆脱对!!的使用。结果是术语的类型从 prop 变为 bool。打开类型信息有助于理解类型错误消息。
term "(!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: prop"
term "(0 < (d::int) --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)) :: bool"
你的原创
您从 ?thesis ::int => int => int => bool` 开始。
declare[[show_types=false]]
lemma "!! d k l :: int. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> -(2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" (*
1. !!d k l. (0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 -->
- (2 * l) < 2 * k - 1 --> k ≤ l -->
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"λd k l. 0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int => int => int => bool" *)
show ?thesis (*
Type unification failed: Clash of types "_ => _" and "bool"
Type error in application: incompatible operand type
Operator: Trueprop :: bool => prop
Operand: ?thesis∷int => int => int => bool ::
int => int => int => bool
Coercion Inference:
Local coercion insertion on the operand failed:
No coercion known for type constructors: "fun" and "bool" *)
oops
摆脱 !!
的显式使用
我摆脱了 !!，现在我得到了 ?thesis :: bool，并且错误消息变成了一个非常常见的令人沮丧的错误，"fails to refine any pending goal"。这意味着某种程度上，我没有将我将要做的事情 show 与证明引擎认为的目标（我猜）相匹配。
lemma "0 < (d::int)
--> ¬ 2 * k + 1 ≤ 2 * l
--> 2 * l ≠ 1
--> - (2 * l) < 2 * k - 1 --> k ≤ l
--> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "bool"
*)
show ?thesis (*
Failed to refine any pending goal
Local statement fails to refine any pending goal
Failed attempt to solve goal by exported rule:
((¬ 2 * ?ka2 + 1 ≤ 2 * ?la2):@T) ==>
((?ka2 ≤ ?la2):@T) ==>
(0 < d --> ¬ 2 * k + 1 ≤ 2 * l --> 2 * l ≠ 1 --> - (2 * l) < 2 * k - 1
--> k ≤ l --> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)):@T *)
oops
现在 ==> 代替 -->，show ?thesis 被接受
现在我将 --> 替换为 ==>。 ?thesis 的类型仍然是 bool，它现在接受 show ?thesis.
lemma "0 < (d::int)
==> ¬ 2 * k + 1 ≤ 2 * l
==> 2 * l ≠ 1
==> - (2 * l) < 2 * k - 1 ==> k ≤ l
==> d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l ::int
assume " ¬ 2 * k + 1 ≤ 2 * l" "k ≤ l"
then have "k=l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto
from this
term "?thesis" (*
"d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" :: "bool"*)
show ?thesis (*
goal (1 subgoal):
1. (d * ((2::int) * k - (2::int)) + d * ((2::int) * l) + d =
d * ((4::int) * k - (1::int))):@T *)
oops
今天不用再费脑筋了。我们必须做的事情有一些微妙之处，即以引擎想要的方式向引擎提供它想要的事实证明。我可以查看其他答案并进一步解决问题。
这个错误一点也不奇怪。看看 ?thesis（通过 term "?thesis"）
"λd k l.
0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶
- (2 * l) < 2 * k - 1 ⟶
k ≤ l ⟶
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
:: "int ⇒ int ⇒ int ⇒ bool"
您可以看到 ⋀ 绑定变量已变成 ?thesis 的参数（因此具有函数类型）。
此外，您在证明中使用了 assume，而没有先从 HOL 蕴涵 --> 到纯蕴涵 ==>。你的引理可以证明如下：
lemma [simp]:
"⋀ d k l ::int. 0 < d ⟶
¬ 2 * k + 1 ≤ 2 * l ⟶
2 * l ≠ 1 ⟶
- (2 * l) < 2 * k - 1 ⟶
k ≤ l ⟶
d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)"
proof -
fix d k l :: int
{ assume "¬ 2 * k + 1 ≤ 2 * l" and "k ≤ l"
then have "k = l" by simp
then have "d * (4 * l - 1) = d * (4 * k - 1) " by auto
moreover have "d * (2 * l - 2) + d * (2 * l) + d = d * (4 * l - 1)" by algebra
ultimately have "d * (2 * k - 2) + d * (2 * l) + d = d * (4 * k - 1)" by auto }
then show "?thesis d k l" by simp
qed
这里我使用原始证明块（在花括号内）在本地证明一个语句，然后用于获得最终结果。
更抽象的是块
{ fix x assume "A x" ... have "B x" ... }
事实结果
!!x. A x ==> B x
这在第 2.2 节中有更详细的描述 Isabelle/Isar Reference Manual.