在Coq中使用从1开始的归纳
在Coq中使用从1开始的归纳
提问于 2019-02-19 01:24:43
我尝试在余数证明中使用从1开始的归纳法。从this question那里我得到了我需要的归纳原理的证明：
Section induction_at_1.
Variable P : nat -> Prop.
Hypothesis p1 : P 1.
Hypothesis pS : forall n, P n -> P (S n).
Theorem induction_at_1:
forall n, n > 0 -> P n.
induction n; intro.
- exfalso; omega.
- destruct n.
+ apply p1.
+ assert (S n >= 1) by omega.
intuition.
Qed.
End induction_at_1.我得到的在结构上看起来与标准归纳非常相似。事实上，Check nat_ind会产生
nat_ind:
forall P : nat -> Prop,
P 0 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, P n而Check induction_at_1产生了
induction_at_1:
forall P : nat -> Prop,
P 1 ->
(forall n : nat, P n -> P (S n)) ->
forall n : nat, n > 0 -> P n当我尝试应用这个归纳原理时，问题就出现了。例如，我想通过归纳法证明
Lemma cancellation:
forall a b c: nat, a > 0 -> a * b = a * c -> b = c.这似乎非常适合我上面的归纳，但是当我像这样开始我的证明时
intros a b c H0 H1.
induction a using induction_at_1.我得到了以下错误，我无法解释它：
Not the right number of induction arguments (expected 2 arguments).由于这两个归纳原则在我看来几乎相同，我不确定为什么这不起作用。有什么想法吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-02-19 11:55:57
我也发现这种行为令人费解，但有几种方法可以绕过它。一种是使用ssreflect归纳策略，称为elim。
From Coq Require Import ssreflect.
Lemma cancellation:
forall a b c: nat, a > 0 -> a * b = a * c -> b = c.
Proof.
intros a b c H.
elim/induction_at_1: a / H.
(* ... *)
Abort.第二行是告诉Coq在H (而不是a)上执行归纳，同时推广a并使用归纳原理induction_at_1。我无法使用常规的Coq induction获得与工作类似的东西。
另一种方法是使用普通自然数归纳法。在这种情况下，我认为引理之后是b上的归纳，同时推广了c (我不确定a上的归纳是否有效)。如果您确实需要为所有n显示某种形式的m <= n -> P n，您可以将n替换为n - m + m (使用m <= n假设应该是可能的)，然后在n - m上通过归纳来证明P (n - m + m)。
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/54752428
复制相关文章
相似问题
腾讯云开发者
