Coq：添加“强归纳”策略

对自然数的“强”（或“完全”）归纳意味着当证明 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，它应该类似于自然数上的标准“归纳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

上下文中带有 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 无关）并且我不知道第二个目标意味着什么。

在这种情况下，要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 tactic.

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

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

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

有关这些策略的更多信息here http://coq.inria.fr/refman/tactic-index.html。你可能应该使用induction before intro- 和split-ing.