这是自然数均匀性的归纳和计算定义。
Inductive ev : nat -> Prop :=
| ev_0 : ev O
| ev_SS : forall n:nat, ev n -> ev (S (S n)).
Definition even (n:nat) : Prop :=
evenb n = true.
以及一个暗示另一个的证明。
Theorem ev__even : forall n,
ev n -> even n.
intros n E.
induction E as [ | n' E' ].
reflexivity. apply IHE'. Qed.
起初，我并没有过多地考虑到这种证明，但是仔细观察后，我发现有些麻烦。问题是，在执行该reflexivity步骤之后，我希望看到上下文
1 subgoal
n' : nat
E : ev (S (S n'))
E' : ev n'
IHE' : ev n' -> even n'
====================================================================== (1/1)
even (S (S n'))
但是我实际上得到的是
1 subgoal
n' : nat
E' : ev n'
IHE' : even n'
====================================================================== (1/1)
even (S (S n'))
尽管该定理仍然可以证明，但令人震惊的是，这些假设神秘地消失了。我想知道如何获得最初期望的上下文。通过网络搜索，我了解到这是对Coq中构造术语的归纳的普遍问题。一种关于SO的提议解决方案建议使用remember关于假设的策略。但是当我在证明中尝试
Theorem ev__even : forall n,
ev n -> even n.
intros n E.
remember E.
induction E as [ | n' E' ].
我在induction步骤中收到以下错误消息。
Error: Abstracting over the term "n" leads to a term
"fun n : nat => forall e : ev n, e = E -> even n" which is ill-typed.
我不太了解。我认为问题在于它E具有一个自由变量，但是在那种情况下，我将被困住，因为如果不引入，就E无法引入n。（generalize dependent n将对此进行概括E）
有什么方法可以获取最初期望的上下文？
我不明白induction这里的策略是什么。每当我不了解战术在做什么时，我都会尝试自己写证明词。如果您手动调用归纳原理，则可以保留原始假设：
Theorem ev__even : forall n, ev n -> even n.
intros n E.
refine (ev_ind even _ _ n E).
- reflexivity.
- intros n' E' IH.
apply IH.
Qed.
这是第二种归纳情况下的上下文：
n : nat
E : ev n
n' : nat
E' : ev n'
IH : even n'
============================
even (S (S n'))
假设
Fixpoint evenb (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n') => evenb n'
end.
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句