Coq：添加“强归纳”策略

Question

Coq：添加“强归纳”策略

8

"Strong" (or "complete") induction on the natural number means that when proving the induction step on n, you can assume the property holds for any 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.

I have managed to prove this theorem without too many difficulties. Now I want to use it in a new tactic, strong_induction, which should be similar to the standard "induction n" technique on the natural numbers. Recall that when using "induction n" when n is a natural number and the goal is P(n), we get two goals: One of the form P(0) and the second of the form P(S(n)), where for the second goal we get P(n) as assumption.

So I want, when the current goal is P(n), to get one new goal, also P(n), but the new assumption "forall k : nat, (k < n -> P(k)))".

The problem is I don't know how to do it technically. My main problem is this: Suppose P is a complex statement, i.e.

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

with a b : nat in the context; how can I tell Coq to do the strong induction on a and not on b? simply doing "apply strong_induction" results in

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

where the assumption is useless (since n does not relate to a) and I have no idea what the second goal means.

- Gadi A

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- user1861759 · Accepted Answer

在这种情况下，要使用强归纳法，您需要更改目标的结论，以使其更符合定理的结论。

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 _ _).

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

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

关于这些策略的更多信息，请点击此处。在使用 intro 和 split 之前，您应该先使用 induction。