程序定点的Coq简化

有没有像simpl的战术Program Fixpoint一样的东西？

特别是，如何证明以下琐碎的陈述？

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即可。

关于程序定点的Coq简化，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/36329256/