The Coq mailing list

[Vincent Laporte <vincent.laporte AT gmail.com>]

Le 2013-10-02 11:39, Fabien Renaud a écrit :
> I tried with Function but simpl only expands to function_terminate
> and I'm stuck.

Hi,

If you use Function, then several objects will be defined: the function
itself and a couple of lemmas, one of them being test_equation.

Function test (l: list nat) {measure length} :=
match l with
| nil => 0
| X::R => (test (tl R))
end.
Proof.
  induction R; intuition.
Defined.

Check test_equation.
(* test_equation
     : forall l : list nat,
       test l = match l with
                | [] => 0
                | _ :: R => test (tl R)
                end
*)

You can use this lemma to simplify some terms. For instance:

Goal ∀ x l, test (x::l) = 0.
  intros x l. rewrite test_equation.
  (* the goal is now: test (tl l) = 0. *)
Abort.

Moreover, there is an induction principle associated with your function
(its name is test_ind but that does not matter much). It might help
proving facts about the function, as in the following:

Lemma foo l : test l = 0.
Proof.
  functional induction test l; auto.
Qed.

Regards,
--
Vincent.