0

似乎有一些关于归纳谓词的东西我不明白，因为我不断遇到它们的问题。我最近的努力是用ev具体语义书籍第 5 章中归纳定义的谓词来理解案例分析。

假设我正在证明

lemma
  shows "ev n ⟹ ev (n - 2)"

我试图在 Isabelle/HOL 中立即开始证明，但是当我尝试或给出奇怪的目标时它会抱怨：

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

这表明：

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)

这不是我所期望的。

当我传递n到案例时，我们改为对自然数的定义进行归纳（注意其他时候它ev正确地进行了归纳，请参见后面的示例）：

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases n)

给出：

proof (state)
goal (2 subgoals):
 1. ⟦ev n; n = 0⟧ ⟹ ev (n - 2)
 2. ⋀nat. ⟦ev n; n = Suc nat⟧ ⟹ ev (n - 2)

这不是我所期望的。但是请注意，即使作为参数，以下内容也可以工作（即它ev不是对自然数进行归纳） ：n

lemma
  shows "ev n ⟹ ev (n - 2)"
proof -
  assume 0: "ev n"
  from this show "ev (n - 2)"
  proof (cases n)

我意识到首先假设ev n然后声明显示必须有一些魔力，ev (n-2)否则不会发生错误。

我理解规则倒置的想法（通过分析可能导致它的案例，得出要反向证明的给定事实）。对于“偶数”谓词，规则反转是：

ev n ==> n = 0 ∨ (∃k. n = Suc (Suc k) ∧ ev k)

这基于归纳定义的谓词是有意义的：

inductive ev :: "nat ⇒ bool" where
ev0: "ev 0" |
evSS: "ev n ⟹ ev (Suc (Suc n))"

但我不明白。为什么不直接做案例工作？或者为什么这个语法无效：

proof (cases ev)

或这个：

proof (cases ev.case)

等等

我认为症结在于，在处理归纳定义谓词时，我不知道这种归纳是否适用于目标或假设，但从教科书的文字来看：

名称规则倒置强调我们是在倒推：通过哪些规则可以证明某些给定的事实？

我假设它正在对目标应用规则倒置，因为它说“通过哪些规则可以证明某些给定的事实”。

此外，ev ==> ev (n-2)书中的这个例子也无济于事，因为前提和结论都ev涉及。

规则倒置的案例分析如何真正发挥作用，为什么我们需要首先假设 Isabelle 为案例分析提供合理的目标？

4

2 回答 2

2

不确定我是否理解整个问题，但这是：

lemma
  shows "ev n ⟹ ev (n - 2)"
proof (cases)

给你：

proof (state)
goal (2 subgoals):
 1. ⟦ev n; ?P⟧ ⟹ ev (n - 2)
 2. ⟦ev n; ¬ ?P⟧ ⟹ ev (n - 2)

因为伊莎贝尔正在分裂 的真相ev n，即真或假。我相信您正在寻找的语法是：

proof (cases rule: ev.cases)

这就是你如何明确地告诉伊莎贝尔它应该使用什么规则来逐案证明。

于 2020-05-20T21:59:51.357 回答
1

这样做的方法就像 Ben Sheffield 所说的那样：

proof (cases rule: ev.cases)

我还注意到：

apply (rule ev.cases)

有效，但我认为通过一个小例子来查看明确概述的案例会有所帮助：

考虑：

lemma "ev n ⟹ ev (n - 2)"

首先检查它的案例定理：

thm ev.cases
⟦ev ?a; ?a = 0 ⟹ ?P; ⋀n. ⟦?a = Suc (Suc n); ev n⟧ ⟹ ?P⟧ ⟹ ?P

然后将目标统一起来，引入新的目标和原来的假设以及所有案例的假设。这就是为什么ev n在所有这些中都有一个。

  apply (rule ev.cases)

有目标：

proof (prove)
goal (3 subgoals):
 1. ev n ⟹ ev ?a
 2. ⟦ev n; ?a = 0⟧ ⟹ ev (n - 2)
 3. ⋀na. ⟦ev n; ?a = Suc (Suc na); ev na⟧ ⟹ ev (n - 2)

你可以做 simp 并照常进行证明。

于 2020-05-21T18:44:23.013 回答