给定 a 和 b 之间的关系，从 (b --> c) 证明蕴含 (a --> c)答案

【问题标题】：Proving implication (a --> c) from (b --> c) given relation between a and b给定 a 和 b 之间的关系，从 (b --> c) 证明蕴含 (a --> c)
【发布时间】：2018-08-29 08:42:40
【问题描述】：

我想证明，如果一个蕴涵是真的 (b --> c)，那么在 a 和 @987654324 之间存在适当关系的情况下，那么其他一些蕴涵也是真的 (a --> c) @。

这是我试图证明的具体玩具示例：

theory Prop imports Main
begin

lemma 
  fixes func1 :: "'a => 'a"
    and func2 :: "'a => 'a"
    and func3 :: "'a => 'a"
  assumes "∀ x y. func1 x = func1 y --> func3 x = func3 y"
      and "∀ x. func1 x = func2 x"
  shows "∀ x y. func2 x = func2 y --> func3 x = func3 y"
proof -
  from assms show ?thesis by auto
qed

end

证明没有成功，Isabelle 2018 继续运行，“by auto”部分显示为紫色。我应该如何证明这种引理？

【问题讨论】：

标签： isabelle

【解决方案1】：

您的问题似乎使简化器（这是auto 的一部分）循环。我真的不明白为什么，但这些事情确实偶尔会发生。

发生这种情况时，有时运行 try0（它只是尝试几种常见的自动证明方法并返回成功的方法）或 sledgehammer（它试图将问题转换为更简单的形式并给出它给外部证明者；如果他们能证明它，它会尝试将证明翻译回给 Isabelle）。

在这种情况下，try0 和sledgehammer 都发现一个简单的apply metis 就可以完成这项工作。像auto 和simp 这样的方法可以做很多事情，包括，最值得注意的是，使用预定义的规则集进行“愚蠢”重写。 metis 在它的作用上更聪明一点，但是你需要手动给它每个它应该使用的事实，而且它不太适合 Isabelle/HOL。

但是，由于这个问题是简单的一阶逻辑，metis 可以在没有明确给出的事实的情况下自行轻松解决它们，并且它设法避免了导致 auto 和 simp 分歧的任何陷阱。

【讨论】：

当然。我认为值得一提的是，您可以在 shows 行之后 add using [[simp_trace,simp_trace_depth_limit=4]] 更好地了解正在发生的事情（尽管仍然难以解释）。