Isabelle/HOL Isar 中错误假设的证明
Proof with false hypothesis in Isabelle/HOL Isar
我试图证明一个引理，该引理在某部分有一个错误的假设。在 Coq 中我曾经写 "congruence" 并且它会摆脱目标。但是，我不确定如何在 Isabelle Isar 中进行。我正在尝试证明关于我的 le 函数的引理：
primrec le::"nat ⇒ nat ⇒ bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ⇒ False | Suc j ⇒ le k j)"
lemma def_le: "le a b = True ⟷ (∃k. a + k = b)"
proof
assume H:"le a b = True"
show "∃k. a + k = b"
proof (induct a)
case 0
show "∃k. 0 + k = b"
proof -
have "0 + b = b" by simp
thus ?thesis by (rule exI)
qed
case Suc
fix n::nat
assume HI:"∃k. n + k = b"
show "∃k. (Suc n) + k = b"
proof (induct b)
case 0
show "∃k. (Suc n) + k = 0"
proof -
have "le (Suc n) 0 = False" by simp
oops
请注意，我的 le 函数是 "less or equal"。在证明的这一点上，我发现我有假设 H 表明 le a b = True，或者在这种情况下 le (Suc n) 0 = True 是错误的。我该如何解决这个引理？
另一个小问题：我想写have "le (Suc n) 0 = False" by (simp only:le.simps)，但这行不通。看来我需要添加一些规则来减少 case 表达式。我错过了什么？
非常感谢您的帮助。
问题不在于很难摆脱伊莎贝尔的一个False假设。事实上，如果假设中存在 False，几乎所有 Isabelle 的证明方法都会立即证明任何事情。不，这里的问题是在证明的那个点，你不再有你需要的假设，因为你没有将它们链接到归纳中。但首先，请允许我发表一些小意见，然后给出具体的建议来修正你的证明。
几点说明
- 伊莎贝尔写
le a b = True或le a b = False有点不合时宜。只需写 le a b 或 ¬le a b.
- 以方便的形式编写定义对于获得良好的自动化非常重要。当然，您的定义有效，但我建议使用以下定义，它可能更自然，并且会免费为您提供方便的归纳法则：
使用功能包：
fun le :: "nat ⇒ nat ⇒ bool" where
"le 0 n = True"
| "le (Suc k) 0 = False"
| "le (Suc k) (Suc n) = le k n"
- Existentials 有时会隐藏重要信息，并且它们往往会与自动化混淆，因为自动化永远不知道如何实例化它们。
如果你证明以下引理，证明是全自动的：
lemma def_le': "le a b ⟷ a + (b - a) = b"
by (induction a arbitrary: b) (simp_all split: nat.split)
使用我的函数定义，它是：
lemma def_le': "le a b ⟷ (a + (b - a) = b)"
by (induction a b rule: le.induct) simp_all
然后你的引理就很简单地得出了：
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
using def_le' by auto
这是因为存在主义使得搜索 space 爆炸式增长。给自动化一些具体的东西来遵循有很大帮助。
实际答案
有很多问题。首先，您可能需要做 induct a arbitrary: b，因为 b 在您的归纳过程中会发生变化（对于 le (Suc a) b，您将必须对 b 进行案例分析，然后在 b = Suc b' 的情况下，您将从 le (Suc a) (Suc b') 转到 le a b')。
其次，在最上面，你有 assume "le a b = True"，但你没有将这个事实链接到归纳法中。如果您在 Isabelle 中进行归纳，则必须将包含归纳变量的所有必需假设链接到归纳命令中，否则它们将无法用于归纳证明。有问题的假设谈论 a 和 b，但是如果你对 a 进行归纳，你将不得不推理一些与 a' 无关的任意变量a。例如：
assume H:"le a b = True"
thus "∃k. a + k = b"
（对 b 的第二次归纳也是如此）
第三，当你在 Isar 中有多个案例时（例如在归纳或案例分析期间），如果它们有不同的假设，你必须用 next 将它们分开。 next 基本上丢弃了所有固定变量和局部假设。通过我之前提到的更改，您需要在 case Suc 之前添加 next，否则伊莎贝尔会抱怨。
第四，Isar中的case命令可以修复变量。在你的 Suc 案例中，归纳变量 a 是固定的；随着对 arbitrary: b 的更改，a 和 b 得到修复。您应该为这些变量指定明确的名称；否则，Isabelle 将发明它们，您将不得不希望它提出的与您使用的相同。那不是好的风格。所以写例如case (Suc a b)。请注意，在使用 case 时，您 而不是 必须修复变量或进行假设。 case 命令会为您处理这个问题，并将局部假设存储在与案例同名的定理集合中，例如Suc 这里。它们被分类为 Suc.prems、Suc.IH、Suc.hyps。此外，当前案例的证明义务存储在 ?case（不是 ?thesis！）。
结论
有了这个（以及一些清理），你的证明看起来像这样：
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
assume "le a b"
thus "∃k. a + k = b"
proof (induct a arbitrary: b)
case 0
show "∃k. 0 + k = b" by simp
next
case (Suc a b)
thus ?case
proof (induct b)
case 0
thus ?case by simp
next
case (Suc b)
thus ?case by simp
qed
qed
next
可以压缩为
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
assume "le a b"
thus "∃k. a + k = b"
proof (induct a arbitrary: b)
case (Suc a b)
thus ?case by (induct b) simp_all
qed simp
next
但实际上，我建议您先证明 le a b ⟷ a + (b - a) = b 这样的具体结果，然后再用它证明存在性命题。
Manuel Eberl 做了困难的部分，我只是回答你关于如何尝试和控制 simp 等问题
在继续之前，我跑题了，澄清一下在另一个网站上说过的话。 "a tip" 这个词被用来表示对 M.E 的信任，但它应该是“在 2 个答案中提供 3 个解释”。如果不向列表发送垃圾邮件，则无法更正邮件列表中的电子邮件。
一些简短的回答是：
- 不能保证完全控制
simp，但如下所示的属性 del 和 only 可以多次控制它到您想要的程度。要查看它没有做的比您想要的更多，需要使用跟踪；下面给出了一个跟踪示例。
- 要完全控制证明步骤，您可以使用 "controlled"
simp，以及 rule、drule 和 erule，以及其他方法。其他人需要给出详尽的清单。
- 大多数具有能够回答 "what's the detailed proof of what
simp, auto, blast, etc does" 专业知识的人都很少愿意投入工作来回答问题。调查 simp 正在做什么可能是一项简单而乏味的工作。
- "Black box proofs" 总是可选的，据我所知，如果我们希望它们 和 具有使它们成为可选的专业知识。使它们成为可选的专业知识通常是一个主要的限制因素。有了专业知识，动力就成了限制因素。
最简单的是什么？它不能取悦所有人
如果你看，你就会明白。人们抱怨 Isabelle 自动化太多，或者他们抱怨自动化太少。
永远不会有太多的自动化，但那是因为对于 Isabelle/HOL，自动化在很大程度上是可选的。 没有自动化 的可能性使得证明可能很有趣，但是只有 没有自动化，在宏伟的计划中，证明只是纯粹的乏味。
有属性only和del，可以用来大部分控制simp。仅从痕迹实验来说，即使simp也会调用其他证明方法，类似于auto调用simp、blast等
我认为你无法阻止 simp 调用线性算术方法。但是线性算术在很多时候并不适用。
设置痕迹，甚至爆炸痕迹
我在这里的回答是概括的，因为还试图确定 auto 的目的。 auto 使用的最大方法之一是 blast。
如果您不关心 blast 何时被 auto 使用或直接调用，则不需要 attribute_setup。 Makarius Wenzel 取出了爆炸痕迹，但随后非常友好地展示了如何实现它的代码。
没有爆破部分，只有declare的使用。在证明中，您可以使用 using 而不是 declare。把你不想要的拿出来。请务必查看 PIDE Simplifier Trace 面板中的新 simp_trace_new 信息。
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
attribute_setup blast_stats = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats b)))
*}
declare[[simp_trace_new mode=full]]
declare[[linarith_trace,rule_trace,blast_trace,blast_stats]]
尝试控制简单，随心所欲 only & del
我不想用你问题中的公式来努力工作。使用 simp，您使用 only 寻找的是没有使用您不期望的规则。
查看 simp 跟踪以了解哪些基本重写已完成且将始终完成，例如 True 和 False 的基本重写。如果你甚至不想那样，那么你必须求助于 rule.
这样的方法
查看是否可以完全关闭 simp 的起点是 apply(simp only:)。
这里有几个例子。我将不得不更加努力地寻找一个示例来说明何时自动使用线性算术：
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp only:) (*
ERROR: simp can't apply any magic whatsoever.
*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp only: add_0) (*
ERROR: Still can't. Rule 'add_0' is used, but it can't be used first.
*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp del: add_0) (*
A LITTLE MAGIC:
It applied at least one rule. See the simp trace. It tried to finish
the job automatically, but couldn't. It says "Trying to refute subgoal 1,
etc.".
Don't trust me about this, but it looks typical of blast. I was under
the impressions that simp doesn't call blast.*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
by(simp) (*
This is your question. I don't want to step through the rules that simp
uses to prove it all.
*)
我试图证明一个引理，该引理在某部分有一个错误的假设。在 Coq 中我曾经写 "congruence" 并且它会摆脱目标。但是，我不确定如何在 Isabelle Isar 中进行。我正在尝试证明关于我的 le 函数的引理：
primrec le::"nat ⇒ nat ⇒ bool" where
"le 0 n = True" |
"le (Suc k) n = (case n of 0 ⇒ False | Suc j ⇒ le k j)"
lemma def_le: "le a b = True ⟷ (∃k. a + k = b)"
proof
assume H:"le a b = True"
show "∃k. a + k = b"
proof (induct a)
case 0
show "∃k. 0 + k = b"
proof -
have "0 + b = b" by simp
thus ?thesis by (rule exI)
qed
case Suc
fix n::nat
assume HI:"∃k. n + k = b"
show "∃k. (Suc n) + k = b"
proof (induct b)
case 0
show "∃k. (Suc n) + k = 0"
proof -
have "le (Suc n) 0 = False" by simp
oops
请注意，我的 le 函数是 "less or equal"。在证明的这一点上，我发现我有假设 H 表明 le a b = True，或者在这种情况下 le (Suc n) 0 = True 是错误的。我该如何解决这个引理？
另一个小问题：我想写have "le (Suc n) 0 = False" by (simp only:le.simps)，但这行不通。看来我需要添加一些规则来减少 case 表达式。我错过了什么？
非常感谢您的帮助。
问题不在于很难摆脱伊莎贝尔的一个False假设。事实上，如果假设中存在 False，几乎所有 Isabelle 的证明方法都会立即证明任何事情。不，这里的问题是在证明的那个点，你不再有你需要的假设，因为你没有将它们链接到归纳中。但首先，请允许我发表一些小意见，然后给出具体的建议来修正你的证明。
几点说明
- 伊莎贝尔写
le a b = True或le a b = False有点不合时宜。只需写le a b或¬le a b. - 以方便的形式编写定义对于获得良好的自动化非常重要。当然，您的定义有效，但我建议使用以下定义，它可能更自然，并且会免费为您提供方便的归纳法则：
使用功能包：
fun le :: "nat ⇒ nat ⇒ bool" where
"le 0 n = True"
| "le (Suc k) 0 = False"
| "le (Suc k) (Suc n) = le k n"
- Existentials 有时会隐藏重要信息，并且它们往往会与自动化混淆，因为自动化永远不知道如何实例化它们。
如果你证明以下引理，证明是全自动的：
lemma def_le': "le a b ⟷ a + (b - a) = b"
by (induction a arbitrary: b) (simp_all split: nat.split)
使用我的函数定义，它是：
lemma def_le': "le a b ⟷ (a + (b - a) = b)"
by (induction a b rule: le.induct) simp_all
然后你的引理就很简单地得出了：
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
using def_le' by auto
这是因为存在主义使得搜索 space 爆炸式增长。给自动化一些具体的东西来遵循有很大帮助。
实际答案
有很多问题。首先，您可能需要做 induct a arbitrary: b，因为 b 在您的归纳过程中会发生变化（对于 le (Suc a) b，您将必须对 b 进行案例分析，然后在 b = Suc b' 的情况下，您将从 le (Suc a) (Suc b') 转到 le a b')。
其次，在最上面，你有 assume "le a b = True"，但你没有将这个事实链接到归纳法中。如果您在 Isabelle 中进行归纳，则必须将包含归纳变量的所有必需假设链接到归纳命令中，否则它们将无法用于归纳证明。有问题的假设谈论 a 和 b，但是如果你对 a 进行归纳，你将不得不推理一些与 a' 无关的任意变量a。例如：
assume H:"le a b = True"
thus "∃k. a + k = b"
（对 b 的第二次归纳也是如此）
第三，当你在 Isar 中有多个案例时（例如在归纳或案例分析期间），如果它们有不同的假设，你必须用 next 将它们分开。 next 基本上丢弃了所有固定变量和局部假设。通过我之前提到的更改，您需要在 case Suc 之前添加 next，否则伊莎贝尔会抱怨。
第四，Isar中的case命令可以修复变量。在你的 Suc 案例中，归纳变量 a 是固定的；随着对 arbitrary: b 的更改，a 和 b 得到修复。您应该为这些变量指定明确的名称；否则，Isabelle 将发明它们，您将不得不希望它提出的与您使用的相同。那不是好的风格。所以写例如case (Suc a b)。请注意，在使用 case 时，您 而不是 必须修复变量或进行假设。 case 命令会为您处理这个问题，并将局部假设存储在与案例同名的定理集合中，例如Suc 这里。它们被分类为 Suc.prems、Suc.IH、Suc.hyps。此外，当前案例的证明义务存储在 ?case（不是 ?thesis！）。
结论
有了这个（以及一些清理），你的证明看起来像这样：
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
assume "le a b"
thus "∃k. a + k = b"
proof (induct a arbitrary: b)
case 0
show "∃k. 0 + k = b" by simp
next
case (Suc a b)
thus ?case
proof (induct b)
case 0
thus ?case by simp
next
case (Suc b)
thus ?case by simp
qed
qed
next
可以压缩为
lemma def_le: "le a b ⟷ (∃k. a + k = b)"
proof
assume "le a b"
thus "∃k. a + k = b"
proof (induct a arbitrary: b)
case (Suc a b)
thus ?case by (induct b) simp_all
qed simp
next
但实际上，我建议您先证明 le a b ⟷ a + (b - a) = b 这样的具体结果，然后再用它证明存在性命题。
Manuel Eberl 做了困难的部分，我只是回答你关于如何尝试和控制 simp 等问题
在继续之前，我跑题了，澄清一下在另一个网站上说过的话。 "a tip" 这个词被用来表示对 M.E 的信任，但它应该是“在 2 个答案中提供 3 个解释”。如果不向列表发送垃圾邮件，则无法更正邮件列表中的电子邮件。
一些简短的回答是：
- 不能保证完全控制
simp，但如下所示的属性del和only可以多次控制它到您想要的程度。要查看它没有做的比您想要的更多，需要使用跟踪；下面给出了一个跟踪示例。 - 要完全控制证明步骤，您可以使用 "controlled"
simp，以及rule、drule和erule，以及其他方法。其他人需要给出详尽的清单。 - 大多数具有能够回答 "what's the detailed proof of what
simp,auto,blast, etc does" 专业知识的人都很少愿意投入工作来回答问题。调查simp正在做什么可能是一项简单而乏味的工作。 - "Black box proofs" 总是可选的，据我所知，如果我们希望它们 和 具有使它们成为可选的专业知识。使它们成为可选的专业知识通常是一个主要的限制因素。有了专业知识，动力就成了限制因素。
最简单的是什么？它不能取悦所有人
如果你看，你就会明白。人们抱怨 Isabelle 自动化太多，或者他们抱怨自动化太少。
永远不会有太多的自动化，但那是因为对于 Isabelle/HOL，自动化在很大程度上是可选的。 没有自动化 的可能性使得证明可能很有趣，但是只有 没有自动化，在宏伟的计划中，证明只是纯粹的乏味。
有属性only和del，可以用来大部分控制simp。仅从痕迹实验来说，即使simp也会调用其他证明方法，类似于auto调用simp、blast等
我认为你无法阻止 simp 调用线性算术方法。但是线性算术在很多时候并不适用。
设置痕迹，甚至爆炸痕迹
我在这里的回答是概括的，因为还试图确定 auto 的目的。 auto 使用的最大方法之一是 blast。
如果您不关心 blast 何时被 auto 使用或直接调用，则不需要 attribute_setup。 Makarius Wenzel 取出了爆炸痕迹，但随后非常友好地展示了如何实现它的代码。
没有爆破部分，只有declare的使用。在证明中，您可以使用 using 而不是 declare。把你不想要的拿出来。请务必查看 PIDE Simplifier Trace 面板中的新 simp_trace_new 信息。
attribute_setup blast_trace = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.trace b)))
*}
attribute_setup blast_stats = {*
Scan.lift
(Parse.$$$ "=" -- Args.$$$ "true" >> K true ||
Parse.$$$ "=" -- Args.$$$ "false" >> K false ||
Scan.succeed true) >>
(fn b => Thm.declaration_attribute (K (Config.put_generic Blast.stats b)))
*}
declare[[simp_trace_new mode=full]]
declare[[linarith_trace,rule_trace,blast_trace,blast_stats]]
尝试控制简单，随心所欲 only & del
我不想用你问题中的公式来努力工作。使用 simp，您使用 only 寻找的是没有使用您不期望的规则。
查看 simp 跟踪以了解哪些基本重写已完成且将始终完成，例如 True 和 False 的基本重写。如果你甚至不想那样，那么你必须求助于 rule.
查看是否可以完全关闭 simp 的起点是 apply(simp only:)。
这里有几个例子。我将不得不更加努力地寻找一个示例来说明何时自动使用线性算术：
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp only:) (*
ERROR: simp can't apply any magic whatsoever.
*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp only: add_0) (*
ERROR: Still can't. Rule 'add_0' is used, but it can't be used first.
*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
apply(simp del: add_0) (*
A LITTLE MAGIC:
It applied at least one rule. See the simp trace. It tried to finish
the job automatically, but couldn't. It says "Trying to refute subgoal 1,
etc.".
Don't trust me about this, but it looks typical of blast. I was under
the impressions that simp doesn't call blast.*)
oops
lemma
"a = 0 --> a + b = (b::'a::comm_monoid_add)"
by(simp) (*
This is your question. I don't want to step through the rules that simp
uses to prove it all.
*)