为什么奇偶情况不同？

Question

在本练习中，auto 证明了 even_mul 引理，但未能证明 odd_mul。

fun is_odd :: "nat ⇒ bool" where
    "is_odd n = (n mod 2 ≠ 0)"

fun is_even :: "nat ⇒ bool" where
    "is_even n = (n mod 2 = 0)"

lemma even_mul : "is_even (n::nat) ⟹ is_even (n * n)"
  by auto

lemma odd_mul : "is_odd (n::nat) ⟹ is_odd (n * n)"
  by auto

我希望能解释一下这两种情况的不同之处，以及如何证明 odd_mul 的提示。

Answer 1

您可以通过在化简规则中添加引理 mod2_eq_if 来证明 odd_mul，如下所示：

lemma odd_mul : "is_odd (n::nat) ⟹ is_odd (n * n)"
  by (simp add: mod2_eq_if)

为了理解为什么 auto 方法证明了 even_mul 但未能证明 odd_mul，让我们看看各自的简化器轨迹（仅显示相关部分）。 even_mul 的轨迹如下所示：

...
[1]Rewriting:
is_even (n * n) ≡ n * n mod 2 = 0 
[1]Applying instance of rewrite rule "Rings.semidom_modulo_class.dvd_imp_mod_0":
?a1 dvd ?b1 ⟹ ?b1 mod ?a1 ≡ 0 
[1]Trying to rewrite:
even (n * n) ⟹ n * n mod 2 ≡ 0 
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
even (n * n) 
[2]Applying instance of rewrite rule "Parity.semiring_parity_class.even_mult_iff":
even (?a1 * ?b1) ≡ even ?a1 ∨ even ?b1 
[2]Rewriting:
even (n * n) ≡ even n ∨ even n 
...

我们可以看到简化器能够使用 Parity 理论中的重写规则 even (?a1 * ?b1) ≡ even ?a1 ∨ even ?b1 因为 even 和 is_even 的定义原来是使用 Rings.semidom_modulo_class 中的 dvd_imp_mod_0 重写 even 时相同。

但是，odd 和 is_odd 不是这种情况，因为 odd a ≡ ¬ 2 dvd a 和简化器无法在没有用户额外帮助的情况下将其重写为使用 is_odd ，如输出面板所示：

theorem odd_mul: is_odd ?n ⟹ is_odd (?n * ?n) 
Failed to finish proof⌂:
goal (1 subgoal):
 1. n mod 2 = Suc 0 ⟹ n * n mod 2 = Suc 0

然而，在 post 顶部的 odd_mul 证明中，我们明确提供了额外的重写规则 mod2_eq_if 来帮助简化器弥合 [=27] 之间的差距=] 和 is_odd 如下面的跟踪所示：

...
[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
is_odd n ⟹ is_odd (n * n) 
[1]Applying instance of rewrite rule "??.unknown":
is_odd ?n1 ≡ ?n1 mod 2 ≠ 0 
[1]Rewriting:
is_odd n ≡ n mod 2 ≠ 0 
[1]Applying instance of rewrite rule "Parity.semiring_parity_class.mod2_eq_if":
?x1 mod 2 ≡ if even ?x1 then 0 else 1 
[1]Rewriting:
n mod 2 ≡ if even n then 0 else 1 
[1]Applying congruence rule:
even n ≡ ?c ⟹ if even n then 0 else 1 ≡ if ?c then 0 else 1 
[2]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
even n ≡ ?c 
[1]SUCCEEDED
...

希望这对您有所帮助。

为什么奇偶情况不同？

Why the odd-even cases differ?

isabelle