有限界量词的消去规则

Question

我有以下目标:

∀x ∈ {0,1,2,3,4,5}. P x

我想把这个目标分解成六个子目标:P 0, P 1, P 2, P 3, P 4和P 5。这很容易通过apply auto完成。但是auto使用的相关规则是什么呢?我这样问是因为我的实际目标看起来更像这样:

∀x ∈ {0..<6}. P x

和apply auto并没有以同样的方式打破这个目标(它给了我

⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x

)。

Answer 1

auto使用的规则是ballI (bounded all introduction)。这将∀x ∈ S. P x转换为x ∈ S ==> P x。

将x ∈ {0,1,2,3,4,5}转换成6个单独的子目标是一个单独的问题。基本上，auto将显式枚举转换为析取，然后将其拆分。

Answer 2

您可以使用如下引理来拆分单个目标:

lemma expand_ballI: "⟦ (n :: nat) > 0; ∀x ∈ {0..< (n - 1)}. P x; P (n - 1) ⟧ ⟹ ∀x ∈ {0..< n}. P x"
  by (induct n, auto simp: less_Suc_eq)

可以重复应用到你的规则中，如下所示:

lemma "∀x ∈ {0..< 6 :: nat}. P x"
  apply (rule expand_ballI, fastforce)+
  apply simp_all

导致目标分割如下:

goal (6 subgoals):
 1. P 0
 2. P (Suc 0)
 3. P 2
 4. P 3
 5. P 4
 6. P 5

Answer 3

使用[simp]引理将集合转换为更方便的集合版本是非常方便的。例:{0..<6} = {0,1,2,3,4,5}