在Coq中,假设我有一个固定点函数f
,其匹配定义在(g x
)上,我想在证明中使用形式(g x = ...
)中的假设。以下是一个最小的工作示例(实际上f
,g
会更复杂):
Definition g (x:nat) := x.
Fixpoint f (x:nat) :=
match g x with
| O => O
| S y => match x with
| O => S O
| S z => f z
end
end.
Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
intros.
unfold f.
rewrite H. (*fails*)
该消息显示Coq被卡住的地方:
(fix f (x0 : nat) : nat :=
match g x0 with
| 0 => 0
| S _ => match x0 with
| 0 => 1
| S z0 => f z0
end
end) x = 0
Error: Found no subterm matching "g x" in the current goal.
但是,命令unfold f. rewrite H.
不起作用。
如何让coq到unfold f
然后使用H
?
Parameter g: nat -> nat.
(* You could restructure f in one of two ways: *)
(* 1. Use a helper then prove an unrolling lemma: *)
Definition fhelp fhat (x:nat) :=
match g x with
| O => O
| S y => match x with
| O => S O
| S z => fhat z
end
end.
Fixpoint f (x:nat) := fhelp f x.
Lemma funroll : forall x, f x = fhelp f x.
destruct x; simpl; reflexivity.
Qed.
Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
intros.
rewrite funroll.
unfold fhelp.
rewrite H.
reflexivity.
Qed.
(* 2. Use Coq's "Function": *)
Function f2 (x:nat) :=
match g x with
| O => O
| S y => match x with
| O => S O
| S z => f2 z
end
end.
Check f2_equation.
Lemma test2 : forall (x : nat), g x = O -> f2 x = O.
Proof.
intros.
rewrite f2_equation.
rewrite H.
reflexivity.
Qed.
我不确定这是否能解决一般问题,但在你的特殊情况下(因为g
如此简单),这有效:
Lemma test : forall (x : nat), g x = O -> f x = O.
Proof.
unfold g.
intros ? H. rewrite H. reflexivity.
Qed.
这是另一个解决方案,但当然是这个简单的例子。也许会给你一些想法。引理测试2:forall(x:nat),g x = O - > f x = O. 证明。 =>前奏; 模式x; 在H中展现g; 重写H; 不重要的。 QED。