0

我试图从上一个问题中证明 Isabelle (2021) 中的以下推理规则：

在此处输入图像描述

特别是，我试图以向前的方式证明这一点，首先使用两个假设来获得A(y)和B(y)，因此A(y) /\ B(y)，对于任意选择的y。但是，我无法弄清楚∀在最后一步中引入背面的正确方法是什么，如下面的问题行所示。

theorem "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)"
proof (rule allI) ―‹forward›
  fix y
  assume "∀x. A(x)"
  from this have 1:"A(y)" by (rule allE)
  assume " ∀x. B(x)"
  from this have 2:"B(y)" by (rule allE)
  from 1 2 have "A(y) ∧ B(y)" by (rule conjI)
  ―‹problem line: applying allI›
  from this have "∀x. A(x) ∧ B(x)" by (rule allI)

有人可以帮助解释什么是正确的假设方法，然后在这里抽象出任意变量y吗？

4

1 回答 1

3

有人可以帮助解释什么是正确的假设方法，然后在这里抽象出任意变量 y 吗？

我不会说只有一种“正确的方法”可以做到这一点。“正确的方法”将取决于您要解决的问题的上下文。

一般来说，您试图证明的定理可以通过以下方式证明simp：

theorem 0: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
  by simp

在大多数情况下，当试图证明这样的结果时，simp是最好的方法。

但是，例如，如果您正在撰写说明性文章/教程并希望展示如何执行证明的各个步骤，那么当然，显式规则应用程序就成为必需品。但是，在这种情况下，仍然有很多可能性。

首先，您可以使用显式块，如下面的示例所示：

(*naive variant*)
theorem 1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then have "∀y. A y ∧ B y" by (rule allI)
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

(*more natural variant*)
theorem 2: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

(*HOL-style*)
theorem 3: "(∀x. A x) ⟶ (∀x. B x) ⟶ (∀x. A x ∧ B x)"
proof(intro impI)
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  {
    fix y 
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By have "A y ∧ B y" by (rule conjI)
  }
  then show "∀y. A y ∧ B y" by (rule allI)
qed

然而，proof- ... qed通常是一个更好的选择，更符合伊莎贝尔的传统风格，例如

theorem alt_1: "∀x. A x ⟹ ∀x. B x ⟹ ∀x. A x ∧ B x"
proof-
  assume 1: "∀x. A(x)" and 2: "∀x. B(x)" 
  have "∀y. A y ∧ B y"
  proof(rule allI)
    fix y
    from 1 have Ay: "A y" by (elim allE)
    from 2 have By: "B y" by (elim allE)
    from Ay By show "A y ∧ B y" by (rule conjI)
  qed
  then have "∀x. B x ⟹ ∀y. A y ∧ B y" by (rule asm_rl)
  then show "∀x. A(x) ⟹ ∀x. B(x) ⟹ ∀x. A(x) ∧ B(x)" by (rule asm_rl)
qed

作为一般参考，我建议在The Isabelle/Isar Reference Manual中的第 2.2 节。

于 2021-08-03T23:32:42.143 回答