Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Coq simpl for Program Fixpoint

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.

like image 653
ouler Avatar asked Mar 31 '16 09:03

ouler


1 Answers

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.

like image 190
gallais Avatar answered Nov 10 '22 09:11

gallais