在进行归纳时使用“依赖诱导”策略保持信息
在进行归纳时使用“依赖诱导”策略保持信息
提问于 2015-12-04 12:12:27
我刚刚遇到Coq induction的问题，在阅读这里的证明时丢弃了关于构造的术语的信息。
作者们使用了这样的东西：
remember (WHILE b DO c END) as cw eqn:Heqcw.在实际归纳H之前重写假设induction H。我真的不喜欢引入一个微不足道的等式的想法，因为它看起来像黑魔法。
这里的一些搜索表明，实际上remember技巧是必要的。然而，有一个答案是这里，它指出新的dependent induction可以用来避免remember的花招。这很好，但是dependent induction本身看起来有点神奇。
我很难理解dependent induction是如何工作的。文档给出了一个需要dependent induction的示例：
Lemma le_minus : forall n:nat, n < 1 -> n = 0.我可以验证induction是如何失败的，dependent induction在这种情况下是如何工作的。但我不能使用remember技巧来复制dependent induction结果。
到目前为止，我试图模仿remember技巧的是：
Require Import Coq.Program.Equality.
Lemma le_minus : forall n:nat, n < 1 -> n = 0.
intros n H. (* dependent induction H works*)
remember (n < 1) as H0. induction H. 但这不管用。任何人都可以用dependent induction remember-ing来解释这里的工作原理？
回答 1
Stack Overflow用户
回答已采纳
发布于 2015-12-04 15:58:23
你能做到的
Require Import Coq.Program.Equality.
Lemma le_minus : forall n:nat, n < 1 -> n = 0.
Proof.
intros n H.
remember 1 as m in H. induction H.
- inversion Heqm. reflexivity.
- inversion Heqm. subst m.
inversion H.
Qed.正如前面提到的这里，问题是Coq不能跟踪在您正在进行归纳的事物的类型中出现的术语的形状。换句话说，在“小于”关系上进行归纳会指示Coq尝试证明一些关于泛型上界的东西，而不是您正在考虑的特定的上限(1)。
请注意，在不使用remember或dependent induction的情况下，总是可以通过稍微概括一下结果来证明这样的目标：
Lemma le_minus_aux :
forall n m, n < m ->
match m with
| 1 => n = 0
| _ => True
end.
Proof.
intros n m H. destruct H.
- destruct n; trivial.
- destruct H; trivial.
Qed.
Lemma le_minus : forall n, n < 1 -> n = 0.
Proof.
intros n H.
apply (le_minus_aux n 1 H).
Qed.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/34088140
复制相关文章
相似问题
腾讯云开发者
