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

Question

我想证明，如果一个蕴涵为真 (b --> c)，那么另外一个蕴涵也为真 (a --> c)，前提是两者之间存在适当的关系a 和 b.

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

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" 部分为紫色。我应该如何证明这种引理？

Answer 1

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

发生这种情况时，它有时可以帮助运行 try0（它只是尝试了几种常见的自动证明方法和 returns 成功的方法）或 sledgehammer（它试图将问题转化为更简单的形式并将其提供给外部证明者；如果他们能够证明它，它就会尝试将证明转化回 Isabelle）。

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

然而，由于这个问题是简单的一阶逻辑，metis可以很容易地自己解决它们，而不需要明确给出事实，并且它设法避免任何导致 auto 和 simp 发散的陷阱。

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

Proving implication (a --> c) from (b --> c) given relation between a and b

isabelle