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).*)
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.
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.
This way, next time you have a bla (S _), you can simply rewrite blaS_red.