Coq simpl für Programm Fixpunkt

Question

Gibt es etwas wie die Taktik simpl für Program Fixpoint s?

Insbesondere, wie kann man die folgende triviale Aussage beweisen?

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

Offensichtlich gibt es keine Program Fixpoint notwendig für dieses Spielzeug Beispiel, aber ich bin das gleiche Problem in einer komplizierteren Umgebung an, wo ich Beendigung der Program Fixpoint manuell beweisen muß.

Answer 1

ich zur Verwendung von Program so nicht benutzt gibt es wahrscheinlich eine bessere Lösung, aber das ist, was ich mit bla durch Entfaltung kam, zu sehen, dass es intern unter Verwendung SearchAbout Fix_subFix_sub und Blick auf die Sätze über diese Funktion definiert wurde.

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 Ihrem Beispiel aus der Praxis, werden Sie wahrscheinlich wollen Reduktion Lemmata einzuführen, so dass Sie jedes Mal die gleiche Arbeit nicht tun müssen. Z.B .:

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. 

Auf diese Weise hat nächstes Mal ein bla (S _), können Sie einfach rewrite blaS_red.