程序定点的Coq简化 [英] Coq simpl for Program Fixpoint

问题描述

是否有针对 Program Fixpoint s的战术 simpl ？

is there anything like the tactic simpl for Program Fixpoints?

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

In particular, how can one proof the following trivial statement?

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 手动。

Obviously, there is no Program Fixpoint necessary for this toy example, but I'm facing the same problem in a more complicated setting where I need to prove termination of the Program Fixpoint manually.

推荐答案

我不习惯使用 Program ，所以可能更好的解决方案，但这是我通过展开 bla 想到的，看到它是使用 Fix_sub 在内部定义的，通过使用 SearchAbout Fix_sub 对该函数进行定理。

I'm not used to using Program so there's probably a better solution but this is what I came up with by unfolding bla, seeing that it was internally defined using Fix_sub and looking at the theorems about that function by using 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.

在您的实际示例中，您可能想引入归约引理，这样您就不会不必每次都做相同的工作。例如：

In your real-life example, you'll probably want to introduce reduction lemmas so that you don't have to do the same work every time. E.g.:

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 _），您只需重写blaS_red 。

This way, next time you have a bla (S _), you can simply rewrite blaS_red.

这篇关于程序定点的Coq简化的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！