Coq：添加“强归纳”策略

Posted 2023-03-28

【中文标题】Coq：添加“强归纳”策略

【英文标题】：Coq: adding a "strong induction" tactic

【发布时间】：2014-01-02 13:15:49

【问题描述】：

对自然数的“强”（或“完全”）归纳意味着在证明 n 上的归纳步骤时，您可以假设该性质对于任何 k 都成立

Theorem strong_induction:
forall P : nat -> Prop,
(forall n : nat, (forall k : nat, (k < n -> P k)) -> P n) ->
forall n : nat, P n.

我已经成功地证明了这个定理，没有太多困难。现在我想在一个新的策略中使用它，strong_induction，它应该类似于自然数上的标准“induction n”技术。回想一下，当 n 是自然数且目标是 P(n) 时使用“归纳 n”时，我们会得到两个目标：一个是 P(0) 形式，第二个是 P(S(n)) 形式，对于第二个目标，我们得到 P(n) 作为假设。

所以我想，当当前目标是 P(n) 时，得到一个新目标，也是 P(n)，但是新假设“forall k : nat, (k P(k)) )”。

问题是我不知道如何在技术上做到这一点。我的主要问题是：假设 P 是一个复杂的语句，即

exists q r : nat, a = b * q + r

在上下文中使用 a b : nat；我如何告诉 Coq 在 a 而不是 b 上做强归纳？简单地做“应用strong_induction”会导致

n : nat
H0 : forall k : nat, k < n -> exists q r : nat, a = b * q + r
______________________________________(1/2)
exists q r : nat, a = b * q + r
______________________________________(2/2)
nat

假设没有用（因为 n 与 a 无关），我不知道第二个目标是什么意思。

【参考方案1】：

在这种情况下，apply strong_induction 需要 change 目标的结论，以便它更好地匹配定理的结论。

Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
change (forall a, (fun c => forall b, b <> 0 -> exists ! q r, c = q * b + r /\ r < b) a).
eapply strong_induction.

您也可以更直接地使用refine 策略。这种策略类似于apply 策略。

Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
refine (strong_induction _ _).

但induction 策略已经处理任意归纳原则。

Goal forall a b, b <> 0 -> exists ! q r, a = q * b + r /\ r < b.
induction a using strong_induction.

更多关于这些策略here。您可能应该在intro-ing 和split-ing 之前使用induction。

【讨论】：

"induction a using strong_induction" 效果很好！另一方面，“改变”策略因“错误：不可转换”而失败。

当更改过于复杂时，您可以尝试使用replace 策略，它会要求提供相等性证明。 change 只是 replace 当证明是微不足道的反身性时。