Metis：未使用的定理在这种情况下意味着什么？答案

【问题标题】：What does Metis: Unused theorems mean in this context?Metis：未使用的定理在这种情况下意味着什么？
【发布时间】：2018-12-10 20:53:27
【问题描述】：

我对 Isabelle 很陌生，如果这个问题的格式不正确，我深表歉意。

我试图证明以下几点：

record 
  Point =
    x :: nat
    y :: nat

definition
  cond :: "Point ⇒ Point ⇒ ????"
where
  "cond point1 point2 ≡ 
     abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"

我的证明是：

lemma cond_proof : "∃ point1 point2 . cond point1 point2 = True"
  sledgehammer
  by (metis Point_ext_def abs_division_segment add_diff_cancel_left' cond_def select_convs(1))

这会触发警告：

Metis: Unused theorems:

请有人解释一下这是什么意思？如果可能的话，请帮助我得出一个满足这个条件的证明。

我对 Isabelle 还是很陌生，所以感谢所有 cmets。

【问题讨论】：

标签： isabelle formal-verification

【解决方案1】：

我可以评论与您的问题相关的一些实际方面。我相信，警告是不言自明的。通常，您可以删除未使用的定理，metis 仍然能够证明感兴趣的定理（参见下面代码清单中的cond_proof_metis）。

引理cond_proof 可以通过展示满足引理中条件的两个点来证明。我相信这种方法可能被认为比使用sledgehammer 找到的默认证明更好。我已经在下面的代码清单中的引理cond_proof_Isar 中展示了如何做到这一点。有更紧凑的方式来展示这个例子。但是，鉴于您对 Isabelle 很陌生，所以我采用了在我看来最自然的方法。

我不确定你是否故意在证明中留下了命令sledgehammer。但是，在大多数情况下，这不是您希望做的事情。一旦sledgehammer 找到了一个证明，您就可以从您的证明中删除命令sledgehammer。

作为旁注，我建议您完成 Tobias Nipkow 等人的“A Proof Assistant for Higher-Order Logic”和 Isabelle/HOL 的“Concrete Semantics”书中的一些示例和练习托拜厄斯·尼普科夫和格温·克莱因。上述参考资料包含许多与您正在处理的问题非常相似的示例。

不幸的是，我对sledgehammer 和metis 的了解不够，无法告诉您为什么在使用sledgehammer 的输出证明定理时会产生警告。有关sledgehammer 和metis 的更多信息，请参阅由 Jasmin Christian Blanchette 编写的“A User's Guide to Sledgehammer for Isabelle/HOL”，可在标准 Isabelle 文档中找到。当然，关于metis 的更多信息也可以在网上找到（例如http://www.gilith.com/metis/）。希望比我知识渊博的人能够提供有关您的查询的更多详细信息。

section ‹Auxiliary commands›
theory Scratch
  imports Complex_Main
begin

record Point =
    x :: nat
    y :: nat

definition
  cond :: "Point ⇒ Point ⇒ bool"
where
  "cond point1 point2 ≡ 
     abs (x point1 - x point2) = 1 ∨ abs (y point1 - y point2) = 1"

(*Point_ext_def was part of the output produced by sledgehammer and is
listed as unused by metis. It can be removed with no effect on the
ability of metis to prove the result of interest.*)
lemma cond_proof_metis : "∃ point1 point2 . cond point1 point2 = True"
  by (metis (*Point_ext_def*) 
      abs_1 add_diff_cancel_left' cond_def of_nat_1_eq_iff select_convs(1))

lemma cond_proof_Isar : "∃point1 point2 . cond point1 point2 = True"
proof(intro exI) 
  define point1::Point where point1: "point1 ≡ ⦇x = 2, y = 0⦈"
  define point2::Point where point2: "point2 ≡ ⦇x = 1, y = 0⦈"
  show "cond point1 point2 = True"
    unfolding cond_def point1 point2 by auto
qed

end

伊莎贝尔版本：伊莎贝尔2020

【讨论】：