Coq:添加"强感应"策略

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中使用它,它应该类似于自然数字上的标准"感应n"技术.回想当使用"感应n"时,当n是自然数并且目标是P(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

ab: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无关),我不知道第二个目标意味着什么.

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.

更多关于这些策略的信息.您应该在使用induction之前使用intro-ing和split-ing.