Coq简化程序修复点

Question

有没有类似于策略simpl用于程序不动点的东西？

特别地，如何证明以下平凡语句？

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).*)

显然，这个玩具示例不需要“程序不动点”，但在更复杂的情况下，我需要手动证明“程序不动点”的终止性。请注意，html标签已保留，无需解释。

- ouler

Answer 1

我不习惯使用程序，所以可能有更好的解决方案，但这是我通过展开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。

- gallais

---

在同样的思路下，你可以为 bla 声明等式引理：forall n, bla n = match n with | 0 => 0 | S n' => S (bla n') end. - eponier

这真的是最好的答案吗？这不会使得“程序不动点”对于大型函数相对繁琐，因为你需要手动编写缩减引理吗？ - Joachim Breitner

像“Equations”这样的较新插件会为您生成简化引理。 - gallais