Coq:添加 "strong induction"策略

Question

对自然数的“强”(或“完全”)归纳意味着在证明对 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 < n -> P(k)))”。

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

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

带有 b :上下文中的 nat ；我如何告诉 Coq 对 a 而不是 b 进行强归纳？简单地做“apply 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 无关)，我不知道第二个目标是什么意思。

Answer 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 .您可能应该使用 induction之前 intro -ing 和 split -ing。