The Coq mailing list

[Thery Laurent <thery AT ns.di.univaq.it>]

Hi,

if having a clean extraction is important, the usual trick to get 
simplification back is to use rewriting.

For this, one way to go is to first define a predicate R with the idea
that  n R m means m = f(n), and shows that it is injective.

Then to define f, you first define fAux(n) = {m: nat | n R m}.
Then f is just the projection of fAux.

It is then easy to prove the rewriting theorem for f from the injectivity 
of R.

This gives for your example:

Require Export Arith.
Require Export Even.
Require Export Peano_dec.
Require Export Wf_nat.

(* A well-founded relation derived from the function*)
 
Inductive fLt : nat -> nat ->  Prop :=
  fLt0: forall (n : nat), even n ->  fLt (S n) n
 | fLt1: forall (n : nat), n <> 1 -> odd n ->  fLt (n - 3) n .
Hint Constructors fLt .

(* It is well-founded *)
 
Lemma WFL: well_founded fLt.y

Proof.
intros n; apply (lt_wf_ind n (Acc fLt)); clear n.
intros n rec; constructor.
intros y l1; generalize rec; inversion_clear l1; clear rec y; intros rec.
constructor.
intros y H1.
generalize rec; clear rec; inversion_clear H1; intros rec.
elim (not_even_and_odd (S n)); auto with arith.
destruct n; simpl; auto.
case H0; auto.
apply rec; auto.
apply le_lt_trans with n; auto with arith; apply le_minus.
apply rec; auto.
destruct n; simpl; auto.
elim (not_even_and_odd 0); auto with arith.
apply le_lt_trans with n; auto with arith; apply le_minus.
Defined.

(* Defining a relation R such that n R f(n) *)
 
Inductive Rf : nat -> nat ->  Prop :=
  Rf0: Rf 1 0
 | Rf1: forall (n m : nat), even n -> Rf (S n) m ->  Rf n m
 | Rf2: forall (n m : nat), ~ n = 1 -> odd n -> Rf (n - 3) m ->  Rf n m .
Hint Constructors Rf .

(* It is injective *)
 
Theorem Rf_injective: forall (n m p : nat), Rf n m -> Rf n p ->  m = p.
intros n m p H; generalize p; elim H; clear p H.
intros p H; inversion_clear H; auto.
elim (not_even_and_odd 1); auto with arith.
case H0; auto.
intros n0 m0 H H0 H1 p H2; generalize H; inversion_clear H2; auto.
intros H2; elim (not_even_and_odd 1); auto with arith.
intros H2; elim (not_even_and_odd n0); auto with arith.
intros n0 m0 H H0 H1 H2 p H3; generalize H; inversion_clear H3; auto.
intros H3; case H3; auto.
intros H3; elim (not_even_and_odd n0); auto with arith.
Qed.

(* A function that realizes Rf *)
 
Definition fAux: forall (n : nat),  ({m : nat | Rf n m}).
intros n; pattern n; apply well_founded_induction with ( A := nat ) ( R := 
fLt ).
apply WFL.
intros x H.
case (eq_nat_dec x 1).
intros H1; exists 0; rewrite H1; auto.
intros H1.
case (even_odd_dec x); auto.
intros H2; case (H (S x)); auto.
intros x1 Hx1; exists x1; auto.
intros H2; case (H (x - 3)); auto.
intros x1 Hx1; exists x1; auto.
Defined.

(* f is the projection of fAux *)
 
Definition f: nat ->  nat.
intros n; case (fAux n).
intros x H; exact x.
Defined.

(* First equation *)
 
Theorem f_0: f 1 = 0.
unfold f.
case (fAux 1); simpl; auto.
intros x H; inversion H; auto.
elim (not_even_and_odd 1); auto with arith.
case H0; auto.
Qed.

(* Second equation *)
 
Theorem f_even: forall n, even n ->  f n = f (n + 1).
intros n H; unfold f; case (fAux n); case (fAux (n + 1)).
intros x Hx x1 Hx1; inversion Hx1.
elim (not_even_and_odd 1); auto with arith.
rewrite H0; auto.
apply Rf_injective with ( n := n + 1 ); auto; simpl; auto.
rewrite plus_comm; auto; simpl; auto.
elim (not_even_and_odd n); auto.
Qed.

(* Third equation *)
 
Theorem f_odd: forall n, odd n ->  f n = f (n - 3).
intros n H; case (eq_nat_dec n 1); intros H1.
rewrite H1; simpl.
rewrite f_even with ( n := 0 ); auto with arith.
unfold f; case (fAux n); case (fAux (n - 3)).
intros x Hx x1 Hx1; inversion Hx1.
case H1; rewrite H0; auto.
elim (not_even_and_odd n); auto.
apply Rf_injective with ( n := n - 3 ); auto; simpl; auto.
Qed.

(* f is correct *)
 
Theorem f_correct: forall (n : nat),  match eq_nat_dec n 1 with
                                        left _ => f n = 0
                                       | right _ =>
                                           match even_odd_dec n with
                                             left _ => f n = f (n + 1)
                                            | right _ => f n = f (n - 3)
                                           end
                                      end.
intros n; case (eq_nat_dec n 1); auto.
intros H; rewrite H; apply f_0.
intros H; case (even_odd_dec n); intros H1.
apply f_even; auto.
apply f_odd; auto.
Qed.


(* Extraction *)

Extraction Inline fAux.
Extraction "test.ml" f.