Coq for Fixpoint

Question

Is there something like simpl tactics for Program Fixpoint s?

In particular, how can one prove 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 for this toy example, but I ran into the same problem in a more complex setup where I need to prove the completion of the Program Fixpoint manually.

Answer 1

I'm not used to using Program , so maybe the best solution, but this is what I came up with, deploying bla , seeing that it was internally defined using Fix_sub and looking at theorems about what 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 xfg Heq. destruct x. reflexivity. f_equal ; apply Heq. Qed. 

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

 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 xfg Heq. destruct x. reflexivity. f_equal ; apply Heq. Qed. 

So the next time you have bla (S _) , you can just rewrite blaS_red .