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

我已经设法证明了这个定理，没有太多困难。现在我想把它用在一种新的策略--强归纳中，它应该类似于自然数上的标准"归纳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

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策略。

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。