コックSIMPL

Question

はProgram Fixpointのための戦術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).*) 

、そこにこのおもちゃの例のために必要な一切Program Fixpointはありませんが、私は手動でProgram Fixpointの終了を証明する必要がより複雑な設定で同じ問題に直面しています。

Answer 1

私はProgramを使用することに慣れていないので、おそらくよりよい解決策があるのですが、これは、私はそれが内部的にFix_subを使用してSearchAbout Fix_subを使用して、その機能についての定理を見て定義されていたことを見て、blaを展開することにより思い付いたものです。

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。同じ考え方で