Coq简化程序固定点
有喜欢的战术什么simpl的Program Fixpoint S'
特别是，如何证明下列琐碎的陈述？
Program Fixpoint bla (n:nat) {measure n} :=
match n with
| 0 => 0
| S n' => S (bla n')
end.
Lemma obvious: forall n, bla n = n.
induction n. reflexivity.
(* I'm stuck here. For a normal fixpoint, I could for instance use
simpl. rewrite IHn. reflexivity. But here, I couldn't find a tactic
transforming bla (S n) to S (bla n).*)
显然，这个玩具例子中没有必要的Program Fixpoint ，但是我在更复杂的设置中面临同样的问题，我需要手动终止Program Fixpoint 。
我不习惯使用Program ，从而可能有一个更好的解决方案，但是这是我想出了通过展开bla ，看到它是使用内部定义Fix_sub ，看着有关使用该功能的定理SearchAbout Fix_sub 。
Lemma obvious: forall n, bla n = n.
Proof.
intro n ; induction n.
reflexivity.
unfold bla ; rewrite fix_sub_eq ; simpl ; fold (bla n).
rewrite IHn ; reflexivity.
(* This can probably be automated using Ltac *)
intros x f g Heq.
destruct x.
reflexivity.
f_equal ; apply Heq.
Qed.
在你现实生活中的例子中，你可能想要引入简化引理，这样你就不必每次都做同样的工作。 例如：
Lemma blaS_red : forall n, bla (S n) = S (bla n).
Proof.
intro n.
unfold bla ; rewrite fix_sub_eq ; simpl ; fold (bla n).
reflexivity.
(* This can probably be automated using Ltac *)
intros x f g Heq.
destruct x.
reflexivity.
f_equal ; apply Heq.
Qed.
这样，下一次你有一个bla (S _) ，你可以简单地rewrite blaS_red 。